# Study TLA+

By [mizuki](https://paragraph.com/@mizuki) · 2021-11-25

---

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](http://lamport.azurewebsites.net/video/videos.html)

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
=======================================

Write`Variables 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'` = `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 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 of`pc = '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](https://lamport.azurewebsites.net/tla/tla.html)[A Summary of TLA+](https://lamport.azurewebsites.net/tla/summary.pdf)

---

*Originally published on [mizuki](https://paragraph.com/@mizuki/study-tla)*