add deterministic coffee machine examples

DES-Lab · Feb 12, 2024 · 5fa6628 · 5fa6628
1 parent 5004146
commit 5fa6628
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 0 deletions.
diff --git a/DotModels/coffee_mealy.dot b/DotModels/coffee_mealy.dot
@@ -0,0 +1,10 @@
+digraph coffee_mealy {
+s0 [label="s0"];
+s1 [label="s1"];
+s0 -> s1  [label="coin/ beep"];
+s0 -> s0  [label="button/ init"];
+s1 -> s1  [label="coin/ beep"];
+s1 -> s0  [label="button/ coffee"];
+__start0 [label="", shape=none];
+__start0 -> s0  [label=""];
+}
diff --git a/DotModels/coffee_moore.dot b/DotModels/coffee_moore.dot
@@ -0,0 +1,13 @@
+digraph g {
+        __start0 [label="" shape="none"];
+        __start0 -> A;
+    	A [shape="record", style="rounded", label="{ A | init }"];
+    	B [shape="record", style="rounded", label="{ B | beep }"];
+    	C [shape="doublecircle", style="rounded", label="{ C | coffee }"];
+    	A -> B [label="coin"];
+    	A -> A [label="button"];
+    	B -> C [label="button"];
+    	B -> B [label="coin"];
+    	C -> B [label="coin"];
+    	C -> A [label="button"];
+    }