[tlaplus] problems with the command-line tools

Hello ---

I'd be grateful for a little help running the command-line tools on Windows. I have placed them in this directory

 Directory of C:\Users\bbeckman\tla\tla

03/14/2019  10:00 AM    <DIR>          .
03/14/2019  10:00 AM    <DIR>          ..
03/14/2019  08:35 AM    <DIR>          com
03/14/2019  08:35 AM    <DIR>          examples
03/14/2019  08:35 AM    <DIR>          javax
03/14/2019  08:35 AM             4,959 License.txt
03/14/2019  08:35 AM    <DIR>          META-INF
03/14/2019  08:35 AM    <DIR>          model
03/14/2019  08:35 AM    <DIR>          pcal
03/14/2019  08:35 AM               645 README
03/14/2019  10:24 AM    <DIR>          states
03/14/2019  08:35 AM    <DIR>          tla2sany
03/14/2019  08:35 AM    <DIR>          tla2tex
03/14/2019  08:35 AM    <DIR>          tlc2
03/14/2019  08:35 AM    <DIR>          util
               2 File(s)          5,604 bytes

I have set my CLASSPATH as follows:

C:\Users\bbeckman\tla\tla>set
...
CLASSPATH=c:\Users\bbeckman\tla\tla
...

Java seems to be accessible:

C:\Users\bbeckman\tla\tla>java -version
java version "1.8.0_201"
Java(TM) SE Runtime Environment (build 1.8.0_201-b09)
Java HotSpot(TM) 64-Bit Server VM (build 25.201-b09, mixed mode)

Now I try to run tlc2.TLC in two different ways, both failing. Way #1, the current directory is the tools directory and the spec I want to check is in another directory (the spec checks out in the Eclipse toolbox, so I do not suspect that the spec is bad):

C:\Users\bbeckman\tla\tla>java tlc2.TLC ..\..\Documents\GitHub\TLASpecs\wire
TLC2 Version 2.13 of 18 July 2018
Running breadth-first search Model-Checking with seed 463029695021380323 with 1 worker on 12 cores with 14500MB heap and 64MB offheap memory (Windows 10 10.0 amd64, Oracle Corporation 1.8.0_201 x86_64).
Parsing file C:\Users\bbeckman\Documents\GitHub\TLASpecs\wire.tla
Parsing file C:\Users\bbeckman\tla\tla\tla2sany\StandardModules\Integers.tla
Parsing file C:\Users\bbeckman\tla\tla\tla2sany\StandardModules\Naturals.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module wire
Starting... (2019-03-14 10:31:01)
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.NullPointerException
java.lang.NullPointerException
        at tlc2.tool.Spec.processSpec(Spec.java:204)
        at tlc2.tool.Tool.init(Tool.java:110)
        at tlc2.tool.AbstractChecker.<init>(AbstractChecker.java:91)
        at tlc2.tool.ModelChecker.<init>(ModelChecker.java:83)
        at tlc2.TLC.process(TLC.java:894)
        at tlc2.TLC.main(TLC.java:220)

Finished in 00s at (2019-03-14 10:31:01)

Ok, so I change the current working directory to where the spec lives, and try to reach over to where the tools live:

C:\Users\bbeckman\Documents\GitHub\TLASpecs>java ..\..\..\tla\tla\tlc2.TLC .\wire
Error: Could not find or load main class ..\..\..\tla\tla\tlc2.TLC

Just in case you don't trust me about the spec, here it is:

-------------------------------- MODULE wire --------------------------------
EXTENDS Integers
(*--algorithm wire
variables
    people = {"alice", "bob"},
    acc = [p \in people |-> 5];
define
    NoOverdrafts == \A p \in people: acc[p] >= 0
end define;    
process Wire \in 1..2
    variables
        sender = "alice",
        receiver = "bob",
        amount \in 1..acc[sender];
begin
    CheckAndWithdraw:
        if amount <= acc[sender] then
                acc[sender] := acc[sender] - amount;
            Deposit:
                acc[receiver] := acc[receiver] + amount;
        end if;
end process;
end algorithm;*)
\* BEGIN TRANSLATION
VARIABLES people, acc, pc

(* define statement *)
NoOverdrafts == \A p \in people: acc[p] >= 0

VARIABLES sender, receiver, amount

vars == << people, acc, pc, sender, receiver, amount >>

ProcSet == (1..2)

Init == (* Global variables *)
        /\ people = {"alice", "bob"}
        /\ acc = [p \in people |-> 5]
        (* Process Wire *)
        /\ sender = [self \in 1..2 |-> "alice"]
        /\ receiver = [self \in 1..2 |-> "bob"]
        /\ amount \in [1..2 -> 1..acc[sender[CHOOSE self \in  1..2 : TRUE]]]
        /\ pc = [self \in ProcSet |-> "CheckAndWithdraw"]

CheckAndWithdraw(self) == /\ pc[self] = "CheckAndWithdraw"
                          /\ IF amount[self] <= acc[sender[self]]
                                THEN /\ acc' = [acc EXCEPT ![sender[self]] = acc[sender[self]] - amount[self]]
                                     /\ pc' = [pc EXCEPT ![self] = "Deposit"]
                                ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
                                     /\ acc' = acc
                          /\ UNCHANGED << people, sender, receiver, amount >>

Deposit(self) == /\ pc[self] = "Deposit"
                 /\ acc' = [acc EXCEPT ![receiver[self]] = acc[receiver[self]] + amount[self]]
                 /\ pc' = [pc EXCEPT ![self] = "Done"]
                 /\ UNCHANGED << people, sender, receiver, amount >>

Wire(self) == CheckAndWithdraw(self) \/ Deposit(self)

Next == (\E self \in 1..2: Wire(self))
           \/ (* Disjunct to prevent deadlock on termination *)
              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

=============================================================================
\* Modification History
\* Last modified Mon Oct 15 18:38:35 PDT 2018 by rebcabin
\* Created Mon Oct 15 13:09:48 PDT 2018 by rebcabin