[tlaplus] Analysis of a PlusCal algorithm is sensitive to placement of labels

["Georgios Kafanas (gkaf)" <kafanas.george@xxxxxxxxx>]

I am trying to implement the 1BitNProcMutex from the PlusCal tutorial session 8, without using a goto statement. However, the resulting algorithm is very sensitive to the labeling of the statements.

This is the module I am using:
```
----------------------------- MODULE OneBitNProcMutex -----------------------------
EXTENDS Integers, TLC

CONSTANT N
ASSUME N \in Nat

Procs == 0..(N-1)

(*
--algorithm 1BitNProcMutex {
  variables can_enter_critical_region = [i \in Procs |-> FALSE] ;
  process (P \in Procs)
  variable higher_priority = {}; lower_priority = {}; proc = self;
  { ncs: while (TRUE) {
           skip ;
    enter: while ( ~ can_enter_critical_region[self] ) {
             can_enter_critical_region[self] := TRUE ;
             higher_priority := { i \in Procs : i < self } ;
         e1: while ( higher_priority /= {} /\ can_enter_critical_region[self] ) {
         e2:   with ( q \in higher_priority ) {
                 proc := q;
               };
         e3:   if ( can_enter_critical_region[proc] ) {
         e4:     can_enter_critical_region[self] := FALSE ;
         e5:     higher_priority := { i \in Procs : i < self } ;
                 await ~ can_enter_critical_region[proc] ;
               } else e6: {
                 higher_priority := higher_priority \ {proc} ;
               } ;
             };
           } ;
           lower_priority := { i \in Procs : i > self } ;
       e7: while ( lower_priority /= {} ) {
       e8:   with ( q \in lower_priority ) {
               proc := q ;
             } ;
       e9:   await ~ can_enter_critical_region[proc] ;
             lower_priority := lower_priority \ {proc};
           } ;          
       cs: skip ;
     exit: can_enter_critical_region[self] := FALSE ;
    }
  }
}
*)

MutualExclusion == \A i, j \in Procs : (i /= j) =>  ~ ((pc[i] = "cs") /\ (pc[j] = "cs"))

=============================================================================
```

The model is tested with N=2 and MutualExclusion added to the list of invariant properties. When removing the label e5, the TLA+ toolbox reports a deadlock.

I would expect that the presence of labels would not affect liveness properties. Am I missing something, or is this a bug?

The version of the TLA+ Toolbox used is 1.7.1.

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/59e2207e-e272-4eaa-868c-a5d5c0b944ebn%40googlegroups.com.