Added benchmarks given by Karsten Wolf

benchmarks/service-tech/benchmarks-contingency.sh

+#!/bin/bash
+
+function sort_file {
+  cat $1 | \
+  sed -e 's/^[[:digit:]]* //' \
+      -e 's/\.pl$//' \
+      -e 's/\.pnet$//' \
+      -e 's/\.spec$//' \
+      -e 's/\.tts$//' \
+      -e 's/\.lola$//' \
+      -e 's/\.tpn$//' | \
+  sort \
+  >$1.sorted
+}
+
+results_our_tool=( positive dontknow error timeout )
+results_other_tool=( positive negative error timeout )
+
+our_tool=slapnet
+
+benchmark_dirs=( 'ibm-soundness' ) # 'sap-reference' )
+benchmark_tools=( 'lola' 'lola' )
+for (( benchmark=0;benchmark<${#benchmark_dirs[@]};benchmark++)); do
+  benchmark_dir=${benchmark_dirs[$benchmark]}
+  other_tool=${benchmark_tools[$benchmark]}
+  echo "$our_tool on $benchmark_dir compared with $other_tool"
+  for result in "${results_our_tool[@]}"; do
+    sort_file $benchmark_dir/$result-$our_tool.list
+  done
+  for result in "${results_other_tool[@]}"; do
+    sort_file $benchmark_dir/$result-$other_tool.list
+  done
+  echo -n "other\\our| "
+  for ((rour=0;rour<${#results_our_tool[@]};rour++)); do
+    printf "%8s | " ${results_our_tool[$rour]}
+    sums_our_tool[$rour]=0
+  done
+  echo
+  echo -n "---------+-"
+  for rour in "${results_our_tool[@]}"; do
+    echo -n "---------+-"
+  done
+  echo "---------"
+  for rother in "${results_other_tool[@]}"; do
+    printf "%8s | " $rother
+    sum_other_tool=0
+    for ((rour=0;rour<${#results_our_tool[@]};rour++)); do
+      n=`comm -12 $benchmark_dir/${results_our_tool[$rour]}-$our_tool.list.sorted $benchmark_dir/$rother-$other_tool.list.sorted | wc -l`
+      printf "%8d | " $n
+      sum_other_tool=$((sum_other_tool + n))
+      sums_our_tool[$rour]=$((${sums_our_tool[$rour]} + n))
+    done
+    printf "%8d\n" $sum_other_tool
+  done
+  echo -n "---------+-"
+  for rour in "${results_our_tool[@]}"; do
+    echo -n "---------+-"
+  done
+  echo "---------"
+  total_sum=0
+  echo -n " our sum | "
+  for ((rour=0;rour<${#results_our_tool[@]};rour++)); do
+    printf "%8d | " ${sums_our_tool[$rour]}
+    total_sum=$((total_sum + ${sums_our_tool[$rour]}))
+  done
+  printf "%8d\n" $total_sum
+  echo -n "---------+-"
+  for rour in "${results_our_tool[@]}"; do
+    echo -n "---------+-"
+  done
+  echo "---------"
+  total_time=0
+  echo -n "our time | "
+  for ((rour=0;rour<${#results_our_tool[@]};rour++)); do
+    result=${results_our_tool[$rour]}
+    result_time=0
+    while read T file; do
+      result_time=$((result_time + T))
+    done <$benchmark_dir/$result-$our_tool.list
+    printf "%1.2e | " $result_time
+    total_time=$((total_time + $result_time))
+  done
+  printf "%1.2e\n" $total_time
+  echo
+done

benchmarks/service-tech/ibm-soundness/README

+IBM BUSINESS PROCESS MODELS
+===========================
+
+About
+-----
+
+* Added by: Niels Lohmann <niels.lohmann@uni-rostock.de>
+* Original source: IBM Zurich Research Lab
+* Net type:
+  * Workflow nets
+  * Free Choice
+* Format: LoLA low-level nets, translated by UML2oWFN
+
+
+Notes
+-----
+
+* The models have been anonymized library by library. Names within library B1
+  hence have no meaning in library B2.
+* Each net has two LoLA task files. One for checking weak termination using
+  LIVEPROP and one for checking safeness using STATEPREDICATE.
+
+
+Soundness Check
+---------------
+
+1. Check for weak termination:
+
+    lola-bpm-liveprop1 net.lola -anet.lola.fin.task
+
+2. Check for safeness:
+
+    lola-bpm-statepredicate1 net.lola -anet.lola.safe.task
+
+The LoLA binaries can be created by
+
+    make lola-bpm-liveprop1 lola-bpm-statepredicate1
+
+inside LoLA's directory.
+
+
+Liveness Check
+--------------
+
+Liveness was checked after connecting the output place
+via a new transition to the input place by the tool
+Anastasia, using the command line
+
+    anastasia net.lola --lola --loopnet --swomt --witness
+
+* 590 nets were found live
+* 796 nets were found non-live
+
+Results for each net and a firing sequence emptying a
+siphon in the non-live case can be found in anastasia.zip.
+
+
+Statistics
+----------
+
+* 1386 nets
+* 66379 places (average: 47, minimum: 4, maximum: 273)
+* 44623 transitions (average: 32, minimum: 3, maximum: 284)
+* 132432 arcs (average: 95, minimum: 6, maximum: 572)
+
+
+References
+----------
+
+* Dirk Fahland, Cédric Favre, Barbara Jobstmann, Jana Koehler, Niels Lohmann,
+  Hagen Völzer, and Karsten Wolf. Instantaneous Soundness Checking of
+  Industrial Business Process Models. In Umeshwar Dayal, Johann Eder, Jana
+  Koehler, and Hajo A. Reijers, editors, Business Process Management, 7th
+  International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009,
+  Proceedings, volume 5701 of Lecture Notes in Computer Science, pages
+  278-293, September 2009. Springer-Verlag.

benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000021__s00000698.lola

+{ Petri net created by UML2oWFN 2.11 }
+
+PLACE
+  alpha, callToTask.s00000743.input.s00000699, callToTask.s00000743.input.s00000709, callToTask.s00000743.inputCriterion.s00000700.used, callToTask.s00000743.output.s00000713, callToTask.s00000743.output.s00000754, callToTask.s00000744.input.s00000709, callToTask.s00000744.input.s00000752, callToTask.s00000744.inputCriterion.s00000700.used, callToTask.s00000744.output.s00000713, callToTask.s00000744.output.s00000754, callToTask.s00000745.input.s00000699, callToTask.s00000745.input.s00000709, callToTask.s00000745.inputCriterion.s00000700.used, callToTask.s00000745.output.s00000702, callToTask.s00000745.output.s00000713, callToTask.s00000745.output.s00000754, callToTask.s00000746.input.s00000699, callToTask.s00000746.input.s00000709, callToTask.s00000746.inputCriterion.s00000700.used, callToTask.s00000746.output.s00000703, callToTask.s00000746.output.s00000713, callToTask.s00000746.output.s00000754, callToTask.s00000747.input.s00000699, callToTask.s00000747.input.s00000709, callToTask.s00000747.inputCriterion.s00000700.used, callToTask.s00000747.output.s00000713, callToTask.s00000747.output.s00000754, callToTask.s00000748.input.s00000699, callToTask.s00000748.input.s00000709, callToTask.s00000748.inputCriterion.s00000700.used, callToTask.s00000748.output.s00000713, callToTask.s00000748.output.s00000754, decision.s00000707.activated, decision.s00000719.activated, endNode.s00000706.input.default, merge.s00000730.activated, merge.s00000742.activated, merge.s00000742.input.s00000709, merge.s00000742.input.s00000737, merge.s00000742.input.s00000740, process.s00000021##s00000698.input.s00000699, process.s00000021##s00000698.output.s00000701, process.s00000021##s00000698.outputCriterion.s00000704_omega;
+
+MARKING
+  alpha:1;
+
+
+TRANSITION callToTask.s00000743.inputCriterion.s00000700
+  CONSUME callToTask.s00000743.input.s00000699:1, callToTask.s00000743.input.s00000709:1;
+  PRODUCE callToTask.s00000743.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000743.outputCriterion.s00000704
+  CONSUME callToTask.s00000743.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000743.output.s00000713:1, callToTask.s00000743.output.s00000754:1;
+
+TRANSITION callToTask.s00000744.inputCriterion.s00000700
+  CONSUME callToTask.s00000744.input.s00000709:1, callToTask.s00000744.input.s00000752:1;
+  PRODUCE callToTask.s00000744.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000744.outputCriterion.s00000704
+  CONSUME callToTask.s00000744.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000744.output.s00000713:1, callToTask.s00000744.output.s00000754:1;
+
+TRANSITION callToTask.s00000745.inputCriterion.s00000700
+  CONSUME callToTask.s00000745.input.s00000699:1, callToTask.s00000745.input.s00000709:1;
+  PRODUCE callToTask.s00000745.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000745.outputCriterion.s00000704
+  CONSUME callToTask.s00000745.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000745.output.s00000702:1, callToTask.s00000745.output.s00000713:1, callToTask.s00000745.output.s00000754:1;
+
+TRANSITION callToTask.s00000746.inputCriterion.s00000700
+  CONSUME callToTask.s00000746.input.s00000699:1, callToTask.s00000746.input.s00000709:1;
+  PRODUCE callToTask.s00000746.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000746.outputCriterion.s00000704
+  CONSUME callToTask.s00000746.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000746.output.s00000703:1, callToTask.s00000746.output.s00000713:1, callToTask.s00000746.output.s00000754:1;
+
+TRANSITION callToTask.s00000747.inputCriterion.s00000700
+  CONSUME callToTask.s00000747.input.s00000699:1, callToTask.s00000747.input.s00000709:1;
+  PRODUCE callToTask.s00000747.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000747.outputCriterion.s00000704
+  CONSUME callToTask.s00000747.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000747.output.s00000713:1, callToTask.s00000747.output.s00000754:1;
+
+TRANSITION callToTask.s00000748.inputCriterion.s00000700
+  CONSUME callToTask.s00000748.input.s00000699:1, callToTask.s00000748.input.s00000709:1;
+  PRODUCE callToTask.s00000748.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000748.outputCriterion.s00000704
+  CONSUME callToTask.s00000748.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000748.output.s00000713:1, callToTask.s00000748.output.s00000754:1;
+
+TRANSITION decision.s00000707.activate.s00000708
+  CONSUME callToTask.s00000747.output.s00000713:1, callToTask.s00000747.output.s00000754:1;
+  PRODUCE decision.s00000707.activated:1;
+
+TRANSITION decision.s00000707.fire.s00000711
+  CONSUME decision.s00000707.activated:1;
+  PRODUCE endNode.s00000706.input.default:1, process.s00000021##s00000698.output.s00000701:1;
+
+TRANSITION decision.s00000707.fire.s00000715
+  CONSUME decision.s00000707.activated:1;
+  PRODUCE merge.s00000742.input.s00000737:1, merge.s00000742.input.s00000740:1;
+
+TRANSITION decision.s00000719.activate.s00000708
+  CONSUME callToTask.s00000748.output.s00000713:1, callToTask.s00000748.output.s00000754:1;
+  PRODUCE decision.s00000719.activated:1;
+
+TRANSITION decision.s00000719.fire.s00000711
+  CONSUME decision.s00000719.activated:1;
+  PRODUCE callToTask.s00000744.input.s00000709:1, callToTask.s00000744.input.s00000752:1;
+
+TRANSITION decision.s00000719.fire.s00000715
+  CONSUME decision.s00000719.activated:1;
+  PRODUCE callToTask.s00000745.input.s00000699:1, callToTask.s00000745.input.s00000709:1;
+
+TRANSITION decision.s00000719.fire.s00000724
+  CONSUME decision.s00000719.activated:1;
+  PRODUCE callToTask.s00000746.input.s00000699:1, callToTask.s00000746.input.s00000709:1;
+
+TRANSITION decision.s00000719.fire.s00000727
+  CONSUME decision.s00000719.activated:1;
+  PRODUCE callToTask.s00000743.input.s00000699:1, callToTask.s00000743.input.s00000709:1;
+
+TRANSITION merge.s00000730.activate.s00000731
+  CONSUME callToTask.s00000744.output.s00000713:1, callToTask.s00000744.output.s00000754:1;
+  PRODUCE merge.s00000730.activated:1;
+
+TRANSITION merge.s00000730.activate.s00000733
+  CONSUME callToTask.s00000745.output.s00000713:1, callToTask.s00000745.output.s00000754:1;
+  PRODUCE merge.s00000730.activated:1;
+
+TRANSITION merge.s00000730.activate.s00000735
+  CONSUME callToTask.s00000746.output.s00000713:1, callToTask.s00000746.output.s00000754:1;
+  PRODUCE merge.s00000730.activated:1;
+
+TRANSITION merge.s00000730.activate.s00000738
+  CONSUME callToTask.s00000743.output.s00000713:1, callToTask.s00000743.output.s00000754:1;
+  PRODUCE merge.s00000730.activated:1;
+
+TRANSITION merge.s00000730.fire.s00000741
+  CONSUME merge.s00000730.activated:1;
+  PRODUCE callToTask.s00000747.input.s00000699:1, callToTask.s00000747.input.s00000709:1;
+
+TRANSITION merge.s00000742.activate.s00000731
+  CONSUME merge.s00000742.input.s00000709:1, process.s00000021##s00000698.input.s00000699:1;
+  PRODUCE merge.s00000742.activated:1;
+
+TRANSITION merge.s00000742.activate.s00000733
+  CONSUME merge.s00000742.input.s00000737:1, merge.s00000742.input.s00000740:1;
+  PRODUCE merge.s00000742.activated:1;
+
+TRANSITION merge.s00000742.fire.s00000741
+  CONSUME merge.s00000742.activated:1;
+  PRODUCE callToTask.s00000748.input.s00000699:1, callToTask.s00000748.input.s00000709:1;
+
+TRANSITION process.s00000021##s00000698.inputCriterion.s00000700
+  CONSUME alpha:1;
+  PRODUCE merge.s00000742.input.s00000709:1, process.s00000021##s00000698.input.s00000699:1;
+
+TRANSITION process.s00000021##s00000698.outputCriterion.s00000704
+  CONSUME callToTask.s00000745.output.s00000702:1, callToTask.s00000746.output.s00000703:1, process.s00000021##s00000698.output.s00000701:1;
+  PRODUCE process.s00000021##s00000698.outputCriterion.s00000704_omega:1;
+
+
+{ END OF FILE }

benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000021__s00000698.lola.fin.task

+EF ( DEADLOCK AND NOT (
+( callToTask.s00000745.output.s00000713 = 0
+AND alpha = 0
+AND merge.s00000742.input.s00000709 = 0
+AND callToTask.s00000743.inputCriterion.s00000700.used = 0
+AND merge.s00000742.activated = 0
+AND ( process.s00000021##s00000698.outputCriterion.s00000704_omega > 0
+OR endNode.s00000706.input.default > 0 )
+AND process.s00000021##s00000698.input.s00000699 = 0
+AND decision.s00000719.activated = 0
+AND callToTask.s00000745.input.s00000709 = 0
+AND callToTask.s00000745.output.s00000702 = 0
+AND callToTask.s00000745.output.s00000754 = 0
+AND callToTask.s00000744.inputCriterion.s00000700.used = 0
+AND callToTask.s00000744.input.s00000709 = 0
+AND callToTask.s00000744.output.s00000754 = 0
+AND callToTask.s00000743.input.s00000709 = 0
+AND callToTask.s00000743.output.s00000754 = 0
+AND callToTask.s00000748.inputCriterion.s00000700.used = 0
+AND callToTask.s00000745.input.s00000699 = 0
+AND callToTask.s00000744.output.s00000713 = 0
+AND callToTask.s00000744.input.s00000752 = 0
+AND callToTask.s00000743.output.s00000713 = 0
+AND callToTask.s00000743.input.s00000699 = 0
+AND merge.s00000742.input.s00000740 = 0
+AND decision.s00000707.activated = 0
+AND merge.s00000742.input.s00000737 = 0
+AND callToTask.s00000745.inputCriterion.s00000700.used = 0
+AND merge.s00000730.activated = 0
+AND callToTask.s00000748.output.s00000713 = 0
+AND callToTask.s00000748.input.s00000709 = 0
+AND callToTask.s00000748.output.s00000754 = 0
+AND callToTask.s00000748.input.s00000699 = 0
+AND callToTask.s00000747.output.s00000713 = 0
+AND callToTask.s00000747.inputCriterion.s00000700.used = 0
+AND callToTask.s00000747.input.s00000709 = 0
+AND callToTask.s00000747.output.s00000754 = 0
+AND callToTask.s00000747.input.s00000699 = 0
+AND callToTask.s00000746.output.s00000713 = 0
+AND callToTask.s00000746.inputCriterion.s00000700.used = 0
+AND callToTask.s00000746.input.s00000709 = 0
+AND callToTask.s00000746.output.s00000703 = 0
+AND callToTask.s00000746.output.s00000754 = 0
+AND process.s00000021##s00000698.output.s00000701 = 0
+AND callToTask.s00000746.input.s00000699 = 0 )
+
+
+))

benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000021__s00000698.lola.safe.task

+EF (
+( callToTask.s00000748.input.s00000699 > 1
+OR callToTask.s00000743.input.s00000699 > 1
+OR callToTask.s00000746.input.s00000709 > 1
+OR callToTask.s00000746.input.s00000699 > 1
+OR callToTask.s00000745.input.s00000709 > 1
+OR callToTask.s00000744.output.s00000713 > 1
+OR callToTask.s00000744.output.s00000754 > 1
+OR callToTask.s00000745.inputCriterion.s00000700.used > 1
+OR callToTask.s00000745.output.s00000754 > 1
+OR callToTask.s00000747.output.s00000754 > 1
+OR callToTask.s00000746.inputCriterion.s00000700.used > 1
+OR callToTask.s00000748.output.s00000754 > 1
+OR callToTask.s00000746.output.s00000703 > 1
+OR callToTask.s00000747.output.s00000713 > 1
+OR callToTask.s00000748.output.s00000713 > 1
+OR callToTask.s00000747.input.s00000699 > 1
+OR callToTask.s00000745.input.s00000699 > 1
+OR callToTask.s00000744.input.s00000709 > 1
+OR callToTask.s00000744.input.s00000752 > 1
+OR callToTask.s00000743.inputCriterion.s00000700.used > 1
+OR merge.s00000742.activated > 1
+OR decision.s00000719.activated > 1
+OR merge.s00000730.activated > 1
+OR merge.s00000742.input.s00000740 > 1
+OR merge.s00000742.input.s00000737 > 1
+OR decision.s00000707.activated > 1
+OR merge.s00000742.activated > 1
+OR callToTask.s00000743.output.s00000754 > 1
+OR callToTask.s00000744.inputCriterion.s00000700.used > 1
+OR merge.s00000730.activated > 1
+OR callToTask.s00000747.input.s00000709 > 1
+OR merge.s00000730.activated > 1
+OR callToTask.s00000748.inputCriterion.s00000700.used > 1
+OR callToTask.s00000746.output.s00000713 > 1
+OR callToTask.s00000746.output.s00000754 > 1
+OR callToTask.s00000743.output.s00000713 > 1
+OR callToTask.s00000745.output.s00000702 > 1
+OR callToTask.s00000747.inputCriterion.s00000700.used > 1
+OR callToTask.s00000745.output.s00000713 > 1
+OR callToTask.s00000748.input.s00000709 > 1
+OR callToTask.s00000743.input.s00000709 > 1
+OR merge.s00000730.activated > 1
+OR merge.s00000730.activated > 1 )
+
+
+)

benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000023__s00000777.lola

+{ Petri net created by UML2oWFN 2.11 }
+
+PLACE
+  alpha, callToTask.s00000747.input.s00000699, callToTask.s00000747.input.s00000709, callToTask.s00000747.inputCriterion.s00000700.used, callToTask.s00000747.output.s00000713, callToTask.s00000747.output.s00000754, callToTask.s00000748.input.s00000699, callToTask.s00000748.input.s00000709, callToTask.s00000748.inputCriterion.s00000700.used, callToTask.s00000748.output.s00000713, callToTask.s00000748.output.s00000754, callToTask.s00000815.input.s00000709, callToTask.s00000815.input.s00000844, callToTask.s00000815.inputCriterion.s00000700.used, callToTask.s00000815.output.s00000713, callToTask.s00000815.output.s00000754, callToTask.s00000815.output.s00000840, callToTask.s00000816.input.s00000709, callToTask.s00000816.input.s00000778, callToTask.s00000816.inputCriterion.s00000700.used, callToTask.s00000816.output.s00000713, callToTask.s00000816.output.s00000824, callToTask.s00000817.input.s00000709, callToTask.s00000817.input.s00000778, callToTask.s00000817.inputCriterion.s00000700.used, callToTask.s00000817.output.s00000713, callToTask.s00000817.output.s00000824, callToTask.s00000818.input.s00000699, callToTask.s00000818.input.s00000709, callToTask.s00000818.inputCriterion.s00000700.used, callToTask.s00000818.output.s00000713, callToTask.s00000818.output.s00000780, callToTask.s00000818.output.s00000827, callToTask.s00000819.input.s00000709, callToTask.s00000819.input.s00000778, callToTask.s00000819.inputCriterion.s00000700.used, callToTask.s00000819.output.s00000713, callToTask.s00000819.output.s00000824, callToTask.s00000820.input.s00000709, callToTask.s00000820.input.s00000778, callToTask.s00000820.inputCriterion.s00000700.used, callToTask.s00000820.output.s00000713, callToTask.s00000820.output.s00000824, callToTask.s00000821.input.s00000699, callToTask.s00000821.input.s00000709, callToTask.s00000821.inputCriterion.s00000700.used, callToTask.s00000821.output.s00000713, callToTask.s00000821.output.s00000781, callToTask.s00000821.output.s00000827, callToTask.s00000822.input.s00000699, callToTask.s00000822.input.s00000709, callToTask.s00000822.inputCriterion.s00000700.used, callToTask.s00000822.output.s00000713, callToTask.s00000822.output.s00000754, decision.s00000707.activated, decision.s00000782.activated, endNode.s00000706.input.default, merge.s00000730.activated, merge.s00000742.activated, merge.s00000742.input.s00000709, merge.s00000742.input.s00000710, merge.s00000742.input.s00000740, process.s00000023##s00000777.input.s00000778, process.s00000023##s00000777.output.s00000754, process.s00000023##s00000777.outputCriterion.s00000704_omega;
+
+MARKING
+  alpha:1;
+
+
+TRANSITION callToTask.s00000747.inputCriterion.s00000700
+  CONSUME callToTask.s00000747.input.s00000699:1, callToTask.s00000747.input.s00000709:1;
+  PRODUCE callToTask.s00000747.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000747.outputCriterion.s00000704
+  CONSUME callToTask.s00000747.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000747.output.s00000713:1, callToTask.s00000747.output.s00000754:1;
+
+TRANSITION callToTask.s00000748.inputCriterion.s00000700
+  CONSUME callToTask.s00000748.input.s00000699:1, callToTask.s00000748.input.s00000709:1;
+  PRODUCE callToTask.s00000748.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000748.outputCriterion.s00000704
+  CONSUME callToTask.s00000748.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000748.output.s00000713:1, callToTask.s00000748.output.s00000754:1;
+
+TRANSITION callToTask.s00000815.inputCriterion.s00000700
+  CONSUME callToTask.s00000815.input.s00000709:1, callToTask.s00000815.input.s00000844:1;
+  PRODUCE callToTask.s00000815.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000815.outputCriterion.s00000704
+  CONSUME callToTask.s00000815.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000815.output.s00000713:1, callToTask.s00000815.output.s00000754:1, callToTask.s00000815.output.s00000840:1;
+
+TRANSITION callToTask.s00000816.inputCriterion.s00000700
+  CONSUME callToTask.s00000816.input.s00000709:1, callToTask.s00000816.input.s00000778:1;
+  PRODUCE callToTask.s00000816.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000816.outputCriterion.s00000704
+  CONSUME callToTask.s00000816.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000816.output.s00000713:1, callToTask.s00000816.output.s00000824:1;
+
+TRANSITION callToTask.s00000817.inputCriterion.s00000700
+  CONSUME callToTask.s00000817.input.s00000709:1, callToTask.s00000817.input.s00000778:1;
+  PRODUCE callToTask.s00000817.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000817.outputCriterion.s00000704
+  CONSUME callToTask.s00000817.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000817.output.s00000713:1, callToTask.s00000817.output.s00000824:1;
+
+TRANSITION callToTask.s00000818.inputCriterion.s00000700
+  CONSUME callToTask.s00000818.input.s00000699:1, callToTask.s00000818.input.s00000709:1;
+  PRODUCE callToTask.s00000818.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000818.outputCriterion.s00000704
+  CONSUME callToTask.s00000818.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000818.output.s00000713:1, callToTask.s00000818.output.s00000780:1, callToTask.s00000818.output.s00000827:1;
+
+TRANSITION callToTask.s00000819.inputCriterion.s00000700
+  CONSUME callToTask.s00000819.input.s00000709:1, callToTask.s00000819.input.s00000778:1;
+  PRODUCE callToTask.s00000819.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000819.outputCriterion.s00000704
+  CONSUME callToTask.s00000819.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000819.output.s00000713:1, callToTask.s00000819.output.s00000824:1;
+
+TRANSITION callToTask.s00000820.inputCriterion.s00000700
+  CONSUME callToTask.s00000820.input.s00000709:1, callToTask.s00000820.input.s00000778:1;
+  PRODUCE callToTask.s00000820.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000820.outputCriterion.s00000704
+  CONSUME callToTask.s00000820.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000820.output.s00000713:1, callToTask.s00000820.output.s00000824:1;
+
+TRANSITION callToTask.s00000821.inputCriterion.s00000700
+  CONSUME callToTask.s00000821.input.s00000699:1, callToTask.s00000821.input.s00000709:1;
+  PRODUCE callToTask.s00000821.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000821.outputCriterion.s00000704
+  CONSUME callToTask.s00000821.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000821.output.s00000713:1, callToTask.s00000821.output.s00000781:1, callToTask.s00000821.output.s00000827:1;
+
+TRANSITION callToTask.s00000822.inputCriterion.s00000700
+  CONSUME callToTask.s00000822.input.s00000699:1, callToTask.s00000822.input.s00000709:1;
+  PRODUCE callToTask.s00000822.inputCriterion.s00000700.used:1;
+
+TRANSITION callToTask.s00000822.outputCriterion.s00000704
+  CONSUME callToTask.s00000822.inputCriterion.s00000700.used:1;
+  PRODUCE callToTask.s00000822.output.s00000713:1, callToTask.s00000822.output.s00000754:1;
+
+TRANSITION decision.s00000707.activate.s00000708
+  CONSUME callToTask.s00000747.output.s00000713:1, callToTask.s00000747.output.s00000754:1;
+  PRODUCE decision.s00000707.activated:1;
+
+TRANSITION decision.s00000707.fire.s00000711
+  CONSUME decision.s00000707.activated:1;
+  PRODUCE endNode.s00000706.input.default:1, process.s00000023##s00000777.output.s00000754:1;
+
+TRANSITION decision.s00000707.fire.s00000715
+  CONSUME decision.s00000707.activated:1;
+  PRODUCE merge.s00000742.input.s00000710:1, merge.s00000742.input.s00000740:1;
+
+TRANSITION decision.s00000782.activate.s00000708
+  CONSUME callToTask.s00000748.output.s00000713:1, callToTask.s00000748.output.s00000754:1;
+  PRODUCE decision.s00000782.activated:1;
+
+TRANSITION decision.s00000782.fire.s00000711
+  CONSUME decision.s00000782.activated:1;
+  PRODUCE callToTask.s00000816.input.s00000709:1, callToTask.s00000816.input.s00000778:1;
+
+TRANSITION decision.s00000782.fire.s00000715
+  CONSUME decision.s00000782.activated:1;
+  PRODUCE callToTask.s00000817.input.s00000709:1, callToTask.s00000817.input.s00000778:1;
+
+TRANSITION decision.s00000782.fire.s00000724
+  CONSUME decision.s00000782.activated:1;
+  PRODUCE callToTask.s00000815.input.s00000709:1, callToTask.s00000815.input.s00000844:1;
+
+TRANSITION decision.s00000782.fire.s00000727
+  CONSUME decision.s00000782.activated:1;
+  PRODUCE callToTask.s00000818.input.s00000699:1, callToTask.s00000818.input.s00000709:1;
+
+TRANSITION decision.s00000782.fire.s00000790
+  CONSUME decision.s00000782.activated:1;
+  PRODUCE callToTask.s00000819.input.s00000709:1, callToTask.s00000819.input.s00000778:1;
+
+TRANSITION decision.s00000782.fire.s00000793
+  CONSUME decision.s00000782.activated:1;
+  PRODUCE callToTask.s00000820.input.s00000709:1, callToTask.s00000820.input.s00000778:1;
+
+TRANSITION decision.s00000782.fire.s00000796
+  CONSUME decision.s00000782.activated:1;
+  PRODUCE callToTask.s00000821.input.s00000699:1, callToTask.s00000821.input.s00000709:1;
+
+TRANSITION decision.s00000782.fire.s00000799
+  CONSUME decision.s00000782.activated:1;
+  PRODUCE callToTask.s00000822.input.s00000699:1, callToTask.s00000822.input.s00000709:1;
+
+TRANSITION merge.s00000730.activate.s00000731
+  CONSUME callToTask.s00000816.output.s00000713:1, callToTask.s00000816.output.s00000824:1;
+  PRODUCE merge.s00000730.activated:1;
+
+TRANSITION merge.s00000730.activate.s00000733
+  CONSUME callToTask.s00000817.output.s00000713:1, callToTask.s00000817.output.s00000824:1;
+  PRODUCE merge.s00000730.activated:1;
+
+TRANSITION merge.s00000730.activate.s00000735
+  CONSUME callToTask.s00000815.output.s00000713:1, callToTask.s00000815.output.s00000754:1;
+  PRODUCE merge.s00000730.activated:1;
+
+TRANSITION merge.s00000730.activate.s00000738
+  CONSUME callToTask.s00000818.output.s00000713:1, callToTask.s00000818.output.s00000827:1;
+  PRODUCE merge.s00000730.activated:1;
+
+TRANSITION merge.s00000730.activate.s00000806
+  CONSUME callToTask.s00000819.output.s00000713:1, callToTask.s00000819.output.s00000824:1;
+  PRODUCE merge.s00000730.activated:1;
+
+TRANSITION merge.s00000730.activate.s00000808
+  CONSUME callToTask.s00000820.output.s00000713:1, callToTask.s00000820.output.s00000824:1;
+  PRODUCE merge.s00000730.activated:1;
+
+TRANSITION merge.s00000730.activate.s00000810
+  CONSUME callToTask.s00000821.output.s00000713:1, callToTask.s00000821.output.s00000827:1;
+  PRODUCE merge.s00000730.activated:1;
+
+TRANSITION merge.s00000730.activate.s00000812
+  CONSUME callToTask.s00000822.output.s00000713:1, callToTask.s00000822.output.s00000754:1;
+  PRODUCE merge.s00000730.activated:1;
+
+TRANSITION merge.s00000730.fire.s00000741
+  CONSUME merge.s00000730.activated:1;
+  PRODUCE callToTask.s00000747.input.s00000699:1, callToTask.s00000747.input.s00000709:1;
+
+TRANSITION merge.s00000742.activate.s00000731
+  CONSUME merge.s00000742.input.s00000709:1, process.s00000023##s00000777.input.s00000778:1;
+  PRODUCE merge.s00000742.activated:1;
+
+TRANSITION merge.s00000742.activate.s00000733
+  CONSUME merge.s00000742.input.s00000710:1, merge.s00000742.input.s00000740:1;
+  PRODUCE merge.s00000742.activated:1;
+
+TRANSITION merge.s00000742.fire.s00000741
+  CONSUME merge.s00000742.activated:1;
+  PRODUCE callToTask.s00000748.input.s00000699:1, callToTask.s00000748.input.s00000709:1;
+
+TRANSITION process.s00000023##s00000777.inputCriterion.s00000700
+  CONSUME alpha:1;
+  PRODUCE merge.s00000742.input.s00000709:1, process.s00000023##s00000777.input.s00000778:1;
+
+TRANSITION process.s00000023##s00000777.outputCriterion.s00000704
+  CONSUME callToTask.s00000815.output.s00000840:1, callToTask.s00000818.output.s00000780:1, callToTask.s00000821.output.s00000781:1, process.s00000023##s00000777.output.s00000754:1;
+  PRODUCE process.s00000023##s00000777.outputCriterion.s00000704_omega:1;
+
+
+{ END OF FILE }

benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000023__s00000777.lola.fin.task

+EF ( DEADLOCK AND NOT (
+( decision.s00000782.activated = 0
+AND process.s00000023##s00000777.input.s00000778 = 0
+AND ( endNode.s00000706.input.default > 0
+OR process.s00000023##s00000777.outp