TLA

Posted on September 2, 2022

Tags: functional

1 Summary

TLA+ is defined by:

VARIABLES
INIT
TRANSITIONS

Programs are state machines. Execution of digital system is a sequence of states. We want to describe all possible sequence of states of a system.

2 Part 1

Every computer has a program counter register(PC) that points to the current line of instruction. PC points to the current state.

int i;
void main()
{i=someNumber(); //pc="start"
 i=i+1;          //pc="middle"
}                //pc="done"

VARIABLES: \(i\)
INIT: \(i \in \mathbb{N}\)
TRANSITIONS: \(i \rightarrow i + 1\)

pc means current state pc pointer pc’ means next state pc pointer

IF pc==“start”
- THEN pc’ == “middle” and i’ (0,1000)
ELSEIF pc==“middle”
- THEN (i’ = i + 1) and (pc’ ==“done”)
ELSE FALSE

Basically saying if we are at this section of code, then our next section of code must satisfy some constraint.

switch 
   case pc == "start:
     Satisfy Constraint(pc,pc')
   case pc == "middle":
     Satisfy Constraint(pc,pc')
    ...

TLA+ notation for arrays:

meta-thought: arrays are really just partial functions and TLA+ makes this explicit.

TLA+ Notation: sqr = [i i^2 ]

code: sqrt[i] = i^2

3 TLA template

mkdir trial1
touch trial1.tla

------------------------------ MODULE trial1 ------------------------------- 
=============================================================================

------------------------------ MODULE trial1 ------------------------------- 
EXTENDS Naturals, TLC
(*--algorithm prog 
end algorithm;*)
=============================================================================

ctrl+shift+P : Check model with TLC –> generate trial1.cfg

SPECIFICATION Spec
\* Add statements after this line.
\* SPECIFICATION
\* Uncomment the previous line and provide the specification name if it's declared
\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.



\* INIT people
\* NEXT Next

\* PROPERTY
\* Uncomment the previous line and add property names

\* INVARIANT
\* Uncomment the previous line and add invariant names

3.1 Example 1

------------------------------ MODULE trial1 ------------------------------- 
EXTENDS Integers
(*--algorithm wire 
    variables
        people = {"a","b"},
        acc = [p \in people |-> 5],
        sender = "a",
        recv = "b",
        cnt = 3;
define 
    NoOver == \A p \in people: acc[p] >= 0
end define;
end algorithm;*)
=============================================================================

Ctrl+Shift+P > Parse module —> This will generate additional code in trial1.tla

INVARIANT
NoOver

4 Example 2

------------------------------ MODULE tutorial2 ------------------------------- 
\* Below we show an example of bad specification,
EXTENDS Naturals, TLC
(*--algorithm prog 
variables 
    a = 0; 
    critical_section = 0;

process Left=0
begin
    L1: a := a + 1; \* <--- This is Bad 
    L2: if a = 1 then 
        critical_section := critical_section + 1;
        L3: critical_section := critical_section - 1;
    end if
end process

process Right=1
begin
    L1: a := a + 1; \* <--- This is Bad
    L2: if a = 1 then 
        critical_section := critical_section + 1;
        L3: critical_section := critical_section - 1;
    end if
end process

end algorithm;*)
DeadlockCondition == critical_section < 2 /\ critical_section >= 0
=============================================================================

------------------------------ MODULE tutorial2 ------------------------------- 
\* Below we show an example of bad specification,
EXTENDS Naturals, TLC
(*--algorithm prog 
variables 
    a = 0; 
    critical_section = 0;

process Left=0
begin
    L1: a := a + 1; \* <--- This is Bad 
    L2: if a = 1 then 
        critical_section := critical_section + 1;
        L3: critical_section := critical_section - 1;
    end if
end process

process Right=1
begin
    L1: a := a + 1; \* <--- This is Bad
    L2: if a = 1 then 
        critical_section := critical_section + 1;
        L3: critical_section := critical_section - 1;
    end if
end process

end algorithm;*)
\* BEGIN TRANSLATION (chksum(pcal) = "48bb4a48" /\ chksum(tla) = "2434b8da")
\* Label L1 of process Left at line 11 col 9 changed to L1_
\* Label L2 of process Left at line 12 col 9 changed to L2_
\* Label L3 of process Left at line 14 col 13 changed to L3_
VARIABLES a, critical_section, pc

vars == << a, critical_section, pc >>

ProcSet == {0} \cup {1}

Init == (* Global variables *)
        /\ a = 0
        /\ critical_section = 0
        /\ pc = [self \in ProcSet |-> CASE self = 0 -> "L1_"
                                        [] self = 1 -> "L1"]

L1_ == /\ pc[0] = "L1_"
       /\ a' = a + 1
       /\ pc' = [pc EXCEPT ![0] = "L2_"]
       /\ UNCHANGED critical_section

L2_ == /\ pc[0] = "L2_"
       /\ IF a = 1
             THEN /\ critical_section' = critical_section + 1
                  /\ pc' = [pc EXCEPT ![0] = "L3_"]
             ELSE /\ pc' = [pc EXCEPT ![0] = "Done"]
                  /\ UNCHANGED critical_section
       /\ a' = a

L3_ == /\ pc[0] = "L3_"
       /\ critical_section' = critical_section - 1
       /\ pc' = [pc EXCEPT ![0] = "Done"]
       /\ a' = a

Left == L1_ \/ L2_ \/ L3_

L1 == /\ pc[1] = "L1"
      /\ a' = a + 1
      /\ pc' = [pc EXCEPT ![1] = "L2"]
      /\ UNCHANGED critical_section

L2 == /\ pc[1] = "L2"
      /\ IF a = 1
            THEN /\ critical_section' = critical_section + 1
                 /\ pc' = [pc EXCEPT ![1] = "L3"]
            ELSE /\ pc' = [pc EXCEPT ![1] = "Done"]
                 /\ UNCHANGED critical_section
      /\ a' = a

L3 == /\ pc[1] = "L3"
      /\ critical_section' = critical_section - 1
      /\ pc' = [pc EXCEPT ![1] = "Done"]
      /\ a' = a

Right == L1 \/ L2 \/ L3

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

Next == Left \/ Right
           \/ Terminating

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

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

\* END TRANSLATION 
DeadlockCondition == critical_section < 2 /\ critical_section >= 0
=============================================================================

INVARIANT
DeadlockCondition

Ctrl+Shift+P > Parse module

5 Example 3

5.1 Original program

int i;
void main()
 {i =someNumber();
  i = i+1;}

5.2 draft of spec

if (pc = "start")
  then ( i \in 0..1000) 
       (pc' = "middle")
  elif ( pc = "middle" )
       then (i' = i+1)
            (pc' = "done")
       else (FALSE)

5.3 Spec

\* SPECIFICATION
\* Uncomment the previous line and provide the specification name if it's declared
\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.


INIT Init
NEXT Next

\* PROPERTY
\* Uncomment the previous line and add property names

\* INVARIANT
\* Uncomment the previous line and add invariant names

------------------------------ MODULE simple ------------------------------- 
(***************************************************************************)
(* First, we write a spec that describes all allowable behaviors of our    *)
(* heros.                                                                  *)
(***************************************************************************)
EXTENDS Naturals
  (*************************************************************************)
  (* This statement imports the definitions of the ordinary operators on   *)
  (* natural numbers, such as +.                                           *)
  (*************************************************************************)
  
(***************************************************************************)
(* We next declare the specification's variables.                          *)
(***************************************************************************)
VARIABLES i, pc


(***************************************************************************)
(* We now define TypeOK to be the type invariant, asserting that the value *)
(* of each variable is an element of the appropriate set.  A type          *)
(* invariant like this is not part of the specification, but it's          *)
(* generally a good idea to include it because it helps the reader         *)
(* understand the spec.  Moreover, having TLC check that it is an          *)
(* invariant of the spec catches errors that, in a typed language, are     *)
(* caught by type checking.                                                *)
(*                                                                         *)
(* Note: TLA+ uses the convention that a list of formulas bulleted by /\   *)
(* or \/ denotes the conjunction or disjunction of those formulas.         *)
(* Indentation of subitems is significant, allowing one to eliminate lots  *)
(* of parentheses.  This makes a large formula much easier to read.        *)
(* However, it does mean that you have to be careful with your indentation.*)
(***************************************************************************)
TypeOK == /\ i \in 0..1000
          


(***************************************************************************)
(* Now we define of the initial predicate, that specifies the initial      *)
(* values of the variables.  I like to name this predicate Init, but the   *)
(* name doesn't matter.                                                    *)
(***************************************************************************)
Init ==  /\ (pc = "start") 
         /\ (i = 0)

(***************************************************************************)
(* Now we define the actions that our hero can perform.  There are three   *)
(* things they can do:                                                     *)
(*                                                                         *)
(*   - At Starting state we can pick any number from 0 to 1000             *)
(*                                                                         *)
(*   - At middle state we can add 1                                        *)
(*                                                                         *)
(*   - At middle state we can add 99                                       *)
(*                                                                         *)
(***************************************************************************)
Pick == \/ /\ pc = "start"
           /\ i' \in 0..1000
           /\ pc' = "middle"

Add1 == \/ /\ pc = "middle"
           /\ i' = i + 1
           /\ pc' = "done"

Add2 == \/ /\ pc = "middle"
           /\ i' = i + 99
           /\ pc' = "yum"




(***************************************************************************)
(* We define the next-state relation, which I like to call Next.  A Next   *)
(* step is a step of one of the six actions defined above.  Hence, Next is *)
(* the disjunction of those actions.                                       *)
(***************************************************************************)
Next == Pick \/ Add1 \/ Add2

Status
Checking coinchange.tla / coinchange.cfg
Errors 1 error(s)
Start: 15:01:27 (Oct 20), end: 15:01:27 (Oct 20)

States
Time	    Diameter	Found	  Distinct	Queue
00:00:00	3	        3,004	  3,004	    2,001
 
Coverage
Module	    Action  Total   Distinct
coinchange  Init	  2	      2

Errors
Deadlock reached.

Error Trace
1: Initial predicate
  i     0
  pc    "start"
2: Pick in simple
  i     0
  pc M  "middle"
3: Add1 in coinchange
  i M   1
  pc M  "done"

The error trace will only show the most recent error.
- Notice i couldve been any number from 0 to 1000 in "start" but the error trace only showed 0.
- Notice how Add2 doesnt show up since it takes the most recent error which is Add1

6 Deadlock

Deadlock means there is no successor state
- All terminating program Deadlocks by definition since last state is the deadlock state

7 Combining models

model A:

VARIABLES: \(i\)
INIT: \(i=0\)
TRANSITIONS: \((i \rightarrow i + 1) \lor (i \rightarrow i)\)

model B:

VARIABLES: \(j\)
INIT: \(j=0\)
TRANSITIONS: \((j \rightarrow j + 1) \lor (j \rightarrow j)\)

model A + B:

VARIABLES: \(i,j\)
INIT: \(i=0, j=0\)
TRANSITIONS: \((i \rightarrow i,j \rightarrow j) \lor (i \rightarrow i + 1,j \rightarrow j) \lor (i \rightarrow i,j \rightarrow j + 1) \lor (i \rightarrow i +1 ,j \rightarrow j+1)\)

  0,0 ---> 1,0 ---> 2,0 ... 
  |   \     |  \     |
  |      \  V    \   |
  0,1 --- > 1,1 ---> 2,1 ...
  |  \      |  \     |
  |     \   V    \   |

\(\bigcirc P\) : P is true in the SUCCESSOR step

graph LR; A[" "]-->B[" "]; B-->C["P"]; C-->D[" "]; D-->E[" "];

\(\square P\) : P is true at ALL times

graph LR; A["P"]-->B["P"]; B-->C["P"]; C-->D["P"]; D-->E["P"];

\(\diamond P\): P is EVENTUALLY true

graph LR; A[" "]-->B[" "]; B-->C[" "]; C-->D["P"]; D-->E[" "];

\(P u Q\) : P will be true UNTIL Q is true

graph LR; A["P"]-->B["P"]; B-->C["P"]; C-->D["Q"]; D-->E[" "];

\(P \leadsto Q\) : When P is true, Q WILL EVENTUALLY be TRUE

graph LR; A[" "]-->B["P"]; B-->C["P"]; C-->D[" "]; D-->E["Q"];