infinite loop when verifying simpleMPSpec

[ywei]

command:
tass verify -verbose simpleMPSpec.mmp -np 2
The infinite loop will occur when the verifier checks all the states and want to return from program.

...
Step 19: State 18 -- simpleMPSpec.mmp line 22 proc 1 [main@10->main@11] "t = m;" -> State 19

begin State 19

onStack = true;
seen = true;
pathCondition : true
begin model state

begin shared variables

s = 0;
t = 5;

end shared variables;
begin process 0
end process 0;
begin process 1

begin stack frame 0

function : main;
location : 11;
i = 5;
j = 7;
k = 0;
m = 5;

end stack frame 0;

end process 1;

end model state

end State 19

Step 20: State 19 -- simpleMPSpec.mmp proc 1 [main@11->main@12] "[implicit return]"
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid
CVC3 prover invoked with query: TRUE under context TRUE
Valid

It seems the transition system keeps adding the implicit return as a new transition. But the DfsSearcher thinks it has seen the state before. So the program loops forever.

[Stephen Siegel]

The logic in the proceedToNext method had a bug. If numProcs>0 and the last statement of the last proc was the current one, then this one would get returned again (causing an infinite loop). Problem was pid was getting set to 0, causing search to start over from beginning.

I probably have to fix the same bug in the Urgent version.