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

*From*: Zixian Cai <fzcz...@xxxxxxxxx>*Date*: Thu, 23 Aug 2018 12:38:48 +1000

Hi, Attached is my TLA module, translated from PlusCal. When I run the model checker, I got the following error:
I don’t quite understand why I’m getting this error as P is declared. When I replace the P in Spec at line 41 with 1..8, the model checker runs fine. Many thanks. Sincerely, Zixian -------------------------------- MODULE Dum -------------------------------- EXTENDS Integers, Sequences, TLC, FiniteSets (* --algorithm dum variables N = 8, P = 1..N; fair process p \in P variable n = 0 begin A: n := n + 1 end process end algorithm *) \* BEGIN TRANSLATION VARIABLES N, P, pc, n vars == << N, P, pc, n >> ProcSet == (P) Init == (* Global variables *) /\ N = 8 /\ P = 1..N (* Process p *) /\ n = [self \in P |-> 0] /\ pc = [self \in ProcSet |-> "A"] A(self) == /\ pc[self] = "A" /\ n' = [n EXCEPT ![self] = n[self] + 1] /\ pc' = [pc EXCEPT ![self] = "Done"] /\ UNCHANGED << N, P >> p(self) == A(self) Next == (\E self \in P: p(self)) \/ (* Disjunct to prevent deadlock on termination *) ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars) Spec == /\ Init /\ [][Next]_vars /\ \A self \in P : WF_vars(p(self)) Termination == <>(\A self \in ProcSet: pc[self] = "Done") \* END TRANSLATION ============================================================================= |

**Follow-Ups**:**Re: [tlaplus] Declared variables found undefined during evaluation***From:*Stephan Merz

- Prev by Date:
**How can I verify spec satisfies the properties for infinite states?** - Next by Date:
**Re: [tlaplus] Declared variables found undefined during evaluation** - Previous by thread:
**Re: [tlaplus] How can I verify spec satisfies the properties for infinite states?** - Next by thread:
**Re: [tlaplus] Declared variables found undefined during evaluation** - Index(es):