[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLA+ Tools on Mac OS X
The lines "--- MODULE <name> ---" and "====" are the top and bottom delimiters of a TLA+ module. In particular, anything that comes after "====" is not read by the tools, and your module is considered empty.
Best regards,
Stephan
On 28 Oct 2013, at 05:02, Charles Gordon <charles...@xxxxxxxxx> wrote:
> I'm having some difficulty getting started with the TLA+ tools on Mac OS X. I installed the TLA Toolbox as per the instructions on the website and it seemed to be working fine. As I started on the Hyperbook I realized that the parser always succeeds, regardless of whether there are errors or not (i.e., the green "Parsed" bar is always there). The only exception is if I get rid of the top line "---- <modulename> ----", when it gives me an error "Could not parse module OneBitClock from file OneBitClock.tla".
>
> I downloaded the Java tools (tla.zip) to see if I could reproduce the problem on the command line, and I can, so I don't think it has anything to do with the Toolbox GUI. After unpacking the tla.zip file, I do this:
>
>> cd tla
>> java -cp /Users/charles/Downloads/tla tla2sany.SANY OneBitClock.tla
>
> ****** SANY2 Version 2.1 created 27 March 2013
>
> Parsing file OneBitClock.tla
> Semantic processing of module OneBitClock
>
>
>
> Here is the OneBitClock.tla file, in total:
>
> ------------------- MODULE OneBitClock ------------------------
>
> ===============================================================
>
> Init1 == (b=0) \/ (b=1)
>
> Next1 == \/ /\ b = 0
> /\ b' = 1
> \/ /\ b = 1
> /\ b' = 0
>
> --
> 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/groups/opt_out.