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

Re: [tlaplus] Defining 3 successive states

Hello Imran,

An action describes how the current state relates to the next. You could
add a variable status and use it to remember what you were about to do:


Init == status = "read"
Next ==  \/  status = "read" /\ status' = "process"
         \/  status = "process" /\ status' = "write"

I am using strings to represent the different states because different
strings are always different (for arbitrary constants a,b I would need
to add an axiom a /= b ). The relation above doesn't do anything beyond
changing the status yet - anything more would go as an additional
conjunct for the status it is intended for.

hope this helps,

On 3/24/19 5:58 AM, Imran Meah wrote:
> I know we can define 2 state states machine (say states A and B) by using Next operator. My question is how do I define 3 or more states.
> For example, read, process, write and I want the state to transition like this 
> read -> process -> write

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.