# About single process system, fairness, and depth-first search option

I have the following module in PlusCal.

(*

--algorithm Untitled
{
variables u = 24 ; v \in 1 .. N;
{
print <<u, v>>;
while (u # 0) {
if (u < v) {
u := v || v := u
};
u := u - v ;
};
print <<"have gcd", v>>;
}
}

\*PlusCal options (-wf)

*)

Here are the observations when running TLC with one worker thread.

1) Model checking this module for termination with N as 30, depth as 50, and Depth-first checked, results in no errors.

2) Model checking this module for termination with N as 30, depth as 50, and Depth-first unchecked, results in an error trace suggesting temporal properties were violated.

3) Uncommenting PlusCal options line and then model checking this module statement for termination with N as 30, depth as 50, and Depth-first unchecked, results in no errors.

4) Uncommenting PlusCal options line and then model checking this module statement for termination with N as 30, depth as 50, and Depth-first checked, results in no errors.

Why does (2) result in an error?

Isn't the above algorithm treated as a single process system?  If so, why is the explored behavior affected by fairness constraints (3)?


• Follow-Ups: