Issues with running TLA toolbox on Mac OS X 10.10.5

[gri...@xxxxxxxxx]

Hi there,

I've just installed the 1.5.1 version of the toolbox on my laptop running Mac OS X 10.10.5. 

I used the following archive file downloaded from the MSR-Inria joint centre to install the toolbox:  TLAToolbox-1.5.1-macosx.cocoa.x86_64.zip.

I've been trying out the OneBit mutex protocol PlusCal example from the TLA+ Hyperbook. 

As far as I can tell the code translated successfully into the TLA+ spec (please see below). 

However, when I'm creating a new model under the spec above, the Model Overview screen is showing the predicates for the initial and next-state relation being greyed-out, and "No behavior spec" being automatically  selected. As a result, I'm getting an NPE when trying to run the model as I guess, the model is not linked to the spec in any way...

I've also tried the One Bit Clock example, and seem to be getting the same results (i.e., "No behavior spec" being automatically selected, and no other options available even though the module appears to be successfully parsed). 

I wonder if I'm missing a configuration parameter of some sort, or the spec is somehow not being properly formulated/formatted? This is my first time trying to use the TLA Toolbox so I won't be surprised...

Many thanks,

-- Gregory

-------------------------------- MODULE Test --------------------------------


=============================================================================
\* Modification History
\* Last modified Sun Oct 25 23:22:06 GMT 2015 by uxac007
\* Created Sun Oct 25 23:22:00 GMT 2015 by uxac007
(**********************************
\* Modification History
\* Created Sun Oct 25 19:52:36 GMT 2015 by uxac007
--algorithm OneBitProtocol {
    variable x \in [{0,1} -> BOOLEAN];
    process (P \in {0,1})
        { r: while (TRUE)
            {   either { with (v \in BOOLEAN) { x[self] := v };
                            goto r
                        }
                or skip;
            e1: x[self] := TRUE;
            e2: if (~x[1-self]) { cs: skip };
        }
    }
}
***********************************)
\* BEGIN TRANSLATION
VARIABLES x, pc

vars == << x, pc >>

ProcSet == ({0,1})

Init == (* Global variables *)
        /\ x \in [{0,1} -> BOOLEAN]
        /\ pc = [self \in ProcSet |-> "r"]

r(self) == /\ pc[self] = "r"
           /\ \/ /\ \E v \in BOOLEAN:
                      x' = [x EXCEPT ![self] = v]
                 /\ pc' = [pc EXCEPT ![self] = "r"]
              \/ /\ TRUE
                 /\ pc' = [pc EXCEPT ![self] = "e1"]
                 /\ x' = x

e1(self) == /\ pc[self] = "e1"
            /\ x' = [x EXCEPT ![self] = TRUE]
            /\ pc' = [pc EXCEPT ![self] = "e2"]

e2(self) == /\ pc[self] = "e2"
            /\ IF ~x[1-self]
                  THEN /\ pc' = [pc EXCEPT ![self] = "cs"]
                  ELSE /\ pc' = [pc EXCEPT ![self] = "r"]
            /\ x' = x

cs(self) == /\ pc[self] = "cs"
            /\ TRUE
            /\ pc' = [pc EXCEPT ![self] = "r"]
            /\ x' = x

P(self) == r(self) \/ e1(self) \/ e2(self) \/ cs(self)

Next == (\E self \in {0,1}: P(self))

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

\* END TRANSLATION