Re: [tlaplus] Issues with running TLA toolbox on Mac OS X 10.10.5

[Stephan Merz <stepha...@xxxxxxxxx>]

The line "====" indicates the end of the module, so TLC does not see any specification. Please move this line and the three following lines to the bottom of the module, following the line \* END TRANSLATION.

Hope this helps,
Stephan

> On 26 Oct 2015, at 16:00, gri...@xxxxxxxxx wrote:
> 
> 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
> 
> -- 
> 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...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.