Merge pull request #6 from lip6/master

use CTL assertion 'AG EF t' enabled for all transition t for Liveness

Author: bnslmn

pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/GlobalPropertySolver.java

@@ -94,8 +94,8 @@ void buildQuasiLivenessProperty(PetriNet spn) {
 	void builLivenessProperty(PetriNet spn) {
 		for (int tid = 0; tid < spn.getTransitionCount(); tid++) {
 			Expression live = Expression.nop(Op.ENABLED, Collections.singletonList(Expression.trans(tid)));
-			Expression ef = Expression.op(Op.AG, live, null);
-			Property LivenessProperty = new Property(ef, PropertyType.INVARIANT, "transition_" + tid);
+			Expression ef = Expression.op(Op.AG, Expression.op(Op.EF, live, null), null);
+			Property LivenessProperty = new Property(ef, PropertyType.CTL, "transition_" + tid);
 			spn.getProperties().add(LivenessProperty);
 		}
 	}