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

[tlaplus] How to append to a chain?

Hi to all, 

I'm trying to add blocks from a CONSTANT BLOCKS to a chain of blocks. 
Here is how I wrote it:

-------------------------------- 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, ?)
          /\ bState' = [bState EXCEPT ![b] = "ADDED"]
Next == \E b \in BLOCKS : Add(b)

I don't know what I should put in the Append statement. 
I appreciate your help.


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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2156bde7-b896-48e9-951a-3e5688505c56n%40googlegroups.com.