Merge branch 'development' into new_reged

Conflicts: src/lib/regions.py src/regionEditor.py src/specEditor.py
csalzberger · Apr 24, 2012 · e434916 · e434916
2 parents 44cce82 + eec259e
commit e434916
Show file tree

Hide file tree

Showing 105 changed files with 4,043 additions and 4,833 deletions.
diff --git a/dist/LTLMoP_GitHub_Setup.py b/dist/LTLMoP_GitHub_Setup.py
diff --git a/src/etc/jtlv/GROne/GROneDebug.java b/src/etc/jtlv/GROne/GROneDebug.java
@@ -139,7 +139,7 @@ public static String analyze(SMVModule env, SMVModule sys) {
 				System.err.println("Error: " + e.getMessage());
 	  }  
 
-		  if (explainSys ==0 && !sysUnreal.equals(Env.FALSE())) {		 
+		  if (explainSys ==0 && !sysUnreal.equals(Env.FALSE())) {
 				 debugInfo += "System is unrealizable because the environment can force a safety violation."+ "\n"; //TRUE if unsat
 		  		 explainSys = 1;
 		  }
@@ -180,7 +180,7 @@ public static String justiceChecks(SMVModule env, SMVModule sys, int explainSys,
 
 		counter_exmple = g.envWinningStates().and(all_init);		 
 		if (counter_exmple.isZero()) {	//no winning environment states		
-			debugInfo += "Specification is realizable.\n";
+			//debugInfo += "Specification is realizable assuming instantaneous actions.\n";
 		}	
 
 		if (!(env.justiceNum()==1 && env.justiceAt(0).equals(Env.TRUE()))) {
@@ -208,7 +208,7 @@ else if ((env.trans().and(Env.prime(env.justiceAt(i-1))).isZero()) | (env.trans(
 						 explainEnv = 1;
 						 i = 0;
 					 //} else if (counter_exmple.isZero() && !env.justiceAt(i-1).equals(Env.TRUE())) {// && (!prev.isZero())) {
-					 } else if (counter_exmple.isZero() && i > 1) {
+					 } else if (i < env.justiceNum()) {
 						 //if we get here, the env is unrealizable because of the current goal
 						 debugInfo += "Environment highlighted goal(s) unrealizable " + (i-1) + "\n";	
 						 explainEnv = 1;
@@ -248,7 +248,7 @@ else if ((sys.trans().and(Env.prime(sys.justiceAt(i-1))).isZero()) | sys.trans()
 					 if (g.calculate_counterstrategy(counter_exmple, true, false)) {
 						 debugInfo += "System highlighted goal(s) inconsistent with transition relation " + (i-1) + "\n";
 						 explainSys = 1;
-					 } else {
+					 } else  {
 					 //if we get here, the sys is unrealizable because of the current goal					 				
 						 debugInfo += "System highlighted goal(s) unrealizable " + (i-1) + "\n";
 						 explainSys = 1;