NullPointer exception in TLC

[MK Bug]

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.

[Stephan Merz]

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

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
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.

[MK Bug]

Hi,

Thanks a lot it did worked. What could be the reason?

Thanks for the observation as well, it did clear many points.

Regards,

Malaika

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CC1132D3-BA18-41DA-816F-17FAC790796B%40gmail.com.

[Markus Kuppe]

On 10.07.19 00:32, MK Bug wrote:
>
> I am facing an error while running TLC 
>
> An error has occurred. See error log for more details.
> java.lang.NullPointerException.

Hi,

without the log we won't be able to diagnose the problem. Please check
the .log file for errors and open a GitHub issue [1].

Thanks
Markus

[1]
https://tla.msr-inria.inria.fr/tlatoolbox/ci/doc/trouble/trouble.html#reporting