pushed merge in primitives.act

2022-02-28 18:58:32 +01:00
1 parent 1bb1d0be40
commit 92b0b36325
@@ -0,0 +1,39 @@
+a._v a.a a.u a.v a._u a.b 
+reset done
+	         0 a.a : 0
+	         0 a.b : 0
+	         1 a._u : 1  [by a.a:=0]
+	      7092 a._v : 1  [by a.b:=0]
+	      7094 a.v : 0  [by a._v:=1]
+	     10468 a.u : 0  [by a._u:=1]
+
+step 1.1 finished
+	     10468 a.a : 1
+	     10468 a.b : 1
+	     15221 a._u : 0  [by a.a:=1]
+	     15335 a.u : 1  [by a._u:=0]
+
+step 1.2 finished
+	     15335 a.a : 0
+	     15335 a.b : 0
+	     80701 a._u : 1  [by a.a:=0]
+	     82427 a.u : 0  [by a._u:=1]
+
+step 2.1 finished
+	     82427 a.a : 1
+	     82427 a.b : 1
+	     82466 a._u : 0  [by a.a:=1]
+	     82957 a.u : 1  [by a._u:=0]
+
+step 2.2 finished
+	     82957 a.a : 0
+	     82957 a.b : 0
+	     82970 a._u : 1  [by a.a:=0]
+	     83010 a.u : 0  [by a._u:=1]
+
+step 3.1 finished
+	     83010 a.b : 1
+	     83425 a._v : 0  [by a.b:=1]
+	     83445 a.v : 1  [by a._v:=0]
+
+step 3.2 finished
@@ -0,0 +1,18 @@
+defproc arbiter (bool a, b, u, v)
+{
+  bool _u, _v;
+  prs {
+   [keeper=0]  a &  _v -> _u-
+   [keeper=0] ~a  | ~_v  -> _u+
+   [keeper=0]  b &  _u -> _v-
+   [keeper=0] ~b  | ~_u  -> _v+
+   [keeper=0] _u  => u-
+   [keeper=0] _v => v-
+  }
+  spec {
+    mk_excllo(_u, _v)
+  }
+}
+
+
+arbiter a;
@@ -0,0 +1,39 @@
+watchall
+cycle
+system "echo 'reset done'"
+set a.a 0
+set a.b 0
+advance 1000000
+status X
+mode run
+system "echo 'step 1.1 finished'"
+set a.a 1
+set a.b 1
+advance 1000000
+status X
+mode run
+system "echo 'step 1.2 finished'"
+set a.a 0
+set a.b 0
+advance 1000000
+status X
+mode run
+system "echo 'step 2.1 finished'"
+set a.a 1
+set a.b 1
+advance 1000000
+status X
+mode run
+system "echo 'step 2.2 finished'"
+set a.a 0
+set a.b 0
+advance 1000000
+status X
+mode run
+system "echo 'step 3.1 finished'"
+set a.a 0
+set a.b 1
+advance 1000000
+status X
+mode run
+system "echo 'step 3.2 finished'"