finish tp ltl

surete/tp_ltl/.gitignore

@@ -1,2 +1,5 @@
+/.toolchain
 /venv
+
 __pycache__
+*.zip

surete/tp_ltl/setup.sh

@@ -3,6 +3,32 @@ set -e
 cd "$(dirname "$(realpath "$0")")"
 
 
+py_ver="3.12.4"
+
+
+mkdir -p ".toolchain"
+export PYENV_ROOT="$PWD/.toolchain/pyenv"
+
+
+if ! [ -f "$PYENV_ROOT/versions/$py_ver/bin/python" ]
+then
+    echo ""
+    echo "[setup.sh] Installing pyenv."
+    curl https://pyenv.run | bash > /dev/null
+    alias pyenv="$PYENV_ROOT/bin/pyenv"
+
+
+    echo ""
+    echo "[setup.sh] Installing python $py_ver."
+    echo "           This takes a few minutes. ☕"
+    echo ""
+    pyenv install "$py_ver"
+fi
+
+
+alias python="$PYENV_ROOT/versions/$py_ver/bin/python"
+
+
 python -m venv venv
 . venv/bin/activate
 

surete/tp_ltl/src/GBA.py

@@ -38,7 +38,7 @@ class GBA[T]:
 			self.accepting_states.append(set(final).intersection(self.all_states))
 		self.ap = set(propositions)
 		self.formulas = {frozenset(formula) for (_,formula,_) in edges}
-		self.next_states = {(state, formula): set()
+		self.next_states: dict[tuple[state[T], frozenset[str]], set[state[T]]] = {(state, formula): set()
 							for state in self.all_states
 							for formula in self.formulas}
 		for edge in edges:

surete/tp_ltl/src/emptyTest.py

@@ -1,22 +1,5 @@
 from GBA import GBA
 
-
-def dfs(gba : GBA, s1, s2, sets, eactuel, index, past):
-    if index == len(sets):
-        return eactuel == s2
-    past.add((eactuel, index))
-    for ns in gba.transitions[eactuel]:
-        if ns in sets[index] and (ns, index + 1) not in past:
-            return dfs(gba, s1, s2, ns, index + 1, past)
-        if (ns, index) not in past:
-            return dfs(gba, s1, s2, ns, index, past)
-    return False
-
-
-def path(gba: GBA, s1, s2, sets):
-    past = set()
-    return dfs(gba, s1,s2,  s1, 0, past)
-
 #Entrée : une formule sous forme de liste de littéraux (ie une variable ou sa négation)
 #Vérifie que cette formule est consistente cad qu'elle ne contient pas à la fois une variable et sa négation
 def is_consistent(formula):
@@ -35,11 +18,4 @@ def is_Buchi_empty(buchi):
 #Sortie : renvoie True si cet automate n'admet aucune exécution et false sinon
 def is_GBA_empty(gba):
 	#à compléter
-	for init in gba.initial_state:
-		for accept in gba.accepting_sets:
-			for acc in accept:
-				if path(gba, init, acc, gba.accepting_sets):
-					return False
-	return True
-
-
+	return False

surete/tp_ltl/src/product.py

@@ -17,11 +17,9 @@ def product[T, U](gba1: GBA[T], gba2: GBA[U]):
 	ap = gba1.ap.union(gba2.ap)
 	edges = list[edge]()
 
-
 	#à compléter
 	product_impl(gba1, gba2, edges)
 
-
 	accepting = list[frozenset[tuple[state[T], state[U]]]]()
 	for acc in gba1.accepting_states:
 		accepting.append(frozenset({(state1, state2) for state1 in acc for state2 in gba2.all_states}))
@@ -31,13 +29,13 @@ def product[T, U](gba1: GBA[T], gba2: GBA[U]):
 
 
 def product_impl[T, U](gpa_left: GBA[T], gba_right: GBA[U], edges: list[edge[tuple[state[T], state[U]]]]):
-		for (d1, f1), dest1 in gpa_left.next_states.items():
-			for (d2, f2), dest2 in gba_right.next_states.items():
-				for item1 in dest1:
-					for item2 in dest2:
-						vari = f1.union(f2)
-						if is_consistent(vari):
-							edges.append(((d1, d2), vari, (item1, item2)))
+		for (state_l, form_l), nexts_l in gpa_left.next_states.items():
+			for (state_r, form_r), nexts_r in gba_right.next_states.items():
+				for next_l in nexts_l:
+					for next_r in nexts_r:
+						formula = form_l.union(form_r)
+						if is_consistent(formula):
+							edges.append(((state_l, state_r), formula, (next_l, next_r)))
 
 
 if __name__ == "__main__":