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

# why need /\ item' = item?

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

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