Re: [tlaplus] About single process system, fairness, and depth-first search option

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

if you look at the TLA+ that is generated without weak fairness, the main formula is

Spec == Init /\ [][Next]_vars

This specification allows for executions that stutter indefinitely from any point onwards, therefore termination is not guaranteed. Invariance to stuttering is a fundamental concept of TLA+, and for verifying liveness properties you always need some fairness conditions in order to rule out indefinite stuttering. When you add the weak fairness option, the specification becomes

Spec == /\ Init /\ [][Next]_vars

        /\ WF_vars(Next)

ensuring that executions cannot halt as long as some action is executable.

NB: I was not even aware of the possibility of passing options to PlusCal via a comment, and the feature appears to be somewhat brittle (for example, it breaks when you have a space between "\*" and "PlusCal"). You may alternatively write "--fair algorithm", and similarly "fair process" when you have multi-process algorithms.

The effect is independent of depth-first or breadth-first search.

Best regards,

Stephan

On 19 Dec 2016, at 08:33, rvpr...@xxxxxxx <venkateshpra...@xxxxxxxxx> wrote:

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)?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.