add jars model for upcoming visualisation

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

Jars/Jars.mch

+MACHINE Jars
+/*
+This is the B model of a puzzle from the movie "Die Hard with a Vengeance":
+ https://www.youtube.com/watch?v=BVtQNK_ZUJg
+ http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm
+Input: one 3 gallon and one 5 gallon jug, and we need to measure precisely 4 gallons
+*/
+DEFINITIONS
+  GOAL == (4:ran(level));
+  gmax == max(ran(maxf))
+SETS
+ Jars = {j3,j5}
+CONSTANTS maxf
+PROPERTIES maxf : Jars --> NATURAL &
+           maxf = {j3 |-> 3, j5 |-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */
+VARIABLES level
+INVARIANT
+  level: Jars --> NATURAL
+INITIALISATION level := Jars * {0}  /* all jars start out empty */
+OPERATIONS
+  FillJar(j) = /* we can completely fill a jar j */
+   PRE j:Jars & level(j)<maxf(j) THEN
+    level(j) := maxf(j)
+   END;
+  EmptyJar(j) = /* we can completely empty a jar j */
+   PRE j:Jars & level(j)>0 THEN
+    level(j) := 0
+   END;
+  Transfer(j1,amount,j2) = /* we can transfer from jar j1 to j2 until either j2 is full or j1 is empty */
+   PRE j1:Jars & j2:Jars & j1 /= j2 & amount>0 &
+                               amount = min({level(j1), maxf(j2)-level(j2)}) THEN
+      level := level <+ { j1|-> level(j1)-amount, j2 |-> level(j2)+amount }
+   END
+END
+