| Hello,
in your module, P is a variable whereas TLC tells you that it expects an operator at line 41. You are shooting yourself in the foot by declaring constants as variables. You want to write the following:
---- MODULE Dum ---- EXTENDS ... CONSTANT N \* make N a constant parameter, to be instantiated in a Toolbox model
P == 1 .. N \* define the constant operator P using the parameter N
(* --algorithm dum ... *)
====
When you create a model in the Toolbox, it will ask you to provide a concrete value (such as 8) for N.
Regards, Stephan
Hi, Attached is my TLA module, translated from PlusCal. When I run the model checker, I got the following error:
TLC threw an unexpected exception. This was probably caused by an error in the spec or model. See the User Output or TLC Console for clues to what happened. The exception was a java.lang.RuntimeException : TLC cannot handle the temporal formula line 41, col 12 to line 41, col 43 of module Dum:
In evaluation, the identifier P is either undefined or not an operator. line 41, col 24 to line 41, col 24 of module Dum
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
=============================================================================
--
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.
|