diff --git a/surete/tp_ltl/.gitignore b/surete/tp_ltl/.gitignore
index 01e7a1f..0b81a20 100644
--- a/surete/tp_ltl/.gitignore
+++ b/surete/tp_ltl/.gitignore
@@ -1,5 +1,2 @@
-/.toolchain
 /venv
-
-__pycache__
-*.zip
+__pycache__
\ No newline at end of file
diff --git a/surete/tp_ltl/run.sh b/surete/tp_ltl/run.sh
new file mode 100755
index 0000000..139a0d5
--- /dev/null
+++ b/surete/tp_ltl/run.sh
@@ -0,0 +1,12 @@
+#!/bin/sh
+set -e
+cd "$(dirname "$(realpath "$0")")"
+
+
+if ! [ -d venv ]
+then ./setup.sh
+fi
+. venv/bin/activate
+
+
+python src/product.py
diff --git a/surete/tp_ltl/setup.sh b/surete/tp_ltl/setup.sh
index 8de0fd3..495b249 100755
--- a/surete/tp_ltl/setup.sh
+++ b/surete/tp_ltl/setup.sh
@@ -3,32 +3,6 @@ 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
 
diff --git a/surete/tp_ltl/src/GBA.py b/surete/tp_ltl/src/GBA.py
index 152a2de..4469cfe 100644
--- a/surete/tp_ltl/src/GBA.py
+++ b/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: dict[tuple[state[T], frozenset[str]], set[state[T]]] = {(state, formula): set()
+		self.next_states = {(state, formula): set()
 							for state in self.all_states
 							for formula in self.formulas}
 		for edge in edges:
diff --git a/surete/tp_ltl/src/emptyTest.py b/surete/tp_ltl/src/emptyTest.py
index ea05e01..5488b9b 100644
--- a/surete/tp_ltl/src/emptyTest.py
+++ b/surete/tp_ltl/src/emptyTest.py
@@ -1,5 +1,22 @@
 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):
@@ -18,4 +35,11 @@ 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
-	return False
+	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
+
+
diff --git a/surete/tp_ltl/src/product.py b/surete/tp_ltl/src/product.py
index 5826df0..95aefde 100644
--- a/surete/tp_ltl/src/product.py
+++ b/surete/tp_ltl/src/product.py
@@ -17,9 +17,11 @@ 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}))
@@ -29,13 +31,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 (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)))
+		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)))
 
 
 if __name__ == "__main__":