TLA+ Tools on Mac OS X

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

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