Merge lp:~verifydtapn-contributers/verifydtapn/algorithmFix into lp:verifydtapn

[Jakob Taankvist]

I think this fix the issue with the trace stack not being updated correctly.

[lp:~verifydtapn-contributers/verifydtapn/algorithmFix]

268. By Jakob Taankvist on 2012-07-14

Made sure the stack magement is allways preformed

[Mathias Grund Sørensen (mathias.grund)]

Looks good

review: Approve

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/DiscreteVerification/NonStrictSearch.cpp'
--- src/DiscreteVerification/NonStrictSearch.cpp	2012-07-13 17:50:33 +0000
+++ src/DiscreteVerification/NonStrictSearch.cpp	2012-07-14 10:41:17 +0000
@@ -23,28 +23,33 @@
 	//Main loop
 	while(pwList.HasWaitingStates()){
 		NonStrictMarking& next_marking = *pwList.GetNextUnexplored();
-		if(livenessQuery && next_marking.passed)	continue;
-		NonStrictMarking marking(next_marking);
-		bool endOfMaxRun = true;
-		next_marking.passed = true;
-		next_marking.inTrace = true;
-		trace.push(&next_marking);
-		validChildren = 0;
-
-		// Generate next markings
-		vector<NonStrictMarking> next = getPossibleNextMarkings(marking);
-
-		if(isDelayPossible(marking)){
-			marking.incrementAge();
-			marking.SetGeneratedBy(NULL);
-			next.push_back(marking);
-		}
-
-		for(vector<NonStrictMarking>::iterator it = next.begin(); it != next.end(); it++){
-			if(addToPW(&(*it), &next_marking)){
-				return true;
-			}
+		bool endOfMaxRun;
+		if(!(livenessQuery && next_marking.passed)){
+			NonStrictMarking marking(next_marking);
+			endOfMaxRun = true;
+			next_marking.passed = true;
+			next_marking.inTrace = true;
+			trace.push(&next_marking);
+			validChildren = 0;
+
+			// Generate next markings
+			vector<NonStrictMarking> next = getPossibleNextMarkings(marking);
+
+			if(isDelayPossible(marking)){
+				marking.incrementAge();
+				marking.SetGeneratedBy(NULL);
+				next.push_back(marking);
+			}
+
+			for(vector<NonStrictMarking>::iterator it = next.begin(); it != next.end(); it++){
+				if(addToPW(&(*it), &next_marking)){
+					return true;
+				}
+				endOfMaxRun = false;
+			}
+		} else {
 			endOfMaxRun = false;
+			validChildren = 0;
 		}
 
 		if(livenessQuery){