choice.in: [*] take, deliver;
-0: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfZero;
-1: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfZero;
-0: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfNonZero;
-1: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfNonZero;
--1: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfPositive;
-0: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfPositive;
-1: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfPositive;
--1: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfNonPositive;
-0: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfNonPositive;
-1: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfNonPositive;
--1: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfNegative;
-0: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfNegative;
-1: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfNegative;
--1: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfNonNegative;
-0: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfNonNegative;
-1: sendto fifo.in; fifo.out: wait, take, sendto choice.in.deMuxIfNonNegative;
-0: sendto fifo.out;
fifo.in: [*] take, deliver;
+0: sendto fifo.in;
+1: sendto fifo.in;
+0: sendto fifo.in;
+1: sendto fifo.in;
+-1: sendto fifo.in;
+0: sendto fifo.in;
+1: sendto fifo.in;
+-1: sendto fifo.in;
+0: sendto fifo.in;
+1: sendto fifo.in;
+-1: sendto fifo.in;
+0: sendto fifo.in;
+1: sendto fifo.in;
+-1: sendto fifo.in;
+0: sendto fifo.in;
+1: sendto fifo.in;
+fifo.out: [2] wait, take, sendto choice.in.deMuxIfZero;
+fifo.out: [2] wait, take, sendto choice.in.deMuxIfNonZero;
+fifo.out: [3] wait, take, sendto choice.in.deMuxIfPositive;
+fifo.out: [3] wait, take, sendto choice.in.deMuxIfNonPositive;
+fifo.out: [3] wait, take, sendto choice.in.deMuxIfNegative;
+fifo.out: [3] wait, take, sendto choice.in.deMuxIfNonNegative;
+0: sendto fifo.out;
+
1: sendto fifo1.in;
fifo1.in: take, deliver;
fifo1.out: take; [*] wait, sendto debug.in;
// expected output
+#expect 1
#expect 2
#expect 1
+#expect 2
#expect 1
#expect 2
// ships required in order to run this code
#ship debug : Debug
#ship choice : Choice
+#ship fifo : Fifo
choice.out1: [*] take, sendto debug.in;
// this should never emit anything
choice.out2: take; [*] notify debug.in;
-debug.in: [*] take, deliver;
+debug.in: notify fifo.out; [*] take, deliver, notify fifo.out;
choice.in1: take; [*] deliver;
choice.in2: take; [*] deliver;
1: sendto choice.in1;
2: sendto choice.in2;
-choice.in: [*] take, deliver;
-
-0: sendto choice.in.muxIfZero;
-1: sendto choice.in.muxIfZero;
-0: sendto choice.in.muxIfNonZero;
-1: sendto choice.in.muxIfNonZero;
--1: sendto choice.in.muxIfPositive;
-0: sendto choice.in.muxIfPositive;
-1: sendto choice.in.muxIfPositive;
--1: sendto choice.in.muxIfNonPositive;
-0: sendto choice.in.muxIfNonPositive;
-1: sendto choice.in.muxIfNonPositive;
--1: sendto choice.in.muxIfNegative;
-0: sendto choice.in.muxIfNegative;
-1: sendto choice.in.muxIfNegative;
--1: sendto choice.in.muxIfNonNegative;
-0: sendto choice.in.muxIfNonNegative;
-1: sendto choice.in.muxIfNonNegative;
+choice.in: [*] take, deliver;
+
+fifo.in: [*] take, deliver;
+-1: sendto fifo.in;
+ 0: sendto fifo.in;
+ 1: sendto fifo.in;
+-1: sendto fifo.in;
+ 0: sendto fifo.in;
+ 1: sendto fifo.in;
+-1: sendto fifo.in;
+ 0: sendto fifo.in;
+ 1: sendto fifo.in;
+-1: sendto fifo.in;
+ 0: sendto fifo.in;
+ 1: sendto fifo.in;
+-1: sendto fifo.in;
+ 0: sendto fifo.in;
+ 1: sendto fifo.in;
+-1: sendto fifo.in;
+ 0: sendto fifo.in;
+ 1: sendto fifo.in;
+fifo.out:
+ [3] wait, take, sendto choice.in.muxIfZero;
+ [3] wait, take, sendto choice.in.muxIfNonZero;
+ [3] wait, take, sendto choice.in.muxIfPositive;
+ [3] wait, take, sendto choice.in.muxIfNonPositive;
+ [3] wait, take, sendto choice.in.muxIfNegative;
+ [3] wait, take, sendto choice.in.muxIfNonNegative;
// expected output
+#expect 1
+#expect 2
#expect 2
#expect 1
#expect 1
#expect 2
+#expect 2
+#expect 1
#expect 1
#expect 2
#expect 2
// ships required in order to run this code
#ship debug : Debug
#ship choice : Choice
+#ship fifo : Fifo
// alternate values from choice1+choice2
choice.out1: [*] wait, take, sendto debug.in;
choice.out2: [*] wait, take, sendto debug.in;
debug.in:
[*] nop;
+ (*) notify fifo.out;
(*) notify choice.out1;
(*) take, deliver;
(*) notify choice.out2;
1: sendto choice.in1;
2: sendto choice.in2;
-choice.in: [*] take, deliver;
+choice.in: [*] take, deliver;
-0: sendto choice.in.swapIfZero;
-1: sendto choice.in.swapIfZero;
-0: sendto choice.in.swapIfNonZero;
-1: sendto choice.in.swapIfNonZero;
--1: sendto choice.in.swapIfPositive;
-0: sendto choice.in.swapIfPositive;
-1: sendto choice.in.swapIfPositive;
--1: sendto choice.in.swapIfNonPositive;
-0: sendto choice.in.swapIfNonPositive;
-1: sendto choice.in.swapIfNonPositive;
--1: sendto choice.in.swapIfNegative;
-0: sendto choice.in.swapIfNegative;
-1: sendto choice.in.swapIfNegative;
--1: sendto choice.in.swapIfNonNegative;
-0: sendto choice.in.swapIfNonNegative;
-1: sendto choice.in.swapIfNonNegative;
+fifo.in: [*] take, deliver;
+-1: sendto fifo.in;
+ 0: sendto fifo.in;
+ 1: sendto fifo.in;
+-1: sendto fifo.in;
+ 0: sendto fifo.in;
+ 1: sendto fifo.in;
+-1: sendto fifo.in;
+ 0: sendto fifo.in;
+ 1: sendto fifo.in;
+-1: sendto fifo.in;
+ 0: sendto fifo.in;
+ 1: sendto fifo.in;
+-1: sendto fifo.in;
+ 0: sendto fifo.in;
+ 1: sendto fifo.in;
+-1: sendto fifo.in;
+ 0: sendto fifo.in;
+ 1: sendto fifo.in;
+fifo.out:
+ [3] wait, take, sendto choice.in.swapIfZero;
+ [3] wait, take, sendto choice.in.swapIfNonZero;
+ [3] wait, take, sendto choice.in.swapIfPositive;
+ [3] wait, take, sendto choice.in.swapIfNonPositive;
+ [3] wait, take, sendto choice.in.swapIfNegative;
+ [3] wait, take, sendto choice.in.swapIfNonNegative;