Code for some experiences (5ce4ede5) · Commits · Sebastien Gamblin / symbolic-representation-for-PDEL

hanabi_smc.py

+76 −24

Original line number	Diff line number	Diff line
		@@ -272,7 +272,7 @@ def get_plays_name(a, c, v, i, p, possible):
		return f"{a}-plays-pos{p}-{c}{v}{i}:{'T' if possible else '⊥'}"

		def get_discards_name(a, c, v, i, p):
		return f"{a}-discard-pos{p}-{c}{v}{i}"
		return f"{a}-discards-pos{p}-{c}{v}{i}"



		@@ -636,6 +636,7 @@ class HanabiSMC(Example):

		for event in self.kts:
		e_name = event.name if isinstance(event, Transformer) else event[0].name
		"""
		if ("plays" in e_name or "discards" in e_name) and action in e_name:
		draw_liste = self.get_draws(e_name[0])
		draw_act = draw_liste[0] if not self.random_generation else random.choice(draw_liste)
		@@ -644,7 +645,8 @@ class HanabiSMC(Example):
		else:
		liste.append([event, draw_act])
		#liste.append(event)
		elif action in e_name:
		"""
		if action in e_name:
		liste.append(event)

		#print("FINDS")
		@@ -705,10 +707,10 @@ class HanabiSMC(Example):
		if get_id_symbol() not in p and getAfterSymbol() not in p:
		n_pointed.append(p)

		if not self.s5:
		formulas.append(Box_a(a, Atom(p)))
		else:
		formulas.append(K(a, Atom(p)))
		#if not self.s5:
		# formulas.append(Box_a(a, Atom(p)))
		#else:
		# formulas.append(K(a, Atom(p)))

		if isinstance(ks, ProbaStructure) and p[0] == a:

		@@ -732,10 +734,13 @@ class HanabiSMC(Example):
		# pass
		with Timer("Model check", show=False, incr=1):
		#print(test)
		print(">>", str(test), Color.get(ks.modelCheck(test, logtime=logtime, show=False, cache=ks.cache), Color.CBOLD))
		res = ks.modelCheck(test, logtime=logtime, show=False) #, cache=ks.cache)
		print(">>", str(test), Color.get(res, Color.CBOLD))

		print("Pointed (flat):", sorted(list(set(n_pointed))))
		print(Color.get("<< MODEL CHECKING \n", Color.CVIOLET, Color.CBOLD))
		return len(formulas)


		def playable_actions(self, ks, ts, show=False):
		"""
		@@ -770,9 +775,6 @@ class HanabiSMC(Example):
		return liste





		def print_datas(current, S5, proba):

		pointed_symb = current.manager.from_formula(
		@@ -818,12 +820,27 @@ def print_datas(current, S5, proba):
		print("POINTED is : ", current.pointed)



		def store_datas(ks, i, name, tps_mc, nbf, tps_pu):
		global DATAS
		DATAS[i] = {}
		DATAS[i]["Dernière action"] = name
		DATAS[i]["SIZE-Law-terminals"] = ks.state_law.get_nodes_informations()["Terminals"]
		DATAS[i]["SIZE-Law-noterminals"] = ks.state_law.get_nodes_informations()["NoTerminals"]
		DATAS[i]["Time-MC"] = tps_mc
		DATAS[i]["Nb_formulas"] = nbf
		DATAS[i]["Time-PU"] = tps_pu
		for agent in ks.omega.keys():
		DATAS[i][f"SIZE-OM-{agent}-terminals"] = ks.omega[agent].get_nodes_informations()["Terminals"]
		DATAS[i][f"SIZE-OM-{agent}-noterminals"] = ks.omega[agent].get_nodes_informations()["NoTerminals"]
		DATAS[i][f"SIZE-PI-{agent}-terminals"] = ks.pi[agent].get_nodes_informations()["Terminals"]
		DATAS[i][f"SIZE-PI-{agent}-noterminals"] = ks.pi[agent].get_nodes_informations()["NoTerminals"]
		print(DATAS[i])


		if __name__ == "__main__":

		PARSER = True
		PARSER = False

		if PARSER:
		print(">> WITH PARSER")
		from my_args import arg_parser
		@@ -841,17 +858,21 @@ if __name__ == "__main__":

		else:
		print(">> WITHOUT PARSER")
		nbCards = 30
		nbCards = 12
		nbA = 2
		nbCH = 2
		normalize = False
		S5 = False
		proba = True
		prof = 4
		prof = 10
		random = False
		modelcheck = False
		modelcheck = True
		product_update = True

		import sys

		sys.setrecursionlimit(2000)

		tokens = True
		Structure.filter_transformer = True

		@@ -862,7 +883,7 @@ if __name__ == "__main__":
		product_update and prof == 0), "If you want to use product_update, we certainly need to has historic and prof > 0."

		#fd = FreshDistributor()
		with Timer("ALL TIME", show=True):
		with Timer("ALL TIME", show=True) as timer_all_time:

		seuil = 1/((nbCards-nbCH)+1)

		@@ -871,6 +892,15 @@ if __name__ == "__main__":
		action_names = ["a-plays-pos0-R11:T"]
		#action_names = ["Announce for b : 1 at [0]"]

		action_names = [
		"Announce for b : 1 at [0]",
		"b-plays-pos0-R13:T",
		f"b-draws-{DRAW_NAME}-R22",
		"a-discards-pos0-R11",
		f"a-draws-{DRAW_NAME}-R31",
		"Announce for a : 1 at [1]"
		]

		cleaning = False

		# print("seuil = ", seuil)
		@@ -897,20 +927,29 @@ if __name__ == "__main__":
		# print_datas(current, S5, proba)

		if modelcheck:
		hanabi_smc.check(current, logtime, hanabi_smc.s5)
		with Timer("mci", show=False) as timer_mc:
		nbf = hanabi_smc.check(current, logtime, hanabi_smc.s5)

		DATAS = {}

		store_datas(ks, 0, "Begin", timer_mc.t, nbf, 0)

		if product_update:

		with Timer("Product_time", show=False):

		#playables = playable_actions(current, ts, show=True)

		print("POINTED is : ", current.pointed)

		print(action_names)
		actions = hanabi_smc.get_actions_to_apply(action_names)
		print([a.name if isinstance(a, Transformer) else a[0].name for a in actions])

		for i, a in enumerate(actions):
		print(Color.get(f"STEP {i} APPLY : {a.name if isinstance(a, Transformer) else a[0].name}", Color.CBLUE, Color.CBOLD))

		# hanabi_smc.playable_actions(current, ts, show=True)

		subname = a.name if isinstance(a, Transformer) else a[0].name
		print(Color.get(f"STEP {i} APPLY : {subname}", Color.CBLUE, Color.CBOLD))

		if cleaning:
		clean = [e for e in current.manager.global_variables_names if
		@@ -920,20 +959,24 @@ if __name__ == "__main__":
		else:
		clean = []

		with Timer("Product Update in", show=False):
		new = current.apply(a, cleaning=clean)
		with Timer("Product Update in", show=False) as timer_pu:
		current = current.apply(a, cleaning=clean)

		# print_datas(new, S5, proba)

		n_pointed = []
		for p in new.pointed:
		for p in current.pointed:
		if get_id_symbol() not in p and getAfterSymbol() not in p:
		n_pointed.append(p)

		print("New pointed (flat) :", n_pointed)

		if modelcheck:
		hanabi_smc.check(new, logtime, hanabi_smc.s5)
		with Timer("mci", show=False) as timer_mc:
		nb_formulas = hanabi_smc.check(current, logtime, hanabi_smc.s5)

		store_datas(current, i+1, subname, timer_mc.t, nb_formulas, timer_pu.t)



		#print("Structure.clean_transformer", Structure.filter_transformer, "NbC", nbCards, "nbA", nbA, "nbCH", nbCH,
		@@ -941,3 +984,12 @@ if __name__ == "__main__":
		# "PU", product_update)

		Timer.memory.print(threshold=0)

		from pprint import pprint

		DATAS["All_time"] = timer_all_time.t
		pprint(DATAS)

		import pickle
		file_pi = open(f"nbA{nbA}-nbH{nbCH}-nbC{nbCards}-norm={normalize}.pkl", 'wb')
		pickle.dump(DATAS, file_pi)

launch_xp.sh

+1 −1

Original line number	Diff line number	Diff line
		@@ -63,7 +63,7 @@ run_process_loop () {

		for i in $(seq 1 "$Nb_loops");
		do
		for proba in "" # "" "-p"
		for proba in "-p" # "" "-p"
		do

		######## SMCPDEL

rendering_of_calculations.py

+686 −114

File changed.

Preview size limit exceeded, changes collapsed.

src/model/SMCPDEL/pySMCPDEL.py

+24 −11

Original line number	Diff line number	Diff line
		@@ -263,6 +263,8 @@ class ProbaStructure(BeliefStructure):

		assert isinstance(belief_transformer, ProbaTransformer)

		print(belief_transformer.name)

		with Timer(f"simple apply {belief_transformer.name}", show=False) as father:

		with Timer("BeliefStructure simple_apply", father=father):
		@@ -400,17 +402,6 @@ class ProbaStructure(BeliefStructure):

		get_sizes = False

		if self.pithetaprime is None:
		with Timer("compute PI THETAPRIME") as t1:
		self.compute_pi_theta_prime()
		self.compute_pi_theta_prime_time = t1.t

		# Used only in denormalized MC
		if self.pithetaprime_marginalized is None and not self.isnormalized:
		with Timer("compute PI THETAPRIME MARG") as t2:
		self.compute_pi_theta_prime_marginalied()
		self.compute_pi_theta_prime_marginalized_time = t2.t

		@memoize(cache)
		def rec_from_formula(form):

		@@ -433,6 +424,17 @@ class ProbaStructure(BeliefStructure):

		"""

		if self.pithetaprime is None:
		with Timer("compute PI THETAPRIME") as t1:
		self.compute_pi_theta_prime()
		self.compute_pi_theta_prime_time = t1.t

		# Used only in denormalized MC
		if self.pithetaprime_marginalized is None and not self.isnormalized:
		with Timer("compute PI THETAPRIME MARG") as t2:
		self.compute_pi_theta_prime_marginalied()
		self.compute_pi_theta_prime_marginalized_time = t2.t

		toforget = [prime(x) for x in self.vocabulary] # prime of v
		to_prime = {x: prime(x) for x in self.vocabulary}

		@@ -523,6 +525,17 @@ class ProbaStructure(BeliefStructure):
		BigΣ_i [ α_i x MargΣ_{WS'} ( Π^d x \|\|φ_i\|\|' x θ') ] 'op' β x_norm MargΣ_{Π^d x θ'}
		"""

		if self.pithetaprime is None:
		with Timer("compute PI THETAPRIME") as t1:
		self.compute_pi_theta_prime()
		self.compute_pi_theta_prime_time = t1.t

		# Used only in denormalized MC
		if self.pithetaprime_marginalized is None and not self.isnormalized:
		with Timer("compute PI THETAPRIME MARG") as t2:
		self.compute_pi_theta_prime_marginalied()
		self.compute_pi_theta_prime_marginalized_time = t2.t

		toforget = [prime(x) for x in self.vocabulary] # prime of v
		to_prime = {x: prime(x) for x in self.vocabulary}

src/model/epistemiclogic/epistemicmodel/epistemic_model_interface.py

+1 −1

Original line number	Diff line number	Diff line
		@@ -195,7 +195,7 @@ class EpistemicModelInterface(metaclass=ABCMeta):
		from src.utils.memoize import memoize
		from src.model.datastructure.real_function import PseudoBooleanFunction
		from src.model.datastructure.add.add_real_function import ADDManager
		from src.model.epistemiclogic.epistemicmodel.symbolic.symbolic_proba_epistemic_model import SymbolicProbaEpistemicModel
		#from src.model.epistemiclogic.epistemicmodel.symbolic.symbolic_proba_epistemic_model import SymbolicProbaEpistemicModel

		data = json.loads(jsonstring)