Added basic TLA+ lecture

Author: OliverKillane

60009 - Distributed Algorithms/60009 - Distributed Algorithms.pdf

@@ -6,6 +6,7 @@
 
 \usepackage[a4paper, total={7in, 10in}]{geometry}
 \input{../common/common.tex}
+\usepackage{packages/tlatex}
 
 \definecolor{threadBlue}{RGB}{204, 229, 255}
 \definecolor{threadYellow}{RGB}{255, 255, 136}
@@ -25,6 +26,8 @@
 
 \addchapter{consensus}
 
+\addchapter{tla_plus}
+
 \addchapter{credit}
 
 \end{document}

60009 - Distributed Algorithms/60009 - Distributed Algorithms.tex

@@ -119,7 +119,7 @@ \subsection{Valent Configurations}
 \subsection{Lemmas}
 \subsubsection{Confluence}
 \begin{center}
-    \includegraphics[width=.6\textwidth]{consensus/images/lemma_confluence.drawio.png}
+    \includegraphics[width=.3\textwidth]{consensus/images/lemma_confluence.drawio.png}
 \end{center}
 Given configuration $C$ and \textit{schedules} $\sigma_1$ and $\sigma_2$ such that set of processes with steps in $\sigma_1$ and $\sigma_2$ are disjoint:
 \[\sigma_1(\sigma_2(C)) \equiv \sigma_2(\sigma_1(C))\]

60009 - Distributed Algorithms/consensus/consensus.tex

@@ -0,0 +1,15 @@
+\* SPECIFICATION
+\* Uncomment the previous line and provide the specification name if it's declared
+\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.
+
+CONSTANTS
+    greeting = "Hello"
+
+INIT Init
+NEXT Next
+
+\* PROPERTY
+\* Uncomment the previous line and add property names
+
+\* INVARIANT
+\* Uncomment the previous line and add invariant names

60009 - Distributed Algorithms/packages/tlatex.sty

