From c8b0c25dbc50019d779f9cac2be4ea4d6c224210 Mon Sep 17 00:00:00 2001 From: Alexander Lieb Date: Sat, 12 Oct 2024 19:59:10 +0200 Subject: [PATCH] unified benchmark --- .../av-protocol-mutants/av-protocol-bisim.txt | 2 +- .../av-protocol-non-bisim-changed-guard.sh} | 2 +- ...> av-protocol-non-bisim-changed-guard.txt} | 0 ...v-protocol-non-bisim-changed-invariant.sh} | 0 ...-protocol-non-bisim-changed-invariant.txt} | 12 ++-- ...=> av-protocol-non-bisim-removed-reset.sh} | 2 +- ...> av-protocol-non-bisim-removed-reset.txt} | 2 +- .../collision-avoidance-bisim.txt | 36 ++++++------ .../collision-avoidance-non-bisim-3.sh | 7 --- ...ision-avoidance-non-bisim-changed-guard.sh | 7 +++ ...ion-avoidance-non-bisim-changed-guard.txt} | 34 +++++------ ...n-avoidance-non-bisim-changed-invariant.sh | 7 +++ ...avoidance-non-bisim-changed-invariant.txt} | 36 ++++++------ ...ision-avoidance-non-bisim-removed-reset.sh | 7 +++ ...ion-avoidance-non-bisim-removed-reset.txt} | 34 +++++------ .../ieee-rcp-mutants/ieee-rcp-bisim.txt | 16 +++--- .../ieee-rcp-mutants/ieee-rcp-non-bisim-1.sh | 7 --- .../ieee-rcp-mutants/ieee-rcp-non-bisim-2.sh | 7 --- .../ieee-rcp-mutants/ieee-rcp-non-bisim-3.sh | 7 --- .../ieee-rcp-non-bisim-changed-guard.sh} | 2 +- ...t => ieee-rcp-non-bisim-changed-guard.txt} | 54 +++++++++--------- .../ieee-rcp-non-bisim-changed-invariant.sh | 7 +++ ... ieee-rcp-non-bisim-changed-invariant.txt} | 56 ++++++++++--------- .../ieee-rcp-non-bisim-removed-reset.sh} | 2 +- ...t => ieee-rcp-non-bisim-removed-reset.txt} | 52 ++++++++--------- 25 files changed, 208 insertions(+), 190 deletions(-) rename examples/strong_timed_bisim_benchmarks/deterministic/{collision-avoidance-mutants/collision-avoidance-non-bisim-2.sh => av-protocol-mutants/av-protocol-non-bisim-changed-guard.sh} (66%) rename examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/{av-protocol-non-bisim-3.txt => av-protocol-non-bisim-changed-guard.txt} (100%) rename examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/{av-protocol-non-bisim-1.sh => av-protocol-non-bisim-changed-invariant.sh} (100%) rename examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/{av-protocol-non-bisim-1.txt => av-protocol-non-bisim-changed-invariant.txt} (93%) rename examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/{av-protocol-non-bisim-3.sh => av-protocol-non-bisim-removed-reset.sh} (66%) rename examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/{av-protocol-non-bisim-2.txt => av-protocol-non-bisim-removed-reset.txt} (98%) delete mode 100644 examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.sh create mode 100644 examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-guard.sh rename examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/{collision-avoidance-non-bisim-1.txt => collision-avoidance-non-bisim-changed-guard.txt} (79%) create mode 100644 examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-invariant.sh rename examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/{collision-avoidance-non-bisim-2.txt => collision-avoidance-non-bisim-changed-invariant.txt} (75%) create mode 100644 examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-removed-reset.sh rename examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/{collision-avoidance-non-bisim-3.tck => collision-avoidance-non-bisim-removed-reset.txt} (77%) delete mode 100644 examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-1.sh delete mode 100644 examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-2.sh delete mode 100644 examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-3.sh rename examples/strong_timed_bisim_benchmarks/deterministic/{collision-avoidance-mutants/collision-avoidance-non-bisim-1.sh => ieee-rcp-mutants/ieee-rcp-non-bisim-changed-guard.sh} (67%) rename examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/{ieee-rcp-non-bisim-3.txt => ieee-rcp-non-bisim-changed-guard.txt} (66%) create mode 100644 examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-invariant.sh rename examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/{ieee-rcp-non-bisim-2.txt => ieee-rcp-non-bisim-changed-invariant.txt} (66%) rename examples/strong_timed_bisim_benchmarks/deterministic/{av-protocol-mutants/av-protocol-non-bisim-2.sh => ieee-rcp-mutants/ieee-rcp-non-bisim-removed-reset.sh} (67%) rename examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/{ieee-rcp-non-bisim-1.txt => ieee-rcp-non-bisim-removed-reset.txt} (70%) diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-bisim.txt b/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-bisim.txt index 0d3dbed5..5263d57b 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-bisim.txt +++ b/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-bisim.txt @@ -84,7 +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} # 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 diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-2.sh b/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.sh similarity index 66% rename from examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-2.sh rename to examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.sh index 8fb367bb..d4c4177a 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-2.sh +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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/deterministic/av-protocol-mutants/av-protocol-non-bisim-3.txt b/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.txt similarity index 100% rename from examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-3.txt rename to examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-guard.txt diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-1.sh b/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-invariant.sh similarity index 100% rename from examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-1.sh rename to examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-invariant.sh diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-1.txt b/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-invariant.txt similarity index 93% rename from examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-1.txt rename to examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-changed-invariant.txt index 4ef5c4f3..df33ace9 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-1.txt +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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))} @@ -89,7 +92,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{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)} @@ -139,4 +142,3 @@ 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} - diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-3.sh b/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-removed-reset.sh similarity index 66% rename from examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-3.sh rename to examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-removed-reset.sh index 4903a71f..7e2625cf 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-3.sh +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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/deterministic/av-protocol-mutants/av-protocol-non-bisim-2.txt b/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-removed-reset.txt similarity index 98% rename from examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-2.txt rename to examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-removed-reset.txt index d4993f4e..c3abc17a 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-2.txt +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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} diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-bisim.txt b/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-bisim.txt index 097f70bd..b6e61b3e 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-bisim.txt +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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,35 +38,34 @@ 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_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} diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.sh b/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.sh deleted file mode 100644 index 8fb367bb..00000000 --- a/examples/strong_timed_bisim_benchmarks/deterministic/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/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-guard.sh b/examples/strong_timed_bisim_benchmarks/deterministic/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/deterministic/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/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-1.txt b/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-guard.txt similarity index 79% rename from examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-1.txt rename to examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-guard.txt index cdc0de90..afb6645e 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-1.txt +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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,35 +38,34 @@ 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_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} diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-invariant.sh b/examples/strong_timed_bisim_benchmarks/deterministic/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/deterministic/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/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-2.txt b/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-invariant.txt similarity index 75% rename from examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-2.txt rename to examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-invariant.txt index f454e38c..e384a451 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-2.txt +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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,39 +34,38 @@ 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_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} diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-removed-reset.sh b/examples/strong_timed_bisim_benchmarks/deterministic/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/deterministic/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/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.tck b/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-removed-reset.txt similarity index 77% rename from examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.tck rename to examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-removed-reset.txt index 09db36e8..17de0cf0 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.tck +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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,35 +38,34 @@ 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_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! diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-bisim.txt b/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-bisim.txt index 3647b24d..a3c719ea 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-bisim.txt +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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,11 +65,11 @@ 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{} 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_IDLE_ACK:REC_ACK:Process_rec_idle_j_emit{} \ No newline at end of file diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-1.sh b/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-1.sh deleted file mode 100644 index 9a7dd7e7..00000000 --- a/examples/strong_timed_bisim_benchmarks/deterministic/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/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-2.sh b/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-2.sh deleted file mode 100644 index bad7c518..00000000 --- a/examples/strong_timed_bisim_benchmarks/deterministic/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/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-3.sh b/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-3.sh deleted file mode 100644 index 683b530e..00000000 --- a/examples/strong_timed_bisim_benchmarks/deterministic/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/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-1.sh b/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-guard.sh similarity index 67% rename from examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-1.sh rename to examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-guard.sh index ada16119..d5b1b74d 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-1.sh +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-3.txt b/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-guard.txt similarity index 66% rename from examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-3.txt rename to examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-guard.txt index 686df721..9936c380 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-3.txt +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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,31 +45,30 @@ 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_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{} - diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-invariant.sh b/examples/strong_timed_bisim_benchmarks/deterministic/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/deterministic/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/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-2.txt b/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-invariant.txt similarity index 66% rename from examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-2.txt rename to examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-changed-invariant.txt index ac2f4a19..c0edc458 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-2.txt +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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,15 +61,14 @@ 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_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{} - diff --git a/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-2.sh b/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-removed-reset.sh similarity index 67% rename from examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-2.sh rename to examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-removed-reset.sh index 899087f6..76ea112d 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-non-bisim-2.sh +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-1.txt b/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-removed-reset.txt similarity index 70% rename from examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-1.txt rename to examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-removed-reset.txt index a33b2b8d..d114540f 100644 --- a/examples/strong_timed_bisim_benchmarks/deterministic/ieee-rcp-mutants/ieee-rcp-non-bisim-1.txt +++ b/examples/strong_timed_bisim_benchmarks/deterministic/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,15 +61,14 @@ 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_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{} -