The trick is that each "label" correspond to a step in time, and each step in time can only change a variable once. The lines
recycle.bin := Append(recycle.bin,itm);
recycle.count := recycle.count + 1;
recycle.capacity := recycle.capacity - itm.size;Update recycle three times, so the translator puts in three labels. You could update all three fields simultaneously like this:
recycle.bin := Append(recycle.bin,itm) || recycle.count := recycle.count + 1 || recycle.capacity := recycle.capacity - itm.size;
H
On 3/20/2025 10:14 PM, Akwasi Asante wrote:
Hello everyone,
I am a few pages into Hillel Wayne's book "Practical TLA+". In Chapter 2 (Pluscal), there is a example Pluscal algorithm titled "recycler". I typed it out into the TLA+ toolbox and got as expected. The book's example generates TLA+ with 2 actions Init and Lbl_1. I decided to try my hand at the same task by slightly modifying the variables used in the example. The toolbox gave me a translation with 6 actions (Init, Lbl_1, ..., Lbl_5); one per assignment within the if-else construct. I did not use any labels within the algorithm. Can someone shed some light on this or should I just keep reading on for the answer? Below is (first) my code, and then (second) the book's example, both with their translations. Thanks for your help.
Mine
------------------------------ MODULE scratch ------------------------------
EXTENDS Sequences, Integers, TLC, FiniteSets
PT == INSTANCE PT
(*--algorithm scratch
variables
\*x = <<1, [a |-> {}]>>; (*sequences/tuples do not require the same element type*)
\*z = {1,2,3,4,5}
trash = [bin |-> <<>>, capacity |-> 10, count |-> 0],
recycle = [bin |-> <<>>, capacity |-> 10, count |-> 0],
trash_type = {"recycle", "trash"},
items = [type: trash_type, size: 1..5],
itm = "";
define
Invariant1 == Len(trash.bin) = trash.count
Invariant2 == Len(recycle.bin) = recycle.count
end define;
begin
while items /= {} do
itm := CHOOSE x \in items: TRUE;
items := (items \ {itm});
if itm.type = "recycle" /\ itm.size < recycle.capacity then
recycle.bin := Append(recycle.bin,itm);
recycle.count := recycle.count + 1;
recycle.capacity := recycle.capacity - itm.size;
elsif itm.type = "trash" /\ itm.size < trash.capacity then
trash.bin := Append(trash.bin, itm);
trash.count := trash.count + 1;
trash.capacity := trash.capacity - itm.size;
end if;
end while;
end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "d94ba62c" /\ chksum(tla) = "7c8ce1a8")
VARIABLES trash, recycle, trash_type, items, itm, pc
(* define statement *)
Invariant1 == Len(trash.bin) = trash.count
Invariant2 == Len(recycle.bin) = recycle.count
vars == << trash, recycle, trash_type, items, itm, pc >>
Init == (* Global variables *)
/\ trash = [bin |-> <<>>, capacity |-> 10, count |-> 0]
/\ recycle = [bin |-> <<>>, capacity |-> 10, count |-> 0]
/\ trash_type = {"recycle", "trash"}
/\ items = [type: trash_type, size: 1..5]
/\ itm = ""
/\ pc = "Lbl_1"
Lbl_1 == /\ pc = "Lbl_1"
/\ IF items /= {}
THEN /\ itm' = (CHOOSE x \in items: TRUE)
/\ items' = (items \ {itm'})
/\ IF itm'.type = "recycle" /\ itm'.size < recycle.capacity
THEN /\ recycle' = [recycle EXCEPT !.bin = Append(recycle.bin,itm')]
/\ pc' = "Lbl_2"
/\ trash' = trash
ELSE /\ IF itm'.type = "trash" /\ itm'.size < trash.capacity
THEN /\ trash' = [trash EXCEPT !.bin = Append(trash.bin, itm')]
/\ pc' = "Lbl_4"
ELSE /\ pc' = "Lbl_1"
/\ trash' = trash
/\ UNCHANGED recycle
ELSE /\ pc' = "Done"
/\ UNCHANGED << trash, recycle, items, itm >>
/\ UNCHANGED trash_type
Lbl_2 == /\ pc = "Lbl_2"
/\ recycle' = [recycle EXCEPT !.count = recycle.count + 1]
/\ pc' = "Lbl_3"
/\ UNCHANGED << trash, trash_type, items, itm >>
Lbl_3 == /\ pc = "Lbl_3"
/\ recycle' = [recycle EXCEPT !.capacity = recycle.capacity - itm.size]
/\ pc' = "Lbl_1"
/\ UNCHANGED << trash, trash_type, items, itm >>
Lbl_4 == /\ pc = "Lbl_4"
/\ trash' = [trash EXCEPT !.count = trash.count + 1]
/\ pc' = "Lbl_5"
/\ UNCHANGED << recycle, trash_type, items, itm >>
Lbl_5 == /\ pc = "Lbl_5"
/\ trash' = [trash EXCEPT !.capacity = trash.capacity - itm.size]
/\ pc' = "Lbl_1"
/\ UNCHANGED << recycle, trash_type, items, itm >>
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars
Next == Lbl_1 \/ Lbl_2 \/ Lbl_3 \/ Lbl_4 \/ Lbl_5
\/ Terminating
Spec == Init /\ [][Next]_vars
Termination == <>(pc = "Done")
\* END TRANSLATION
=============================================================================
BOOK
------------------------------ MODULE recycler ------------------------------
EXTENDS Sequences, Integers, TLC, FiniteSets
(*--algorithm recycler
variables
capacity \in [trash: 1..10, recycle: 1..10],
bins = [trash |-> <<>>, recycle |-> <<>>],
count = [trash |-> 0, recycle |-> 0],
item = [type: {"recycle", "trash"}, size: (1..6)],
items \in item \X item \X item \X item,
curr = ""; \* helper: current item
macro add_item(type) begin
bins[type] := Append(bins[type], curr);
capacity[type] := capacity[type] - curr.size;
count[type] := count[type] + 1
end macro
begin
while items /= <<>> do
curr := Head(items);
items := Tail(items);
if curr.type = "recycle" /\ curr.size < capacity.recycle then
add_item("recycle");
elsif curr.size < capacity.trash then
add_item("trash");
end if;
end while;
assert capacity.trash >= 0 /\ capacity.recycle >= 0;
assert Len(bins.trash) = count.trash;
assert Len(bins.recycle) = count.recycle;
end algorithm;
*)
\* BEGIN TRANSLATION (chksum(pcal) = "b5dd3eef" /\ chksum(tla) = "676d113a")
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: {"recycle", "trash"}, 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 5.")
/\ Assert(Len(bins.trash) = count.trash,
"Failure of assertion at line 30, column 5.")
/\ Assert(Len(bins.recycle) = count.recycle,
"Failure of assertion at line 31, column 5.")
/\ pc' = "Done"
/\ UNCHANGED << capacity, bins, count, items, curr >>
/\ item' = item
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars
Next == Lbl_1
\/ Terminating
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 view this discussion visit https://groups.google.com/d/msgid/tlaplus/43a0fae8-ee97-45a0-955b-a0e543135099n%40googlegroups.com.