Re: [tlaplus] How to append to a chain?

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

On Thu, Feb 11, 2021 at 3:41 PM Rachel Delafon <bad.restuko@xxxxxxxxx> wrote:

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)
=================================================================

On Thu, Feb 11, 2021 at 10:55 AM Vahid Heidaripour <v.heidaripour@xxxxxxxxx> wrote:
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.

--
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.

--
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/CAMCHOhN64NWoQEP7UxPZ6emFY9ZhBPnw9SQzpCsdbPBCejPhAQ%40mail.gmail.com.