Re: [tlaplus] TLA+ Tools on Mac OS X

[Charles Gordon <charles...@xxxxxxxxx>]

Yep, it even says that clearly in the hyperbook; I was just copying and pasting out the text in the "ascii" popups and didn't read that paragraph. Thanks!

On Monday, October 28, 2013 12:44:57 AM UTC-7, Stephan Merz wrote:
> 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.