| Hello,
I cannot reproduce your error: when copying and pasting your spec into the Toolbox, creating a model with Z=10 and checking the invariant NUMCHECK (+ absence of deadlock), TLC computes 80 states (60 distinct states) and terminates normally without finding an error. May I suggest that you delete the specification from the Toolbox (in the sidebar, click on the icon "T+", right-click on module Testing in the list, choose "Delete" and confirm), then reload it.
Two observations:
- The TLA+ translation doesn't correspond to the PlusCal algorithm (the statement labeled A adds Z to alice_account whereas the TLA+ translation subtracts Z). When you edit your PlusCal algorithm, you have to regenerate the TLA+ (File -> Translate PlusCal Algorithm).
- NUMCHECK only mentions the constant Z, it is independent of the reachable states of your specification. Better make it an assumption
ASSUME Z \in Nat /\ Z < 1000
that TLC will check only once at startup instead of at every state that it computes.
Regards, Stephan
Hi,
I am facing an error while running TLC
An error has occurred. See error log for more details.
java.lang.NullPointerException.
------------------------------ MODULE Testing ------------------------------
EXTENDS Naturals, TLC
CONSTANT Z
(* --algorithm transfer
variables alice_account = 10, bob_account = 10, money \in 1..20;
begin
A: alice_account := alice_account + Z;
B: bob_account := bob_account + money;
end algorithm *)
\* BEGIN TRANSLATION
VARIABLES alice_account, bob_account, money, pc
vars == << alice_account, bob_account, money, pc >>
Init == (* Global variables *)
/\ alice_account = 10
/\ bob_account = 10
/\ money \in 1..20
/\ pc = "A"
A == /\ pc = "A"
/\ alice_account' = alice_account - Z
/\ pc' = "B"
/\ UNCHANGED << bob_account, money >>
B == /\ pc = "B"
/\ bob_account' = bob_account + money
/\ pc' = "Done"
/\ UNCHANGED << alice_account, money >>
Next == A \/ B
\/ (* Disjunct to prevent deadlock on termination *)
(pc = "Done" /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(pc = "Done")
\* END TRANSLATION
NUMCHECK == Z \in Nat /\ Z < 1000
=============================================================================
My Model contains :
Z = 10
and in invariant I have checked this NUMCHECK
Thanks in advance.
--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CA%2BkanULdBcArS%3D6je0LVSfdOFih2coihtRZQdaC8y_u-oE%2BU6A%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CC1132D3-BA18-41DA-816F-17FAC790796B%40gmail.com.
For more options, visit https://groups.google.com/d/optout.
|