问没有通过追加或尾调用更新TLA+序列

EN

---- MODULE transfer ----
EXTENDS Naturals, TLC, Sequences

(* --algorithm transfer

\* Simple algorithm:
\*  1. Start with a shared-memory list with one element.
\*  2. A process adds arbitrary numbers of elements to the list.
\*  3. Another process removes arbitrary numbers of elements from the list, 
\*     but only if the list has more than one item in it. This check is 
\*     applied just before trying to removing an element. 
\* Is it true that the list will always have a length of 1? 
\* You would expect this to be false, since the adder process can add more elements 
\* than the remover process can consume.

variables stack = <<0>>

process Adder = 0
  begin
      AddElement:
        stack := Append(stack, Len(stack));
        either goto AddElement
        or skip
        end either;
end process;

process Remover = 1
  begin
      RemoveElement:
        \* Pop from the front of the stack
        if Len(stack) > 1 then
            stack := Tail(stack);
        end if;
        either goto RemoveElement
        or skip
        end either;
end process;

end algorithm *)

IsStackAlwaysUnitLength == Len(stack) = 1

====

process Adder = 0
  begin
      AddElement:
        print stack;
        print "Adder applied!";
        stack := Append(stack, Len(stack));
        print stack;
        print "Adder task complete!";
        \* Force 
        either goto AddElement
        or skip
        end either;
end process;

process Remover = 1
  begin
      RemoveElement:
        \* Pop from the front of the stack
        print stack;
        print "Remover applied!";
        if Len(stack) > 1 then
            stack := Tail(stack);
            print stack;
            print "Remover task complete!";
        else
            print "Remover task complete!";
        end if;
        either goto RemoveElement
        or skip
        end either;
end process;

<<0>>
"Adder applied!"
<<0>>
"Adder task complete!"
<<0>>
<<0>>
"Remover applied!"
"Remover applied!"
"Remover task complete!"
"Remover task complete!"
<<0>>
"Adder applied!"
<<0>>
"Adder task complete!"

---- MODULE transfer ----
EXTENDS Naturals, TLC, Sequences

(* --algorithm transfer

variables stack = <<0>>

process Adder = 0
  begin
      AddElement:
        stack := Append(stack, Len(stack));
        either goto AddElement
        or skip
        end either;
end process;

process Remover = 1
  begin
      RemoveElement:
        \* Pop from the front of the stack
        if Len(stack) > 1 then
            stack := Tail(stack);
        end if;
        either goto RemoveElement
        or skip
        end either;
end process;

end algorithm *)
\* BEGIN TRANSLATION
VARIABLES stack, pc

vars == << stack, pc >>

ProcSet == {0} \cup {1}

Init == (* Global variables *)
        /\ stack = <<0>>
        /\ pc = [self \in ProcSet |-> CASE self = 0 -> "AddElement"
                                        [] self = 1 -> "RemoveElement"]

AddElement == /\ pc[0] = "AddElement"
              /\ stack' = [stack EXCEPT ![0] = Append(stack, Len(stack))]
              /\ \/ /\ pc' = [pc EXCEPT ![0] = "AddElement"]
                 \/ /\ TRUE
                    /\ pc' = [pc EXCEPT ![0] = "Done"]

Adder == AddElement

RemoveElement == /\ pc[1] = "RemoveElement"
                 /\ IF Len(stack) > 1
                       THEN /\ stack' = [stack EXCEPT ![1] = Tail(stack)]
                       ELSE /\ TRUE
                            /\ stack' = stack
                 /\ \/ /\ pc' = [pc EXCEPT ![1] = "RemoveElement"]
                    \/ /\ TRUE
                       /\ pc' = [pc EXCEPT ![1] = "Done"]

Remover == RemoveElement

Next == Adder \/ Remover
           \/ (* Disjunct to prevent deadlock on termination *)
              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

IsStackAlwaysUnitLength == Len(stack) = 1

====