added two examples: HourClock demonstrates the use of the prime operator

bendisposto · May 23, 2012 · 1ca29f1 · 1ca29f1
1 parent 4537913
commit 1ca29f1
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 0 deletions.
diff --git a/examples/tla/Functions b/examples/tla/Functions
@@ -0,0 +1,5 @@
+LET
+	f[x \in 1..10] == x+x
+	g == [x \in 1..10 |-> x * x]
+IN  
+	f[2] = f[2]
diff --git a/examples/tla/HourClock b/examples/tla/HourClock
@@ -0,0 +1,6 @@
+\* Calculation the next state of the hour clock *\
+LET
+	Current == hr = 12
+	Next == hr' = IF hr # 12 THEN hr + 1 ELSE 1
+IN 
+	Current /\ Next