Re: [tlaplus] why need /\ item' = item?

[Stephan Merz <stepha...@xxxxxxxxx>]

Did you experiment what happens when you comment out the conjunct?

The next-state action needs to fix the values of all variables in the successor state. Since neither the THEN nor the ELSE branch of action Lbl_1 fix the value of variable `item' (note that you have both variables `item' and `items'), the PlusCal translator inserted the conjunct to ensure that `item' doesn't change.

Without such UNCHANGED conjuncts, the value of the variable in the successor state of an action would be completely unconstrained, which is certainly not what you want, and TLC would signal an error.

Since the value of `item' never changes during executions, perhaps it would make more sense to declare it as a constant parameter (or a definition) rather than a variable?

Regards,
Stephan


> On 23 Jan 2019, at 09:00, john con <conjo...@xxxxxxxxx> wrote:
> 
> ------------------------------ MODULE recycler ------------------------------
> EXTENDS Sequences, Integers, TLC, FiniteSets
> 
> \* BEGIN TRANSLATION
> VARIABLES capacity, bins, count, item, items, curr, pc
> 
> vars == << capacity, bins, count, item, items, curr, pc >>
> 
> Init == (* Global variables *)
>        /\ capacity \in [trash: 1..10, recycle: 1..10]
>        /\ bins = [trash |-> <<>>, recycle |-> <<>>]
>        /\ count = [trash |-> 0, recycle |-> 0]
>        /\ item = [type: {"trash", "recycle"}, size: 1..6]
>        /\ items \in item \X item \X item \X item
>        /\ curr = ""
>        /\ pc = "Lbl_1"
> 
> Lbl_1 == /\ pc = "Lbl_1"
>         /\ IF items /= <<>>
>               THEN /\ curr' = Head(items)
>                    /\ items' = Tail(items)
>                    /\ IF curr'.type = "recycle" /\ curr'.size < capacity.recycle
>                          THEN /\ bins' = [bins EXCEPT !["recycle"] = Append(bins["recycle"], curr')]
>                               /\ capacity' = [capacity EXCEPT !["recycle"] = capacity["recycle"] - curr'.size]
>                               /\ count' = [count EXCEPT !["recycle"] = count["recycle"] + 1]
>                          ELSE /\ IF curr'.size < capacity.trash
>                                     THEN /\ bins' = [bins EXCEPT !["trash"] = Append(bins["trash"], curr')]
>                                          /\ capacity' = [capacity EXCEPT !["trash"] = capacity["trash"] - curr'.size]
>                                          /\ count' = [count EXCEPT !["trash"] = count["trash"] + 1]
>                                     ELSE /\ TRUE
>                                          /\ UNCHANGED << capacity, bins, 
>                                                          count >>
>                    /\ pc' = "Lbl_1"
>               ELSE /\ Assert(capacity.trash >= 0 /\ capacity.recycle >= 0, 
>                              "Failure of assertion at line 29, column 6.")
>                    /\ Assert(Len(bins.trash) = count.trash, 
>                              "Failure of assertion at line 30, column 6.")
>                    /\ Assert(Len(bins.recycle) = count.recycle, 
>                              "Failure of assertion at line 31, column 6.")
>                    /\ pc' = "Done"
>                    /\ UNCHANGED << capacity, bins, count, items, curr >>
>         /\ item' = item  (* why need this ? *)
> 
> Next == Lbl_1
>           \/ (* Disjunct to prevent deadlock on termination *)
>              (pc = "Done" /\ UNCHANGED vars)
> 
> Spec == Init /\ [][Next]_vars
> 
> Termination == <>(pc = "Done")
> 
> \* END TRANSLATION
> 
> =============================================================================
> 
> -- 
> 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...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.