problems with the command-line tools

[Brian Beckman]

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

[Markus Kuppe]

On 14.03.19 10:36, Brian Beckman wrote:
> Hello --- 
>
> I'd be grateful for a little help running the command-line tools on
> Windows. I have placed them in this directory
>

> [...]


Hi Brian,

in the spec/model directory you want to run:

java -cp C:\Users\bbeckman\tla\tla tlc2.TLC wire.tla

but it will break on Java 11. Alternatively, you could just let the
Toolbox handle all of it for you.

Cheers
Markus

[Brian Beckman]

TY, Markus. That worked. I'll make a mental note that it won't with Java 11. 

(RE Toolbox, as an aside, I stay with command-line tools as much as possible to avoid RSI issues with the mouse in GUIs, but I know I'm a corner-case)