I study TLA+ for thinking algorithm of distributed system.

Converting C lang code to TLA+.This post contains only information from these videos. The TLA+ Video Course

This is original code. I will convert this code.

int i;
void main(){
    i = someNumber(); // someNumber() returns a number in {0...1000}
    i = i + 1; 
}

WriteVariables state

int i;      // i = 0. In C language, global variables is initialized to zero.
void main(){
    i = someNumber(); // i in { 0...1000 }
    i = i + 1; // i = i + 1
}

Add program controll state (pc)

int i;      // i = 0, pc = "start" 
void main(){
    i = someNumber(); // i in { 0...1000 }, pc = "middle"
    i = i + 1; // i = i + 1, pc = "done"
} // pc = "done"

This expression is same as above C code. (In original video, uses THEN and block, but this note emits it)

if the current value of pc is "start":
    next i is in { 0...1000 }
    next pc is "middle"
else if the current value of pc is "middle":
    next i is i + 1
    next pc = "done"
else:
    no next state

Initial state formula i=0, pc=start

Convert some sentences as follows:

• the current value of pc => pc

• is => =

• next i => i'

if pc = "start":
    i' = in { 0...1000 }
    pc' = "middle"
else if pc = "middle":
    i' = i + 1
    pc' = "done"
else:
    no next state

Convert some sentences as follows:in => ∈

if pc = "start":
    i' ∈ { 0...1000 }
    pc' = "middle"
else if pc = "middle":
    i' = i + 1
    pc' = "done"
else:
    no next state

this code is single formula, implicit and(∧)

i' ∈ { 0...1000 }
pc' = "middle"

so, show

if pc = "start":
    (i' ∈ { 0...1000 }) ∧ (pc' = "middle")
else if pc = "middle":
    (i' = i + 1) ∧ (pc' = "done")
else:
    no next state

i=17, pc=start,i'=543, pc' = middleis true, because it enough above expression,

i=17, pc=middle,i'=123, pc' = doneis false, because i' dose not equal i+1,

no next state => false

Too hard to use ∧ in computer ('∧`)

• ∈ => \in

• ∧ => /\

if pc = "start":
    (i' \in { 0...1000 }) /\ (pc' = "middle")
else if pc = "middle":
    (i' = i + 1) /\ (pc' = "done")
else:
    no next state

I define two words as follows define A = (i' ∈ { 0...1000 }) ∧ (pc' = "middle") define B = (i' = i + 1) ∧ (pc' = "done")when the case of (pc = 'start') /\ A or the case of(pc = 'middle') /\ B, this formula is true.

or is ||, so this formula is((pc = 'start') /\ A || ((pc = 'middle') /\ B)

((pc = 'start') /\ ((i' ∈ { 0...1000 }) ∧ (pc' = "middle"))) ||
  ((pc = 'middle') /\ (i' = i + 1) ∧ (pc' = "done")) 

Remove useless parentheses

(pc = 'start' /\ i' ∈ { 0...1000 } /\ pc' = "middle") ||
  (pc = 'middle' /\ i' = i + 1 /\ pc' = "done") 

(pc = 'start' /\ i' ∈ { 0...1000 } /\ pc' = "middle")

Add /\ to the front ofpc = 'start'

    /\ pc = 'start'
    /\ i' ∈ { 0...1000 }
    /\ pc' = "middle"
\/
    /\ pc = 'middle'
    /\ i' = i + 1
    /\ pc' = "done"

Init == (pc = "start") /\ (i = 0)

Next == 
  /\ pc = 'start'
    /\ i' ∈ { 0...1000 }
    /\ pc' = "middle"
\/
    /\ pc = 'middle'
    /\ i' = i + 1
    /\ pc' = "done"

Extends Integer
Variables i, pc

Init == (pc = "start") /\ (i = 0)

Next == 
  /\ pc = 'start'
    /\ i' ∈ { 0...1000 }
    /\ pc' = "middle"
\/
    /\ pc = 'middle'
    /\ i' = i + 1
    /\ pc' = "done"

Extends is like import context. Extends Integer loads some arithmetic operator +,-,*, ... If you want to use prefix -, you should write Extends Naturals

Declares all variables in code.

The TLA+ Home PageA Summary of TLA+