[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLA+ Toolbox 1.5.4 release


just to reproduce the behavior that you describe, I followed to the letter the instructions in section 2.3 of the hyperbook. Attached is the screenshot of the (expected) result. I am working in Mac OS (version 10.13.2), Toolbox v1.5.4, Oracle Java 8. If you could not resolve your issue, perhaps attach your TLA+ module.


On 1 Jan 2018, at 21:44, Thomas Clifford <thomascl...@xxxxxxxxx> wrote:

Good day,  I have just downloaded and installed the Win32/64 version of TLA+ Toolbox, v1.5.4, and I'm going through the 
hyperbook, at the point where it creates a OneBitClock.  It tells me the code given will show errors because the 'b' variable is not 
defined, but when I save the code without adding the 'VARIABLE b' line to the code, no error window or dialog pops up.
I also cannot find in any of the menus or preferences where to enable/disable the 'Parsing Errors view'.

I'm running Windows Pro 7, Sun Java 8_144.

Thank you and I look forward to learning more about correcting disconnects between process analysis / design / specification and the 
development of software.