Next batch of LTL-related fixes from Joachim Klein (jltl2ba-fix-multiple-labels.patch, SimpleLTL-simplify-NEXT-AND-keep-order.patch, jltl2ba-fix-comments-for-release.patch, jltl2dstar-NBAAnalysis-dont-assume-NBA-is-disjoint.patch).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9153 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/jltl2ba/Alternating.java

@@ -213,7 +213,7 @@ public class Alternating {
 			final_set.set(done.size());
 			break;
 
-		case RELEASE: /* p V q <-> (p && q) || (p && X (p V q)) */
+		case RELEASE: /* p V q <-> (p && q) || (q && X (p V q)) */
 			for (t1 = buildAlternating(p.right); t1 != null; t1 = t1.nxt) {
 				ATrans tmp;
 
@@ -225,7 +225,7 @@ public class Alternating {
 					}
 				}
 
-				tmp = t1.clone(); /* p */
+				tmp = t1.clone(); /* q */
 				tmp.to.set(done.size()); /* X (p V q) */
 				tmp.nxt = t;
 				t = tmp;

prism/src/jltl2ba/Buchi.java

@@ -52,6 +52,9 @@ public class Buchi {
 	private int btrans_count;
 	private int rank;
 	
+	// the highest id used for a BState.id
+	private int max_id;
+
 	public static class BState {
 		Generalized.GState gstate;
 		public int id;
@@ -132,6 +135,7 @@ public class Buchi {
 		g_init = g.g_init;
 		_final = g._final;
 		// gstates = g.gstates;
+		max_id = g.getGStateID();
 		
 		int i;
 		BState s = new BState();
@@ -566,6 +570,23 @@ public class Buchi {
 		}
 		retargetAllBTrans();
 
+		 /*
+		  * As merging equivalent states can change the 'final' attribute of
+		  * the remaining state, it is possible that now there are two
+		  * different states with the same id and final values.
+		  * This would lead to multiply-defined labels in the generated neverclaim.
+		  * We iterate over all states and assign new ids (previously unassigned)
+		  * to these states to disambiguate.
+		  * Fix from ltl3ba.
+		  */
+		for (s = bstates.nxt; s != bstates; s = s.nxt) {          /* For all states s*/
+			for (BState s2 = s.nxt; s2 != bstates; s2 = s2.nxt) { /*  and states s2 to the right of s */
+				if(s._final == s2._final && s.id == s2.id) {      /* if final and id match */
+					s.id = ++max_id;                              /* disambiguate by assigning unused id */
+				}
+			}
+		}
+
 		return changed;
 	}
 

prism/src/jltl2ba/Generalized.java

@@ -200,6 +200,12 @@ public class Generalized {
 		// print(System.out, a.sym_table);
 	}
 	
+	/** Get the highest ID of a GState */
+	public int getGStateID()
+	{
+		return gstate_id;
+	}
+
 	/*is the transition final for i ? */
 	private boolean isFinal(Alternating a, MyBitSet from, Alternating.ATrans at, int i)
 	{

prism/src/jltl2ba/SimpleLTL.java

@@ -442,7 +442,7 @@ public class SimpleLTL {
 			/* X p && X q == X (p && q) */
 			if (right.kind == LTLType.NEXT && left.kind == LTLType.NEXT) {
 				rv = new SimpleLTL(LTLType.NEXT,
-						new SimpleLTL(LTLType.AND, right.left, left.left));
+						new SimpleLTL(LTLType.AND, left.left, right.left));
 				break;
 			}
 

prism/src/jltl2dstar/NBAAnalysis.java

@@ -63,7 +63,7 @@ public class NBAAnalysis {
 	public SCCs getSCCs() {
 		if (_sccs == null) {
 			_sccs = new SCCs();
-			GraphAlgorithms.calculateSCCs(_nba, _sccs, false);
+			GraphAlgorithms.calculateSCCs(_nba, _sccs, true);
 		}
 		return _sccs;
 	}