Commit db099581 authored by Philipp Meyer's avatar Philipp Meyer

Added results for termination on sap benchmarks

parent fcfb3082

Too many changes to show.

To preserve performance only 1000 of 1000+ files are displayed.
......@@ -18,7 +18,8 @@ results_other_tool=( positive negative error timeout )
our_tool=slapnet
benchmark_dirs=( 'ibm-soundness' ) # 'sap-reference' )
#benchmark_dirs=( 'ibm-soundness' )
benchmark_dirs=( 'sap-reference' )
benchmark_tools=( 'sara' )
for (( benchmark=0;benchmark<${#benchmark_dirs[@]};benchmark++)); do
benchmark_dir=${benchmark_dirs[$benchmark]}
......
#!/bin/bash
#benchmarks=( 'ibm-soundness' 'sap-reference' )
#benchmarks=( 'sap-reference' )
benchmarks=( 'ibm-soundness' )
benchmarks=( 'sap-reference' )
#benchmarks=( 'ibm-soundness' )
extensions=( 'pnet' 'tpn' 'lola' )
executable='/home/philipp/local/lola-2.0/src/lola'
......
#!/bin/bash
#benchmarks=( 'ibm-soundness' 'sap-reference' )
#benchmarks=( 'sap-reference' )
benchmarks=( 'ibm-soundness' )
benchmarks=( 'sap-reference' )
#benchmarks=( 'ibm-soundness' )
extensions=( 'pnet' 'tpn' 'lola' )
executable='/home/philipp/local/sara-1.0/src/sara'
......@@ -18,6 +18,7 @@ for benchmark in ${benchmarks[@]}; do
pushd .
cd $(dirname $file)
base=$(basename $file)
echo "testing $file with $base"
(
set -o pipefail;
timeout 60 $executable -i $base.terminating.sara 2>&1 | tee $base.out
......
#!/bin/bash
#benchmarks=( 'ibm-soundness' 'sap-reference' )
#benchmarks=( 'sap-reference' )
benchmarks=( 'ibm-soundness' )
benchmarks=( 'sap-reference' )
#benchmarks=( 'ibm-soundness' )
extensions=( 'pnet' 'tpn' 'lola' )
executable='../../slapnet'
......@@ -17,7 +17,7 @@ for benchmark in ${benchmarks[@]}; do
T="$(date +%s%N)"
(
set -o pipefail;
timeout 60 $executable --$ext --termination-by-reachability $file -o $file.terminating | tee $file.out
timeout 60 $executable --$ext --validate-identifiers --termination-by-reachability -o $file.terminating $file | tee $file.out
)
result=$?
T=$(($(date +%s%N)-T))
......
PROBLEM termination_by_reachability:
GOAL REACHABILITY;
FILE Model.18wm__0_____u__.xml.tpn.terminating TYPE LOLA;
INITIAL 'i:1,'m1:1,i:1;
FINAL COVER;
CONSTRAINTS 'sigma>1,'i+-1i>0,'o+-1o>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___InputCondition+-1p_Model_18wm__0_____u___Model_18wm__0_____u___InputCondition>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Split_and__18yh_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Split_and__18yh_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Join_and__18yh_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Join_and__18yh_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Split_xor__18x0_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Split_xor__18x0_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Join_xor__18x0_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Join_xor__18x0_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___outputCondition+-1p_Model_18wm__0_____u___Model_18wm__0_____u___outputCondition>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__and__18yh_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__and__18yh_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Find_Object__18xe_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Find_Object__18xe_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Material_Search__18xs_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Material_Search__18xs_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Document_Search__18y6_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Document_Search__18y6_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__and__18ys_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__and__18ys_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__xor__18x0_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__xor__18x0_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__Join_Yes_xor__18x0_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__Join_Yes_xor__18x0_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__and__18ys_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__and__18ys_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__and__18ys_+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__and__18ys_>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Split_busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Split_busy>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__busy>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__busy>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Skip_busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Skip_busy>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__busy>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__busy>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__busy>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__busy>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__busy>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__busy>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Join_No_xor__18x0__busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Join_No_xor__18x0__busy>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Yes_xor__18x0__busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Yes_xor__18x0__busy>0,'p_Model_18wm__0_____u___Model_18wm__0_____u___Output_busy+-1p_Model_18wm__0_____u___Model_18wm__0_____u___Output_busy>0;
EF ('sigma >= 1 AND ('i - i) >= 0 AND ('o - o) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___InputCondition - p_Model_18wm__0_____u___Model_18wm__0_____u___InputCondition) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Split_and__18yh_ - p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Split_and__18yh_) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Join_and__18yh_ - p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Join_and__18yh_) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Split_xor__18x0_ - p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Split_xor__18x0_) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Join_xor__18x0_ - p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Join_xor__18x0_) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___outputCondition - p_Model_18wm__0_____u___Model_18wm__0_____u___outputCondition) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__and__18yh_ - p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__and__18yh_) >= 0 AND ('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__Find_Object__18xe_) >= 0 AND ('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__Material_Search__18xs_) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Document_Search__18y6_ - p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Document_Search__18y6_) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__and__18ys_ - p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__and__18ys_) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__xor__18x0_ - p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__xor__18x0_) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__Join_Yes_xor__18x0_ - p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__Join_Yes_xor__18x0_) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__and__18ys_ - p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__and__18ys_) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__and__18ys_ - p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__and__18ys_) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Split_busy - p_Model_18wm__0_____u___Model_18wm__0_____u___Split_busy) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__busy - p_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__busy) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__busy - p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__busy) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Skip_busy - p_Model_18wm__0_____u___Model_18wm__0_____u___Skip_busy) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__busy - p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__busy) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__busy - p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__busy) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__busy - p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__busy) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__busy - p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__busy) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__busy - p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__busy) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__busy - p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__busy) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Join_No_xor__18x0__busy - p_Model_18wm__0_____u___Model_18wm__0_____u___Join_No_xor__18x0__busy) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Yes_xor__18x0__busy - p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Yes_xor__18x0__busy) >= 0 AND ('p_Model_18wm__0_____u___Model_18wm__0_____u___Output_busy - p_Model_18wm__0_____u___Model_18wm__0_____u___Output_busy) >= 0)
PROBLEM termination_by_reachability:
GOAL REACHABILITY;
FILE Model.19op__0_____u__.xml.tpn.terminating TYPE LOLA;
INITIAL 'i:1,'m1:1,i:1;
FINAL COVER;
CONSTRAINTS 'sigma>1,'i+-1i>0,'o+-1o>0,'p_Model_19op__0_____u___Model_19op__0_____u___InputCondition+-1p_Model_19op__0_____u___Model_19op__0_____u___InputCondition>0,'p_Model_19op__0_____u___Model_19op__0_____u___Split_Split_Product_Design__19pa_+-1p_Model_19op__0_____u___Model_19op__0_____u___Split_Split_Product_Design__19pa_>0,'p_Model_19op__0_____u___Model_19op__0_____u___Split_Join_Product_Design__19pa_+-1p_Model_19op__0_____u___Model_19op__0_____u___Split_Join_Product_Design__19pa_>0,'p_Model_19op__0_____u___Model_19op__0_____u___Join_Split_xor__19qz_+-1p_Model_19op__0_____u___Model_19op__0_____u___Join_Split_xor__19qz_>0,'p_Model_19op__0_____u___Model_19op__0_____u___Join_Join_xor__19qz_+-1p_Model_19op__0_____u___Model_19op__0_____u___Join_Join_xor__19qz_>0,'p_Model_19op__0_____u___Model_19op__0_____u___outputCondition+-1p_Model_19op__0_____u___Model_19op__0_____u___outputCondition>0,'p_Model_19op__0_____u___Model_19op__0_____u___Split_Yes_Product_Design__19pa__Product_Design__19pa_+-1p_Model_19op__0_____u___Model_19op__0_____u___Split_Yes_Product_Design__19pa__Product_Design__19pa_>0,'p_Model_19op__0_____u___Model_19op__0_____u___Product_Design__19pa__and__19qo_+-1p_Model_19op__0_____u___Model_19op__0_____u___Product_Design__19pa__and__19qo_>0,'p_Model_19op__0_____u___Model_19op__0_____u___and__19qo__Design_BOM___Material_Master_Processing__19po_+-1p_Model_19op__0_____u___Model_19op__0_____u___and__19qo__Design_BOM___Material_Master_Processing__19po_>0,'p_Model_19op__0_____u___Model_19op__0_____u___and__19qo__Design_BOM___Material_BOM_Processing__19q2_+-1p_Model_19op__0_____u___Model_19op__0_____u___and__19qo__Design_BOM___Material_BOM_Processing__19q2_>0,'p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_Master_Processing__19po__and__19r6_+-1p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_Master_Processing__19po__and__19r6_>0,'p_Model_19op__0_____u___Model_19op__0_____u___and__19r6__xor__19qz_+-1p_Model_19op__0_____u___Model_19op__0_____u___and__19r6__xor__19qz_>0,'p_Model_19op__0_____u___Model_19op__0_____u___xor__19qz__Join_Yes_xor__19qz_+-1p_Model_19op__0_____u___Model_19op__0_____u___xor__19qz__Join_Yes_xor__19qz_>0,'p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_BOM_Processing__19q2__and__19r6_+-1p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_BOM_Processing__19q2__and__19r6_>0,'p_Model_19op__0_____u___Model_19op__0_____u___Split_busy+-1p_Model_19op__0_____u___Model_19op__0_____u___Split_busy>0,'p_Model_19op__0_____u___Model_19op__0_____u___Split_No_Product_Design__19pa__busy+-1p_Model_19op__0_____u___Model_19op__0_____u___Split_No_Product_Design__19pa__busy>0,'p_Model_19op__0_____u___Model_19op__0_____u___Split_Yes_Product_Design__19pa__busy+-1p_Model_19op__0_____u___Model_19op__0_____u___Split_Yes_Product_Design__19pa__busy>0,'p_Model_19op__0_____u___Model_19op__0_____u___Skip_busy+-1p_Model_19op__0_____u___Model_19op__0_____u___Skip_busy>0,'p_Model_19op__0_____u___Model_19op__0_____u___Product_Design__19pa__busy+-1p_Model_19op__0_____u___Model_19op__0_____u___Product_Design__19pa__busy>0,'p_Model_19op__0_____u___Model_19op__0_____u___and__19qo__busy+-1p_Model_19op__0_____u___Model_19op__0_____u___and__19qo__busy>0,'p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_Master_Processing__19po__busy+-1p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_Master_Processing__19po__busy>0,'p_Model_19op__0_____u___Model_19op__0_____u___and__19r6__busy+-1p_Model_19op__0_____u___Model_19op__0_____u___and__19r6__busy>0,'p_Model_19op__0_____u___Model_19op__0_____u___xor__19qz__busy+-1p_Model_19op__0_____u___Model_19op__0_____u___xor__19qz__busy>0,'p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_BOM_Processing__19q2__busy+-1p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_BOM_Processing__19q2__busy>0,'p_Model_19op__0_____u___Model_19op__0_____u___Join_No_xor__19qz__busy+-1p_Model_19op__0_____u___Model_19op__0_____u___Join_No_xor__19qz__busy>0,'p_Model_19op__0_____u___Model_19op__0_____u___Join_Yes_xor__19qz__busy+-1p_Model_19op__0_____u___Model_19op__0_____u___Join_Yes_xor__19qz__busy>0,'p_Model_19op__0_____u___Model_19op__0_____u___Output_busy+-1p_Model_19op__0_____u___Model_19op__0_____u___Output_busy>0;
EF ('sigma >= 1 AND ('i - i) >= 0 AND ('o - o) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___InputCondition - p_Model_19op__0_____u___Model_19op__0_____u___InputCondition) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Split_Split_Product_Design__19pa_ - p_Model_19op__0_____u___Model_19op__0_____u___Split_Split_Product_Design__19pa_) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Split_Join_Product_Design__19pa_ - p_Model_19op__0_____u___Model_19op__0_____u___Split_Join_Product_Design__19pa_) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Join_Split_xor__19qz_ - p_Model_19op__0_____u___Model_19op__0_____u___Join_Split_xor__19qz_) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Join_Join_xor__19qz_ - p_Model_19op__0_____u___Model_19op__0_____u___Join_Join_xor__19qz_) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___outputCondition - p_Model_19op__0_____u___Model_19op__0_____u___outputCondition) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Split_Yes_Product_Design__19pa__Product_Design__19pa_ - p_Model_19op__0_____u___Model_19op__0_____u___Split_Yes_Product_Design__19pa__Product_Design__19pa_) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Product_Design__19pa__and__19qo_ - p_Model_19op__0_____u___Model_19op__0_____u___Product_Design__19pa__and__19qo_) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___and__19qo__Design_BOM___Material_Master_Processing__19po_ - p_Model_19op__0_____u___Model_19op__0_____u___and__19qo__Design_BOM___Material_Master_Processing__19po_) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___and__19qo__Design_BOM___Material_BOM_Processing__19q2_ - p_Model_19op__0_____u___Model_19op__0_____u___and__19qo__Design_BOM___Material_BOM_Processing__19q2_) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_Master_Processing__19po__and__19r6_ - p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_Master_Processing__19po__and__19r6_) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___and__19r6__xor__19qz_ - p_Model_19op__0_____u___Model_19op__0_____u___and__19r6__xor__19qz_) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___xor__19qz__Join_Yes_xor__19qz_ - p_Model_19op__0_____u___Model_19op__0_____u___xor__19qz__Join_Yes_xor__19qz_) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_BOM_Processing__19q2__and__19r6_ - p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_BOM_Processing__19q2__and__19r6_) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Split_busy - p_Model_19op__0_____u___Model_19op__0_____u___Split_busy) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Split_No_Product_Design__19pa__busy - p_Model_19op__0_____u___Model_19op__0_____u___Split_No_Product_Design__19pa__busy) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Split_Yes_Product_Design__19pa__busy - p_Model_19op__0_____u___Model_19op__0_____u___Split_Yes_Product_Design__19pa__busy) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Skip_busy - p_Model_19op__0_____u___Model_19op__0_____u___Skip_busy) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Product_Design__19pa__busy - p_Model_19op__0_____u___Model_19op__0_____u___Product_Design__19pa__busy) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___and__19qo__busy - p_Model_19op__0_____u___Model_19op__0_____u___and__19qo__busy) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_Master_Processing__19po__busy - p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_Master_Processing__19po__busy) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___and__19r6__busy - p_Model_19op__0_____u___Model_19op__0_____u___and__19r6__busy) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___xor__19qz__busy - p_Model_19op__0_____u___Model_19op__0_____u___xor__19qz__busy) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_BOM_Processing__19q2__busy - p_Model_19op__0_____u___Model_19op__0_____u___Design_BOM___Material_BOM_Processing__19q2__busy) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Join_No_xor__19qz__busy - p_Model_19op__0_____u___Model_19op__0_____u___Join_No_xor__19qz__busy) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Join_Yes_xor__19qz__busy - p_Model_19op__0_____u___Model_19op__0_____u___Join_Yes_xor__19qz__busy) >= 0 AND ('p_Model_19op__0_____u___Model_19op__0_____u___Output_busy - p_Model_19op__0_____u___Model_19op__0_____u___Output_busy) >= 0)
PROBLEM termination_by_reachability:
GOAL REACHABILITY;
FILE Model.1bt1__0_____u__.xml.tpn.terminating TYPE LOLA;
INITIAL 'i:1,'m1:1,i:1;
FINAL COVER;
CONSTRAINTS 'sigma>1,'i+-1i>0,'o+-1o>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___InputCondition+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___InputCondition>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Split_and__1bxi_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Split_and__1bxi_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Join_and__1bxi_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Join_and__1bxi_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Split_and__1bxp_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Split_and__1bxp_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Join_and__1bxp_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Join_and__1bxp_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Split_Sales_and_Operations_Planning__1byz_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Split_Sales_and_Operations_Planning__1byz_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Join_Sales_and_Operations_Planning__1byz_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Join_Sales_and_Operations_Planning__1byz_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Split_or__1bye_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Split_or__1bye_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Join_or__1bye_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Join_or__1bye_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Split_Material_Requirements_Planning__1bx4_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Split_Material_Requirements_Planning__1bx4_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Join_Material_Requirements_Planning__1bx4_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Join_Material_Requirements_Planning__1bx4_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Split_Long_Term_Planning__1bvu_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Split_Long_Term_Planning__1bvu_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Join_Long_Term_Planning__1bvu_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Join_Long_Term_Planning__1bvu_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___OutputCondition+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___OutputCondition>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Yes_and__1bxi__and__1bxi_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Yes_and__1bxi__and__1bxi_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Yes_and__1bxp__and__1bxp_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Yes_and__1bxp__and__1bxp_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Yes_Sales_and_Operations_Planning__1byz__Sales_and_Operations_Planning__1byz_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Yes_Sales_and_Operations_Planning__1byz__Sales_and_Operations_Planning__1byz_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxi__Master_Production_Scheduling__1bzd_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxi__Master_Production_Scheduling__1bzd_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Master_Production_Scheduling__1bzd__or__1bye_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Master_Production_Scheduling__1bzd__or__1bye_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bye__Join_Yes_or__1bye_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bye__Join_Yes_or__1bye_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bye__or__1byl_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bye__or__1byl_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1byl__Material_Requirements_Planning__1bx4_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1byl__Material_Requirements_Planning__1bx4_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Material_Requirements_Planning__1bx4__Join_Yes_Material_Requirements_Planning__1bx4_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Material_Requirements_Planning__1bx4__Join_Yes_Material_Requirements_Planning__1bx4_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxp__Long_Term_Planning__1bvu_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxp__Long_Term_Planning__1bvu_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Long_Term_Planning__1bvu__Join_Yes_Long_Term_Planning__1bvu_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Long_Term_Planning__1bvu__Join_Yes_Long_Term_Planning__1bvu_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Sales_and_Operations_Planning__1byz__or__1bwq_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Sales_and_Operations_Planning__1byz__or__1bwq_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bwq__or__1bxb_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bwq__or__1bxb_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bxb__Demand_Management__1btx_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bxb__Demand_Management__1btx_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Demand_Management__1btx__and__1bxw_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Demand_Management__1btx__and__1bxw_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxw__and__1bxi_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxw__and__1bxi_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxw__and__1bxp_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxw__and__1bxp_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxw__or__1byl_+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxw__or__1byl_>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_No_and__1bxi__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_No_and__1bxi__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Yes_and__1bxi__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Yes_and__1bxi__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_No_and__1bxp__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_No_and__1bxp__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Yes_and__1bxp__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Yes_and__1bxp__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_No_Sales_and_Operations_Planning__1byz__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_No_Sales_and_Operations_Planning__1byz__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Yes_Sales_and_Operations_Planning__1byz__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Yes_Sales_and_Operations_Planning__1byz__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Skip_busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Skip_busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxi__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxi__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Master_Production_Scheduling__1bzd__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Master_Production_Scheduling__1bzd__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bye__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bye__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1byl__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1byl__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Material_Requirements_Planning__1bx4__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Material_Requirements_Planning__1bx4__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxp__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxp__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Long_Term_Planning__1bvu__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Long_Term_Planning__1bvu__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Sales_and_Operations_Planning__1byz__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Sales_and_Operations_Planning__1byz__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bwq__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bwq__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bxb__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___or__1bxb__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Demand_Management__1btx__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Demand_Management__1btx__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxw__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___and__1bxw__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_No_or__1bye__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_No_or__1bye__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Yes_or__1bye__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Yes_or__1bye__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_No_Material_Requirements_Planning__1bx4__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_No_Material_Requirements_Planning__1bx4__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Yes_Material_Requirements_Planning__1bx4__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Yes_Material_Requirements_Planning__1bx4__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_No_Long_Term_Planning__1bvu__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_No_Long_Term_Planning__1bvu__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Yes_Long_Term_Planning__1bvu__busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Yes_Long_Term_Planning__1bvu__busy>0,'p_Model_1bt1__0_____u___Model_1bt1__0_____u___Output_busy+-1p_Model_1bt1__0_____u___Model_1bt1__0_____u___Output_busy>0;
EF ('sigma >= 1 AND ('i - i) >= 0 AND ('o - o) >= 0 AND ('p_Model_1bt1__0_____u___Model_1bt1__0_____u___InputCondition - p_Model_1bt1__0_____u___Model_1bt1__0_____u___InputCondition) >= 0 AND ('p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Split_and__1bxi_ - p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Split_and__1bxi_) >= 0 AND ('p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Join_and__1bxi_ - p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Join_and__1bxi_) >= 0 AND ('p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Split_and__1bxp_ - p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Split_and__1bxp_) >= 0 AND ('p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Join_and__1bxp_ - p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Join_and__1bxp_) >= 0 AND ('p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Split_Sales_and_Operations_Planning__1byz_ - p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Split_Sales_and_Operations_Planning__1byz_) >= 0 AND ('p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Join_Sales_and_Operations_Planning__1byz_ - p_Model_1bt1__0_____u___Model_1bt1__0_____u___Split_Join_Sales_and_Operations_Planning__1byz_) >= 0 AND ('p_Model_1bt1__0_____u___Model_1bt1__0_____u___Join_Split_or__1bye_ - p_Model_1bt1__0_____u___Model_1bt1__0____