Hello, hard to tell what you actually did – the second screenshot shows that TLC is not running but does not indicate any trace of it having run previously. Attached is the module that you are supposed to write. Create a new model from it, enter "Init1" and "Next1" in the fields "Init" and "Next" of the model overview pane, and hit the green triangle to run TLC. You should see the error described in the hyperbook. Regards, Stephan
Attachment:
OneBitClock.tla
Description: Binary data
> On 5 Jan 2017, at 07:08, jsma...@xxxxxxxxx wrote: > > Hi, > > I feel somewhat silly posting this as I can see this is a very entry level problem - but I've been stuck on it long enough it's time to reach out. > > For background, I've started working through the current Hyperbook. The first issue I hit, in section 2.3, I found if you literally copy + paste the "ASCII version" of the code, you'll just hit a parser error: > > Lexical error ... encountered "\u2019" (8217) > > Having gotten used to Windows mangling quotes such that ASCII wasn't ASCII at all, I changed b’ into b' and moved on. > > Moving on, I created a model, ran the model checker and it ran fine, then inserted the "string" as defined in section 2.5. The attempt to break the model at this point doesn't seem to work for me, as I've saved, parsed, recreated the model, and generally done what I can to make it produce an error and been unsuccessful. > > Hopefully with these screenshots someone can point me in the right direction. They include all relevant versions. > > https://d86c84grgz45x.cloudfront.net/tla1.PNG > https://d86c84grgz45x.cloudfront.net/tla2.PNG > > PS I'm using the 32-bit Toolbox because the 64-bit version just gave me a Java error on start. > > Thanks in advance for any advice. > > -- > 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 https://groups.google.com/group/tlaplus. > For more options, visit https://groups.google.com/d/optout.