Subscribe to mizuki

<100 subscribers

Subscribe to mizuki

<100 subscribers

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 control 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' = middleis true, because it enough above expression,

Case 2

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

And finish

no next state => false

Step 8: Using ASCII characters

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: Result 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+

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 control 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' = middleis true, because it enough above expression,

Case 2

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

And finish

no next state => false

Step 8: Using ASCII characters

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

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: Result 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+

No activity yet

mizuki

No activity yet

No activity yet

No activity yet

Study TLA+

Study TLA+

TL;DR

Follows

Step 1: Start point

Step 2: Add variables state as comments

Step 3: Define program control state variables

Step 4: Re-Write those function driven by pc

Note initial state

Step 4: Make it more simple

Step 5: Make it looks like mathematical expression

Step 6: Show and, or

Step 7: Check whether this expression is correct

Case 1

Case 2

And finish

Step 8: Using ASCII characters

Step 9: Using variables

Step 10: ReFactoring

Step 11: Result code

Step 12: Add extends, variables

Extends

Variables

Ref

TL;DR

Follows

Step 1: Start point

Step 2: Add variables state as comments

Step 3: Define program control state variables

Step 4: Re-Write those function driven by pc

Note initial state

Step 4: Make it more simple

Step 5: Make it looks like mathematical expression

Step 6: Show and, or

Step 7: Check whether this expression is correct

Case 1

Case 2

And finish

Step 8: Using ASCII characters

Step 9: Using variables

Step 10: ReFactoring

Step 11: Result code

Step 12: Add extends, variables

Extends

Variables

Ref