Re: [tlaplus] NullPointer exception in TLC

On Wed, Jul 10, 2019 at 1:10 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

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

On 10 Jul 2019, at 09:32, MK Bug <android.ruba@xxxxxxxxx> wrote:

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.