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:
VARIABLE status
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,
Martin