I study TLA+ for thinking algorithm of distributed system

TL;DR

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

Follows

Step 1: Start point

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; 
}

Step 2: Add variables state as comments

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
}

Step 3: Define program controll state variables

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"

Step 4: Re-Write those function driven by pc

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

Note initial state

Initial state formula i=0, pc=start

Step 4: Make it more simple

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

Step 5: Make it looks like mathematical expression

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

Step 6: Show `and`, `or`

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

Step 7: Check whether this expression is correct

Case 1

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

Case 2

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

And finish

no next state => false

Step 8: Using ASCII charactors

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

Step 9: Using variables

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"))

Step 10: ReFactoring

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"

Step 11: Rsult code

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

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

Step 12: Add `extends`, `variables`

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

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

Variables

Declares all variables in code.

Ref

The TLA+ Home Page
A Summary of TLA+

Studyh TLA+ (1)