Hi Vahid,
in the Init action, the variable chain is a set.
However, the variable chain in Add action seems to be a sequence. Indeed the operator append aims at adding an element to the end of a sequence.
Since you want to build a chain of blocks, using a sequence makes sense. So the first thing to do consists in modifying the Init action as followed
/\ chain = <<"genesis">>
In the Add action, if you want to add a block b which is an element to the end of your chain which is a sequence, this is a way of formalizing it:
/\ chain' = Append(chain, b)
Note that predicate canAdd will be true before the first execution of action Add.
Once one element is added to your chain this predicate will be always false which prevents Add from being fired again.
I do not think this is what you really want this is why I advise you to comment or remove this predicate from action Add.
You will find below a new spec that includes my comments.
Hope that helps
Rachel
-------------------------------- MODULE Chain -------------------
EXTENDS Sequences
CONSTANT BLOCKS \* The set of blocks
VARIABLE chain, bState \* bState[b] is the state of block b.
TypeOK == bState \in [BLOCKS -> {"ADDED", "NOTADDED"}]
Init == /\ bState = [b \in BLOCKS |-> "NOTADDED"]
/\ chain = <<"genesis">>
canAdd == \A b \in BLOCKS : bState[b] \in {"NOTADDED"}
notAdded == \A b \in BLOCKS : bState[b] # "ADDED"
Add(b) == /\ bState[b] = "NOTADDED"
\* /\ canAdd
/\ chain' = Append(chain, b)
/\ bState' = [bState EXCEPT ![b] = "ADDED"]
Next == \E b \in BLOCKS : Add(b)
=================================================================