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

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