How to append to a chain?

[Vahid Heidaripour]

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.

V.

[Rachel Delafon]

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)

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

[Vahid Heidaripour]

Thank you for your response.

I understand that it's wrong, the way that I added 'canAdd'.

I changed it like this:

-------------------------------- MODULE Tree --------------------------------
EXTENDS Integers, Sequences

CONSTANT BLOCKS \* The set of blocks

VARIABLE chain, bState, round \* bState[b] is the state of block b.
vars == <<chain, bState, round>>

TypeOK == /\ round \in Nat
          /\ bState \in [BLOCKS -> {"ADDED", "NOTADDED"}]

Init == /\ bState = [b \in BLOCKS |-> "NOTADDED"]

        /\ round = 1
        /\ chain = <<<<"genesis", 0, "nil">>>> \* <<name, round, parent>>

Add(b) == /\ bState[b] = "NOTADDED"

          /\ IF chain[Len(chain)][2] < round
             THEN /\ chain' = Append(chain, <<b, round, chain[Len(chain)][1]>>)

                  /\ bState' = [bState EXCEPT ![b] = "ADDED"]

                  /\ round' = round + 1
             ELSE UNCHANGED vars

         
Next == \E b \in BLOCKS : Add(b)

=============================================================================

Cheers,

Vahid

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAMCHOhN64NWoQEP7UxPZ6emFY9ZhBPnw9SQzpCsdbPBCejPhAQ%40mail.gmail.com.