@@ -0,0 +1,20 @@
+\tlatex
+\@x{}\moduleLeftDash\@xx{ {\MODULE} 24HourClock}\moduleRightDash\@xx{}%
+\@x{ {\EXTENDS} Naturals ,\, TLC}%
+\@x{ {\VARIABLE} hour}%
+\@x{}\midbar\@xx{}%
+\@x{ Init\@s{4.12} \.{\defeq} hour \.{\in} 0 \.{\dotdot} 23}%
+\@x{ Next \.{\defeq} hour \.{'} \.{=} ( hour \.{+} 1 ) \.{\%} 24}%
+\@x{\@s{39.83} \.{\land} (}%
+ \@x{\@s{55.04} ( hour \.{\leq} 12 \.{\land} PrintT ( {\langle}\@w{[Morning]\
+ time:} ,\, hour {\rangle} ) )}%
+ \@x{\@s{43.93} \.{\lor} ( hour \.{>} 12 \.{\land} hour \.{<} 18 \.{\land}
+ PrintT ( {\langle}\@w{[Afternoon]\ time:} ,\, hour {\rangle} ) )}%
+ \@x{\@s{43.93} \.{\lor} ( hour \.{\geq} 18 \.{\land} PrintT (
+ {\langle}\@w{[Evening]\ time:} ,\, hour {\rangle} ) )}%
+\@x{\@s{39.83} )}%
+ \@x{ Spec\@s{1.46} \.{\defeq} Init \.{\land} {\langle} Next {\rangle}_{
+ hour}}%
+\@x{}\midbar\@xx{}%
+\@x{ Typed \.{\defeq} {\Box} Init}%
+\@x{}\bottombar\@xx{}%

60009 - Distributed Algorithms/tla_plus/code/.gitkeep

@@ -0,0 +1,15 @@
+---- MODULE 24HourClock ----
+EXTENDS Naturals, TLC
+VARIABLE hour
+-----------------------
+Init == hour \in 0..23
+Next == hour' = (hour + 1) % 24
+        /\ (
+            (hour <= 12 /\ PrintT(<<"[Morning] time:", hour>>)) 
+         \/ (hour > 12 /\ hour < 18 /\ PrintT(<<"[Afternoon] time:", hour>>)) 
+         \/ (hour >= 18 /\ PrintT(<<"[Evening] time:", hour>>))
+        )
+Spec == Init /\ <<Next>>_hour
+-----------------------
+Typed == []Init
+====

60009 - Distributed Algorithms/tla_plus/code/24HourClock.cfg

@@ -0,0 +1,15 @@
+\* SPECIFICATION
+\* Uncomment the previous line and provide the specification name if it's declared
+\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.
+
+CONSTANTS
+    greeting = "Hello"
+
+INIT Init
+NEXT Next
+
+\* PROPERTY
+\* Uncomment the previous line and add property names
+
+\* INVARIANT
+\* Uncomment the previous line and add invariant names

60009 - Distributed Algorithms/tla_plus/code/24HourClock.dvi

@@ -0,0 +1,12 @@
+\tlatex
+\@x{}\moduleLeftDash\@xx{ {\MODULE} OneBitClock}\moduleRightDash\@xx{}%
+\@x{ {\VARIABLE} b}%
+\@x{ Type \.{\defeq} b \.{\in} \{ 0 ,\, 1 \}}%
+\@x{}\midbar\@xx{}%
+\@x{ Init\@s{4.12} \.{\defeq} b \.{=} 0 \.{\lor} b \.{=} 1}%
+ \@x{ Next \.{\defeq} ( ( b \.{=} 0 ) \.{\land} ( b \.{'} \.{=} 1 ) ) \.{\lor}
+ ( ( b \.{=} 1 ) \.{\land} ( b \.{'} \.{=} 0 ) )}%
+\@x{ Spec\@s{1.46} \.{\defeq} Init \.{\land} {\Box} [ Next ]_{ b}}%
+\@x{}\midbar\@xx{}%
+\@x{ Typed \.{\defeq} {\Box} Type}%
+\@x{}\bottombar\@xx{}%

60009 - Distributed Algorithms/tla_plus/code/24HourClock.tex

@@ -0,0 +1,10 @@
+---- MODULE OneBitClock ----
+VARIABLE b
+Type == b \in {0,1}
+-----------------------------
+Init == b=0 \/ b=1
+Next == ((b=0) /\ (b'=1)) \/ ((b=1) /\ (b'=0))
+Spec == Init /\ [][Next]_b
+-----------------------------
+Typed == []Type
+====

60009 - Distributed Algorithms/tla_plus/code/24HourClock.tla

@@ -0,0 +1,15 @@
+\* SPECIFICATION
+\* Uncomment the previous line and provide the specification name if it's declared
+\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.
+
+CONSTANTS
+    greeting = "Hello"
+
+INIT Init
+NEXT Next
+
+\* PROPERTY
+\* Uncomment the previous line and add property names
+
+\* INVARIANT
+\* Uncomment the previous line and add invariant names

60009 - Distributed Algorithms/tla_plus/code/OneBitClock.cfg

@@ -0,0 +1,11 @@
+\tlatex
+\@x{}\moduleLeftDash\@xx{ {\MODULE} TwelveHourClock}\moduleRightDash\@xx{}%
+\@x{ {\EXTENDS} Naturals}%
+\@x{ {\VARIABLE} hour}%
+\@x{}\midbar\@xx{}%
+\@x{ Init\@s{4.12} \.{\defeq} hour \.{\in} 0 \.{\dotdot} 11}%
+\@x{ Next \.{\defeq} hour \.{'} \.{=} ( hour \.{+} 1 ) \.{\%} 12}%
+\@x{ Spec\@s{1.46} \.{\defeq} Init \.{\land} {\Box} [ Next ]_{ hour}}%
+\@x{}\midbar\@xx{}%
+\@x{ Typed \.{\defeq} {\Box} Init}%
+\@x{}\bottombar\@xx{}%

60009 - Distributed Algorithms/tla_plus/code/OneBitClock.tex

@@ -0,0 +1,10 @@
+---- MODULE TwelveHourClock ----
+EXTENDS Naturals
+VARIABLE hour
+-----------------------
+Init == hour \in 0..11
+Next == hour' = (hour + 1) % 12 
+Spec == Init /\ [][Next]_hour
+-----------------------
+Typed == []Init
+====