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

# Step 1: Start point

This is original code. I will convert this code.

int i;
void main(){
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
}


# 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.