diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.txt b/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.txt index af6478d6..33eba338 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.txt +++ b/examples/strong_timed_bisim_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/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-bisim.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-bisim.txt index 57b3b7ab..eec8ec17 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-bisim.txt +++ b/examples/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/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-2.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.sh similarity index 66% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-2.sh rename to examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.sh index 8fb367bb..d4c4177a 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-2.sh +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/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/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-3.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.txt similarity index 97% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-3.txt rename to examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.txt index b9991a63..063a2336 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-3.txt +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/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/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-1.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-changed-invariant.sh similarity index 100% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-1.sh rename to examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-changed-invariant.sh diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-1.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-changed-invariant.txt similarity index 91% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-1.txt rename to examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-changed-invariant.txt index 538985c9..6a62a6e2 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-1.txt +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-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/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-3.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-removed-reset.sh similarity index 66% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-3.sh rename to examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-removed-reset.sh index 4903a71f..7e2625cf 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-3.sh +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/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/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-2.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-removed-reset.txt similarity index 96% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-2.txt rename to examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-removed-reset.txt index 346edc5a..6ed7c501 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-2.txt +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/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 index 94899f8c..4d16c461 100644 --- 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/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-bisim.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-bisim.txt index ab1ed2b9..d61b3143 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-bisim.txt +++ b/examples/strong_timed_bisim_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 \ No newline at end of file diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.sh deleted file mode 100644 index 8fb367bb..00000000 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.sh +++ /dev/null @@ -1,7 +0,0 @@ -#!/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-2.txt" diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-guard.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-guard.sh new file mode 100644 index 00000000..35233d0d --- /dev/null +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/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/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-1.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-guard.txt similarity index 76% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-1.txt rename to examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-guard.txt index c71a0ff7..2a66df67 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-1.txt +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-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/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-invariant.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-invariant.sh new file mode 100644 index 00000000..4feb856b --- /dev/null +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/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/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-2.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-invariant.txt similarity index 72% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-2.txt rename to examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-invariant.txt index 2c955717..1ec6bedc 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-2.txt +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-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/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-removed-reset.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-removed-reset.sh new file mode 100644 index 00000000..66471e9f --- /dev/null +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/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" diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.tck b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-removed-reset.txt similarity index 74% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.tck rename to examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-removed-reset.txt index 18cfcaab..76af6b94 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.tck +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-removed-reset.txt @@ -1,12 +1,15 @@ # # This file has been generated automatically with uppaal-to-tchecker # -system:collision_avoidance_reset_13.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{} 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{} - +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{} # Mutation! +edge:Process:s2_5:s2_2:Process__empty_slave_recv{do:Process_clock_c3=0} # Non-deterministic Choice diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance.txt index d5c7e371..b23d6bb0 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance.txt +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance.txt @@ -56,7 +56,6 @@ 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_c3 == 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_c3 == 0)} @@ -70,3 +69,4 @@ event:Process__data0 event:Process__data0_recv 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 \ No newline at end of file diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-bisim.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-bisim.txt index 3647b24d..7a0e1395 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-bisim.txt +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-bisim.txt @@ -1,7 +1,10 @@ # # This file has been generated automatically with uppaal-to-tchecker -# -system:ieee_rcp_bisim.xml +# +# the original model has been published by +# Aurore Collomb-Annichini & Mihaela Sighireanu (2001): +# Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. +system:ieee_rcp.xml # no iodecl # compilation of process Process process:Process @@ -15,10 +18,10 @@ clock:1:Process_yr # global event: Process_snd_req_i # snd_ack_i:(broadcast (channel)) # global event: Process_snd_ack_i -# rec_idle_j:(broadcast (channel)) -# global event: Process_rec_idle_j # rec_req_j:(broadcast (channel)) # global event: Process_rec_req_j +# rec_idle_j:(broadcast (channel)) +# global event: Process_rec_idle_j # rec_ack_j:(broadcast (channel)) # global event: Process_rec_ack_j location:Process:REC_IDLE{invariant:(1 && (Process_yr <= 42))} @@ -34,7 +37,6 @@ location:Process:REC_IDLE_ACK{initial::invariant:(1 && (Process_xr <= 42))} event:Process_snd_idle_i event:Process_snd_idle_i_emit edge:Process:REC_REQ_IDLE:REC_REQ_IDLE:Process_snd_idle_i_emit{} -edge:Process:REC_REQ_IDLE:REC_REQ_IDLE:Process_snd_idle_i_emit{} event:Process_snd_req_i event:Process_snd_req_i_emit edge:Process:REC_IDLE_REC:REC_IDLE_REC:Process_snd_req_i_emit{} @@ -63,6 +65,7 @@ edge:Process:EMPTY:REC_ACK:Process_snd_ack_i_emit{do:Process_xr=0;Process_yr=0} edge:Process:EMPTY:REC_REQ:Process_snd_req_i_emit{do:Process_xr=0;Process_yr=0} edge:Process:REC_REQ:EMPTY:Process_rec_req_j_emit{} edge:Process:REC_REQ_ACK:REC_REQ_ACK:Process_snd_ack_i_emit{} +edge:Process:REC_REQ_ACK:REC_REQ_ACK:Process_snd_ack_i_emit{} # Mutation edge:Process:REC_ACK:REC_ACK_IDLE:Process_snd_idle_i_emit{do:Process_yr=0} edge:Process:REC_REQ_ACK:REC_ACK:Process_rec_req_j_emit{} edge:Process:REC_REQ:REC_REQ_ACK:Process_snd_ack_i_emit{} @@ -70,4 +73,4 @@ edge:Process:REC_ACK_REQ:REC_REQ:Process_rec_ack_j_emit{} edge:Process:REC_ACK_REQ:REC_ACK_REQ:Process_snd_req_i_emit{} edge:Process:REC_ACK:REC_ACK_REQ:Process_snd_req_i_emit{do:Process_yr=0} edge:Process:REC_IDLE_ACK:REC_ACK:Process_rec_idle_j_emit{} - +edge:Process:REC_REQ_ACK:REC_IDLE_ACK:Process_rec_req_j_emit{} # Added Nondeterministic Choice diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-1.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-1.sh deleted file mode 100644 index 9a7dd7e7..00000000 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-1.sh +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/bash - -# This file is a part of the TChecker project. -# -# See files AUTHORS and LICENSE for copyright details. - -cat "$(dirname $0)/ieee-rcp-non-bisim-1.txt" diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-2.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-2.sh deleted file mode 100644 index bad7c518..00000000 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-2.sh +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/bash - -# This file is a part of the TChecker project. -# -# See files AUTHORS and LICENSE for copyright details. - -cat "$(dirname $0)/ieee-rcp-non-bisim-2.txt" diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-3.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-3.sh deleted file mode 100644 index 683b530e..00000000 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-3.sh +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/bash - -# This file is a part of the TChecker project. -# -# See files AUTHORS and LICENSE for copyright details. - -cat "$(dirname $0)/ieee-rcp-non-bisim-3.txt" diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-1.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-guard.sh similarity index 67% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-1.sh rename to examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-guard.sh index ada16119..d5b1b74d 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-1.sh +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-guard.sh @@ -4,4 +4,4 @@ # # See files AUTHORS and LICENSE for copyright details. -cat "$(dirname $0)/collision-avoidance-non-bisim-1.txt" +cat "$(dirname $0)/ieee-rcp-non-bisim-changed-guard.txt" diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-3.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-guard.txt similarity index 64% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-3.txt rename to examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-guard.txt index 88eef8aa..a588fbcd 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-3.txt +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-guard.txt @@ -1,36 +1,39 @@ # # This file has been generated automatically with uppaal-to-tchecker -# -system:ieee_rcp_reset_6.xml +# +# the original model has been published by +# Aurore Collomb-Annichini & Mihaela Sighireanu (2001): +# Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. +system:ieee_rcp.xml # no iodecl # compilation of process Process process:Process -# x:(clock) -clock:1:Process_x -# y:(clock) -clock:1:Process_y +# xr:(clock) +clock:1:Process_xr +# yr:(clock) +clock:1:Process_yr # snd_idle_i:(broadcast (channel)) # global event: Process_snd_idle_i # snd_req_i:(broadcast (channel)) # global event: Process_snd_req_i # snd_ack_i:(broadcast (channel)) # global event: Process_snd_ack_i -# rec_idle_j:(broadcast (channel)) -# global event: Process_rec_idle_j # rec_req_j:(broadcast (channel)) # global event: Process_rec_req_j +# rec_idle_j:(broadcast (channel)) +# global event: Process_rec_idle_j # rec_ack_j:(broadcast (channel)) # global event: Process_rec_ack_j -location:Process:REC_IDLE{invariant:(1 && (Process_y <= 42))} -location:Process:REC_IDLE_REC{invariant:(1 && (Process_x <= 42))} -location:Process:REC_REQ_ACK{invariant:(1 && (Process_x <= 42))} -location:Process:REC_ACK{invariant:(1 && (Process_y <= 42))} -location:Process:REC_REQ_IDLE{invariant:(1 && (Process_x <= 42))} -location:Process:REC_ACK_REQ{invariant:(1 && (Process_x <= 42))} +location:Process:REC_IDLE{invariant:(1 && (Process_yr <= 42))} +location:Process:REC_IDLE_REC{invariant:(1 && (Process_xr <= 42))} +location:Process:REC_REQ_ACK{invariant:(1 && (Process_xr <= 42))} +location:Process:REC_ACK{invariant:(1 && (Process_yr <= 42))} +location:Process:REC_REQ_IDLE{invariant:(1 && (Process_xr <= 42))} +location:Process:REC_ACK_REQ{invariant:(1 && (Process_xr <= 42))} location:Process:EMPTY{} -location:Process:REC_ACK_IDLE{invariant:(1 && (Process_x <= 42))} -location:Process:REC_REQ{invariant:(1 && (Process_y <= 42))} -location:Process:REC_IDLE_ACK{initial::invariant:(1 && (Process_x <= 42))} +location:Process:REC_ACK_IDLE{invariant:(1 && (Process_xr <= 42))} +location:Process:REC_REQ{invariant:(1 && (Process_yr <= 42))} +location:Process:REC_IDLE_ACK{initial::invariant:(1 && (Process_xr <= 42))} event:Process_snd_idle_i event:Process_snd_idle_i_emit edge:Process:REC_REQ_IDLE:REC_REQ_IDLE:Process_snd_idle_i_emit{} @@ -42,32 +45,32 @@ edge:Process:REC_ACK_IDLE:REC_ACK_IDLE:Process_snd_idle_i_emit{} event:Process_snd_ack_i event:Process_snd_ack_i_emit edge:Process:REC_IDLE_ACK:REC_IDLE_ACK:Process_snd_ack_i_emit{} -edge:Process:REC_REQ:REC_REQ_IDLE:Process_snd_idle_i_emit{} -edge:Process:REC_IDLE:REC_IDLE_ACK:Process_snd_ack_i_emit{do:Process_y=0} +edge:Process:REC_REQ:REC_REQ_IDLE:Process_snd_idle_i_emit{do:Process_yr=0} +edge:Process:REC_IDLE:REC_IDLE_ACK:Process_snd_ack_i_emit{do:Process_yr=0} event:Process_rec_req_j event:Process_rec_req_j_emit edge:Process:REC_REQ_IDLE:REC_IDLE:Process_rec_req_j_emit{} event:Process_rec_idle_j event:Process_rec_idle_j_emit edge:Process:REC_IDLE_REC:REC_REQ:Process_rec_idle_j_emit{} -edge:Process:REC_IDLE:REC_IDLE_REC:Process_snd_req_i_emit{do:Process_y=0} +edge:Process:REC_IDLE:REC_IDLE_REC:Process_snd_req_i_emit{do:Process_yr=0} event:Process_rec_ack_j event:Process_rec_ack_j_emit edge:Process:REC_ACK_IDLE:REC_IDLE:Process_rec_ack_j_emit{} edge:Process:REC_REQ:REC_REQ:Process_snd_req_i_emit{} edge:Process:EMPTY:REC_IDLE:Process_snd_idle_i_emit{} -edge:Process:REC_IDLE:EMPTY:Process_rec_idle_j_emit{} +edge:Process:REC_IDLE:EMPTY:Process_rec_idle_j_emit{provided:Process_xr<=2} # Mutation! edge:Process:REC_ACK:EMPTY:Process_rec_ack_j_emit{} -edge:Process:EMPTY:REC_ACK:Process_snd_ack_i_emit{do:Process_x=0;Process_y=0} -edge:Process:EMPTY:REC_REQ:Process_snd_req_i_emit{do:Process_x=0;Process_y=0} +edge:Process:EMPTY:REC_ACK:Process_snd_ack_i_emit{do:Process_xr=0;Process_yr=0} +edge:Process:EMPTY:REC_REQ:Process_snd_req_i_emit{do:Process_xr=0;Process_yr=0} edge:Process:REC_REQ:EMPTY:Process_rec_req_j_emit{} edge:Process:REC_REQ_ACK:REC_REQ_ACK:Process_snd_ack_i_emit{} -edge:Process:REC_ACK:REC_ACK_IDLE:Process_snd_idle_i_emit{do:Process_y=0} +edge:Process:REC_ACK:REC_ACK_IDLE:Process_snd_idle_i_emit{do:Process_yr=0} edge:Process:REC_REQ_ACK:REC_ACK:Process_rec_req_j_emit{} edge:Process:REC_REQ:REC_REQ_ACK:Process_snd_ack_i_emit{} edge:Process:REC_ACK_REQ:REC_REQ:Process_rec_ack_j_emit{} -edge:Process:REC_ACK_REQ:REC_REQ:Process_rec_ack_j_emit{} edge:Process:REC_ACK_REQ:REC_ACK_REQ:Process_snd_req_i_emit{} -edge:Process:REC_ACK:REC_ACK_REQ:Process_snd_req_i_emit{do:Process_y=0} +edge:Process:REC_ACK:REC_ACK_REQ:Process_snd_req_i_emit{do:Process_yr=0} edge:Process:REC_IDLE_ACK:REC_ACK:Process_rec_idle_j_emit{} +edge:Process:REC_REQ_ACK:REC_IDLE_ACK:Process_rec_req_j_emit{} # Added Nondeterministic Choice diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-invariant.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-invariant.sh new file mode 100644 index 00000000..e206f237 --- /dev/null +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-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)/ieee-rcp-non-bisim-changed-invariant.txt" diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-2.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-invariant.txt similarity index 64% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-2.txt rename to examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-invariant.txt index e290b864..d45fa1ec 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-2.txt +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-invariant.txt @@ -1,36 +1,39 @@ # # This file has been generated automatically with uppaal-to-tchecker -# -system:ieee_rcp_reset_24.xml +# +# the original model has been published by +# Aurore Collomb-Annichini & Mihaela Sighireanu (2001): +# Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. +system:ieee_rcp.xml # no iodecl # compilation of process Process process:Process -# x:(clock) -clock:1:Process_x -# y:(clock) -clock:1:Process_y +# xr:(clock) +clock:1:Process_xr +# yr:(clock) +clock:1:Process_yr # snd_idle_i:(broadcast (channel)) # global event: Process_snd_idle_i # snd_req_i:(broadcast (channel)) # global event: Process_snd_req_i # snd_ack_i:(broadcast (channel)) # global event: Process_snd_ack_i -# rec_idle_j:(broadcast (channel)) -# global event: Process_rec_idle_j # rec_req_j:(broadcast (channel)) # global event: Process_rec_req_j +# rec_idle_j:(broadcast (channel)) +# global event: Process_rec_idle_j # rec_ack_j:(broadcast (channel)) # global event: Process_rec_ack_j -location:Process:REC_IDLE{invariant:(1 && (Process_y <= 42))} -location:Process:REC_IDLE_REC{invariant:(1 && (Process_x <= 42))} -location:Process:REC_REQ_ACK{invariant:(1 && (Process_x <= 42))} -location:Process:REC_ACK{invariant:(1 && (Process_y <= 42))} -location:Process:REC_REQ_IDLE{invariant:(1 && (Process_x <= 42))} -location:Process:REC_ACK_REQ{invariant:(1 && (Process_x <= 42))} -location:Process:EMPTY{} -location:Process:REC_ACK_IDLE{invariant:(1 && (Process_x <= 42))} -location:Process:REC_REQ{invariant:(1 && (Process_y <= 42))} -location:Process:REC_IDLE_ACK{initial::invariant:(1 && (Process_x <= 42))} +location:Process:REC_IDLE{invariant:(1 && (Process_yr <= 42))} +location:Process:REC_IDLE_REC{invariant:(1 && (Process_xr <= 42))} +location:Process:REC_REQ_ACK{invariant:(1 && (Process_xr <= 42))} +location:Process:REC_ACK{invariant:(1 && (Process_yr <= 42))} +location:Process:REC_REQ_IDLE{invariant:(1 && (Process_xr <= 42))} +location:Process:REC_ACK_REQ{invariant:(1 && (Process_xr <= 42))} +location:Process:EMPTY{invariant:(1 && (Process_xr <= 42))} # Mutation! +location:Process:REC_ACK_IDLE{invariant:(1 && (Process_xr <= 42))} +location:Process:REC_REQ{invariant:(1 && (Process_yr <= 42))} +location:Process:REC_IDLE_ACK{initial::invariant:(1 && (Process_xr <= 42))} event:Process_snd_idle_i event:Process_snd_idle_i_emit edge:Process:REC_REQ_IDLE:REC_REQ_IDLE:Process_snd_idle_i_emit{} @@ -42,15 +45,15 @@ edge:Process:REC_ACK_IDLE:REC_ACK_IDLE:Process_snd_idle_i_emit{} event:Process_snd_ack_i event:Process_snd_ack_i_emit edge:Process:REC_IDLE_ACK:REC_IDLE_ACK:Process_snd_ack_i_emit{} -edge:Process:REC_REQ:REC_REQ_IDLE:Process_snd_idle_i_emit{do:Process_y=0} -edge:Process:REC_IDLE:REC_IDLE_ACK:Process_snd_ack_i_emit{do:Process_y=0} +edge:Process:REC_REQ:REC_REQ_IDLE:Process_snd_idle_i_emit{do:Process_yr=0} +edge:Process:REC_IDLE:REC_IDLE_ACK:Process_snd_ack_i_emit{do:Process_yr=0} event:Process_rec_req_j event:Process_rec_req_j_emit edge:Process:REC_REQ_IDLE:REC_IDLE:Process_rec_req_j_emit{} event:Process_rec_idle_j event:Process_rec_idle_j_emit edge:Process:REC_IDLE_REC:REC_REQ:Process_rec_idle_j_emit{} -edge:Process:REC_IDLE:REC_IDLE_REC:Process_snd_req_i_emit{do:Process_y=0} +edge:Process:REC_IDLE:REC_IDLE_REC:Process_snd_req_i_emit{do:Process_yr=0} event:Process_rec_ack_j event:Process_rec_ack_j_emit edge:Process:REC_ACK_IDLE:REC_IDLE:Process_rec_ack_j_emit{} @@ -58,16 +61,15 @@ edge:Process:REC_REQ:REC_REQ:Process_snd_req_i_emit{} edge:Process:EMPTY:REC_IDLE:Process_snd_idle_i_emit{} edge:Process:REC_IDLE:EMPTY:Process_rec_idle_j_emit{} edge:Process:REC_ACK:EMPTY:Process_rec_ack_j_emit{} -edge:Process:EMPTY:REC_ACK:Process_snd_ack_i_emit{do:Process_x=0;Process_y=0} -edge:Process:EMPTY:REC_REQ:Process_snd_req_i_emit{do:Process_x=0;Process_y=0} +edge:Process:EMPTY:REC_ACK:Process_snd_ack_i_emit{do:Process_xr=0;Process_yr=0} +edge:Process:EMPTY:REC_REQ:Process_snd_req_i_emit{do:Process_xr=0;Process_yr=0} edge:Process:REC_REQ:EMPTY:Process_rec_req_j_emit{} edge:Process:REC_REQ_ACK:REC_REQ_ACK:Process_snd_ack_i_emit{} -edge:Process:REC_ACK:REC_ACK_IDLE:Process_snd_idle_i_emit{do:Process_y=0} +edge:Process:REC_ACK:REC_ACK_IDLE:Process_snd_idle_i_emit{do:Process_yr=0} edge:Process:REC_REQ_ACK:REC_ACK:Process_rec_req_j_emit{} edge:Process:REC_REQ:REC_REQ_ACK:Process_snd_ack_i_emit{} edge:Process:REC_ACK_REQ:REC_REQ:Process_rec_ack_j_emit{} -edge:Process:REC_ACK_REQ:REC_REQ:Process_rec_ack_j_emit{} -edge:Process:REC_ACK_REQ:REC_ACK_REQ:Process_snd_req_i_emit{do:Process_y=0} -edge:Process:REC_ACK:REC_ACK_REQ:Process_snd_req_i_emit{do:Process_y=0} +edge:Process:REC_ACK_REQ:REC_ACK_REQ:Process_snd_req_i_emit{} +edge:Process:REC_ACK:REC_ACK_REQ:Process_snd_req_i_emit{do:Process_yr=0} edge:Process:REC_IDLE_ACK:REC_ACK:Process_rec_idle_j_emit{} - +edge:Process:REC_REQ_ACK:REC_IDLE_ACK:Process_rec_req_j_emit{} # Added Nondeterministic Choice diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-2.sh b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-removed-reset.sh similarity index 67% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-2.sh rename to examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-removed-reset.sh index 899087f6..76ea112d 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/av-protocol-mutants/av-protocol-non-bisim-2.sh +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-removed-reset.sh @@ -4,4 +4,4 @@ # # See files AUTHORS and LICENSE for copyright details. -cat "$(dirname $0)/av-protocol-non-bisim-2.txt" +cat "$(dirname $0)/ieee-rcp-non-bisim-removed-reset.txt" diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-1.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-removed-reset.txt similarity index 68% rename from examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-1.txt rename to examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-removed-reset.txt index 8aeadb0e..78780f6d 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-1.txt +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-removed-reset.txt @@ -1,36 +1,39 @@ # # This file has been generated automatically with uppaal-to-tchecker -# -system:ieee_rcp_reset_20.xml +# +# the original model has been published by +# Aurore Collomb-Annichini & Mihaela Sighireanu (2001): +# Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. +system:ieee_rcp.xml # no iodecl # compilation of process Process process:Process -# x:(clock) -clock:1:Process_x -# y:(clock) -clock:1:Process_y +# xr:(clock) +clock:1:Process_xr +# yr:(clock) +clock:1:Process_yr # snd_idle_i:(broadcast (channel)) # global event: Process_snd_idle_i # snd_req_i:(broadcast (channel)) # global event: Process_snd_req_i # snd_ack_i:(broadcast (channel)) # global event: Process_snd_ack_i -# rec_idle_j:(broadcast (channel)) -# global event: Process_rec_idle_j # rec_req_j:(broadcast (channel)) # global event: Process_rec_req_j +# rec_idle_j:(broadcast (channel)) +# global event: Process_rec_idle_j # rec_ack_j:(broadcast (channel)) # global event: Process_rec_ack_j -location:Process:REC_IDLE{invariant:(1 && (Process_y <= 42))} -location:Process:REC_IDLE_REC{invariant:(1 && (Process_x <= 42))} -location:Process:REC_REQ_ACK{invariant:(1 && (Process_x <= 42))} -location:Process:REC_ACK{invariant:(1 && (Process_y <= 42))} -location:Process:REC_REQ_IDLE{invariant:(1 && (Process_x <= 42))} -location:Process:REC_ACK_REQ{invariant:(1 && (Process_x <= 42))} +location:Process:REC_IDLE{invariant:(1 && (Process_yr <= 42))} +location:Process:REC_IDLE_REC{invariant:(1 && (Process_xr <= 42))} +location:Process:REC_REQ_ACK{invariant:(1 && (Process_xr <= 42))} +location:Process:REC_ACK{invariant:(1 && (Process_yr <= 42))} +location:Process:REC_REQ_IDLE{invariant:(1 && (Process_xr <= 42))} +location:Process:REC_ACK_REQ{invariant:(1 && (Process_xr <= 42))} location:Process:EMPTY{} -location:Process:REC_ACK_IDLE{invariant:(1 && (Process_x <= 42))} -location:Process:REC_REQ{invariant:(1 && (Process_y <= 42))} -location:Process:REC_IDLE_ACK{initial::invariant:(1 && (Process_x <= 42))} +location:Process:REC_ACK_IDLE{invariant:(1 && (Process_xr <= 42))} +location:Process:REC_REQ{invariant:(1 && (Process_yr <= 42))} +location:Process:REC_IDLE_ACK{initial::invariant:(1 && (Process_xr <= 42))} event:Process_snd_idle_i event:Process_snd_idle_i_emit edge:Process:REC_REQ_IDLE:REC_REQ_IDLE:Process_snd_idle_i_emit{} @@ -42,15 +45,15 @@ edge:Process:REC_ACK_IDLE:REC_ACK_IDLE:Process_snd_idle_i_emit{} event:Process_snd_ack_i event:Process_snd_ack_i_emit edge:Process:REC_IDLE_ACK:REC_IDLE_ACK:Process_snd_ack_i_emit{} -edge:Process:REC_REQ:REC_REQ_IDLE:Process_snd_idle_i_emit{do:Process_y=0} -edge:Process:REC_IDLE:REC_IDLE_ACK:Process_snd_ack_i_emit{do:Process_y=0} +edge:Process:REC_REQ:REC_REQ_IDLE:Process_snd_idle_i_emit{do:Process_yr=0} +edge:Process:REC_IDLE:REC_IDLE_ACK:Process_snd_ack_i_emit{do:Process_yr=0} event:Process_rec_req_j event:Process_rec_req_j_emit edge:Process:REC_REQ_IDLE:REC_IDLE:Process_rec_req_j_emit{} event:Process_rec_idle_j event:Process_rec_idle_j_emit edge:Process:REC_IDLE_REC:REC_REQ:Process_rec_idle_j_emit{} -edge:Process:REC_IDLE:REC_IDLE_REC:Process_snd_req_i_emit{do:Process_y=0} +edge:Process:REC_IDLE:REC_IDLE_REC:Process_snd_req_i_emit{do:Process_yr=0} event:Process_rec_ack_j event:Process_rec_ack_j_emit edge:Process:REC_ACK_IDLE:REC_IDLE:Process_rec_ack_j_emit{} @@ -58,16 +61,15 @@ edge:Process:REC_REQ:REC_REQ:Process_snd_req_i_emit{} edge:Process:EMPTY:REC_IDLE:Process_snd_idle_i_emit{} edge:Process:REC_IDLE:EMPTY:Process_rec_idle_j_emit{} edge:Process:REC_ACK:EMPTY:Process_rec_ack_j_emit{} -edge:Process:EMPTY:REC_ACK:Process_snd_ack_i_emit{do:Process_x=0;Process_y=0} -edge:Process:EMPTY:REC_REQ:Process_snd_req_i_emit{do:Process_x=0;Process_y=0} +edge:Process:EMPTY:REC_ACK:Process_snd_ack_i_emit{do:Process_xr=0} # Mutation! +edge:Process:EMPTY:REC_REQ:Process_snd_req_i_emit{do:Process_xr=0;Process_yr=0} edge:Process:REC_REQ:EMPTY:Process_rec_req_j_emit{} edge:Process:REC_REQ_ACK:REC_REQ_ACK:Process_snd_ack_i_emit{} -edge:Process:REC_ACK:REC_ACK_IDLE:Process_snd_idle_i_emit{do:Process_x=0;Process_y=0} +edge:Process:REC_ACK:REC_ACK_IDLE:Process_snd_idle_i_emit{do:Process_yr=0} edge:Process:REC_REQ_ACK:REC_ACK:Process_rec_req_j_emit{} edge:Process:REC_REQ:REC_REQ_ACK:Process_snd_ack_i_emit{} edge:Process:REC_ACK_REQ:REC_REQ:Process_rec_ack_j_emit{} -edge:Process:REC_ACK_REQ:REC_REQ:Process_rec_ack_j_emit{} edge:Process:REC_ACK_REQ:REC_ACK_REQ:Process_snd_req_i_emit{} -edge:Process:REC_ACK:REC_ACK_REQ:Process_snd_req_i_emit{do:Process_y=0} +edge:Process:REC_ACK:REC_ACK_REQ:Process_snd_req_i_emit{do:Process_yr=0} edge:Process:REC_IDLE_ACK:REC_ACK:Process_rec_idle_j_emit{} - +edge:Process:REC_REQ_ACK:REC_IDLE_ACK:Process_rec_req_j_emit{} # Added Nondeterministic Choice diff --git a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp.txt b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp.txt index 85a6fa6b..c037d660 100644 --- a/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp.txt +++ b/examples/strong_timed_bisim_benchmarks/nondeterministic/ieee-rcp.txt @@ -68,8 +68,8 @@ edge:Process:REC_REQ_ACK:REC_REQ_ACK:Process_snd_ack_i_emit{} edge:Process:REC_ACK:REC_ACK_IDLE:Process_snd_idle_i_emit{do:Process_yr=0} edge:Process:REC_REQ_ACK:REC_ACK:Process_rec_req_j_emit{} edge:Process:REC_REQ:REC_REQ_ACK:Process_snd_ack_i_emit{} -edge:Process:REC_ACK_REQ:REC_REQ:Process_rec_ack_j_emit{provided:(Process_xr <= 5)} -edge:Process:REC_ACK_REQ:REC_REQ:Process_rec_ack_j_emit{provided:(Process_xr>=5)} +edge:Process:REC_ACK_REQ:REC_REQ:Process_rec_ack_j_emit{} edge:Process:REC_ACK_REQ:REC_ACK_REQ:Process_snd_req_i_emit{} edge:Process:REC_ACK:REC_ACK_REQ:Process_snd_req_i_emit{do:Process_yr=0} edge:Process:REC_IDLE_ACK:REC_ACK:Process_rec_idle_j_emit{} +edge:Process:REC_REQ_ACK:REC_IDLE_ACK:Process_rec_req_j_emit{} # Added Nondeterministic Choice