[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Removing a label in a PlusCal algorithm changes the verification outcome



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

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

When removing the label e5, the TLA+ toolbox report a violation of the MutualExclusion invariant. I would expect that the presence of labels did not affect the correctness of invariance properties. Am I missing something, or is this a bug?

The version of the TLA+ Toolbox I am using 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/9ad59a2b-4a16-4f22-9d38-1101c348ee47n%40googlegroups.com.