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.