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.