Skip to content

GitLab

peregrine
peregrine
Commit fcfb3082 authored by Philipp Meyer's avatar Philipp Meyer
Browse files
Options

Ran sara on benchmarks for termination

parent a6f74eb6
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 4879 additions and 499 deletions

Too many changes to show.

To preserve performance only 1000 of 1000+ files are displayed.
Plain diff Email patch
benchmarks/service-tech/benchmarks-contingency.sh
View file @ fcfb3082
......@@ -19,7 +19,7 @@ results_other_tool=( positive negative error timeout )
our_tool=slapnet
benchmark_dirs=( 'ibm-soundness' ) # 'sap-reference' )
benchmark_tools=( 'lola' 'lola' )
benchmark_tools=( 'sara' )
for (( benchmark=0;benchmark<${#benchmark_dirs[@]};benchmark++)); do
benchmark_dir=${benchmark_dirs[$benchmark]}
other_tool=${benchmark_tools[$benchmark]}
......
benchmarks/service-tech/ibm-soundness/deadlock-free.negative 0 → 100644
View file @ fcfb3082
This diff is collapsed.
benchmarks/service-tech/ibm-soundness/deadlock-free.positive 0 → 100644
View file @ fcfb3082
This diff is collapsed.
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000021__s00000698.lola.terminating.sara 0 → 100644
View file @ fcfb3082
PROBLEM termination_by_reachability:
GOAL REACHABILITY;
FILE A.s00000021__s00000698.lola.terminating TYPE LOLA;
INITIAL 'alpha:1,'m1:1,alpha:1;
FINAL COVER;
CONSTRAINTS 'sigma>1,'alpha+-1alpha>0,'callToTask.s00000743.input.s00000699+-1callToTask.s00000743.input.s00000699>0,'callToTask.s00000743.input.s00000709+-1callToTask.s00000743.input.s00000709>0,'callToTask.s00000743.inputCriterion.s00000700.used+-1callToTask.s00000743.inputCriterion.s00000700.used>0,'callToTask.s00000743.output.s00000713+-1callToTask.s00000743.output.s00000713>0,'callToTask.s00000743.output.s00000754+-1callToTask.s00000743.output.s00000754>0,'callToTask.s00000744.input.s00000709+-1callToTask.s00000744.input.s00000709>0,'callToTask.s00000744.input.s00000752+-1callToTask.s00000744.input.s00000752>0,'callToTask.s00000744.inputCriterion.s00000700.used+-1callToTask.s00000744.inputCriterion.s00000700.used>0,'callToTask.s00000744.output.s00000713+-1callToTask.s00000744.output.s00000713>0,'callToTask.s00000744.output.s00000754+-1callToTask.s00000744.output.s00000754>0,'callToTask.s00000745.input.s00000699+-1callToTask.s00000745.input.s00000699>0,'callToTask.s00000745.input.s00000709+-1callToTask.s00000745.input.s00000709>0,'callToTask.s00000745.inputCriterion.s00000700.used+-1callToTask.s00000745.inputCriterion.s00000700.used>0,'callToTask.s00000745.output.s00000702+-1callToTask.s00000745.output.s00000702>0,'callToTask.s00000745.output.s00000713+-1callToTask.s00000745.output.s00000713>0,'callToTask.s00000745.output.s00000754+-1callToTask.s00000745.output.s00000754>0,'callToTask.s00000746.input.s00000699+-1callToTask.s00000746.input.s00000699>0,'callToTask.s00000746.input.s00000709+-1callToTask.s00000746.input.s00000709>0,'callToTask.s00000746.inputCriterion.s00000700.used+-1callToTask.s00000746.inputCriterion.s00000700.used>0,'callToTask.s00000746.output.s00000703+-1callToTask.s00000746.output.s00000703>0,'callToTask.s00000746.output.s00000713+-1callToTask.s00000746.output.s00000713>0,'callToTask.s00000746.output.s00000754+-1callToTask.s00000746.output.s00000754>0,'callToTask.s00000747.input.s00000699+-1callToTask.s00000747.input.s00000699>0,'callToTask.s00000747.input.s00000709+-1callToTask.s00000747.input.s00000709>0,'callToTask.s00000747.inputCriterion.s00000700.used+-1callToTask.s00000747.inputCriterion.s00000700.used>0,'callToTask.s00000747.output.s00000713+-1callToTask.s00000747.output.s00000713>0,'callToTask.s00000747.output.s00000754+-1callToTask.s00000747.output.s00000754>0,'callToTask.s00000748.input.s00000699+-1callToTask.s00000748.input.s00000699>0,'callToTask.s00000748.input.s00000709+-1callToTask.s00000748.input.s00000709>0,'callToTask.s00000748.inputCriterion.s00000700.used+-1callToTask.s00000748.inputCriterion.s00000700.used>0,'callToTask.s00000748.output.s00000713+-1callToTask.s00000748.output.s00000713>0,'callToTask.s00000748.output.s00000754+-1callToTask.s00000748.output.s00000754>0,'decision.s00000707.activated+-1decision.s00000707.activated>0,'decision.s00000719.activated+-1decision.s00000719.activated>0,'endNode.s00000706.input.default+-1endNode.s00000706.input.default>0,'merge.s00000730.activated+-1merge.s00000730.activated>0,'merge.s00000742.activated+-1merge.s00000742.activated>0,'merge.s00000742.input.s00000709+-1merge.s00000742.input.s00000709>0,'merge.s00000742.input.s00000737+-1merge.s00000742.input.s00000737>0,'merge.s00000742.input.s00000740+-1merge.s00000742.input.s00000740>0,'process.s00000021##s00000698.input.s00000699+-1process.s00000021##s00000698.input.s00000699>0,'process.s00000021##s00000698.output.s00000701+-1process.s00000021##s00000698.output.s00000701>0,'process.s00000021##s00000698.outputCriterion.s00000704_omega+-1process.s00000021##s00000698.outputCriterion.s00000704_omega>0;
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000021__s00000698.lola.terminating.task1
View file @ fcfb3082
EF ('sigma >= 1 AND 'alpha >= alpha AND 'callToTask.s00000743.input.s00000699 >= callToTask.s00000743.input.s00000699 AND 'callToTask.s00000743.input.s00000709 >= callToTask.s00000743.input.s00000709 AND 'callToTask.s00000743.inputCriterion.s00000700.used >= callToTask.s00000743.inputCriterion.s00000700.used AND 'callToTask.s00000743.output.s00000713 >= callToTask.s00000743.output.s00000713 AND 'callToTask.s00000743.output.s00000754 >= callToTask.s00000743.output.s00000754 AND 'callToTask.s00000744.input.s00000709 >= callToTask.s00000744.input.s00000709 AND 'callToTask.s00000744.input.s00000752 >= callToTask.s00000744.input.s00000752 AND 'callToTask.s00000744.inputCriterion.s00000700.used >= callToTask.s00000744.inputCriterion.s00000700.used AND 'callToTask.s00000744.output.s00000713 >= callToTask.s00000744.output.s00000713 AND 'callToTask.s00000744.output.s00000754 >= callToTask.s00000744.output.s00000754 AND 'callToTask.s00000745.input.s00000699 >= callToTask.s00000745.input.s00000699 AND 'callToTask.s00000745.input.s00000709 >= callToTask.s00000745.input.s00000709 AND 'callToTask.s00000745.inputCriterion.s00000700.used >= callToTask.s00000745.inputCriterion.s00000700.used AND 'callToTask.s00000745.output.s00000702 >= callToTask.s00000745.output.s00000702 AND 'callToTask.s00000745.output.s00000713 >= callToTask.s00000745.output.s00000713 AND 'callToTask.s00000745.output.s00000754 >= callToTask.s00000745.output.s00000754 AND 'callToTask.s00000746.input.s00000699 >= callToTask.s00000746.input.s00000699 AND 'callToTask.s00000746.input.s00000709 >= callToTask.s00000746.input.s00000709 AND 'callToTask.s00000746.inputCriterion.s00000700.used >= callToTask.s00000746.inputCriterion.s00000700.used AND 'callToTask.s00000746.output.s00000703 >= callToTask.s00000746.output.s00000703 AND 'callToTask.s00000746.output.s00000713 >= callToTask.s00000746.output.s00000713 AND 'callToTask.s00000746.output.s00000754 >= callToTask.s00000746.output.s00000754 AND 'callToTask.s00000747.input.s00000699 >= callToTask.s00000747.input.s00000699 AND 'callToTask.s00000747.input.s00000709 >= callToTask.s00000747.input.s00000709 AND 'callToTask.s00000747.inputCriterion.s00000700.used >= callToTask.s00000747.inputCriterion.s00000700.used AND 'callToTask.s00000747.output.s00000713 >= callToTask.s00000747.output.s00000713 AND 'callToTask.s00000747.output.s00000754 >= callToTask.s00000747.output.s00000754 AND 'callToTask.s00000748.input.s00000699 >= callToTask.s00000748.input.s00000699 AND 'callToTask.s00000748.input.s00000709 >= callToTask.s00000748.input.s00000709 AND 'callToTask.s00000748.inputCriterion.s00000700.used >= callToTask.s00000748.inputCriterion.s00000700.used AND 'callToTask.s00000748.output.s00000713 >= callToTask.s00000748.output.s00000713 AND 'callToTask.s00000748.output.s00000754 >= callToTask.s00000748.output.s00000754 AND 'decision.s00000707.activated >= decision.s00000707.activated AND 'decision.s00000719.activated >= decision.s00000719.activated AND 'endNode.s00000706.input.default >= endNode.s00000706.input.default AND 'merge.s00000730.activated >= merge.s00000730.activated AND 'merge.s00000742.activated >= merge.s00000742.activated AND 'merge.s00000742.input.s00000709 >= merge.s00000742.input.s00000709 AND 'merge.s00000742.input.s00000737 >= merge.s00000742.input.s00000737 AND 'merge.s00000742.input.s00000740 >= merge.s00000742.input.s00000740 AND 'process.s00000021##s00000698.input.s00000699 >= process.s00000021##s00000698.input.s00000699 AND 'process.s00000021##s00000698.output.s00000701 >= process.s00000021##s00000698.output.s00000701 AND 'process.s00000021##s00000698.outputCriterion.s00000704_omega >= process.s00000021##s00000698.outputCriterion.s00000704_omega)
EF ('sigma >= 1 AND ('alpha - alpha) >= 0 AND ('callToTask.s00000743.input.s00000699 - callToTask.s00000743.input.s00000699) >= 0 AND ('callToTask.s00000743.input.s00000709 - callToTask.s00000743.input.s00000709) >= 0 AND ('callToTask.s00000743.inputCriterion.s00000700.used - callToTask.s00000743.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000743.output.s00000713 - callToTask.s00000743.output.s00000713) >= 0 AND ('callToTask.s00000743.output.s00000754 - callToTask.s00000743.output.s00000754) >= 0 AND ('callToTask.s00000744.input.s00000709 - callToTask.s00000744.input.s00000709) >= 0 AND ('callToTask.s00000744.input.s00000752 - callToTask.s00000744.input.s00000752) >= 0 AND ('callToTask.s00000744.inputCriterion.s00000700.used - callToTask.s00000744.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000744.output.s00000713 - callToTask.s00000744.output.s00000713) >= 0 AND ('callToTask.s00000744.output.s00000754 - callToTask.s00000744.output.s00000754) >= 0 AND ('callToTask.s00000745.input.s00000699 - callToTask.s00000745.input.s00000699) >= 0 AND ('callToTask.s00000745.input.s00000709 - callToTask.s00000745.input.s00000709) >= 0 AND ('callToTask.s00000745.inputCriterion.s00000700.used - callToTask.s00000745.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000745.output.s00000702 - callToTask.s00000745.output.s00000702) >= 0 AND ('callToTask.s00000745.output.s00000713 - callToTask.s00000745.output.s00000713) >= 0 AND ('callToTask.s00000745.output.s00000754 - callToTask.s00000745.output.s00000754) >= 0 AND ('callToTask.s00000746.input.s00000699 - callToTask.s00000746.input.s00000699) >= 0 AND ('callToTask.s00000746.input.s00000709 - callToTask.s00000746.input.s00000709) >= 0 AND ('callToTask.s00000746.inputCriterion.s00000700.used - callToTask.s00000746.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000746.output.s00000703 - callToTask.s00000746.output.s00000703) >= 0 AND ('callToTask.s00000746.output.s00000713 - callToTask.s00000746.output.s00000713) >= 0 AND ('callToTask.s00000746.output.s00000754 - callToTask.s00000746.output.s00000754) >= 0 AND ('callToTask.s00000747.input.s00000699 - callToTask.s00000747.input.s00000699) >= 0 AND ('callToTask.s00000747.input.s00000709 - callToTask.s00000747.input.s00000709) >= 0 AND ('callToTask.s00000747.inputCriterion.s00000700.used - callToTask.s00000747.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000747.output.s00000713 - callToTask.s00000747.output.s00000713) >= 0 AND ('callToTask.s00000747.output.s00000754 - callToTask.s00000747.output.s00000754) >= 0 AND ('callToTask.s00000748.input.s00000699 - callToTask.s00000748.input.s00000699) >= 0 AND ('callToTask.s00000748.input.s00000709 - callToTask.s00000748.input.s00000709) >= 0 AND ('callToTask.s00000748.inputCriterion.s00000700.used - callToTask.s00000748.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000748.output.s00000713 - callToTask.s00000748.output.s00000713) >= 0 AND ('callToTask.s00000748.output.s00000754 - callToTask.s00000748.output.s00000754) >= 0 AND ('decision.s00000707.activated - decision.s00000707.activated) >= 0 AND ('decision.s00000719.activated - decision.s00000719.activated) >= 0 AND ('endNode.s00000706.input.default - endNode.s00000706.input.default) >= 0 AND ('merge.s00000730.activated - merge.s00000730.activated) >= 0 AND ('merge.s00000742.activated - merge.s00000742.activated) >= 0 AND ('merge.s00000742.input.s00000709 - merge.s00000742.input.s00000709) >= 0 AND ('merge.s00000742.input.s00000737 - merge.s00000742.input.s00000737) >= 0 AND ('merge.s00000742.input.s00000740 - merge.s00000742.input.s00000740) >= 0 AND ('process.s00000021##s00000698.input.s00000699 - process.s00000021##s00000698.input.s00000699) >= 0 AND ('process.s00000021##s00000698.output.s00000701 - process.s00000021##s00000698.output.s00000701) >= 0 AND ('process.s00000021##s00000698.outputCriterion.s00000704_omega - process.s00000021##s00000698.outputCriterion.s00000704_omega) >= 0)
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000023__s00000777.lola.terminating.sara 0 → 100644
View file @ fcfb3082
PROBLEM termination_by_reachability:
GOAL REACHABILITY;
FILE A.s00000023__s00000777.lola.terminating TYPE LOLA;
INITIAL 'alpha:1,'m1:1,alpha:1;
FINAL COVER;
CONSTRAINTS 'sigma>1,'alpha+-1alpha>0,'callToTask.s00000747.input.s00000699+-1callToTask.s00000747.input.s00000699>0,'callToTask.s00000747.input.s00000709+-1callToTask.s00000747.input.s00000709>0,'callToTask.s00000747.inputCriterion.s00000700.used+-1callToTask.s00000747.inputCriterion.s00000700.used>0,'callToTask.s00000747.output.s00000713+-1callToTask.s00000747.output.s00000713>0,'callToTask.s00000747.output.s00000754+-1callToTask.s00000747.output.s00000754>0,'callToTask.s00000748.input.s00000699+-1callToTask.s00000748.input.s00000699>0,'callToTask.s00000748.input.s00000709+-1callToTask.s00000748.input.s00000709>0,'callToTask.s00000748.inputCriterion.s00000700.used+-1callToTask.s00000748.inputCriterion.s00000700.used>0,'callToTask.s00000748.output.s00000713+-1callToTask.s00000748.output.s00000713>0,'callToTask.s00000748.output.s00000754+-1callToTask.s00000748.output.s00000754>0,'callToTask.s00000815.input.s00000709+-1callToTask.s00000815.input.s00000709>0,'callToTask.s00000815.input.s00000844+-1callToTask.s00000815.input.s00000844>0,'callToTask.s00000815.inputCriterion.s00000700.used+-1callToTask.s00000815.inputCriterion.s00000700.used>0,'callToTask.s00000815.output.s00000713+-1callToTask.s00000815.output.s00000713>0,'callToTask.s00000815.output.s00000754+-1callToTask.s00000815.output.s00000754>0,'callToTask.s00000815.output.s00000840+-1callToTask.s00000815.output.s00000840>0,'callToTask.s00000816.input.s00000709+-1callToTask.s00000816.input.s00000709>0,'callToTask.s00000816.input.s00000778+-1callToTask.s00000816.input.s00000778>0,'callToTask.s00000816.inputCriterion.s00000700.used+-1callToTask.s00000816.inputCriterion.s00000700.used>0,'callToTask.s00000816.output.s00000713+-1callToTask.s00000816.output.s00000713>0,'callToTask.s00000816.output.s00000824+-1callToTask.s00000816.output.s00000824>0,'callToTask.s00000817.input.s00000709+-1callToTask.s00000817.input.s00000709>0,'callToTask.s00000817.input.s00000778+-1callToTask.s00000817.input.s00000778>0,'callToTask.s00000817.inputCriterion.s00000700.used+-1callToTask.s00000817.inputCriterion.s00000700.used>0,'callToTask.s00000817.output.s00000713+-1callToTask.s00000817.output.s00000713>0,'callToTask.s00000817.output.s00000824+-1callToTask.s00000817.output.s00000824>0,'callToTask.s00000818.input.s00000699+-1callToTask.s00000818.input.s00000699>0,'callToTask.s00000818.input.s00000709+-1callToTask.s00000818.input.s00000709>0,'callToTask.s00000818.inputCriterion.s00000700.used+-1callToTask.s00000818.inputCriterion.s00000700.used>0,'callToTask.s00000818.output.s00000713+-1callToTask.s00000818.output.s00000713>0,'callToTask.s00000818.output.s00000780+-1callToTask.s00000818.output.s00000780>0,'callToTask.s00000818.output.s00000827+-1callToTask.s00000818.output.s00000827>0,'callToTask.s00000819.input.s00000709+-1callToTask.s00000819.input.s00000709>0,'callToTask.s00000819.input.s00000778+-1callToTask.s00000819.input.s00000778>0,'callToTask.s00000819.inputCriterion.s00000700.used+-1callToTask.s00000819.inputCriterion.s00000700.used>0,'callToTask.s00000819.output.s00000713+-1callToTask.s00000819.output.s00000713>0,'callToTask.s00000819.output.s00000824+-1callToTask.s00000819.output.s00000824>0,'callToTask.s00000820.input.s00000709+-1callToTask.s00000820.input.s00000709>0,'callToTask.s00000820.input.s00000778+-1callToTask.s00000820.input.s00000778>0,'callToTask.s00000820.inputCriterion.s00000700.used+-1callToTask.s00000820.inputCriterion.s00000700.used>0,'callToTask.s00000820.output.s00000713+-1callToTask.s00000820.output.s00000713>0,'callToTask.s00000820.output.s00000824+-1callToTask.s00000820.output.s00000824>0,'callToTask.s00000821.input.s00000699+-1callToTask.s00000821.input.s00000699>0,'callToTask.s00000821.input.s00000709+-1callToTask.s00000821.input.s00000709>0,'callToTask.s00000821.inputCriterion.s00000700.used+-1callToTask.s00000821.inputCriterion.s00000700.used>0,'callToTask.s00000821.output.s00000713+-1callToTask.s00000821.output.s00000713>0,'callToTask.s00000821.output.s00000781+-1callToTask.s00000821.output.s00000781>0,'callToTask.s00000821.output.s00000827+-1callToTask.s00000821.output.s00000827>0,'callToTask.s00000822.input.s00000699+-1callToTask.s00000822.input.s00000699>0,'callToTask.s00000822.input.s00000709+-1callToTask.s00000822.input.s00000709>0,'callToTask.s00000822.inputCriterion.s00000700.used+-1callToTask.s00000822.inputCriterion.s00000700.used>0,'callToTask.s00000822.output.s00000713+-1callToTask.s00000822.output.s00000713>0,'callToTask.s00000822.output.s00000754+-1callToTask.s00000822.output.s00000754>0,'decision.s00000707.activated+-1decision.s00000707.activated>0,'decision.s00000782.activated+-1decision.s00000782.activated>0,'endNode.s00000706.input.default+-1endNode.s00000706.input.default>0,'merge.s00000730.activated+-1merge.s00000730.activated>0,'merge.s00000742.activated+-1merge.s00000742.activated>0,'merge.s00000742.input.s00000709+-1merge.s00000742.input.s00000709>0,'merge.s00000742.input.s00000710+-1merge.s00000742.input.s00000710>0,'merge.s00000742.input.s00000740+-1merge.s00000742.input.s00000740>0,'process.s00000023##s00000777.input.s00000778+-1process.s00000023##s00000777.input.s00000778>0,'process.s00000023##s00000777.output.s00000754+-1process.s00000023##s00000777.output.s00000754>0,'process.s00000023##s00000777.outputCriterion.s00000704_omega+-1process.s00000023##s00000777.outputCriterion.s00000704_omega>0;
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000023__s00000777.lola.terminating.task1
View file @ fcfb3082
EF ('sigma >= 1 AND 'alpha >= alpha AND 'callToTask.s00000747.input.s00000699 >= callToTask.s00000747.input.s00000699 AND 'callToTask.s00000747.input.s00000709 >= callToTask.s00000747.input.s00000709 AND 'callToTask.s00000747.inputCriterion.s00000700.used >= callToTask.s00000747.inputCriterion.s00000700.used AND 'callToTask.s00000747.output.s00000713 >= callToTask.s00000747.output.s00000713 AND 'callToTask.s00000747.output.s00000754 >= callToTask.s00000747.output.s00000754 AND 'callToTask.s00000748.input.s00000699 >= callToTask.s00000748.input.s00000699 AND 'callToTask.s00000748.input.s00000709 >= callToTask.s00000748.input.s00000709 AND 'callToTask.s00000748.inputCriterion.s00000700.used >= callToTask.s00000748.inputCriterion.s00000700.used AND 'callToTask.s00000748.output.s00000713 >= callToTask.s00000748.output.s00000713 AND 'callToTask.s00000748.output.s00000754 >= callToTask.s00000748.output.s00000754 AND 'callToTask.s00000815.input.s00000709 >= callToTask.s00000815.input.s00000709 AND 'callToTask.s00000815.input.s00000844 >= callToTask.s00000815.input.s00000844 AND 'callToTask.s00000815.inputCriterion.s00000700.used >= callToTask.s00000815.inputCriterion.s00000700.used AND 'callToTask.s00000815.output.s00000713 >= callToTask.s00000815.output.s00000713 AND 'callToTask.s00000815.output.s00000754 >= callToTask.s00000815.output.s00000754 AND 'callToTask.s00000815.output.s00000840 >= callToTask.s00000815.output.s00000840 AND 'callToTask.s00000816.input.s00000709 >= callToTask.s00000816.input.s00000709 AND 'callToTask.s00000816.input.s00000778 >= callToTask.s00000816.input.s00000778 AND 'callToTask.s00000816.inputCriterion.s00000700.used >= callToTask.s00000816.inputCriterion.s00000700.used AND 'callToTask.s00000816.output.s00000713 >= callToTask.s00000816.output.s00000713 AND 'callToTask.s00000816.output.s00000824 >= callToTask.s00000816.output.s00000824 AND 'callToTask.s00000817.input.s00000709 >= callToTask.s00000817.input.s00000709 AND 'callToTask.s00000817.input.s00000778 >= callToTask.s00000817.input.s00000778 AND 'callToTask.s00000817.inputCriterion.s00000700.used >= callToTask.s00000817.inputCriterion.s00000700.used AND 'callToTask.s00000817.output.s00000713 >= callToTask.s00000817.output.s00000713 AND 'callToTask.s00000817.output.s00000824 >= callToTask.s00000817.output.s00000824 AND 'callToTask.s00000818.input.s00000699 >= callToTask.s00000818.input.s00000699 AND 'callToTask.s00000818.input.s00000709 >= callToTask.s00000818.input.s00000709 AND 'callToTask.s00000818.inputCriterion.s00000700.used >= callToTask.s00000818.inputCriterion.s00000700.used AND 'callToTask.s00000818.output.s00000713 >= callToTask.s00000818.output.s00000713 AND 'callToTask.s00000818.output.s00000780 >= callToTask.s00000818.output.s00000780 AND 'callToTask.s00000818.output.s00000827 >= callToTask.s00000818.output.s00000827 AND 'callToTask.s00000819.input.s00000709 >= callToTask.s00000819.input.s00000709 AND 'callToTask.s00000819.input.s00000778 >= callToTask.s00000819.input.s00000778 AND 'callToTask.s00000819.inputCriterion.s00000700.used >= callToTask.s00000819.inputCriterion.s00000700.used AND 'callToTask.s00000819.output.s00000713 >= callToTask.s00000819.output.s00000713 AND 'callToTask.s00000819.output.s00000824 >= callToTask.s00000819.output.s00000824 AND 'callToTask.s00000820.input.s00000709 >= callToTask.s00000820.input.s00000709 AND 'callToTask.s00000820.input.s00000778 >= callToTask.s00000820.input.s00000778 AND 'callToTask.s00000820.inputCriterion.s00000700.used >= callToTask.s00000820.inputCriterion.s00000700.used AND 'callToTask.s00000820.output.s00000713 >= callToTask.s00000820.output.s00000713 AND 'callToTask.s00000820.output.s00000824 >= callToTask.s00000820.output.s00000824 AND 'callToTask.s00000821.input.s00000699 >= callToTask.s00000821.input.s00000699 AND 'callToTask.s00000821.input.s00000709 >= callToTask.s00000821.input.s00000709 AND 'callToTask.s00000821.inputCriterion.s00000700.used >= callToTask.s00000821.inputCriterion.s00000700.used AND 'callToTask.s00000821.output.s00000713 >= callToTask.s00000821.output.s00000713 AND 'callToTask.s00000821.output.s00000781 >= callToTask.s00000821.output.s00000781 AND 'callToTask.s00000821.output.s00000827 >= callToTask.s00000821.output.s00000827 AND 'callToTask.s00000822.input.s00000699 >= callToTask.s00000822.input.s00000699 AND 'callToTask.s00000822.input.s00000709 >= callToTask.s00000822.input.s00000709 AND 'callToTask.s00000822.inputCriterion.s00000700.used >= callToTask.s00000822.inputCriterion.s00000700.used AND 'callToTask.s00000822.output.s00000713 >= callToTask.s00000822.output.s00000713 AND 'callToTask.s00000822.output.s00000754 >= callToTask.s00000822.output.s00000754 AND 'decision.s00000707.activated >= decision.s00000707.activated AND 'decision.s00000782.activated >= decision.s00000782.activated AND 'endNode.s00000706.input.default >= endNode.s00000706.input.default AND 'merge.s00000730.activated >= merge.s00000730.activated AND 'merge.s00000742.activated >= merge.s00000742.activated AND 'merge.s00000742.input.s00000709 >= merge.s00000742.input.s00000709 AND 'merge.s00000742.input.s00000710 >= merge.s00000742.input.s00000710 AND 'merge.s00000742.input.s00000740 >= merge.s00000742.input.s00000740 AND 'process.s00000023##s00000777.input.s00000778 >= process.s00000023##s00000777.input.s00000778 AND 'process.s00000023##s00000777.output.s00000754 >= process.s00000023##s00000777.output.s00000754 AND 'process.s00000023##s00000777.outputCriterion.s00000704_omega >= process.s00000023##s00000777.outputCriterion.s00000704_omega)
EF ('sigma >= 1 AND ('alpha - alpha) >= 0 AND ('callToTask.s00000747.input.s00000699 - callToTask.s00000747.input.s00000699) >= 0 AND ('callToTask.s00000747.input.s00000709 - callToTask.s00000747.input.s00000709) >= 0 AND ('callToTask.s00000747.inputCriterion.s00000700.used - callToTask.s00000747.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000747.output.s00000713 - callToTask.s00000747.output.s00000713) >= 0 AND ('callToTask.s00000747.output.s00000754 - callToTask.s00000747.output.s00000754) >= 0 AND ('callToTask.s00000748.input.s00000699 - callToTask.s00000748.input.s00000699) >= 0 AND ('callToTask.s00000748.input.s00000709 - callToTask.s00000748.input.s00000709) >= 0 AND ('callToTask.s00000748.inputCriterion.s00000700.used - callToTask.s00000748.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000748.output.s00000713 - callToTask.s00000748.output.s00000713) >= 0 AND ('callToTask.s00000748.output.s00000754 - callToTask.s00000748.output.s00000754) >= 0 AND ('callToTask.s00000815.input.s00000709 - callToTask.s00000815.input.s00000709) >= 0 AND ('callToTask.s00000815.input.s00000844 - callToTask.s00000815.input.s00000844) >= 0 AND ('callToTask.s00000815.inputCriterion.s00000700.used - callToTask.s00000815.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000815.output.s00000713 - callToTask.s00000815.output.s00000713) >= 0 AND ('callToTask.s00000815.output.s00000754 - callToTask.s00000815.output.s00000754) >= 0 AND ('callToTask.s00000815.output.s00000840 - callToTask.s00000815.output.s00000840) >= 0 AND ('callToTask.s00000816.input.s00000709 - callToTask.s00000816.input.s00000709) >= 0 AND ('callToTask.s00000816.input.s00000778 - callToTask.s00000816.input.s00000778) >= 0 AND ('callToTask.s00000816.inputCriterion.s00000700.used - callToTask.s00000816.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000816.output.s00000713 - callToTask.s00000816.output.s00000713) >= 0 AND ('callToTask.s00000816.output.s00000824 - callToTask.s00000816.output.s00000824) >= 0 AND ('callToTask.s00000817.input.s00000709 - callToTask.s00000817.input.s00000709) >= 0 AND ('callToTask.s00000817.input.s00000778 - callToTask.s00000817.input.s00000778) >= 0 AND ('callToTask.s00000817.inputCriterion.s00000700.used - callToTask.s00000817.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000817.output.s00000713 - callToTask.s00000817.output.s00000713) >= 0 AND ('callToTask.s00000817.output.s00000824 - callToTask.s00000817.output.s00000824) >= 0 AND ('callToTask.s00000818.input.s00000699 - callToTask.s00000818.input.s00000699) >= 0 AND ('callToTask.s00000818.input.s00000709 - callToTask.s00000818.input.s00000709) >= 0 AND ('callToTask.s00000818.inputCriterion.s00000700.used - callToTask.s00000818.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000818.output.s00000713 - callToTask.s00000818.output.s00000713) >= 0 AND ('callToTask.s00000818.output.s00000780 - callToTask.s00000818.output.s00000780) >= 0 AND ('callToTask.s00000818.output.s00000827 - callToTask.s00000818.output.s00000827) >= 0 AND ('callToTask.s00000819.input.s00000709 - callToTask.s00000819.input.s00000709) >= 0 AND ('callToTask.s00000819.input.s00000778 - callToTask.s00000819.input.s00000778) >= 0 AND ('callToTask.s00000819.inputCriterion.s00000700.used - callToTask.s00000819.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000819.output.s00000713 - callToTask.s00000819.output.s00000713) >= 0 AND ('callToTask.s00000819.output.s00000824 - callToTask.s00000819.output.s00000824) >= 0 AND ('callToTask.s00000820.input.s00000709 - callToTask.s00000820.input.s00000709) >= 0 AND ('callToTask.s00000820.input.s00000778 - callToTask.s00000820.input.s00000778) >= 0 AND ('callToTask.s00000820.inputCriterion.s00000700.used - callToTask.s00000820.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000820.output.s00000713 - callToTask.s00000820.output.s00000713) >= 0 AND ('callToTask.s00000820.output.s00000824 - callToTask.s00000820.output.s00000824) >= 0 AND ('callToTask.s00000821.input.s00000699 - callToTask.s00000821.input.s00000699) >= 0 AND ('callToTask.s00000821.input.s00000709 - callToTask.s00000821.input.s00000709) >= 0 AND ('callToTask.s00000821.inputCriterion.s00000700.used - callToTask.s00000821.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000821.output.s00000713 - callToTask.s00000821.output.s00000713) >= 0 AND ('callToTask.s00000821.output.s00000781 - callToTask.s00000821.output.s00000781) >= 0 AND ('callToTask.s00000821.output.s00000827 - callToTask.s00000821.output.s00000827) >= 0 AND ('callToTask.s00000822.input.s00000699 - callToTask.s00000822.input.s00000699) >= 0 AND ('callToTask.s00000822.input.s00000709 - callToTask.s00000822.input.s00000709) >= 0 AND ('callToTask.s00000822.inputCriterion.s00000700.used - callToTask.s00000822.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000822.output.s00000713 - callToTask.s00000822.output.s00000713) >= 0 AND ('callToTask.s00000822.output.s00000754 - callToTask.s00000822.output.s00000754) >= 0 AND ('decision.s00000707.activated - decision.s00000707.activated) >= 0 AND ('decision.s00000782.activated - decision.s00000782.activated) >= 0 AND ('endNode.s00000706.input.default - endNode.s00000706.input.default) >= 0 AND ('merge.s00000730.activated - merge.s00000730.activated) >= 0 AND ('merge.s00000742.activated - merge.s00000742.activated) >= 0 AND ('merge.s00000742.input.s00000709 - merge.s00000742.input.s00000709) >= 0 AND ('merge.s00000742.input.s00000710 - merge.s00000742.input.s00000710) >= 0 AND ('merge.s00000742.input.s00000740 - merge.s00000742.input.s00000740) >= 0 AND ('process.s00000023##s00000777.input.s00000778 - process.s00000023##s00000777.input.s00000778) >= 0 AND ('process.s00000023##s00000777.output.s00000754 - process.s00000023##s00000777.output.s00000754) >= 0 AND ('process.s00000023##s00000777.outputCriterion.s00000704_omega - process.s00000023##s00000777.outputCriterion.s00000704_omega) >= 0)
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000023__s00000863.lola.terminating.sara 0 → 100644
View file @ fcfb3082
PROBLEM termination_by_reachability:
GOAL REACHABILITY;
FILE A.s00000023__s00000863.lola.terminating TYPE LOLA;
INITIAL 'alpha:1,'m1:1,alpha:1;
FINAL COVER;
CONSTRAINTS 'sigma>1,'alpha+-1alpha>0,'callToProcess.s00000698.input.s00000699+-1callToProcess.s00000698.input.s00000699>0,'callToProcess.s00000698.input.s00000709+-1callToProcess.s00000698.input.s00000709>0,'callToProcess.s00000698.inputCriterion.s00000700.used+-1callToProcess.s00000698.inputCriterion.s00000700.used>0,'callToProcess.s00000698.output.s00000701+-1callToProcess.s00000698.output.s00000701>0,'callToProcess.s00000698.output.s00000713+-1callToProcess.s00000698.output.s00000713>0,'callToProcess.s00000777.input.s00000709+-1callToProcess.s00000777.input.s00000709>0,'callToProcess.s00000777.input.s00000778+-1callToProcess.s00000777.input.s00000778>0,'callToProcess.s00000777.inputCriterion.s00000700.used+-1callToProcess.s00000777.inputCriterion.s00000700.used>0,'callToProcess.s00000777.output.s00000713+-1callToProcess.s00000777.output.s00000713>0,'callToProcess.s00000777.output.s00000754+-1callToProcess.s00000777.output.s00000754>0,'callToProcess.s00000846.input.s00000699+-1callToProcess.s00000846.input.s00000699>0,'callToProcess.s00000846.input.s00000709+-1callToProcess.s00000846.input.s00000709>0,'callToProcess.s00000846.inputCriterion.s00000700.used+-1callToProcess.s00000846.inputCriterion.s00000700.used>0,'callToProcess.s00000846.output.s00000713+-1callToProcess.s00000846.output.s00000713>0,'callToProcess.s00000846.output.s00000754+-1callToProcess.s00000846.output.s00000754>0,'callToTask.s00000880.input.s00000709+-1callToTask.s00000880.input.s00000709>0,'callToTask.s00000880.inputCriterion.s00000700.used+-1callToTask.s00000880.inputCriterion.s00000700.used>0,'callToTask.s00000880.output.s00000713+-1callToTask.s00000880.output.s00000713>0,'callToTask.s00000880.output.s00000891+-1callToTask.s00000880.output.s00000891>0,'callToTask.s00000881.input.s00000699+-1callToTask.s00000881.input.s00000699>0,'callToTask.s00000881.input.s00000709+-1callToTask.s00000881.input.s00000709>0,'callToTask.s00000881.inputCriterion.s00000700.used+-1callToTask.s00000881.inputCriterion.s00000700.used>0,'callToTask.s00000881.output.s00000713+-1callToTask.s00000881.output.s00000713>0,'callToTask.s00000881.output.s00000754+-1callToTask.s00000881.output.s00000754>0,'callToTask.s00000882.input.s00000699+-1callToTask.s00000882.input.s00000699>0,'callToTask.s00000882.input.s00000709+-1callToTask.s00000882.input.s00000709>0,'callToTask.s00000882.inputCriterion.s00000700.used+-1callToTask.s00000882.inputCriterion.s00000700.used>0,'callToTask.s00000882.output.s00000713+-1callToTask.s00000882.output.s00000713>0,'callToTask.s00000882.output.s00000754+-1callToTask.s00000882.output.s00000754>0,'callToTask.s00000883.input.s00000709+-1callToTask.s00000883.input.s00000709>0,'callToTask.s00000883.input.s00000778+-1callToTask.s00000883.input.s00000778>0,'callToTask.s00000883.inputCriterion.s00000700.used+-1callToTask.s00000883.inputCriterion.s00000700.used>0,'callToTask.s00000883.output.s00000713+-1callToTask.s00000883.output.s00000713>0,'callToTask.s00000883.output.s00000891+-1callToTask.s00000883.output.s00000891>0,'callToTask.s00000884.input.s00000699+-1callToTask.s00000884.input.s00000699>0,'callToTask.s00000884.input.s00000709+-1callToTask.s00000884.input.s00000709>0,'callToTask.s00000884.inputCriterion.s00000700.used+-1callToTask.s00000884.inputCriterion.s00000700.used>0,'callToTask.s00000884.output.s00000713+-1callToTask.s00000884.output.s00000713>0,'callToTask.s00000884.output.s00000754+-1callToTask.s00000884.output.s00000754>0,'callToTask.s00000885.input.s00000709+-1callToTask.s00000885.input.s00000709>0,'callToTask.s00000885.input.s00000778+-1callToTask.s00000885.input.s00000778>0,'callToTask.s00000885.inputCriterion.s00000700.used+-1callToTask.s00000885.inputCriterion.s00000700.used>0,'callToTask.s00000885.output.s00000713+-1callToTask.s00000885.output.s00000713>0,'callToTask.s00000885.output.s00000891+-1callToTask.s00000885.output.s00000891>0,'callToTask.s00000886.input.s00000699+-1callToTask.s00000886.input.s00000699>0,'callToTask.s00000886.input.s00000709+-1callToTask.s00000886.input.s00000709>0,'callToTask.s00000886.inputCriterion.s00000700.used+-1callToTask.s00000886.inputCriterion.s00000700.used>0,'callToTask.s00000886.output.s00000713+-1callToTask.s00000886.output.s00000713>0,'callToTask.s00000886.output.s00000754+-1callToTask.s00000886.output.s00000754>0,'callToTask.s00000887.inputCriterion.s00000858.used+-1callToTask.s00000887.inputCriterion.s00000858.used>0,'callToTask.s00000887.output.s00000713+-1callToTask.s00000887.output.s00000713>0,'callToTask.s00000887.output.s00000866+-1callToTask.s00000887.output.s00000866>0,'callToTask.s00000887.output.s00000867+-1callToTask.s00000887.output.s00000867>0,'callToTask.s00000888.inputCriterion.s00000700.used+-1callToTask.s00000888.inputCriterion.s00000700.used>0,'callToTask.s00000888.output.s00000713+-1callToTask.s00000888.output.s00000713>0,'callToTask.s00000888.output.s00000849+-1callToTask.s00000888.output.s00000849>0,'callToTask.s00000889.input.s00000699+-1callToTask.s00000889.input.s00000699>0,'callToTask.s00000889.input.s00000709+-1callToTask.s00000889.input.s00000709>0,'callToTask.s00000889.inputCriterion.s00000858.used+-1callToTask.s00000889.inputCriterion.s00000858.used>0,'callToTask.s00000889.output.s00000713+-1callToTask.s00000889.output.s00000713>0,'callToTask.s00000889.output.s00000754+-1callToTask.s00000889.output.s00000754>0,'callToTask.s00000890.input.s00000699+-1callToTask.s00000890.input.s00000699>0,'callToTask.s00000890.input.s00000709+-1callToTask.s00000890.input.s00000709>0,'callToTask.s00000890.inputCriterion.s00000858.used+-1callToTask.s00000890.inputCriterion.s00000858.used>0,'callToTask.s00000890.output.s00000713+-1callToTask.s00000890.output.s00000713>0,'callToTask.s00000890.output.s00000754+-1callToTask.s00000890.output.s00000754>0,'decision.s00000868.activated+-1decision.s00000868.activated>0,'decision.s00000874.activated+-1decision.s00000874.activated>0,'decision.s00000876.activated+-1decision.s00000876.activated>0,'endNode.s00000706.input.default+-1endNode.s00000706.input.default>0,'merge.s00000730.activated+-1merge.s00000730.activated>0,'merge.s00000742.activated+-1merge.s00000742.activated>0,'process.s00000023##s00000863.input.s00000864+-1process.s00000023##s00000863.input.s00000864>0,'process.s00000023##s00000863.input.s00000865+-1process.s00000023##s00000863.input.s00000865>0,'process.s00000023##s00000863.output.s00000754+-1process.s00000023##s00000863.output.s00000754>0,'process.s00000023##s00000863.outputCriterion.s00000704_omega+-1process.s00000023##s00000863.outputCriterion.s00000704_omega>0;
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000023__s00000863.lola.terminating.task1
View file @ fcfb3082
EF ('sigma >= 1 AND 'alpha >= alpha AND 'callToProcess.s00000698.input.s00000699 >= callToProcess.s00000698.input.s00000699 AND 'callToProcess.s00000698.input.s00000709 >= callToProcess.s00000698.input.s00000709 AND 'callToProcess.s00000698.inputCriterion.s00000700.used >= callToProcess.s00000698.inputCriterion.s00000700.used AND 'callToProcess.s00000698.output.s00000701 >= callToProcess.s00000698.output.s00000701 AND 'callToProcess.s00000698.output.s00000713 >= callToProcess.s00000698.output.s00000713 AND 'callToProcess.s00000777.input.s00000709 >= callToProcess.s00000777.input.s00000709 AND 'callToProcess.s00000777.input.s00000778 >= callToProcess.s00000777.input.s00000778 AND 'callToProcess.s00000777.inputCriterion.s00000700.used >= callToProcess.s00000777.inputCriterion.s00000700.used AND 'callToProcess.s00000777.output.s00000713 >= callToProcess.s00000777.output.s00000713 AND 'callToProcess.s00000777.output.s00000754 >= callToProcess.s00000777.output.s00000754 AND 'callToProcess.s00000846.input.s00000699 >= callToProcess.s00000846.input.s00000699 AND 'callToProcess.s00000846.input.s00000709 >= callToProcess.s00000846.input.s00000709 AND 'callToProcess.s00000846.inputCriterion.s00000700.used >= callToProcess.s00000846.inputCriterion.s00000700.used AND 'callToProcess.s00000846.output.s00000713 >= callToProcess.s00000846.output.s00000713 AND 'callToProcess.s00000846.output.s00000754 >= callToProcess.s00000846.output.s00000754 AND 'callToTask.s00000880.input.s00000709 >= callToTask.s00000880.input.s00000709 AND 'callToTask.s00000880.inputCriterion.s00000700.used >= callToTask.s00000880.inputCriterion.s00000700.used AND 'callToTask.s00000880.output.s00000713 >= callToTask.s00000880.output.s00000713 AND 'callToTask.s00000880.output.s00000891 >= callToTask.s00000880.output.s00000891 AND 'callToTask.s00000881.input.s00000699 >= callToTask.s00000881.input.s00000699 AND 'callToTask.s00000881.input.s00000709 >= callToTask.s00000881.input.s00000709 AND 'callToTask.s00000881.inputCriterion.s00000700.used >= callToTask.s00000881.inputCriterion.s00000700.used AND 'callToTask.s00000881.output.s00000713 >= callToTask.s00000881.output.s00000713 AND 'callToTask.s00000881.output.s00000754 >= callToTask.s00000881.output.s00000754 AND 'callToTask.s00000882.input.s00000699 >= callToTask.s00000882.input.s00000699 AND 'callToTask.s00000882.input.s00000709 >= callToTask.s00000882.input.s00000709 AND 'callToTask.s00000882.inputCriterion.s00000700.used >= callToTask.s00000882.inputCriterion.s00000700.used AND 'callToTask.s00000882.output.s00000713 >= callToTask.s00000882.output.s00000713 AND 'callToTask.s00000882.output.s00000754 >= callToTask.s00000882.output.s00000754 AND 'callToTask.s00000883.input.s00000709 >= callToTask.s00000883.input.s00000709 AND 'callToTask.s00000883.input.s00000778 >= callToTask.s00000883.input.s00000778 AND 'callToTask.s00000883.inputCriterion.s00000700.used >= callToTask.s00000883.inputCriterion.s00000700.used AND 'callToTask.s00000883.output.s00000713 >= callToTask.s00000883.output.s00000713 AND 'callToTask.s00000883.output.s00000891 >= callToTask.s00000883.output.s00000891 AND 'callToTask.s00000884.input.s00000699 >= callToTask.s00000884.input.s00000699 AND 'callToTask.s00000884.input.s00000709 >= callToTask.s00000884.input.s00000709 AND 'callToTask.s00000884.inputCriterion.s00000700.used >= callToTask.s00000884.inputCriterion.s00000700.used AND 'callToTask.s00000884.output.s00000713 >= callToTask.s00000884.output.s00000713 AND 'callToTask.s00000884.output.s00000754 >= callToTask.s00000884.output.s00000754 AND 'callToTask.s00000885.input.s00000709 >= callToTask.s00000885.input.s00000709 AND 'callToTask.s00000885.input.s00000778 >= callToTask.s00000885.input.s00000778 AND 'callToTask.s00000885.inputCriterion.s00000700.used >= callToTask.s00000885.inputCriterion.s00000700.used AND 'callToTask.s00000885.output.s00000713 >= callToTask.s00000885.output.s00000713 AND 'callToTask.s00000885.output.s00000891 >= callToTask.s00000885.output.s00000891 AND 'callToTask.s00000886.input.s00000699 >= callToTask.s00000886.input.s00000699 AND 'callToTask.s00000886.input.s00000709 >= callToTask.s00000886.input.s00000709 AND 'callToTask.s00000886.inputCriterion.s00000700.used >= callToTask.s00000886.inputCriterion.s00000700.used AND 'callToTask.s00000886.output.s00000713 >= callToTask.s00000886.output.s00000713 AND 'callToTask.s00000886.output.s00000754 >= callToTask.s00000886.output.s00000754 AND 'callToTask.s00000887.inputCriterion.s00000858.used >= callToTask.s00000887.inputCriterion.s00000858.used AND 'callToTask.s00000887.output.s00000713 >= callToTask.s00000887.output.s00000713 AND 'callToTask.s00000887.output.s00000866 >= callToTask.s00000887.output.s00000866 AND 'callToTask.s00000887.output.s00000867 >= callToTask.s00000887.output.s00000867 AND 'callToTask.s00000888.inputCriterion.s00000700.used >= callToTask.s00000888.inputCriterion.s00000700.used AND 'callToTask.s00000888.output.s00000713 >= callToTask.s00000888.output.s00000713 AND 'callToTask.s00000888.output.s00000849 >= callToTask.s00000888.output.s00000849 AND 'callToTask.s00000889.input.s00000699 >= callToTask.s00000889.input.s00000699 AND 'callToTask.s00000889.input.s00000709 >= callToTask.s00000889.input.s00000709 AND 'callToTask.s00000889.inputCriterion.s00000858.used >= callToTask.s00000889.inputCriterion.s00000858.used AND 'callToTask.s00000889.output.s00000713 >= callToTask.s00000889.output.s00000713 AND 'callToTask.s00000889.output.s00000754 >= callToTask.s00000889.output.s00000754 AND 'callToTask.s00000890.input.s00000699 >= callToTask.s00000890.input.s00000699 AND 'callToTask.s00000890.input.s00000709 >= callToTask.s00000890.input.s00000709 AND 'callToTask.s00000890.inputCriterion.s00000858.used >= callToTask.s00000890.inputCriterion.s00000858.used AND 'callToTask.s00000890.output.s00000713 >= callToTask.s00000890.output.s00000713 AND 'callToTask.s00000890.output.s00000754 >= callToTask.s00000890.output.s00000754 AND 'decision.s00000868.activated >= decision.s00000868.activated AND 'decision.s00000874.activated >= decision.s00000874.activated AND 'decision.s00000876.activated >= decision.s00000876.activated AND 'endNode.s00000706.input.default >= endNode.s00000706.input.default AND 'merge.s00000730.activated >= merge.s00000730.activated AND 'merge.s00000742.activated >= merge.s00000742.activated AND 'process.s00000023##s00000863.input.s00000864 >= process.s00000023##s00000863.input.s00000864 AND 'process.s00000023##s00000863.input.s00000865 >= process.s00000023##s00000863.input.s00000865 AND 'process.s00000023##s00000863.output.s00000754 >= process.s00000023##s00000863.output.s00000754 AND 'process.s00000023##s00000863.outputCriterion.s00000704_omega >= process.s00000023##s00000863.outputCriterion.s00000704_omega)
EF ('sigma >= 1 AND ('alpha - alpha) >= 0 AND ('callToProcess.s00000698.input.s00000699 - callToProcess.s00000698.input.s00000699) >= 0 AND ('callToProcess.s00000698.input.s00000709 - callToProcess.s00000698.input.s00000709) >= 0 AND ('callToProcess.s00000698.inputCriterion.s00000700.used - callToProcess.s00000698.inputCriterion.s00000700.used) >= 0 AND ('callToProcess.s00000698.output.s00000701 - callToProcess.s00000698.output.s00000701) >= 0 AND ('callToProcess.s00000698.output.s00000713 - callToProcess.s00000698.output.s00000713) >= 0 AND ('callToProcess.s00000777.input.s00000709 - callToProcess.s00000777.input.s00000709) >= 0 AND ('callToProcess.s00000777.input.s00000778 - callToProcess.s00000777.input.s00000778) >= 0 AND ('callToProcess.s00000777.inputCriterion.s00000700.used - callToProcess.s00000777.inputCriterion.s00000700.used) >= 0 AND ('callToProcess.s00000777.output.s00000713 - callToProcess.s00000777.output.s00000713) >= 0 AND ('callToProcess.s00000777.output.s00000754 - callToProcess.s00000777.output.s00000754) >= 0 AND ('callToProcess.s00000846.input.s00000699 - callToProcess.s00000846.input.s00000699) >= 0 AND ('callToProcess.s00000846.input.s00000709 - callToProcess.s00000846.input.s00000709) >= 0 AND ('callToProcess.s00000846.inputCriterion.s00000700.used - callToProcess.s00000846.inputCriterion.s00000700.used) >= 0 AND ('callToProcess.s00000846.output.s00000713 - callToProcess.s00000846.output.s00000713) >= 0 AND ('callToProcess.s00000846.output.s00000754 - callToProcess.s00000846.output.s00000754) >= 0 AND ('callToTask.s00000880.input.s00000709 - callToTask.s00000880.input.s00000709) >= 0 AND ('callToTask.s00000880.inputCriterion.s00000700.used - callToTask.s00000880.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000880.output.s00000713 - callToTask.s00000880.output.s00000713) >= 0 AND ('callToTask.s00000880.output.s00000891 - callToTask.s00000880.output.s00000891) >= 0 AND ('callToTask.s00000881.input.s00000699 - callToTask.s00000881.input.s00000699) >= 0 AND ('callToTask.s00000881.input.s00000709 - callToTask.s00000881.input.s00000709) >= 0 AND ('callToTask.s00000881.inputCriterion.s00000700.used - callToTask.s00000881.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000881.output.s00000713 - callToTask.s00000881.output.s00000713) >= 0 AND ('callToTask.s00000881.output.s00000754 - callToTask.s00000881.output.s00000754) >= 0 AND ('callToTask.s00000882.input.s00000699 - callToTask.s00000882.input.s00000699) >= 0 AND ('callToTask.s00000882.input.s00000709 - callToTask.s00000882.input.s00000709) >= 0 AND ('callToTask.s00000882.inputCriterion.s00000700.used - callToTask.s00000882.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000882.output.s00000713 - callToTask.s00000882.output.s00000713) >= 0 AND ('callToTask.s00000882.output.s00000754 - callToTask.s00000882.output.s00000754) >= 0 AND ('callToTask.s00000883.input.s00000709 - callToTask.s00000883.input.s00000709) >= 0 AND ('callToTask.s00000883.input.s00000778 - callToTask.s00000883.input.s00000778) >= 0 AND ('callToTask.s00000883.inputCriterion.s00000700.used - callToTask.s00000883.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000883.output.s00000713 - callToTask.s00000883.output.s00000713) >= 0 AND ('callToTask.s00000883.output.s00000891 - callToTask.s00000883.output.s00000891) >= 0 AND ('callToTask.s00000884.input.s00000699 - callToTask.s00000884.input.s00000699) >= 0 AND ('callToTask.s00000884.input.s00000709 - callToTask.s00000884.input.s00000709) >= 0 AND ('callToTask.s00000884.inputCriterion.s00000700.used - callToTask.s00000884.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000884.output.s00000713 - callToTask.s00000884.output.s00000713) >= 0 AND ('callToTask.s00000884.output.s00000754 - callToTask.s00000884.output.s00000754) >= 0 AND ('callToTask.s00000885.input.s00000709 - callToTask.s00000885.input.s00000709) >= 0 AND ('callToTask.s00000885.input.s00000778 - callToTask.s00000885.input.s00000778) >= 0 AND ('callToTask.s00000885.inputCriterion.s00000700.used - callToTask.s00000885.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000885.output.s00000713 - callToTask.s00000885.output.s00000713) >= 0 AND ('callToTask.s00000885.output.s00000891 - callToTask.s00000885.output.s00000891) >= 0 AND ('callToTask.s00000886.input.s00000699 - callToTask.s00000886.input.s00000699) >= 0 AND ('callToTask.s00000886.input.s00000709 - callToTask.s00000886.input.s00000709) >= 0 AND ('callToTask.s00000886.inputCriterion.s00000700.used - callToTask.s00000886.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000886.output.s00000713 - callToTask.s00000886.output.s00000713) >= 0 AND ('callToTask.s00000886.output.s00000754 - callToTask.s00000886.output.s00000754) >= 0 AND ('callToTask.s00000887.inputCriterion.s00000858.used - callToTask.s00000887.inputCriterion.s00000858.used) >= 0 AND ('callToTask.s00000887.output.s00000713 - callToTask.s00000887.output.s00000713) >= 0 AND ('callToTask.s00000887.output.s00000866 - callToTask.s00000887.output.s00000866) >= 0 AND ('callToTask.s00000887.output.s00000867 - callToTask.s00000887.output.s00000867) >= 0 AND ('callToTask.s00000888.inputCriterion.s00000700.used - callToTask.s00000888.inputCriterion.s00000700.used) >= 0 AND ('callToTask.s00000888.output.s00000713 - callToTask.s00000888.output.s00000713) >= 0 AND ('callToTask.s00000888.output.s00000849 - callToTask.s00000888.output.s00000849) >= 0 AND ('callToTask.s00000889.input.s00000699 - callToTask.s00000889.input.s00000699) >= 0 AND ('callToTask.s00000889.input.s00000709 - callToTask.s00000889.input.s00000709) >= 0 AND ('callToTask.s00000889.inputCriterion.s00000858.used - callToTask.s00000889.inputCriterion.s00000858.used) >= 0 AND ('callToTask.s00000889.output.s00000713 - callToTask.s00000889.output.s00000713) >= 0 AND ('callToTask.s00000889.output.s00000754 - callToTask.s00000889.output.s00000754) >= 0 AND ('callToTask.s00000890.input.s00000699 - callToTask.s00000890.input.s00000699) >= 0 AND ('callToTask.s00000890.input.s00000709 - callToTask.s00000890.input.s00000709) >= 0 AND ('callToTask.s00000890.inputCriterion.s00000858.used - callToTask.s00000890.inputCriterion.s00000858.used) >= 0 AND ('callToTask.s00000890.output.s00000713 - callToTask.s00000890.output.s00000713) >= 0 AND ('callToTask.s00000890.output.s00000754 - callToTask.s00000890.output.s00000754) >= 0 AND ('decision.s00000868.activated - decision.s00000868.activated) >= 0 AND ('decision.s00000874.activated - decision.s00000874.activated) >= 0 AND ('decision.s00000876.activated - decision.s00000876.activated) >= 0 AND ('endNode.s00000706.input.default - endNode.s00000706.input.default) >= 0 AND ('merge.s00000730.activated - merge.s00000730.activated) >= 0 AND ('merge.s00000742.activated - merge.s00000742.activated) >= 0 AND ('process.s00000023##s00000863.input.s00000864 - process.s00000023##s00000863.input.s00000864) >= 0 AND ('process.s00000023##s00000863.input.s00000865 - process.s00000023##s00000863.input.s00000865) >= 0 AND ('process.s00000023##s00000863.output.s00000754 - process.s00000023##s00000863.output.s00000754) >= 0 AND ('process.s00000023##s00000863.outputCriterion.s00000704_omega - process.s00000023##s00000863.outputCriterion.s00000704_omega) >= 0)
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000025__s00001059.lola.terminating.sara 0 → 100644
View file @ fcfb3082
PROBLEM termination_by_reachability:
GOAL REACHABILITY;
FILE A.s00000025__s00001059.lola.terminating TYPE LOLA;
INITIAL 'alpha:1,'m1:1,alpha:1;
FINAL COVER;
CONSTRAINTS 'sigma>1,'alpha+-1alpha>0,'callToProcess.s00001005.inputCriterion.s00000858.used+-1callToProcess.s00001005.inputCriterion.s00000858.used>0,'callToProcess.s00001005.output.s00000713+-1callToProcess.s00001005.output.s00000713>0,'callToProcess.s00001009.inputCriterion.s00000700.used+-1callToProcess.s00001009.inputCriterion.s00000700.used>0,'callToProcess.s00001009.output.s00000713+-1callToProcess.s00001009.output.s00000713>0,'callToProcess.s00001009.output.s00000849+-1callToProcess.s00001009.output.s00000849>0,'callToProcess.s00001051.inputCriterion.s00000858.used+-1callToProcess.s00001051.inputCriterion.s00000858.used>0,'callToProcess.s00001051.output.s00000713+-1callToProcess.s00001051.output.s00000713>0,'callToProcess.s00001051.output.s00000919+-1callToProcess.s00001051.output.s00000919>0,'callToService.s00001076.inputCriterion.s00000700.used+-1callToService.s00001076.inputCriterion.s00000700.used>0,'callToService.s00001076.output.s00000713+-1callToService.s00001076.output.s00000713>0,'callToService.s00001076.output.s00000866+-1callToService.s00001076.output.s00000866>0,'callToService.s00001076.output.s00000918+-1callToService.s00001076.output.s00000918>0,'callToService.s00001076.output.s00001078+-1callToService.s00001076.output.s00001078>0,'callToService.s00001077.input.s00000709+-1callToService.s00001077.input.s00000709>0,'callToService.s00001077.input.s00001080+-1callToService.s00001077.input.s00001080>0,'callToService.s00001077.inputCriterion.s00000858.used+-1callToService.s00001077.inputCriterion.s00000858.used>0,'callToService.s00001077.output.s00000713+-1callToService.s00001077.output.s00000713>0,'callToService.s00001077.output.s00001027+-1callToService.s00001077.output.s00001027>0,'callToTask.s00001020.input.s00000709+-1callToTask.s00001020.input.s00000709>0,'callToTask.s00001020.input.s00001079+-1callToTask.s00001020.input.s00001079>0,'callToTask.s00001020.input.s00001080+-1callToTask.s00001020.input.s00001080>0,'callToTask.s00001020.inputCriterion.s00000700.used+-1callToTask.s00001020.inputCriterion.s00000700.used>0,'callToTask.s00001020.output.s00000713+-1callToTask.s00001020.output.s00000713>0,'callToTask.s00001020.output.s00000866+-1callToTask.s00001020.output.s00000866>0,'callToTask.s00001020.output.s00000961+-1callToTask.s00001020.output.s00000961>0,'callToTask.s00001073.input.s00000709+-1callToTask.s00001073.input.s00000709>0,'callToTask.s00001073.input.s00000916+-1callToTask.s00001073.input.s00000916>0,'callToTask.s00001073.input.s00001079+-1callToTask.s00001073.input.s00001079>0,'callToTask.s00001073.input.s00001080+-1callToTask.s00001073.input.s00001080>0,'callToTask.s00001073.inputCriterion.s00000858.used+-1callToTask.s00001073.inputCriterion.s00000858.used>0,'callToTask.s00001073.output.s00000713+-1callToTask.s00001073.output.s00000713>0,'callToTask.s00001073.output.s00000866+-1callToTask.s00001073.output.s00000866>0,'callToTask.s00001073.output.s00001078+-1callToTask.s00001073.output.s00001078>0,'callToTask.s00001074.input.s00000709+-1callToTask.s00001074.input.s00000709>0,'callToTask.s00001074.input.s00001080+-1callToTask.s00001074.input.s00001080>0,'callToTask.s00001074.inputCriterion.s00000858.used+-1callToTask.s00001074.inputCriterion.s00000858.used>0,'callToTask.s00001074.output.s00000713+-1callToTask.s00001074.output.s00000713>0,'callToTask.s00001074.output.s00000866+-1callToTask.s00001074.output.s00000866>0,'callToTask.s00001074.output.s00000918+-1callToTask.s00001074.output.s00000918>0,'callToTask.s00001074.output.s00001078+-1callToTask.s00001074.output.s00001078>0,'callToTask.s00001075.input.s00000737+-1callToTask.s00001075.input.s00000737>0,'callToTask.s00001075.inputCriterion.s00000858.used+-1callToTask.s00001075.inputCriterion.s00000858.used>0,'callToTask.s00001075.output.s00000713+-1callToTask.s00001075.outp