added non-deterministic benchmarks

Echtzeitsysteme · Oct 15, 2024 · 5e2fe42 · 5e2fe42
1 parent c8b0c25
commit 5e2fe42
Show file tree

Hide file tree

Showing 29 changed files with 228 additions and 204 deletions.
diff --git a/...isim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.txt b/...isim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.txt
@@ -89,7 +89,7 @@ edge:Process:sample:call_observe:Process__zero_recv{provided:(Process_clock_A_c
 edge:Process:sample:call_observe:Process__one_recv{provided:(Process_clock_A_c == 781)}
 event:Process__errMode3
 event:Process__errMode3_recv
-edge:Process:newPn:sample:Process__errMode3_recv{provided:(Process_clock_A_c >= 30)}
+edge:Process:newPn:sample:Process__errMode3_recv{provided:(Process_clock_A_c >= 30)} # Mutation!
 event:Process__errMode1
 event:Process__errMode1_recv
 edge:Process:newPn:sample:Process__errMode1_recv{provided:(Process_clock_A_c < 30)}

diff --git a/.../strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-bisim.txt b/.../strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-bisim.txt
@@ -84,8 +84,7 @@ event:Process__fast_recv
 edge:Process:call_check:ex_jam:Process__fast_recv{do:Process_clock_A_c=0}
 event:Process_A_observe
 event:Process_A_observe_emit
-edge:Process:call_observe:call_check:Process_A_observe_emit{do:Process_clock_A_c=0}
-edge:Process:call_observe:call_check:Process_A_observe_emit{do:Process_clock_A_c=0}
+edge:Process:call_observe:call_check:Process_A_observe_emit{do:Process_clock_A_c=0} # Mutation!
 edge:Process:sample:call_observe:Process__zero_recv{provided:(Process_clock_A_c == 781)}
 edge:Process:sample:call_observe:Process__one_recv{provided:(Process_clock_A_c == 781)}
 event:Process__errMode3
@@ -140,4 +139,6 @@ edge:Process:idle:ex_start:Process_k_emit{provided:(Process_clock_A_c == 781)}
 event:Process_l
 event:Process_l_emit
 edge:Process:start:idle:Process_l_emit{do:Process_clock_A_c=0}
+edge:Process:ex_silence2:idle:Process__zero_recv{do:Process_clock_A_c=0} # Non-deterministic Choice
+
 
diff --git a/...utants/collision-avoidance-non-bisim-2.sh → ...ts/av-protocol-non-bisim-changed-guard.sh b/...utants/collision-avoidance-non-bisim-2.sh → ...ts/av-protocol-non-bisim-changed-guard.sh
@@ -4,4 +4,4 @@
 #
 # See files AUTHORS and LICENSE for copyright details.
 
-cat "$(dirname $0)/collision-avoidance-non-bisim-2.txt"
+cat "$(dirname $0)/av-protocol-non-bisim-changed-guard.txt"
diff --git a/...tocol-mutants/av-protocol-non-bisim-3.txt → ...s/av-protocol-non-bisim-changed-guard.txt b/...tocol-mutants/av-protocol-non-bisim-3.txt → ...s/av-protocol-non-bisim-changed-guard.txt
@@ -85,12 +85,11 @@ edge:Process:call_check:ex_jam:Process__fast_recv{do:Process_clock_A_c=0}
 event:Process_A_observe
 event:Process_A_observe_emit
 edge:Process:call_observe:call_check:Process_A_observe_emit{}
-edge:Process:call_observe:call_check:Process_A_observe_emit{}
 edge:Process:sample:call_observe:Process__zero_recv{provided:(Process_clock_A_c == 781)}
 edge:Process:sample:call_observe:Process__one_recv{provided:(Process_clock_A_c == 781)}
 event:Process__errMode3
 event:Process__errMode3_recv
-edge:Process:newPn:sample:Process__errMode3_recv{provided:(Process_clock_A_c >= 30)}
+edge:Process:newPn:sample:Process__errMode3_recv{provided:(Process_clock_A_c >= 30)} # Mutation!
 event:Process__errMode1
 event:Process__errMode1_recv
 edge:Process:newPn:sample:Process__errMode1_recv{provided:(Process_clock_A_c < 30)}
@@ -140,4 +139,6 @@ edge:Process:idle:ex_start:Process_k_emit{provided:(Process_clock_A_c == 781)}
 event:Process_l
 event:Process_l_emit
 edge:Process:start:idle:Process_l_emit{do:Process_clock_A_c=0}
+edge:Process:ex_silence2:idle:Process__zero_recv{do:Process_clock_A_c=0} # Non-deterministic Choice
+
 
diff --git a/...otocol-mutants/av-protocol-non-bisim-1.sh → ...v-protocol-non-bisim-changed-invariant.sh b/...otocol-mutants/av-protocol-non-bisim-1.sh → ...v-protocol-non-bisim-changed-invariant.sh
diff --git a/...tocol-mutants/av-protocol-non-bisim-1.txt → ...-protocol-non-bisim-changed-invariant.txt b/...tocol-mutants/av-protocol-non-bisim-1.txt → ...-protocol-non-bisim-changed-invariant.txt
@@ -1,7 +1,10 @@
 # 
 # This file has been generated automatically with uppaal-to-tchecker
-# 
-system:av_protocol_reset_9.xml
+#
+# the original model was published by
+# Klaus Havelund, Arne Skou, Kim G. Larsen & Kristian Lund (1997): Formal Modeling and Analysis of an Audio/Video Protocol:
+# An Industrial Case Study Using UPPAAL. In: RTSS’97, pp. 2–13, doi:10.1109/REAL.1997.641264 
+system:av_protocol.xml
 # no iodecl
 # compilation of process Process
 process:Process
@@ -60,7 +63,7 @@ location:Process:ex_jam{invariant:(1 && (Process_clock_A_c <= 781))}
 location:Process:check_eof{}
 location:Process:stop{invariant:(1 && (Process_clock_A_c <= 50000))}
 location:Process:transmit{invariant:(1 && (Process_clock_A_c <= 781))}
-location:Process:ex_silence2{invariant:(1 && (Process_clock_A_c <= 781))}
+location:Process:ex_silence2{invariant:(1 && (Process_clock_A_c <= 782))} # Mutation!
 location:Process:goto_idle{}
 location:Process:other_started{invariant:(1 && (Process_clock_A_c <= 3124))}
 location:Process:ex_silence1{invariant:(1 && (Process_clock_A_c <= 2343))}
@@ -85,12 +88,11 @@ edge:Process:call_check:ex_jam:Process__fast_recv{do:Process_clock_A_c=0}
 event:Process_A_observe
 event:Process_A_observe_emit
 edge:Process:call_observe:call_check:Process_A_observe_emit{}
-edge:Process:call_observe:call_check:Process_A_observe_emit{}
 edge:Process:sample:call_observe:Process__zero_recv{provided:(Process_clock_A_c == 781)}
 edge:Process:sample:call_observe:Process__one_recv{provided:(Process_clock_A_c == 781)}
 event:Process__errMode3
 event:Process__errMode3_recv
-edge:Process:newPn:sample:Process__errMode3_recv{do:Process_clock_A_c=0:provided:(Process_clock_A_c > 30)}
+edge:Process:newPn:sample:Process__errMode3_recv{provided:(Process_clock_A_c > 30)}
 event:Process__errMode1
 event:Process__errMode1_recv
 edge:Process:newPn:sample:Process__errMode1_recv{provided:(Process_clock_A_c < 30)}
@@ -140,4 +142,5 @@ edge:Process:idle:ex_start:Process_k_emit{provided:(Process_clock_A_c == 781)}
 event:Process_l
 event:Process_l_emit
 edge:Process:start:idle:Process_l_emit{do:Process_clock_A_c=0}
+edge:Process:ex_silence2:idle:Process__zero_recv{do:Process_clock_A_c=0} # Non-deterministic Choice
 
diff --git a/...otocol-mutants/av-protocol-non-bisim-3.sh → ...ts/av-protocol-non-bisim-removed-reset.sh b/...otocol-mutants/av-protocol-non-bisim-3.sh → ...ts/av-protocol-non-bisim-removed-reset.sh
@@ -4,4 +4,4 @@
 #
 # See files AUTHORS and LICENSE for copyright details.
 
-cat "$(dirname $0)/av-protocol-non-bisim-3.txt"
+cat "$(dirname $0)/av-protocol-non-bisim-removed-reset.txt"
diff --git a/...tocol-mutants/av-protocol-non-bisim-2.txt → ...s/av-protocol-non-bisim-removed-reset.txt b/...tocol-mutants/av-protocol-non-bisim-2.txt → ...s/av-protocol-non-bisim-removed-reset.txt
@@ -69,7 +69,7 @@ location:Process:idle{}
 location:Process:start{initial:}
 event:Process__zero
 event:Process__zero_recv
-edge:Process:until_silence:until_silence:Process__zero_recv{}
+edge:Process:until_silence:until_silence:Process__zero_recv{} # Mutation
 event:Process__one
 event:Process__one_recv
 edge:Process:until_silence:stop:Process__one_recv{do:Process_clock_A_c=0}
@@ -85,7 +85,6 @@ edge:Process:call_check:ex_jam:Process__fast_recv{do:Process_clock_A_c=0}
 event:Process_A_observe
 event:Process_A_observe_emit
 edge:Process:call_observe:call_check:Process_A_observe_emit{}
-edge:Process:call_observe:call_check:Process_A_observe_emit{}
 edge:Process:sample:call_observe:Process__zero_recv{provided:(Process_clock_A_c == 781)}
 edge:Process:sample:call_observe:Process__one_recv{provided:(Process_clock_A_c == 781)}
 event:Process__errMode3
@@ -140,4 +139,6 @@ edge:Process:idle:ex_start:Process_k_emit{provided:(Process_clock_A_c == 781)}
 event:Process_l
 event:Process_l_emit
 edge:Process:start:idle:Process_l_emit{do:Process_clock_A_c=0}
+edge:Process:ex_silence2:idle:Process__zero_recv{do:Process_clock_A_c=0} # Non-deterministic Choice
+
 
diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol.txt
@@ -88,7 +88,6 @@ edge:Process:call_check:ex_jam:Process__fast_recv{do:Process_clock_A_c=0}
 event:Process_A_observe
 event:Process_A_observe_emit
 edge:Process:call_observe:call_check:Process_A_observe_emit{}
-edge:Process:call_observe:call_check:Process_A_observe_emit{}
 edge:Process:sample:call_observe:Process__zero_recv{provided:(Process_clock_A_c == 781)}
 edge:Process:sample:call_observe:Process__one_recv{provided:(Process_clock_A_c == 781)}
 event:Process__errMode3
@@ -143,3 +142,4 @@ edge:Process:idle:ex_start:Process_k_emit{provided:(Process_clock_A_c == 781)}
 event:Process_l
 event:Process_l_emit
 edge:Process:start:idle:Process_l_emit{do:Process_clock_A_c=0}
+edge:Process:ex_silence2:idle:Process__zero_recv{do:Process_clock_A_c=0} # Non-deterministic Choice
diff --git a/...sim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-bisim.txt b/...sim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-bisim.txt
@@ -1,12 +1,15 @@
 # 
 # This file has been generated automatically with uppaal-to-tchecker
 # 
-system:collision_avoidance_reset_2.xml
+# the original model was published by
+# Henrik E. Jensen, Kim G. Larsen & Arne Skou (1996): Modelling and analysis of a collision avoidance protocol using Spin and Uppaal.
+# In: DIMACS’96.
+system:collision_avoidance.xml
 # no iodecl
 # compilation of process Process
 process:Process
-# clock_c2:(clock)
-clock:1:Process_clock_c2
+# clock_c3:(clock)
+clock:1:Process_clock_c3
 # a:(broadcast (channel))
 # global event: Process_a
 # _from_medium_slave:(broadcast (channel))
@@ -35,36 +38,35 @@ location:Process:s2_1{}
 location:Process:s2_0{initial:}
 event:Process__from_medium_slave
 event:Process__from_medium_slave_recv
-edge:Process:s2_4:s2_4:Process__from_medium_slave_recv{provided:(Process_clock_c2 <= 2)}
+edge:Process:s2_4:s2_4:Process__from_medium_slave_recv{provided:(Process_clock_c3 <= 2)}
 event:Process__empty_slave
 event:Process__empty_slave_recv
-edge:Process:s2_5:s2_0:Process__empty_slave_recv{do:Process_clock_c2=0}
+edge:Process:s2_5:s2_0:Process__empty_slave_recv{do:Process_clock_c3=0} # Mutation! Added Reset
 event:Process__to_medium_slave
 event:Process__to_medium_slave_emit
-edge:Process:s2_4:s2_5:Process__to_medium_slave_emit{provided:(Process_clock_c2 == 2)}
+edge:Process:s2_4:s2_5:Process__to_medium_slave_emit{provided:(Process_clock_c3 == 2)}
 event:Process__in_2
 event:Process__in_2_recv
-edge:Process:s2_3:s2_4:Process__in_2_recv{provided:(Process_clock_c2 == 1)}
+edge:Process:s2_3:s2_4:Process__in_2_recv{provided:(Process_clock_c3 == 1)}
 event:Process_a
 event:Process_a_emit
-edge:Process:s2_1:s2_3:Process_a_emit{provided:(Process_clock_c2 == 0)}
-edge:Process:s2_2:s2_2:Process__from_medium_slave_recv{provided:(Process_clock_c2 <= 2)}
-edge:Process:s2_2:s2_0:Process_a_emit{provided:(Process_clock_c2 == 2)}
+edge:Process:s2_1:s2_3:Process_a_emit{provided:(Process_clock_c3 == 0)}
+edge:Process:s2_2:s2_2:Process__from_medium_slave_recv{provided:(Process_clock_c3 <= 2)}
+edge:Process:s2_2:s2_0:Process_a_emit{provided:(Process_clock_c3 == 2)}
 event:Process__out_2
 event:Process__out_2_emit
-edge:Process:s2_1:s2_2:Process__out_2_emit{provided:(Process_clock_c2 == 0)}
-edge:Process:s2_1:s2_2:Process__out_2_emit{provided:(Process_clock_c2 == 0)}
+edge:Process:s2_1:s2_2:Process__out_2_emit{provided:(Process_clock_c3 == 0)}
 event:Process__data1
 event:Process__data1_recv
-edge:Process:s2_1:s2_0:Process__data1_recv{provided:(Process_clock_c2 == 0)}
+edge:Process:s2_1:s2_0:Process__data1_recv{provided:(Process_clock_c3 == 0)}
 event:Process__data2
 event:Process__data2_recv
-edge:Process:s2_1:s2_0:Process__data2_recv{provided:(Process_clock_c2 == 0)}
+edge:Process:s2_1:s2_0:Process__data2_recv{provided:(Process_clock_c3 == 0)}
 event:Process__data3
 event:Process__data3_recv
-edge:Process:s2_1:s2_0:Process__data3_recv{provided:(Process_clock_c2 == 0)}
+edge:Process:s2_1:s2_0:Process__data3_recv{provided:(Process_clock_c3 == 0)}
 event:Process__data0
 event:Process__data0_recv
-edge:Process:s2_1:s2_0:Process__data0_recv{provided:(Process_clock_c2 == 0)}
-edge:Process:s2_0:s2_1:Process__from_medium_slave_recv{do:Process_clock_c2=0}
-
+edge:Process:s2_1:s2_0:Process__data0_recv{provided:(Process_clock_c3 == 0)}
+edge:Process:s2_0:s2_1:Process__from_medium_slave_recv{do:Process_clock_c3=0}
+edge:Process:s2_5:s2_2:Process__empty_slave_recv{do:Process_clock_c3=0} # Non-deterministic Choice
diff --git a/...enchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.sh b/...enchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.sh
diff --git a/...ndeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-guard.sh b/...ndeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-guard.sh
@@ -0,0 +1,7 @@
+#!/bin/bash
+
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+cat "$(dirname $0)/collision-avoidance-non-bisim-changed-guard.txt"
diff --git a/...tants/collision-avoidance-non-bisim-1.txt → ...ion-avoidance-non-bisim-changed-guard.txt b/...tants/collision-avoidance-non-bisim-1.txt → ...ion-avoidance-non-bisim-changed-guard.txt
@@ -1,12 +1,15 @@
 # 
 # This file has been generated automatically with uppaal-to-tchecker
 # 
-system:collision_avoidance_change_guard_1.xml
+# the original model was published by
+# Henrik E. Jensen, Kim G. Larsen & Arne Skou (1996): Modelling and analysis of a collision avoidance protocol using Spin and Uppaal.
+# In: DIMACS’96.
+system:collision_avoidance.xml
 # no iodecl
 # compilation of process Process
 process:Process
-# clock_c2:(clock)
-clock:1:Process_clock_c2
+# clock_c3:(clock)
+clock:1:Process_clock_c3
 # a:(broadcast (channel))
 # global event: Process_a
 # _from_medium_slave:(broadcast (channel))
@@ -35,36 +38,35 @@ location:Process:s2_1{}
 location:Process:s2_0{initial:}
 event:Process__from_medium_slave
 event:Process__from_medium_slave_recv
-edge:Process:s2_4:s2_4:Process__from_medium_slave_recv{provided:(Process_clock_c2 < 2)}
+edge:Process:s2_4:s2_4:Process__from_medium_slave_recv{provided:(Process_clock_c3 < 2)} # Mutation!
 event:Process__empty_slave
 event:Process__empty_slave_recv
 edge:Process:s2_5:s2_0:Process__empty_slave_recv{}
 event:Process__to_medium_slave
 event:Process__to_medium_slave_emit
-edge:Process:s2_4:s2_5:Process__to_medium_slave_emit{provided:(Process_clock_c2 == 2)}
+edge:Process:s2_4:s2_5:Process__to_medium_slave_emit{provided:(Process_clock_c3 == 2)}
 event:Process__in_2
 event:Process__in_2_recv
-edge:Process:s2_3:s2_4:Process__in_2_recv{provided:(Process_clock_c2 == 1)}
+edge:Process:s2_3:s2_4:Process__in_2_recv{provided:(Process_clock_c3 == 1)}
 event:Process_a
 event:Process_a_emit
-edge:Process:s2_1:s2_3:Process_a_emit{provided:(Process_clock_c2 == 0)}
-edge:Process:s2_2:s2_2:Process__from_medium_slave_recv{provided:(Process_clock_c2 <= 2)}
-edge:Process:s2_2:s2_0:Process_a_emit{provided:(Process_clock_c2 == 2)}
+edge:Process:s2_1:s2_3:Process_a_emit{provided:(Process_clock_c3 == 0)}
+edge:Process:s2_2:s2_2:Process__from_medium_slave_recv{provided:(Process_clock_c3 <= 2)}
+edge:Process:s2_2:s2_0:Process_a_emit{provided:(Process_clock_c3 == 2)}
 event:Process__out_2
 event:Process__out_2_emit
-edge:Process:s2_1:s2_2:Process__out_2_emit{provided:(Process_clock_c2 == 0)}
-edge:Process:s2_1:s2_2:Process__out_2_emit{provided:(Process_clock_c2 == 0)}
+edge:Process:s2_1:s2_2:Process__out_2_emit{provided:(Process_clock_c3 == 0)}
 event:Process__data1
 event:Process__data1_recv
-edge:Process:s2_1:s2_0:Process__data1_recv{provided:(Process_clock_c2 == 0)}
+edge:Process:s2_1:s2_0:Process__data1_recv{provided:(Process_clock_c3 == 0)}
 event:Process__data2
 event:Process__data2_recv
-edge:Process:s2_1:s2_0:Process__data2_recv{provided:(Process_clock_c2 == 0)}
+edge:Process:s2_1:s2_0:Process__data2_recv{provided:(Process_clock_c3 == 0)}
 event:Process__data3
 event:Process__data3_recv
-edge:Process:s2_1:s2_0:Process__data3_recv{provided:(Process_clock_c2 == 0)}
+edge:Process:s2_1:s2_0:Process__data3_recv{provided:(Process_clock_c3 == 0)}
 event:Process__data0
 event:Process__data0_recv
-edge:Process:s2_1:s2_0:Process__data0_recv{provided:(Process_clock_c2 == 0)}
-edge:Process:s2_0:s2_1:Process__from_medium_slave_recv{do:Process_clock_c2=0}
-
+edge:Process:s2_1:s2_0:Process__data0_recv{provided:(Process_clock_c3 == 0)}
+edge:Process:s2_0:s2_1:Process__from_medium_slave_recv{do:Process_clock_c3=0}
+edge:Process:s2_5:s2_2:Process__empty_slave_recv{do:Process_clock_c3=0} # Non-deterministic Choice
diff --git a/...erministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-invariant.sh b/...erministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-invariant.sh
@@ -0,0 +1,7 @@
+#!/bin/bash
+
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+cat "$(dirname $0)/collision-avoidance-non-bisim-changed-invariant.txt"
diff --git a/...tants/collision-avoidance-non-bisim-2.txt → ...avoidance-non-bisim-changed-invariant.txt b/...tants/collision-avoidance-non-bisim-2.txt → ...avoidance-non-bisim-changed-invariant.txt
@@ -1,12 +1,15 @@
 # 
 # This file has been generated automatically with uppaal-to-tchecker
 # 
-system:collision_avoidance_reset_1.xml
+# the original model was published by
+# Henrik E. Jensen, Kim G. Larsen & Arne Skou (1996): Modelling and analysis of a collision avoidance protocol using Spin and Uppaal.
+# In: DIMACS’96.
+system:collision_avoidance.xml
 # no iodecl
 # compilation of process Process
 process:Process
-# clock_c2:(clock)
-clock:1:Process_clock_c2
+# clock_c3:(clock)
+clock:1:Process_clock_c3
 # a:(broadcast (channel))
 # global event: Process_a
 # _from_medium_slave:(broadcast (channel))
@@ -31,40 +34,39 @@ location:Process:s2_3{}
 location:Process:s2_4{}
 location:Process:s2_2{}
 location:Process:s2_5{}
-location:Process:s2_1{}
+location:Process:s2_1{invariant:(Process_clock_c3 <= 0)} # Mutation!
 location:Process:s2_0{initial:}
 event:Process__from_medium_slave
 event:Process__from_medium_slave_recv
-edge:Process:s2_4:s2_4:Process__from_medium_slave_recv{do:Process_clock_c2=0:provided:(Process_clock_c2 <= 2)}
+edge:Process:s2_4:s2_4:Process__from_medium_slave_recv{provided:(Process_clock_c3 <= 2)}
 event:Process__empty_slave
 event:Process__empty_slave_recv
 edge:Process:s2_5:s2_0:Process__empty_slave_recv{}
 event:Process__to_medium_slave
 event:Process__to_medium_slave_emit
-edge:Process:s2_4:s2_5:Process__to_medium_slave_emit{provided:(Process_clock_c2 == 2)}
+edge:Process:s2_4:s2_5:Process__to_medium_slave_emit{provided:(Process_clock_c3 == 2)}
 event:Process__in_2
 event:Process__in_2_recv
-edge:Process:s2_3:s2_4:Process__in_2_recv{provided:(Process_clock_c2 == 1)}
+edge:Process:s2_3:s2_4:Process__in_2_recv{provided:(Process_clock_c3 == 1)}
 event:Process_a
 event:Process_a_emit
-edge:Process:s2_1:s2_3:Process_a_emit{provided:(Process_clock_c2 == 0)}
-edge:Process:s2_2:s2_2:Process__from_medium_slave_recv{provided:(Process_clock_c2 <= 2)}
-edge:Process:s2_2:s2_0:Process_a_emit{provided:(Process_clock_c2 == 2)}
+edge:Process:s2_1:s2_3:Process_a_emit{provided:(Process_clock_c3 == 0)}
+edge:Process:s2_2:s2_2:Process__from_medium_slave_recv{provided:(Process_clock_c3 <= 2)}
+edge:Process:s2_2:s2_0:Process_a_emit{provided:(Process_clock_c3 == 2)}
 event:Process__out_2
 event:Process__out_2_emit
-edge:Process:s2_1:s2_2:Process__out_2_emit{provided:(Process_clock_c2 == 0)}
-edge:Process:s2_1:s2_2:Process__out_2_emit{provided:(Process_clock_c2 == 0)}
+edge:Process:s2_1:s2_2:Process__out_2_emit{provided:(Process_clock_c3 == 0)}
 event:Process__data1
 event:Process__data1_recv
-edge:Process:s2_1:s2_0:Process__data1_recv{provided:(Process_clock_c2 == 0)}
+edge:Process:s2_1:s2_0:Process__data1_recv{provided:(Process_clock_c3 == 0)}
 event:Process__data2
 event:Process__data2_recv
-edge:Process:s2_1:s2_0:Process__data2_recv{provided:(Process_clock_c2 == 0)}
+edge:Process:s2_1:s2_0:Process__data2_recv{provided:(Process_clock_c3 == 0)}
 event:Process__data3
 event:Process__data3_recv
-edge:Process:s2_1:s2_0:Process__data3_recv{provided:(Process_clock_c2 == 0)}
+edge:Process:s2_1:s2_0:Process__data3_recv{provided:(Process_clock_c3 == 0)}
 event:Process__data0
 event:Process__data0_recv
-edge:Process:s2_1:s2_0:Process__data0_recv{provided:(Process_clock_c2 == 0)}
-edge:Process:s2_0:s2_1:Process__from_medium_slave_recv{do:Process_clock_c2=0}
-
+edge:Process:s2_1:s2_0:Process__data0_recv{provided:(Process_clock_c3 == 0)}
+edge:Process:s2_0:s2_1:Process__from_medium_slave_recv{do:Process_clock_c3=0}
+edge:Process:s2_5:s2_2:Process__empty_slave_recv{do:Process_clock_c3=0} # Non-deterministic Choice
diff --git a/...ndeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-removed-reset.sh b/...ndeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-removed-reset.sh
@@ -0,0 +1,7 @@
+#!/bin/bash
+
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+cat "$(dirname $0)/collision-avoidance-non-bisim-removed-reset.txt"