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

Re: [tlaplus] Problem with instance substitutions

Stephan, you are correct that there is no mention of motion in case. But this is due to me trying to get one thing working at a time. I was stuck on motions when next function wouldn't work. (I had MNext == mState = \E m \in M : MotionResponse(m) vs MNext == \E m \in M : MotionResponse(m). Was getting an error about nested arg. Didn't even notice I put "mState =" into the equation until after...ummm...2-3hrs of experimenting.)

So I'm just moving slowly as I attempt to put a spec together from scratch vs the ones from the video and books. Slow frustrating process as is the case with programming and now TLA^+.

Now that I have it working, I'm going to fill out the rest of the spec.

Lastly, yes, your comment helps. I'm writing down everything that seems to be unclear or not clearly stated from my perspective to create a help doc for those of use who need a little more hand holding until we can walk on our own.

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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.