Hi.
> it assigns the value of x in the next state as 7
Even for primed variables, it's just a formula (predicate). Not an assignment.
You can read x'= 7 as "It evaluates to true when the value of x in the next state is 7".
So Action A is just a formula that evaluates to true when x in current state is 5 and x's next state value is 7.
In short, actions are formulas over the state transitions (pair of current state and next state).
Maybe thinking like below might help to understand the TLA+ concept.
- TLA+ spec never defines the instructions of the system like ordinary programming languages. Rather, it defines the possible state transitions of the system.
- TLC explores the states that satisfy the spec.
Let's say we have the following spec:
Init == x = 5
A == /\ x = 5
/\ x' = 7
Next == A
When we run TLC, it works like:
- Find initial state (i.e. the assignment of the variables) that satisfy Init formula (x = 5)
- Starting from initial state, find next state that satisfy Next formula (current value of x is 5, so if next value of x is 7, it satisfies A)
- Update the current state and try to find next state, but there's no variable assignment that satisfies Next so it terminates with reporting Deadlock.