Convence model in TLA (both tla files can be run with the same cfg)

Convergence.tla

---------------------------- MODULE Convergence ----------------------------
EXTENDS TLC, Integers


abs(n) == IF n < 0 THEN -n ELSE n

(***************************************************************************
--algorithm Convergence

variables
  position = 0, stepsLeft \in 1..10;

define
  EventuallyAlwaysAtZero == <>[](position = 0)
end define;

fair process StepNegative = "stepNegative"
begin
  StepNegative:
    await stepsLeft > 0;
    with newPosition = position - 1 do
      await abs(newPosition) < stepsLeft;
      position := newPosition;
      stepsLeft := stepsLeft - 1;
      goto StepNegative;
    end with;
end process;

fair process StepPositive = "stepPositive"
begin
  StepPositive:
    await stepsLeft > 0;
    with newPosition = position + 1 do
      await abs(newPosition) < stepsLeft;
      position := newPosition;
      stepsLeft := stepsLeft - 1;
      goto StepPositive;
    end with;
end process;
end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "a5da5ef1" /\ chksum(tla) = "bbeca4f1")
\* Label StepNegative of process StepNegative at line 20 col 5 changed to StepNegative_
\* Label StepPositive of process StepPositive at line 32 col 5 changed to StepPositive_
VARIABLES position, stepsLeft, pc

(* define statement *)
EventuallyAlwaysAtZero == <>[](position = 0)


vars == << position, stepsLeft, pc >>

ProcSet == {"stepNegative"} \cup {"stepPositive"}

Init == (* Global variables *)
        /\ position = 0
        /\ stepsLeft \in 1..10
        /\ pc = [self \in ProcSet |-> CASE self = "stepNegative" -> "StepNegative_"
                                        [] self = "stepPositive" -> "StepPositive_"]

StepNegative_ == /\ pc["stepNegative"] = "StepNegative_"
                 /\ stepsLeft > 0
                 /\ LET newPosition == position - 1 IN
                      /\ abs(newPosition) < stepsLeft
                      /\ position' = newPosition
                      /\ stepsLeft' = stepsLeft - 1
                      /\ pc' = [pc EXCEPT !["stepNegative"] = "StepNegative_"]

StepNegative == StepNegative_

StepPositive_ == /\ pc["stepPositive"] = "StepPositive_"
                 /\ stepsLeft > 0
                 /\ LET newPosition == position + 1 IN
                      /\ abs(newPosition) < stepsLeft
                      /\ position' = newPosition
                      /\ stepsLeft' = stepsLeft - 1
                      /\ pc' = [pc EXCEPT !["stepPositive"] = "StepPositive_"]

StepPositive == StepPositive_

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == StepNegative \/ StepPositive
           \/ Terminating

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(StepNegative)
        /\ WF_vars(StepPositive)

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

\* END TRANSLATION 

=============================================================================
\* Modification History
\* Last modified Wed Feb 16 13:40:01 BRT 2022 by gusbicalho
\* Created Wed Feb 16 13:25:56 BRT 2022 by gusbicalho

ConvergenceNonDet.tla

---------------------------- MODULE ConvergenceNonDet ----------------------------
EXTENDS TLC, Integers


abs(n) == IF n < 0 THEN -n ELSE n

(***************************************************************************
--algorithm ConvergenceNonDet

variables
  position = 0, stepsLeft \in 1..10;

define
  EventuallyAlwaysAtZero == <>[](position = 0)
end define;

fair process TakeStep = "takeStep"
begin
  TakeStep:
    await stepsLeft > 0;
    with newPosition \in {position - 1, position + 1} do
      await abs(newPosition) < stepsLeft;
      position := newPosition;
      stepsLeft := stepsLeft - 1;
      goto TakeStep;
    end with;
end process;
end algorithm; *)

\* BEGIN TRANSLATION (chksum(pcal) = "9d5585c9" /\ chksum(tla) = "ca972378")
\* Label TakeStep of process TakeStep at line 20 col 5 changed to TakeStep_
VARIABLES position, stepsLeft, pc

(* define statement *)
EventuallyAlwaysAtZero == <>[](position = 0)


vars == << position, stepsLeft, pc >>

ProcSet == {"takeStep"}

Init == (* Global variables *)
        /\ position = 0
        /\ stepsLeft \in 1..10
        /\ pc = [self \in ProcSet |-> "TakeStep_"]

TakeStep_ == /\ pc["takeStep"] = "TakeStep_"
             /\ stepsLeft > 0
             /\ \E newPosition \in {position - 1, position + 1}:
                  /\ abs(newPosition) < stepsLeft
                  /\ position' = newPosition
                  /\ stepsLeft' = stepsLeft - 1
                  /\ pc' = [pc EXCEPT !["takeStep"] = "TakeStep_"]

TakeStep == TakeStep_

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == TakeStep
           \/ Terminating

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(TakeStep)

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

\* END TRANSLATION 

=============================================================================
\* Modification History
\* Last modified Wed Feb 16 13:49:53 BRT 2022 by gusbicalho
\* Created Wed Feb 16 13:25:56 BRT 2022 by gusbicalho

MC.cfg

\* SPECIFICATION definition
SPECIFICATION
Spec
\* PROPERTY definition
PROPERTY
EventuallyAlwaysAtZero