Skip to content

Commit

Permalink
unified benchmark
Browse files Browse the repository at this point in the history
  • Loading branch information
@alzeha
alzeha committed Oct 12, 2024
1 parent 661ef25 commit c8b0c25
Show file tree
Hide file tree
Showing 25 changed files with 208 additions and 190 deletions.
2 changes: 1 addition & 1 deletion ...les/strong_timed_bisim_benchmarks/deterministic/av-protocol-mutants/av-protocol-bisim.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion ...utants/collision-avoidance-non-bisim-2.sh → ...ts/av-protocol-non-bisim-changed-guard.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
0 ...tocol-mutants/av-protocol-non-bisim-3.txt → ...s/av-protocol-non-bisim-changed-guard.txt
View file
File renamed without changes.
0 ...otocol-mutants/av-protocol-non-bisim-1.sh → ...v-protocol-non-bisim-changed-invariant.sh
View file
File renamed without changes.
12 changes: 7 additions & 5 deletions ...tocol-mutants/av-protocol-non-bisim-1.txt → ...-protocol-non-bisim-changed-invariant.txt
View file
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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))}
Expand Down Expand Up @@ -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)}
Expand Down Expand Up @@ -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}

2 changes: 1 addition & 1 deletion ...otocol-mutants/av-protocol-non-bisim-3.sh → ...ts/av-protocol-non-bisim-removed-reset.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
2 changes: 1 addition & 1 deletion ...tocol-mutants/av-protocol-non-bisim-2.txt → ...s/av-protocol-non-bisim-removed-reset.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
36 changes: 19 additions & 17 deletions ..._bisim_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-bisim.txt
View file
Original file line number Diff line number Diff line change
@@ -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))
Expand Down Expand Up @@ -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}
7 changes: 0 additions & 7 deletions ...m_benchmarks/deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-3.sh
View file

This file was deleted.

7 changes: 7 additions & 0 deletions .../deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-guard.sh
View file
Original file line number Diff line number Diff line change
@@ -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"
34 changes: 18 additions & 16 deletions ...tants/collision-avoidance-non-bisim-1.txt → ...ion-avoidance-non-bisim-changed-guard.txt
View file
Original file line number Diff line number Diff line change
@@ -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))
Expand Down Expand Up @@ -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}
7 changes: 7 additions & 0 deletions ...erministic/collision-avoidance-mutants/collision-avoidance-non-bisim-changed-invariant.sh
View file
Original file line number Diff line number Diff line change
@@ -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"
36 changes: 19 additions & 17 deletions ...tants/collision-avoidance-non-bisim-2.txt → ...avoidance-non-bisim-changed-invariant.txt
View file
Original file line number Diff line number Diff line change
@@ -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))
Expand All @@ -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}
7 changes: 7 additions & 0 deletions .../deterministic/collision-avoidance-mutants/collision-avoidance-non-bisim-removed-reset.sh
View file
Original file line number Diff line number Diff line change
@@ -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"
34 changes: 18 additions & 16 deletions ...tants/collision-avoidance-non-bisim-3.tck → ...ion-avoidance-non-bisim-removed-reset.txt
View file
Original file line number Diff line number Diff line change
@@ -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))
Expand Down Expand Up @@ -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!
Loading

0 comments on commit c8b0c25

Please sign in to comment.