# Study TLA+

**Published by:** [mizuki](https://paragraph.com/@mizuki/)
**Published on:** 2021-11-25
**URL:** https://paragraph.com/@mizuki/study-tla

## Content

I study TLA+ for thinking algorithm of distributed system.TL;DRConverting C lang code to TLA+.This post contains only information from these videos. The TLA+ Video CourseFollowsStep 1: Start pointThis 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 commentsWriteVariables stateint 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 variablesAdd 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 pcThis 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 stateInitial state formula i=0, pc=startStep 4: Make it more simpleConvert some sentences as follows:the current value of pc => pcis => =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 expressionConvert 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, orthis code is single formula, implicit and(∧)i' ∈ { 0...1000 } pc' = "middle" so, showif 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 correctCase 1i=17, pc=start,i'=543, pc' = middleis true, because it enough above expression,Case 2i=17, pc=middle,i'=123, pc' = doneis false, because i' dose not equal i+1,And finishno next state => falseStep 8: Using ASCII charactersToo 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 variablesI 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: ReFactoringRemove 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 codeInit == (pc = "start") /\ (i = 0) Next == /\ pc = 'start' /\ i' ∈ { 0...1000 } /\ pc' = "middle" \/ /\ pc = 'middle' /\ i' = i + 1 /\ pc' = "done" Step 12: Add extends, variablesExtends Integer Variables i, pc Init == (pc = "start") /\ (i = 0) Next == /\ pc = 'start' /\ i' ∈ { 0...1000 } /\ pc' = "middle" \/ /\ pc = 'middle' /\ i' = i + 1 /\ pc' = "done" ExtendsExtends is like import context. Extends Integer loads some arithmetic operator +,-,*, ... If you want to use prefix -, you should write Extends NaturalsVariablesDeclares all variables in code.RefThe TLA+ Home PageA Summary of TLA+

## Publication Information

- [mizuki](https://paragraph.com/@mizuki/): Publication homepage
- [All Posts](https://paragraph.com/@mizuki/): More posts from this publication
- [RSS Feed](https://api.paragraph.com/blogs/rss/@mizuki): Subscribe to updates
- [Twitter](https://twitter.com/mizuki_sonoko): Follow on Twitter