More refactoring and Todos

lip6 · Mar 4, 2021 · 39ad766 · 39ad766
1 parent 461bc8f
commit 39ad766
Showing 1 changed file with 6 additions and 3 deletions.
diff --git a/...ip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java b/...ip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java
@@ -24,6 +24,9 @@ public GlobalPropertySolver(String solverPath) {
 	}
 
 	// oneSafe
+
+	// TODO: javadoc
+
 	void buildOneSafeProperty() {
 
 		for (int pid = 0; pid < spn.getPlaceCount(); pid++) {
@@ -38,8 +41,8 @@ void buildOneSafeProperty() {
 
 	void buildStableMarkingProperty() {
 		for (int pid = 0; pid < spn.getPlaceCount(); pid++) {
-			Expression stable = Expression.op(Op.EQ, Expression.var(0), Expression.constant(spn.getMarks().get(0)));
-			Expression ef = Expression.op(Op.EF, stable, null);
+			Expression stable = Expression.op(Op.EQ, Expression.var(pid), Expression.constant(spn.getMarks().get(pid)));
+			Expression ef = Expression.op(Op.AG, stable, null);
 			Property stableMarkingProperty = new Property(ef, PropertyType.INVARIANT, "place_" + pid);
 			spn.getProperties().add(stableMarkingProperty);
 		}
@@ -121,7 +124,7 @@ public boolean solveProperty(String examination, MccTranslator reader) {
 				e.printStackTrace();
 			}
 		}
-
+		// TODO: change this
 		// boolean isOneSafe = true;
 		for (Entry<String, Boolean> e : doneProps.entrySet()) {
 			if (!e.getValue()) {