Added results for deadlock-freeness

benchmarks/service-tech/benchmarks-contingency.sh

@@ -20,7 +20,7 @@ our_tool=slapnet
 
 #benchmark_dirs=( 'ibm-soundness' )
 benchmark_dirs=( 'sap-reference' )
-benchmark_tools=( 'sara' )
+benchmark_tools=( 'lola' )
 for (( benchmark=0;benchmark<${#benchmark_dirs[@]};benchmark++)); do
   benchmark_dir=${benchmark_dirs[$benchmark]}
   other_tool=${benchmark_tools[$benchmark]}

benchmarks/service-tech/run-benchmarks-lola.sh

@@ -3,7 +3,8 @@
 #benchmarks=( 'ibm-soundness' 'sap-reference' )
 benchmarks=( 'sap-reference' )
 #benchmarks=( 'ibm-soundness' )
-extensions=( 'pnet' 'tpn' 'lola' )
+#extensions=( 'pnet' 'tpn' 'lola' )
+extensions=( 'tpn' )
 executable='/home/philipp/local/lola-2.0/src/lola'
 
 for benchmark in ${benchmarks[@]}; do
@@ -17,7 +18,7 @@ for benchmark in ${benchmarks[@]}; do
       T="$(date +%s%N)"
       (
         set -o pipefail;
-        $executable -f $file.terminating.task1 $file.terminating --markinglimit=1000000 2>&1 | tee $file.out
+        $executable -f $file.df.task1 $file.df --markinglimit=10000000 2>&1 | tee $file.out
       )
       result=$?
       ryes=$(grep "result: yes" $file.out)

benchmarks/service-tech/run-benchmarks.sh

@@ -3,7 +3,8 @@
 #benchmarks=( 'ibm-soundness' 'sap-reference' )
 benchmarks=( 'sap-reference' )
 #benchmarks=( 'ibm-soundness' )
-extensions=( 'pnet' 'tpn' 'lola' )
+#extensions=( 'pnet' 'tpn' 'lola' )
+extensions=( 'tpn' )
 executable='../../slapnet'
 
 for benchmark in ${benchmarks[@]}; do
@@ -17,7 +18,7 @@ for benchmark in ${benchmarks[@]}; do
       T="$(date +%s%N)"
       (
         set -o pipefail;
-        timeout 60 $executable --$ext --validate-identifiers --termination-by-reachability -o $file.terminating $file | tee $file.out
+        timeout 60 $executable --$ext --no-refinement --deadlock-free-unless-final $file | tee $file.out
       )
       result=$?
       T=$(($(date +%s%N)-T))

benchmarks/service-tech/sap-reference/deadlock-free.positive

+sap-reference/models/Model.3zzv__0_____u__.xml
+sap-reference/models/Model.g0mo__0_____u__.xml
+sap-reference/models/Model.kxnh__0_____u__.xml

benchmarks/service-tech/sap-reference/models/Model.18wm__0_____u__.xml.tpn.df

+PLACE i,o,p_Model_18wm__0_____u___Model_18wm__0_____u___InputCondition,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Split_and__18yh_,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Join_and__18yh_,p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Split_xor__18x0_,p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Join_xor__18x0_,p_Model_18wm__0_____u___Model_18wm__0_____u___outputCondition,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__and__18yh_,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Find_Object__18xe_,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Material_Search__18xs_,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Document_Search__18y6_,p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__and__18ys_,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__xor__18x0_,p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__Join_Yes_xor__18x0_,p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__and__18ys_,p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__and__18ys_,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Skip_busy,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Join_No_xor__18x0__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Yes_xor__18x0__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Output_busy;
+
+MARKING i:1;
+
+TRANSITION __Model_18wm__0_____u___Model_18wm__0_____u___start
+CONSUME i:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___InputCondition:1;
+
+TRANSITION __Model_18wm__0_____u___Model_18wm__0_____u___end
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___outputCondition:1;
+PRODUCE o:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Split_join_InputCondition
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___InputCondition:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Split_busy:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Split_split_Split_Split_and__18yh_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_busy:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Split_and__18yh_:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__join_Split_Split_and__18yh_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Split_and__18yh_:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__busy:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__split_Split_Join_and__18yh_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__busy:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Join_and__18yh_:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__join_Split_Split_and__18yh_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Split_and__18yh_:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__busy:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__split_Split_Join_and__18yh__Split_Yes_and__18yh__and__18yh_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__busy:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Join_and__18yh_:1,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__and__18yh_:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Skip_join_Split_Join_and__18yh_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Join_and__18yh_:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Skip_busy:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Skip_split_Join_Split_xor__18x0_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Skip_busy:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Split_xor__18x0_:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__join_Split_Yes_and__18yh__and__18yh_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__and__18yh_:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__busy:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__split_and__18yh__Find_Object__18xe__and__18yh__Material_Search__18xs__and__18yh__Document_Search__18y6_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__busy:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Document_Search__18y6_:1,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Find_Object__18xe_:1,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Material_Search__18xs_:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__join_and__18yh__Find_Object__18xe_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Find_Object__18xe_:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__busy:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__split_Find_Object__18xe__and__18ys_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__busy:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__and__18ys_:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__join_Find_Object__18xe__and__18ys__Material_Search__18xs__and__18ys__Document_Search__18y6__and__18ys_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__and__18ys_:1,p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__and__18ys_:1,p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__and__18ys_:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__busy:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__split_and__18ys__xor__18x0_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__busy:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__xor__18x0_:1;
+
+TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__join_and__18ys__xor__18x0_
+CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__xor__18x0_:1;
+PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__busy:1;