Skip to content

GitLab

2.12.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

Commit 4f283fdf authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Tested ibm benchmark for termination by reachability

parent 1363ee6d
Expand all Hide whitespace changes
Inline Side-by-side
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000021__s00000698.lola.terminating 0 → 100644
View file @ 4f283fdf
PLACE 'sigma,'m1,'m2,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,'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,'m1:1,alpha:1;
TRANSITION 'switch
CONSUME 'm1:1;
PRODUCE 'm2:1;
TRANSITION callToTask.s00000743.inputCriterion.s00000700
CONSUME 'callToTask.s00000743.input.s00000699:1,'callToTask.s00000743.input.s00000709:1,callToTask.s00000743.input.s00000699:1,callToTask.s00000743.input.s00000709:1,'m1:1;
PRODUCE 'callToTask.s00000743.inputCriterion.s00000700.used:1,callToTask.s00000743.inputCriterion.s00000700.used:1,'m1:1;
TRANSITION 'callToTask.s00000743.inputCriterion.s00000700
CONSUME 'callToTask.s00000743.input.s00000699:1,'callToTask.s00000743.input.s00000709:1,'m2:1;
PRODUCE 'callToTask.s00000743.inputCriterion.s00000700.used:1,'sigma:1,'m2:1;
TRANSITION callToTask.s00000743.outputCriterion.s00000704
CONSUME 'callToTask.s00000743.inputCriterion.s00000700.used:1,callToTask.s00000743.inputCriterion.s00000700.used:1,'m1:1;
PRODUCE 'callToTask.s00000743.output.s00000713:1,'callToTask.s00000743.output.s00000754:1,callToTask.s00000743.output.s00000713:1,callToTask.s00000743.output.s00000754:1,'m1:1;
TRANSITION 'callToTask.s00000743.outputCriterion.s00000704
CONSUME 'callToTask.s00000743.inputCriterion.s00000700.used:1,'m2:1;
PRODUCE 'callToTask.s00000743.output.s00000713:1,'callToTask.s00000743.output.s00000754:1,'sigma:1,'m2:1;
TRANSITION callToTask.s00000744.inputCriterion.s00000700
CONSUME 'callToTask.s00000744.input.s00000709:1,'callToTask.s00000744.input.s00000752:1,callToTask.s00000744.input.s00000709:1,callToTask.s00000744.input.s00000752:1,'m1:1;
PRODUCE 'callToTask.s00000744.inputCriterion.s00000700.used:1,callToTask.s00000744.inputCriterion.s00000700.used:1,'m1:1;
TRANSITION 'callToTask.s00000744.inputCriterion.s00000700
CONSUME 'callToTask.s00000744.input.s00000709:1,'callToTask.s00000744.input.s00000752:1,'m2:1;
PRODUCE 'callToTask.s00000744.inputCriterion.s00000700.used:1,'sigma:1,'m2:1;
TRANSITION callToTask.s00000744.outputCriterion.s00000704
CONSUME 'callToTask.s00000744.inputCriterion.s00000700.used:1,callToTask.s00000744.inputCriterion.s00000700.used:1,'m1:1;
PRODUCE 'callToTask.s00000744.output.s00000713:1,'callToTask.s00000744.output.s00000754:1,callToTask.s00000744.output.s00000713:1,callToTask.s00000744.output.s00000754:1,'m1:1;
TRANSITION 'callToTask.s00000744.outputCriterion.s00000704
CONSUME 'callToTask.s00000744.inputCriterion.s00000700.used:1,'m2:1;
PRODUCE 'callToTask.s00000744.output.s00000713:1,'callToTask.s00000744.output.s00000754:1,'sigma:1,'m2:1;
TRANSITION callToTask.s00000745.inputCriterion.s00000700
CONSUME 'callToTask.s00000745.input.s00000699:1,'callToTask.s00000745.input.s00000709:1,callToTask.s00000745.input.s00000699:1,callToTask.s00000745.input.s00000709:1,'m1:1;
PRODUCE 'callToTask.s00000745.inputCriterion.s00000700.used:1,callToTask.s00000745.inputCriterion.s00000700.used:1,'m1:1;
TRANSITION 'callToTask.s00000745.inputCriterion.s00000700
CONSUME 'callToTask.s00000745.input.s00000699:1,'callToTask.s00000745.input.s00000709:1,'m2:1;
PRODUCE 'callToTask.s00000745.inputCriterion.s00000700.used:1,'sigma:1,'m2:1;
TRANSITION callToTask.s00000745.outputCriterion.s00000704
CONSUME 'callToTask.s00000745.inputCriterion.s00000700.used:1,callToTask.s00000745.inputCriterion.s00000700.used:1,'m1:1;
PRODUCE 'callToTask.s00000745.output.s00000702:1,'callToTask.s00000745.output.s00000713:1,'callToTask.s00000745.output.s00000754:1,callToTask.s00000745.output.s00000702:1,callToTask.s00000745.output.s00000713:1,callToTask.s00000745.output.s00000754:1,'m1:1;
TRANSITION 'callToTask.s00000745.outputCriterion.s00000704
CONSUME 'callToTask.s00000745.inputCriterion.s00000700.used:1,'m2:1;
PRODUCE 'callToTask.s00000745.output.s00000702:1,'callToTask.s00000745.output.s00000713:1,'callToTask.s00000745.output.s00000754:1,'sigma:1,'m2:1;
TRANSITION callToTask.s00000746.inputCriterion.s00000700
CONSUME 'callToTask.s00000746.input.s00000699:1,'callToTask.s00000746.input.s00000709:1,callToTask.s00000746.input.s00000699:1,callToTask.s00000746.input.s00000709:1,'m1:1;
PRODUCE 'callToTask.s00000746.inputCriterion.s00000700.used:1,callToTask.s00000746.inputCriterion.s00000700.used:1,'m1:1;
TRANSITION 'callToTask.s00000746.inputCriterion.s00000700
CONSUME 'callToTask.s00000746.input.s00000699:1,'callToTask.s00000746.input.s00000709:1,'m2:1;
PRODUCE 'callToTask.s00000746.inputCriterion.s00000700.used:1,'sigma:1,'m2:1;
TRANSITION callToTask.s00000746.outputCriterion.s00000704
CONSUME 'callToTask.s00000746.inputCriterion.s00000700.used:1,callToTask.s00000746.inputCriterion.s00000700.used:1,'m1:1;
PRODUCE 'callToTask.s00000746.output.s00000703:1,'callToTask.s00000746.output.s00000713:1,'callToTask.s00000746.output.s00000754:1,callToTask.s00000746.output.s00000703:1,callToTask.s00000746.output.s00000713:1,callToTask.s00000746.output.s00000754:1,'m1:1;
TRANSITION 'callToTask.s00000746.outputCriterion.s00000704
CONSUME 'callToTask.s00000746.inputCriterion.s00000700.used:1,'m2:1;
PRODUCE 'callToTask.s00000746.output.s00000703:1,'callToTask.s00000746.output.s00000713:1,'callToTask.s00000746.output.s00000754:1,'sigma:1,'m2:1;
TRANSITION callToTask.s00000747.inputCriterion.s00000700
CONSUME 'callToTask.s00000747.input.s00000699:1,'callToTask.s00000747.input.s00000709:1,callToTask.s00000747.input.s00000699:1,callToTask.s00000747.input.s00000709:1,'m1:1;
PRODUCE 'callToTask.s00000747.inputCriterion.s00000700.used:1,callToTask.s00000747.inputCriterion.s00000700.used:1,'m1:1;
TRANSITION 'callToTask.s00000747.inputCriterion.s00000700
CONSUME 'callToTask.s00000747.input.s00000699:1,'callToTask.s00000747.input.s00000709:1,'m2:1;
PRODUCE 'callToTask.s00000747.inputCriterion.s00000700.used:1,'sigma:1,'m2:1;
TRANSITION callToTask.s00000747.outputCriterion.s00000704
CONSUME 'callToTask.s00000747.inputCriterion.s00000700.used:1,callToTask.s00000747.inputCriterion.s00000700.used:1,'m1:1;
PRODUCE 'callToTask.s00000747.output.s00000713:1,'callToTask.s00000747.output.s00000754:1,callToTask.s00000747.output.s00000713:1,callToTask.s00000747.output.s00000754:1,'m1:1;
TRANSITION 'callToTask.s00000747.outputCriterion.s00000704
CONSUME 'callToTask.s00000747.inputCriterion.s00000700.used:1,'m2:1;
PRODUCE 'callToTask.s00000747.output.s00000713:1,'callToTask.s00000747.output.s00000754:1,'sigma:1,'m2:1;
TRANSITION callToTask.s00000748.inputCriterion.s00000700
CONSUME 'callToTask.s00000748.input.s00000699:1,'callToTask.s00000748.input.s00000709:1,callToTask.s00000748.input.s00000699:1,callToTask.s00000748.input.s00000709:1,'m1:1;
PRODUCE 'callToTask.s00000748.inputCriterion.s00000700.used:1,callToTask.s00000748.inputCriterion.s00000700.used:1,'m1:1;
TRANSITION 'callToTask.s00000748.inputCriterion.s00000700
CONSUME 'callToTask.s00000748.input.s00000699:1,'callToTask.s00000748.input.s00000709:1,'m2:1;
PRODUCE 'callToTask.s00000748.inputCriterion.s00000700.used:1,'sigma:1,'m2:1;
TRANSITION callToTask.s00000748.outputCriterion.s00000704
CONSUME 'callToTask.s00000748.inputCriterion.s00000700.used:1,callToTask.s00000748.inputCriterion.s00000700.used:1,'m1:1;
PRODUCE 'callToTask.s00000748.output.s00000713:1,'callToTask.s00000748.output.s00000754:1,callToTask.s00000748.output.s00000713:1,callToTask.s00000748.output.s00000754:1,'m1:1;
TRANSITION 'callToTask.s00000748.outputCriterion.s00000704
CONSUME 'callToTask.s00000748.inputCriterion.s00000700.used:1,'m2:1;
PRODUCE 'callToTask.s00000748.output.s00000713:1,'callToTask.s00000748.output.s00000754:1,'sigma:1,'m2:1;
TRANSITION decision.s00000707.activate.s00000708
CONSUME 'callToTask.s00000747.output.s00000713:1,'callToTask.s00000747.output.s00000754:1,callToTask.s00000747.output.s00000713:1,callToTask.s00000747.output.s00000754:1,'m1:1;
PRODUCE 'decision.s00000707.activated:1,decision.s00000707.activated:1,'m1:1;
TRANSITION 'decision.s00000707.activate.s00000708
CONSUME 'callToTask.s00000747.output.s00000713:1,'callToTask.s00000747.output.s00000754:1,'m2:1;
PRODUCE 'decision.s00000707.activated:1,'sigma:1,'m2:1;
TRANSITION decision.s00000707.fire.s00000711
CONSUME 'decision.s00000707.activated:1,decision.s00000707.activated:1,'m1:1;
PRODUCE 'endNode.s00000706.input.default:1,'process.s00000021##s00000698.output.s00000701:1,endNode.s00000706.input.default:1,process.s00000021##s00000698.output.s00000701:1,'m1:1;
TRANSITION 'decision.s00000707.fire.s00000711
CONSUME 'decision.s00000707.activated:1,'m2:1;
PRODUCE 'endNode.s00000706.input.default:1,'process.s00000021##s00000698.output.s00000701:1,'sigma:1,'m2:1;
TRANSITION decision.s00000707.fire.s00000715
CONSUME 'decision.s00000707.activated:1,decision.s00000707.activated:1,'m1:1;
PRODUCE 'merge.s00000742.input.s00000737:1,'merge.s00000742.input.s00000740:1,merge.s00000742.input.s00000737:1,merge.s00000742.input.s00000740:1,'m1:1;
TRANSITION 'decision.s00000707.fire.s00000715
CONSUME 'decision.s00000707.activated:1,'m2:1;
PRODUCE 'merge.s00000742.input.s00000737:1,'merge.s00000742.input.s00000740:1,'sigma:1,'m2:1;
TRANSITION decision.s00000719.activate.s00000708
CONSUME 'callToTask.s00000748.output.s00000713:1,'callToTask.s00000748.output.s00000754:1,callToTask.s00000748.output.s00000713:1,callToTask.s00000748.output.s00000754:1,'m1:1;
PRODUCE 'decision.s00000719.activated:1,decision.s00000719.activated:1,'m1:1;
TRANSITION 'decision.s00000719.activate.s00000708
CONSUME 'callToTask.s00000748.output.s00000713:1,'callToTask.s00000748.output.s00000754:1,'m2:1;
PRODUCE 'decision.s00000719.activated:1,'sigma:1,'m2:1;
TRANSITION decision.s00000719.fire.s00000711
CONSUME 'decision.s00000719.activated:1,decision.s00000719.activated:1,'m1:1;
PRODUCE 'callToTask.s00000744.input.s00000709:1,'callToTask.s00000744.input.s00000752:1,callToTask.s00000744.input.s00000709:1,callToTask.s00000744.input.s00000752:1,'m1:1;
TRANSITION 'decision.s00000719.fire.s00000711
CONSUME 'decision.s00000719.activated:1,'m2:1;
PRODUCE 'callToTask.s00000744.input.s00000709:1,'callToTask.s00000744.input.s00000752:1,'sigma:1,'m2:1;
TRANSITION decision.s00000719.fire.s00000715
CONSUME 'decision.s00000719.activated:1,decision.s00000719.activated:1,'m1:1;
PRODUCE 'callToTask.s00000745.input.s00000699:1,'callToTask.s00000745.input.s00000709:1,callToTask.s00000745.input.s00000699:1,callToTask.s00000745.input.s00000709:1,'m1:1;
TRANSITION 'decision.s00000719.fire.s00000715
CONSUME 'decision.s00000719.activated:1,'m2:1;
PRODUCE 'callToTask.s00000745.input.s00000699:1,'callToTask.s00000745.input.s00000709:1,'sigma:1,'m2:1;
TRANSITION decision.s00000719.fire.s00000724
CONSUME 'decision.s00000719.activated:1,decision.s00000719.activated:1,'m1:1;
PRODUCE 'callToTask.s00000746.input.s00000699:1,'callToTask.s00000746.input.s00000709:1,callToTask.s00000746.input.s00000699:1,callToTask.s00000746.input.s00000709:1,'m1:1;
TRANSITION 'decision.s00000719.fire.s00000724
CONSUME 'decision.s00000719.activated:1,'m2:1;
PRODUCE 'callToTask.s00000746.input.s00000699:1,'callToTask.s00000746.input.s00000709:1,'sigma:1,'m2:1;
TRANSITION decision.s00000719.fire.s00000727
CONSUME 'decision.s00000719.activated:1,decision.s00000719.activated:1,'m1:1;
PRODUCE 'callToTask.s00000743.input.s00000699:1,'callToTask.s00000743.input.s00000709:1,callToTask.s00000743.input.s00000699:1,callToTask.s00000743.input.s00000709:1,'m1:1;
TRANSITION 'decision.s00000719.fire.s00000727
CONSUME 'decision.s00000719.activated:1,'m2:1;
PRODUCE 'callToTask.s00000743.input.s00000699:1,'callToTask.s00000743.input.s00000709:1,'sigma:1,'m2:1;
TRANSITION merge.s00000730.activate.s00000731
CONSUME 'callToTask.s00000744.output.s00000713:1,'callToTask.s00000744.output.s00000754:1,callToTask.s00000744.output.s00000713:1,callToTask.s00000744.output.s00000754:1,'m1:1;
PRODUCE 'merge.s00000730.activated:1,merge.s00000730.activated:1,'m1:1;
TRANSITION 'merge.s00000730.activate.s00000731
CONSUME 'callToTask.s00000744.output.s00000713:1,'callToTask.s00000744.output.s00000754:1,'m2:1;
PRODUCE 'merge.s00000730.activated:1,'sigma:1,'m2:1;
TRANSITION merge.s00000730.activate.s00000733
CONSUME 'callToTask.s00000745.output.s00000713:1,'callToTask.s00000745.output.s00000754:1,callToTask.s00000745.output.s00000713:1,callToTask.s00000745.output.s00000754:1,'m1:1;
PRODUCE 'merge.s00000730.activated:1,merge.s00000730.activated:1,'m1:1;
TRANSITION 'merge.s00000730.activate.s00000733
CONSUME 'callToTask.s00000745.output.s00000713:1,'callToTask.s00000745.output.s00000754:1,'m2:1;
PRODUCE 'merge.s00000730.activated:1,'sigma:1,'m2:1;
TRANSITION merge.s00000730.activate.s00000735
CONSUME 'callToTask.s00000746.output.s00000713:1,'callToTask.s00000746.output.s00000754:1,callToTask.s00000746.output.s00000713:1,callToTask.s00000746.output.s00000754:1,'m1:1;
PRODUCE 'merge.s00000730.activated:1,merge.s00000730.activated:1,'m1:1;
TRANSITION 'merge.s00000730.activate.s00000735
CONSUME 'callToTask.s00000746.output.s00000713:1,'callToTask.s00000746.output.s00000754:1,'m2:1;
PRODUCE 'merge.s00000730.activated:1,'sigma:1,'m2:1;
TRANSITION merge.s00000730.activate.s00000738
CONSUME 'callToTask.s00000743.output.s00000713:1,'callToTask.s00000743.output.s00000754:1,callToTask.s00000743.output.s00000713:1,callToTask.s00000743.output.s00000754:1,'m1:1;
PRODUCE 'merge.s00000730.activated:1,merge.s00000730.activated:1,'m1:1;
TRANSITION 'merge.s00000730.activate.s00000738
CONSUME 'callToTask.s00000743.output.s00000713:1,'callToTask.s00000743.output.s00000754:1,'m2:1;
PRODUCE 'merge.s00000730.activated:1,'sigma:1,'m2:1;
TRANSITION merge.s00000730.fire.s00000741
CONSUME 'merge.s00000730.activated:1,merge.s00000730.activated:1,'m1:1;
PRODUCE 'callToTask.s00000747.input.s00000699:1,'callToTask.s00000747.input.s00000709:1,callToTask.s00000747.input.s00000699:1,callToTask.s00000747.input.s00000709:1,'m1:1;
TRANSITION 'merge.s00000730.fire.s00000741
CONSUME 'merge.s00000730.activated:1,'m2:1;
PRODUCE 'callToTask.s00000747.input.s00000699:1,'callToTask.s00000747.input.s00000709:1,'sigma:1,'m2:1;
TRANSITION merge.s00000742.activate.s00000731
CONSUME 'merge.s00000742.input.s00000709:1,'process.s00000021##s00000698.input.s00000699:1,merge.s00000742.input.s00000709:1,process.s00000021##s00000698.input.s00000699:1,'m1:1;
PRODUCE 'merge.s00000742.activated:1,merge.s00000742.activated:1,'m1:1;
TRANSITION 'merge.s00000742.activate.s00000731
CONSUME 'merge.s00000742.input.s00000709:1,'process.s00000021##s00000698.input.s00000699:1,'m2:1;
PRODUCE 'merge.s00000742.activated:1,'sigma:1,'m2:1;
TRANSITION merge.s00000742.activate.s00000733
CONSUME 'merge.s00000742.input.s00000737:1,'merge.s00000742.input.s00000740:1,merge.s00000742.input.s00000737:1,merge.s00000742.input.s00000740:1,'m1:1;
PRODUCE 'merge.s00000742.activated:1,merge.s00000742.activated:1,'m1:1;
TRANSITION 'merge.s00000742.activate.s00000733
CONSUME 'merge.s00000742.input.s00000737:1,'merge.s00000742.input.s00000740:1,'m2:1;
PRODUCE 'merge.s00000742.activated:1,'sigma:1,'m2:1;
TRANSITION merge.s00000742.fire.s00000741
CONSUME 'merge.s00000742.activated:1,merge.s00000742.activated:1,'m1:1;
PRODUCE 'callToTask.s00000748.input.s00000699:1,'callToTask.s00000748.input.s00000709:1,callToTask.s00000748.input.s00000699:1,callToTask.s00000748.input.s00000709:1,'m1:1;
TRANSITION 'merge.s00000742.fire.s00000741
CONSUME 'merge.s00000742.activated:1,'m2:1;
PRODUCE 'callToTask.s00000748.input.s00000699:1,'callToTask.s00000748.input.s00000709:1,'sigma:1,'m2:1;
TRANSITION process.s00000021##s00000698.inputCriterion.s00000700
CONSUME 'alpha:1,alpha:1,'m1:1;
PRODUCE 'merge.s00000742.input.s00000709:1,'process.s00000021##s00000698.input.s00000699:1,merge.s00000742.input.s00000709:1,process.s00000021##s00000698.input.s00000699:1,'m1:1;
TRANSITION 'process.s00000021##s00000698.inputCriterion.s00000700
CONSUME 'alpha:1,'m2:1;
PRODUCE 'merge.s00000742.input.s00000709:1,'process.s00000021##s00000698.input.s00000699:1,'sigma:1,'m2:1;
TRANSITION process.s00000021##s00000698.outputCriterion.s00000704
CONSUME 'callToTask.s00000745.output.s00000702:1,'callToTask.s00000746.output.s00000703:1,'process.s00000021##s00000698.output.s00000701:1,callToTask.s00000745.output.s00000702:1,callToTask.s00000746.output.s00000703:1,process.s00000021##s00000698.output.s00000701:1,'m1:1;
PRODUCE 'process.s00000021##s00000698.outputCriterion.s00000704_omega:1,process.s00000021##s00000698.outputCriterion.s00000704_omega:1,'m1:1;
TRANSITION 'process.s00000021##s00000698.outputCriterion.s00000704
CONSUME 'callToTask.s00000745.output.s00000702:1,'callToTask.s00000746.output.s00000703:1,'process.s00000021##s00000698.output.s00000701:1,'m2:1;
PRODUCE 'process.s00000021##s00000698.outputCriterion.s00000704_omega:1,'sigma:1,'m2:1;
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000021__s00000698.lola.terminating.task1 0 → 100644
View file @ 4f283fdf
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))
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000023__s00000777.lola.terminating.task1 0 → 100644
View file @ 4f283fdf
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))
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000023__s00000863.lola.terminating.task1 0 → 100644
View file @ 4f283fdf
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))
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000025__s00001059.lola.terminating.task1 0 → 100644
View file @ 4f283fdf
EF ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((('sigma >= 1 AND 'alpha >= alpha) AND 'callToProcess.s00001005.inputCriterion.s00000858.used >= callToProcess.s00001005.inputCriterion.s00000858.used) AND 'callToProcess.s00001005.output.s00000713 >= callToProcess.s00001005.output.s00000713) AND 'callToProcess.s00001009.inputCriterion.s00000700.used >= callToProcess.s00001009.inputCriterion.s00000700.used) AND 'callToProcess.s00001009.output.s00000713 >= callToProcess.s00001009.output.s00000713) AND 'callToProcess.s00001009.output.s00000849 >= callToProcess.s00001009.output.s00000849) AND 'callToProcess.s00001051.inputCriterion.s00000858.used >= callToProcess.s00001051.inputCriterion.s00000858.used) AND 'callToProcess.s00001051.output.s00000713 >= callToProcess.s00001051.output.s00000713) AND 'callToProcess.s00001051.output.s00000919 >= callToProcess.s00001051.output.s00000919) AND 'callToService.s00001076.inputCriterion.s00000700.used >= callToService.s00001076.inputCriterion.s00000700.used) AND 'callToService.s00001076.output.s00000713 >= callToService.s00001076.output.s00000713) AND 'callToService.s00001076.output.s00000866 >= callToService.s00001076.output.s00000866) AND 'callToService.s00001076.output.s00000918 >= callToService.s00001076.output.s00000918) AND 'callToService.s00001076.output.s00001078 >= callToService.s00001076.output.s00001078) AND 'callToService.s00001077.input.s00000709 >= callToService.s00001077.input.s00000709) AND 'callToService.s00001077.input.s00001080 >= callToService.s00001077.input.s00001080) AND 'callToService.s00001077.inputCriterion.s00000858.used >= callToService.s00001077.inputCriterion.s00000858.used) AND 'callToService.s00001077.output.s00000713 >= callToService.s00001077.output.s00000713) AND 'callToService.s00001077.output.s00001027 >= callToService.s00001077.output.s00001027) AND 'callToTask.s00001020.input.s00000709 >= callToTask.s00001020.input.s00000709) AND 'callToTask.s00001020.input.s00001079 >= callToTask.s00001020.input.s00001079) AND 'callToTask.s00001020.input.s00001080 >= callToTask.s00001020.input.s00001080) AND 'callToTask.s00001020.inputCriterion.s00000700.used >= callToTask.s00001020.inputCriterion.s00000700.used) AND 'callToTask.s00001020.output.s00000713 >= callToTask.s00001020.output.s00000713) AND 'callToTask.s00001020.output.s00000866 >= callToTask.s00001020.output.s00000866) AND 'callToTask.s00001020.output.s00000961 >= callToTask.s00001020.output.s00000961) AND 'callToTask.s00001073.input.s00000709 >= callToTask.s00001073.input.s00000709) AND 'callToTask.s00001073.input.s00000916 >= callToTask.s00001073.input.s00000916) AND 'callToTask.s00001073.input.s00001079 >= callToTask.s00001073.input.s00001079) AND 'callToTask.s00001073.input.s00001080 >= callToTask.s00001073.input.s00001080) AND 'callToTask.s00001073.inputCriterion.s00000858.used >= callToTask.s00001073.inputCriterion.s00000858.used) AND 'callToTask.s00001073.output.s00000713 >= callToTask.s00001073.output.s00000713) AND 'callToTask.s00001073.output.s00000866 >= callToTask.s00001073.output.s00000866) AND 'callToTask.s00001073.output.s00001078 >= callToTask.s00001073.output.s00001078) AND 'callToTask.s00001074.input.s00000709 >= callToTask.s00001074.input.s00000709) AND 'callToTask.s00001074.input.s00001080 >= callToTask.s00001074.input.s00001080) AND 'callToTask.s00001074.inputCriterion.s00000858.used >= callToTask.s00001074.inputCriterion.s00000858.used) AND 'callToTask.s00001074.output.s00000713 >= callToTask.s00001074.output.s00000713) AND 'callToTask.s00001074.output.s00000866 >= callToTask.s00001074.output.s00000866) AND 'callToTask.s00001074.output.s00000918 >= callToTask.s00001074.output.s00000918) AND 'callToTask.s00001074.output.s00001078 >= callToTask.s00001074.output.s00001078) AND 'callToTask.s00001075.input.s00000737 >= callToTask.s00001075.input.s00000737) AND 'callToTask.s00001075.inputCriterion.s00000858.used >= callToTask.s00001075.inputCriterion.s00000858.used) AND 'callToTask.s00001075.output.s00000713 >= callToTask.s00001075.output.s00000713) AND 'callToTask.s00001075.output.s00000866 >= callToTask.s00001075.output.s00000866) AND 'callToTask.s00001075.output.s00001078 >= callToTask.s00001075.output.s00001078) AND 'decision.s00001060.activated >= decision.s00001060.activated) AND 'decision.s00001063.activated >= decision.s00001063.activated) AND 'decision.s00001063.input.s00000709 >= decision.s00001063.input.s00000709) AND 'decision.s00001063.input.s00000710 >= decision.s00001063.input.s00000710) AND 'decision.s00001066.activated >= decision.s00001066.activated) AND 'decision.s00001070.activated >= decision.s00001070.activated) AND 'endNode.s00000706.input.default >= endNode.s00000706.input.default) AND 'endNode.s00000952.input.default >= endNode.s00000952.input.default) AND 'fork.s00000981.activated.s00000711 >= fork.s00000981.activated.s00000711) AND 'fork.s00000981.activated.s00000715 >= fork.s00000981.activated.s00000715) AND 'fork.s00000981.input.s00000709 >= fork.s00000981.input.s00000709) AND 'fork.s00000981.input.s00000710 >= fork.s00000981.input.s00000710) AND 'fork.s00000981.input.s00000737 >= fork.s00000981.input.s00000737) AND 'merge.s00000730.activated >= merge.s00000730.activated) AND 'merge.s00000730.input.s00000709 >= merge.s00000730.input.s00000709) AND 'merge.s00000730.input.s00000710 >= merge.s00000730.input.s00000710) AND 'merge.s00000730.input.s00000734 >= merge.s00000730.input.s00000734) AND 'merge.s00000730.input.s00000736 >= merge.s00000730.input.s00000736) AND 'merge.s00000730.input.s00000737 >= merge.s00000730.input.s00000737) AND 'merge.s00000730.input.s00000740 >= merge.s00000730.input.s00000740) 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.s00000734 >= merge.s00000742.input.s00000734) AND 'merge.s00000742.input.s00000736 >= merge.s00000742.input.s00000736) AND 'merge.s00000742.input.s00000737 >= merge.s00000742.input.s00000737) AND 'merge.s00000742.input.s00000740 >= merge.s00000742.input.s00000740) AND 'merge.s00000856.activated >= merge.s00000856.activated) AND 'merge.s00000856.input.s00000710 >= merge.s00000856.input.s00000710) AND 'process.s00000025##s00001059.input.s00000847 >= process.s00000025##s00001059.input.s00000847) AND 'process.s00000025##s00001059.output.s00000866 >= process.s00000025##s00001059.output.s00000866) AND 'process.s00000025##s00001059.outputCriterion.s00000704_omega >= process.s00000025##s00001059.outputCriterion.s00000704_omega))
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000025__s00001098.lola.terminating.task1 0 → 100644
View file @ 4f283fdf
EF (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((('sigma >= 1 AND 'alpha >= alpha) AND 'callToProcess.s00000846.input.s00000709 >= callToProcess.s00000846.input.s00000709) AND 'callToProcess.s00000846.input.s00000847 >= callToProcess.s00000846.input.s00000847) AND 'callToProcess.s00000846.inputCriterion.s00000700.used >= callToProcess.s00000846.inputCriterion.s00000700.used) AND 'callToProcess.s00000846.output.s00000713 >= callToProcess.s00000846.output.s00000713) AND 'callToProcess.s00000846.output.s00000849 >= callToProcess.s00000846.output.s00000849) AND 'callToProcess.s00001009.inputCriterion.s00000700.used >= callToProcess.s00001009.inputCriterion.s00000700.used) AND 'callToProcess.s00001009.output.s00000713 >= callToProcess.s00001009.output.s00000713) AND 'callToProcess.s00001009.output.s00000849 >= callToProcess.s00001009.output.s00000849) AND 'callToProcess.s00001059.input.s00000709 >= callToProcess.s00001059.input.s00000709) AND 'callToProcess.s00001059.input.s00000847 >= callToProcess.s00001059.input.s00000847) AND 'callToProcess.s00001059.inputCriterion.s00000700.used >= callToProcess.s00001059.inputCriterion.s00000700.used) AND 'callToProcess.s00001059.output.s00000717 >= callToProcess.s00001059.output.s00000717) AND 'callToProcess.s00001081.input.s00000709 >= callToProcess.s00001081.input.s00000709) AND 'callToProcess.s00001081.input.s00000847 >= callToProcess.s00001081.input.s00000847) AND 'callToProcess.s00001081.inputCriterion.s00000700.used >= callToProcess.s00001081.inputCriterion.s00000700.used) AND 'callToProcess.s00001081.output.s00000713 >= callToProcess.s00001081.output.s00000713) AND 'callToProcess.s00001081.output.s00000849 >= callToProcess.s00001081.output.s00000849) AND 'callToProcess.s00001081.output.s00000867 >= callToProcess.s00001081.output.s00000867) AND 'callToService.s00001114.input.s00000709 >= callToService.s00001114.input.s00000709) AND 'callToService.s00001114.inputCriterion.s00000700.used >= callToService.s00001114.inputCriterion.s00000700.used) AND 'callToService.s00001114.output.s00000713 >= callToService.s00001114.output.s00000713) AND 'callToService.s00001114.output.s00000849 >= callToService.s00001114.output.s00000849) AND 'callToService.s00001114.output.s00001027 >= callToService.s00001114.output.s00001027) AND 'callToService.s00001115.inputCriterion.s00000700.used >= callToService.s00001115.inputCriterion.s00000700.used) AND 'callToService.s00001115.output.s00000713 >= callToService.s00001115.output.s00000713) AND 'callToService.s00001115.output.s00000849 >= callToService.s00001115.output.s00000849) AND 'callToTask.s00001075.inputCriterion.s00000858.used >= callToTask.s00001075.inputCriterion.s00000858.used) AND 'callToTask.s00001075.output.s00000713 >= callToTask.s00001075.output.s00000713) AND 'callToTask.s00001075.output.s00000848 >= callToTask.s00001075.output.s00000848) AND 'callToTask.s00001108.input.s00000709 >= callToTask.s00001108.input.s00000709) AND 'callToTask.s00001108.input.s00000861 >= callToTask.s00001108.input.s00000861) AND 'callToTask.s00001108.input.s00001028 >= callToTask.s00001108.input.s00001028) AND 'callToTask.s00001108.inputCriterion.s00000700.used >= callToTask.s00001108.inputCriterion.s00000700.used) AND 'callToTask.s00001108.output.s00000713 >= callToTask.s00001108.output.s00000713) AND 'callToTask.s00001108.output.s00000848 >= callToTask.s00001108.output.s00000848) AND 'callToTask.s00001108.output.s00001029 >= callToTask.s00001108.output.s00001029) AND 'callToTask.s00001109.inputCriterion.s00000700.used >= callToTask.s00001109.inputCriterion.s00000700.used) AND 'callToTask.s00001109.output.s00000713 >= callToTask.s00001109.output.s00000713) AND 'callToTask.s00001109.output.s00000900 >= callToTask.s00001109.output.s00000900) AND 'callToTask.s00001109.output.s00001029 >= callToTask.s00001109.output.s00001029) AND 'callToTask.s00001110.inputCriterion.s00000700.used >= callToTask.s00001110.inputCriterion.s00000700.used) AND 'callToTask.s00001110.output.s00000713 >= callToTask.s00001110.output.s00000713) AND 'callToTask.s00001110.output.s00001029 >= callToTask.s00001110.output.s00001029) AND 'callToTask.s00001111.input.s00000709 >= callToTask.s00001111.input.s00000709) AND 'callToTask.s00001111.input.s00001028 >= callToTask.s00001111.input.s00001028) AND 'callToTask.s00001111.inputCriterion.s00000700.used >= callToTask.s00001111.inputCriterion.s00000700.used) AND 'callToTask.s00001111.output.s00000713 >= callToTask.s00001111.output.s00000713) AND 'callToTask.s00001111.output.s00000848 >= callToTask.s00001111.output.s00000848) AND 'callToTask.s00001111.output.s00001029 >= callToTask.s00001111.output.s00001029) AND 'callToTask.s00001112.inputCriterion.s00000700.used >= callToTask.s00001112.inputCriterion.s00000700.used) AND 'callToTask.s00001112.output.s00000713 >= callToTask.s00001112.output.s00000713) AND 'callToTask.s00001112.output.s00000849 >= callToTask.s00001112.output.s00000849) AND 'callToTask.s00001113.inputCriterion.s00000858.used >= callToTask.s00001113.inputCriterion.s00000858.used) AND 'callToTask.s00001113.output.s00000713 >= callToTask.s00001113.output.s00000713) AND 'callToTask.s00001113.output.s00000849 >= callToTask.s00001113.output.s00000849) AND 'decision.s00001099.activated >= decision.s00001099.activated) AND 'decision.s00001102.activated >= decision.s00001102.activated) AND 'decision.s00001105.activated >= decision.s00001105.activated) AND 'endNode.s00000706.input.default >= endNode.s00000706.input.default) AND 'merge.s00000730.activated >= merge.s00000730.activated) AND 'merge.s00000730.input.s00000709 >= merge.s00000730.input.s00000709) AND 'merge.s00000730.input.s00000732 >= merge.s00000730.input.s00000732) AND 'merge.s00000730.input.s00000736 >= merge.s00000730.input.s00000736) AND 'merge.s00000730.input.s00000737 >= merge.s00000730.input.s00000737) AND 'merge.s00000730.input.s00000740 >= merge.s00000730.input.s00000740) AND 'merge.s00000742.activated >= merge.s00000742.activated) AND 'merge.s00000742.input.s00000737 >= merge.s00000742.input.s00000737) AND 'process.s00000025##s00001098.input.s00000847 >= process.s00000025##s00001098.input.s00000847) AND 'process.s00000025##s00001098.output.s00000849 >= process.s00000025##s00001098.output.s00000849) AND 'process.s00000025##s00001098.outputCriterion.s00000704_omega >= process.s00000025##s00001098.outputCriterion.s00000704_omega))
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000029__s00001009.lola.terminating.task1 0 → 100644
View file @ 4f283fdf
EF (((((((((((((((((((((((((((((((((((((((((((((((((((((('sigma >= 1 AND 'alpha >= alpha) AND 'callToProcess.s00001005.inputCriterion.s00000858.used >= callToProcess.s00001005.inputCriterion.s00000858.used) AND 'callToProcess.s00001005.output.s00000713 >= callToProcess.s00001005.output.s00000713) AND 'callToProcess.s00001005.output.s00000961 >= callToProcess.s00001005.output.s00000961) AND 'callToService.s00001024.inputCriterion.s00000700.used >= callToService.s00001024.inputCriterion.s00000700.used) AND 'callToService.s00001024.output.s00000713 >= callToService.s00001024.output.s00000713) AND 'callToService.s00001024.output.s00001029 >= callToService.s00001024.output.s00001029) AND 'callToTask.s00001020.inputCriterion.s00000700.used >= callToTask.s00001020.inputCriterion.s00000700.used) AND 'callToTask.s00001020.output.s00000713 >= callToTask.s00001020.output.s00000713) AND 'callToTask.s00001020.output.s00000866 >= callToTask.s00001020.output.s00000866) AND 'callToTask.s00001020.output.s00000961 >= callToTask.s00001020.output.s00000961) AND 'callToTask.s00001021.input.s00000709 >= callToTask.s00001021.input.s00000709) AND 'callToTask.s00001021.input.s00000847 >= callToTask.s00001021.input.s00000847) AND 'callToTask.s00001021.input.s00001010 >= callToTask.s00001021.input.s00001010) AND 'callToTask.s00001021.inputCriterion.s00000700.used >= callToTask.s00001021.inputCriterion.s00000700.used) AND 'callToTask.s00001021.output.s00000713 >= callToTask.s00001021.output.s00000713) AND 'callToTask.s00001021.output.s00000849 >= callToTask.s00001021.output.s00000849) AND 'callToTask.s00001021.output.s00001027 >= callToTask.s00001021.output.s00001027) AND 'callToTask.s00001022.input.s00000709 >= callToTask.s00001022.input.s00000709) AND 'callToTask.s00001022.input.s00000847 >= callToTask.s00001022.input.s00000847) AND 'callToTask.s00001022.input.s00001010 >= callToTask.s00001022.input.s00001010) AND 'callToTask.s00001022.inputCriterion.s00000700.used >= callToTask.s00001022.inputCriterion.s00000700.used) AND 'callToTask.s00001022.output.s00000713 >= callToTask.s00001022.output.s00000713) AND 'callToTask.s00001022.output.s00000849 >= callToTask.s00001022.output.s00000849) AND 'callToTask.s00001023.input.s00000709 >= callToTask.s00001023.input.s00000709) AND 'callToTask.s00001023.input.s00000847 >= callToTask.s00001023.input.s00000847) AND 'callToTask.s00001023.inputCriterion.s00000700.used >= callToTask.s00001023.inputCriterion.s00000700.used) AND 'callToTask.s00001023.output.s00000713 >= callToTask.s00001023.output.s00000713) AND 'callToTask.s00001023.output.s00000849 >= callToTask.s00001023.output.s00000849) AND 'callToTask.s00001025.input.s00000709 >= callToTask.s00001025.input.s00000709) AND 'callToTask.s00001025.input.s00000847 >= callToTask.s00001025.input.s00000847) AND 'callToTask.s00001025.inputCriterion.s00000858.used >= callToTask.s00001025.inputCriterion.s00000858.used) AND 'callToTask.s00001025.output.s00000713 >= callToTask.s00001025.output.s00000713) AND 'callToTask.s00001025.output.s00000961 >= callToTask.s00001025.output.s00000961) AND 'callToTask.s00001026.inputCriterion.s00000858.used >= callToTask.s00001026.inputCriterion.s00000858.used) AND 'callToTask.s00001026.output.s00000713 >= callToTask.s00001026.output.s00000713) AND 'callToTask.s00001026.output.s00000849 >= callToTask.s00001026.output.s00000849) AND 'decision.s00001011.activated >= decision.s00001011.activated) AND 'decision.s00001014.activated >= decision.s00001014.activated) AND 'decision.s00001014.input.s00000710 >= decision.s00001014.input.s00000710) AND 'decision.s00001014.input.s00000737 >= decision.s00001014.input.s00000737) AND 'decision.s00001017.activated >= decision.s00001017.activated) AND 'endNode.s00000706.input.default >= endNode.s00000706.input.default) AND 'endNode.s00000850.input.default >= endNode.s00000850.input.default) AND 'merge.s00000730.activated >= merge.s00000730.activated) AND 'merge.s00000730.input.s00000710 >= merge.s00000730.input.s00000710) AND 'merge.s00000730.input.s00000737 >= merge.s00000730.input.s00000737) AND 'merge.s00000742.activated >= merge.s00000742.activated) AND 'merge.s00000742.input.s00000709 >= merge.s00000742.input.s00000709) AND 'process.s00000029##s00001009.input.s00000847 >= process.s00000029##s00001009.input.s00000847) AND 'process.s00000029##s00001009.input.s00001010 >= process.s00000029##s00001009.input.s00001010) AND 'process.s00000029##s00001009.output.s00000849 >= process.s00000029##s00001009.output.s00000849) AND 'process.s00000029##s00001009.outputCriterion.s00000704_omega >= process.s00000029##s00001009.outputCriterion.s00000704_omega))
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000029__s00001081.lola.terminating.task1 0 → 100644
View file @ 4f283fdf
EF ((((((((((((((((((((((((((((((((((((((((((((((((((((('sigma >= 1 AND 'alpha >= alpha) AND 'callToProcess.s00001009.inputCriterion.s00000700.used >= callToProcess.s00001009.inputCriterion.s00000700.used) AND 'callToProcess.s00001009.output.s00000713 >= callToProcess.s00001009.output.s00000713) AND 'callToProcess.s00001009.output.s00000849 >= callToProcess.s00001009.output.s00000849) AND 'callToProcess.s00001051.input.s00000709 >= callToProcess.s00001051.input.s00000709) AND 'callToProcess.s00001051.input.s00000847 >= callToProcess.s00001051.input.s00000847) AND 'callToProcess.s00001051.inputCriterion.s00000858.used >= callToProcess.s00001051.inputCriterion.s00000858.used) AND 'callToProcess.s00001051.output.s00000713 >= callToProcess.s00001051.output.s00000713) AND 'callToProcess.s00001051.output.s00000919 >= callToProcess.s00001051.output.s00000919) AND 'callToService.s00001096.input.s00000709 >= callToService.s00001096.input.s00000709) AND 'callToService.s00001096.inputCriterion.s00000700.used >= callToService.s00001096.inputCriterion.s00000700.used) AND 'callToService.s00001096.output.s00000713 >= callToService.s00001096.output.s00000713) AND 'callToService.s00001096.output.s00001027 >= callToService.s00001096.output.s00001027) AND 'callToService.s00001096.output.s00001029 >= callToService.s00001096.output.s00001029) AND 'callToTask.s00000887.input.s00000709 >= callToTask.s00000887.input.s00000709) AND 'callToTask.s00000887.input.s00000847 >= callToTask.s00000887.input.s00000847) AND 'callToTask.s00000887.inputCriterion.s00000858.used >= callToTask.s00000887.inputCriterion.s00000858.used) AND 'callToTask.s00000887.output.s00000713 >= callToTask.s00000887.output.s00000713) AND 'callToTask.s00000887.output.s00000849 >= callToTask.s00000887.output.s00000849) AND 'callToTask.s00000887.output.s00000867 >= callToTask.s00000887.output.s00000867) AND 'callToTask.s00001091.input.s00000709 >= callToTask.s00001091.input.s00000709) AND 'callToTask.s00001091.input.s00001028 >= callToTask.s00001091.input.s00001028) AND 'callToTask.s00001091.inputCriterion.s00000700.used >= callToTask.s00001091.inputCriterion.s00000700.used) AND 'callToTask.s00001091.output.s00000713 >= callToTask.s00001091.output.s00000713) AND 'callToTask.s00001091.output.s00001029 >= callToTask.s00001091.output.s00001029) AND 'callToTask.s00001092.inputCriterion.s00000700.used >= callToTask.s00001092.inputCriterion.s00000700.used) AND 'callToTask.s00001092.output.s00000713 >= callToTask.s00001092.output.s00000713) AND 'callToTask.s00001092.output.s00001029 >= callToTask.s00001092.output.s00001029) AND 'callToTask.s00001093.input.s00000709 >= callToTask.s00001093.input.s00000709) AND 'callToTask.s00001093.input.s00000847 >= callToTask.s00001093.input.s00000847) AND 'callToTask.s00001093.inputCriterion.s00000858.used >= callToTask.s00001093.inputCriterion.s00000858.used) AND 'callToTask.s00001093.output.s00000713 >= callToTask.s00001093.output.s00000713) AND 'callToTask.s00001093.output.s00000849 >= callToTask.s00001093.output.s00000849) AND 'callToTask.s00001094.inputCriterion.s00000700.used >= callToTask.s00001094.inputCriterion.s00000700.used) AND 'callToTask.s00001094.output.s00000713 >= callToTask.s00001094.output.s00000713) AND 'callToTask.s00001094.output.s00001082 >= callToTask.s00001094.output.s00001082) AND 'callToTask.s00001095.input.s00000709 >= callToTask.s00001095.input.s00000709) AND 'callToTask.s00001095.input.s00000847 >= callToTask.s00001095.input.s00000847) AND 'callToTask.s00001095.inputCriterion.s00000700.used >= callToTask.s00001095.inputCriterion.s00000700.used) AND 'callToTask.s00001095.output.s00000713 >= callToTask.s00001095.output.s00000713) AND 'callToTask.s00001095.output.s00001082 >= callToTask.s00001095.output.s00001082) AND 'decision.s00001083.activated >= decision.s00001083.activated) AND 'decision.s00001088.activated >= decision.s00001088.activated) AND 'endNode.s00000706.input.default >= endNode.s00000706.input.default) AND 'merge.s00000730.activated >= merge.s00000730.activated) AND 'merge.s00000730.input.s00000739 >= merge.s00000730.input.s00000739) AND 'merge.s00000730.input.s00000740 >= merge.s00000730.input.s00000740) AND 'merge.s00000742.activated >= merge.s00000742.activated) AND 'merge.s00000742.input.s00000710 >= merge.s00000742.input.s00000710) AND 'process.s00000029##s00001081.input.s00000847 >= process.s00000029##s00001081.input.s00000847) AND 'process.s00000029##s00001081.output.s00000849 >= process.s00000029##s00001081.output.s00000849) AND 'process.s00000029##s00001081.outputCriterion.s00000704_omega >= process.s00000029##s00001081.outputCriterion.s00000704_omega))
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000029__s00001116.lola.terminating.task1 0 → 100644
View file @ 4f283fdf
EF (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((('sigma >= 1 AND 'alpha >= alpha) AND 'callToProcess.s00001009.inputCriterion.s00000700.used >= callToProcess.s00001009.inputCriterion.s00000700.used) AND 'callToProcess.s00001009.output.s00000713 >= callToProcess.s00001009.output.s00000713) AND 'callToProcess.s00001009.output.s00000849 >= callToProcess.s00001009.output.s00000849) AND 'callToProcess.s00001059.input.s00000709 >= callToProcess.s00001059.input.s00000709) AND 'callToProcess.s00001059.input.s00000847 >= callToProcess.s00001059.input.s00000847) AND 'callToProcess.s00001059.inputCriterion.s00000700.used >= callToProcess.s00001059.inputCriterion.s00000700.used) AND 'callToProcess.s00001059.output.s00000713 >= callToProcess.s00001059.output.s00000713) AND 'callToProcess.s00001081.input.s00000709 >= callToProcess.s00001081.input.s00000709) AND 'callToProcess.s00001081.input.s00000847 >= callToProcess.s00001081.input.s00000847) AND 'callToProcess.s00001081.inputCriterion.s00000700.used >= callToProcess.s00001081.inputCriterion.s00000700.used) AND 'callToProcess.s00001081.output.s00000713 >= callToProcess.s00001081.output.s00000713) AND 'callToProcess.s00001081.output.s00000849 >= callToProcess.s00001081.output.s00000849) AND 'callToService.s00001115.inputCriterion.s00000700.used >= callToService.s00001115.inputCriterion.s00000700.used) AND 'callToService.s00001115.output.s00000713 >= callToService.s00001115.output.s00000713) AND 'callToService.s00001115.output.s00000849 >= callToService.s00001115.output.s00000849) AND 'callToService.s00001133.inputCriterion.s00000700.used >= callToService.s00001133.inputCriterion.s00000700.used) AND 'callToService.s00001133.output.s00000713 >= callToService.s00001133.output.s00000713) AND 'callToService.s00001133.output.s00000849 >= callToService.s00001133.output.s00000849) AND 'callToService.s00001133.output.s00001027 >= callToService.s00001133.output.s00001027) AND 'callToService.s00001134.input.s00000709 >= callToService.s00001134.input.s00000709) AND 'callToService.s00001134.inputCriterion.s00000700.used >= callToService.s00001134.inputCriterion.s00000700.used) AND 'callToService.s00001134.output.s00000713 >= callToService.s00001134.output.s00000713) AND 'callToService.s00001134.output.s00000849 >= callToService.s00001134.output.s00000849) AND 'callToService.s00001134.output.s00001027 >= callToService.s00001134.output.s00001027) AND 'callToTask.s00000887.input.s00000709 >= callToTask.s00000887.input.s00000709) AND 'callToTask.s00000887.input.s00000847 >= callToTask.s00000887.input.s00000847) AND 'callToTask.s00000887.inputCriterion.s00000858.used >= callToTask.s00000887.inputCriterion.s00000858.used) AND 'callToTask.s00000887.output.s00000713 >= callToTask.s00000887.output.s00000713) AND 'callToTask.s00000887.output.s00000849 >= callToTask.s00000887.output.s00000849) AND 'callToTask.s00001109.inputCriterion.s00000700.used >= callToTask.s00001109.inputCriterion.s00000700.used) AND 'callToTask.s00001109.output.s00000713 >= callToTask.s00001109.output.s00000713) AND 'callToTask.s00001109.output.s00000900 >= callToTask.s00001109.output.s00000900) AND 'callToTask.s00001109.output.s00001029 >= callToTask.s00001109.output.s00001029) AND 'callToTask.s00001110.inputCriterion.s00000700.used >= callToTask.s00001110.inputCriterion.s00000700.used) AND 'callToTask.s00001110.output.s00000713 >= callToTask.s00001110.output.s00000713) AND 'callToTask.s00001110.output.s00001029 >= callToTask.s00001110.output.s00001029) AND 'callToTask.s00001131.inputCriterion.s00000700.used >= callToTask.s00001131.inputCriterion.s00000700.used) AND 'callToTask.s00001131.output.s00000713 >= callToTask.s00001131.output.s00000713) AND 'callToTask.s00001131.output.s00000849 >= callToTask.s00001131.output.s00000849) AND 'callToTask.s00001132.input.s00000709 >= callToTask.s00001132.input.s00000709) AND 'callToTask.s00001132.input.s00000847 >= callToTask.s00001132.input.s00000847) AND 'callToTask.s00001132.inputCriterion.s00000700.used >= callToTask.s00001132.inputCriterion.s00000700.used) AND 'callToTask.s00001132.output.s00000713 >= callToTask.s00001132.output.s00000713) AND 'callToTask.s00001132.output.s00000849 >= callToTask.s00001132.output.s00000849) AND 'decision.s00001119.activated >= decision.s00001119.activated) AND 'decision.s00001122.activated >= decision.s00001122.activated) AND 'decision.s00001122.input.s00000709 >= decision.s00001122.input.s00000709) AND 'decision.s00001122.input.s00000710 >= decision.s00001122.input.s00000710) AND 'decision.s00001125.activated >= decision.s00001125.activated) AND 'decision.s00001125.input.s00000709 >= decision.s00001125.input.s00000709) AND 'decision.s00001125.input.s00000710 >= decision.s00001125.input.s00000710) AND 'decision.s00001128.activated >= decision.s00001128.activated) AND 'decision.s00001128.input.s00000709 >= decision.s00001128.input.s00000709) AND 'decision.s00001128.input.s00000710 >= decision.s00001128.input.s00000710) AND 'merge.s00000730.activated >= merge.s00000730.activated) AND 'merge.s00000730.input.s00000709 >= merge.s00000730.input.s00000709) AND 'merge.s00000730.input.s00000710 >= merge.s00000730.input.s00000710) AND 'merge.s00000730.input.s00000734 >= merge.s00000730.input.s00000734) AND 'merge.s00000730.input.s00000736 >= merge.s00000730.input.s00000736) AND 'merge.s00000742.activated >= merge.s00000742.activated) AND 'merge.s00000742.input.s00000737 >= merge.s00000742.input.s00000737) AND 'merge.s00000742.input.s00000740 >= merge.s00000742.input.s00000740) AND 'merge.s00000856.activated >= merge.s00000856.activated) AND 'process.s00000029##s00001116.input.s00001117 >= process.s00000029##s00001116.input.s00001117) AND 'process.s00000029##s00001116.output.s00001118 >= process.s00000029##s00001116.output.s00001118) AND 'process.s00000029##s00001116.outputCriterion.s00000704_omega >= process.s00000029##s00001116.outputCriterion.s00000704_omega))
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000029__s00001135.lola.terminating.task1 0 → 100644
View file @ 4f283fdf
EF ((((((((((((((((((((((((((((((((((((((((((((((((((('sigma >= 1 AND 'alpha >= alpha) AND 'callToProcess.s00001009.inputCriterion.s00000700.used >= callToProcess.s00001009.inputCriterion.s00000700.used) AND 'callToProcess.s00001009.output.s00000713 >= callToProcess.s00001009.output.s00000713) AND 'callToProcess.s00001009.output.s00000849 >= callToProcess.s00001009.output.s00000849) AND 'callToService.s00001143.input.s00000709 >= callToService.s00001143.input.s00000709) AND 'callToService.s00001143.inputCriterion.s00000858.used >= callToService.s00001143.inputCriterion.s00000858.used) AND 'callToService.s00001143.output.s00000713 >= callToService.s00001143.output.s00000713) AND 'callToService.s00001143.output.s00000849 >= callToService.s00001143.output.s00000849) AND 'callToService.s00001143.output.s00001027 >= callToService.s00001143.output.s00001027) AND 'callToService.s00001144.inputCriterion.s00000858.used >= callToService.s00001144.inputCriterion.s00000858.used) AND 'callToService.s00001144.output.s00000713 >= callToService.s00001144.output.s00000713) AND 'callToService.s00001144.output.s00000849 >= callToService.s00001144.output.s00000849) AND 'callToService.s00001144.output.s00001145 >= callToService.s00001144.output.s00001145) AND 'callToTask.s00000887.input.s00000709 >= callToTask.s00000887.input.s00000709) AND 'callToTask.s00000887.input.s00000847 >= callToTask.s00000887.input.s00000847) AND 'callToTask.s00000887.inputCriterion.s00000858.used >= callToTask.s00000887.inputCriterion.s00000858.used) AND 'callToTask.s00000887.output.s00000713 >= callToTask.s00000887.output.s00000713) AND 'callToTask.s00000887.output.s00000849 >= callToTask.s00000887.output.s00000849) AND 'callToTask.s00000887.output.s00000867 >= callToTask.s00000887.output.s00000867) AND 'callToTask.s00001139.inputCriterion.s00000700.used >= callToTask.s00001139.inputCriterion.s00000700.used) AND 'callToTask.s00001139.output.s00000713 >= callToTask.s00001139.output.s00000713) AND 'callToTask.s00001139.output.s00000918 >= callToTask.s00001139.output.s00000918) AND 'callToTask.s00001139.output.s00001029 >= callToTask.s00001139.output.s00001029) AND 'callToTask.s00001140.input.s00000709 >= callToTask.s00001140.input.s00000709) AND 'callToTask.s00001140.input.s00000916 >= callToTask.s00001140.input.s00000916) AND 'callToTask.s00001140.inputCriterion.s00000858.used >= callToTask.s00001140.inputCriterion.s00000858.used) AND 'callToTask.s00001140.output.s00000713 >= callToTask.s00001140.output.s00000713) AND 'callToTask.s00001140.output.s00000867 >= callToTask.s00001140.output.s00000867) AND 'callToTask.s00001141.input.s00000709 >= callToTask.s00001141.input.s00000709) AND 'callToTask.s00001141.input.s00000847 >= callToTask.s00001141.input.s00000847) AND 'callToTask.s00001141.inputCriterion.s00000858.used >= callToTask.s00001141.inputCriterion.s00000858.used) AND 'callToTask.s00001141.output.s00000713 >= callToTask.s00001141.output.s00000713) AND 'callToTask.s00001141.output.s00000849 >= callToTask.s00001141.output.s00000849) AND 'callToTask.s00001141.output.s00001145 >= callToTask.s00001141.output.s00001145) AND 'callToTask.s00001142.input.s00000709 >= callToTask.s00001142.input.s00000709) AND 'callToTask.s00001142.input.s00000847 >= callToTask.s00001142.input.s00000847) AND 'callToTask.s00001142.input.s00001146 >= callToTask.s00001142.input.s00001146) AND 'callToTask.s00001142.inputCriterion.s00000858.used >= callToTask.s00001142.inputCriterion.s00000858.used) AND 'callToTask.s00001142.output.s00000713 >= callToTask.s00001142.output.s00000713) AND 'callToTask.s00001142.output.s00000849 >= callToTask.s00001142.output.s00000849) AND 'decision.s00001136.activated >= decision.s00001136.activated) AND 'fork.s00000981.activated.s00000711 >= fork.s00000981.activated.s00000711) AND 'fork.s00000981.activated.s00000715 >= fork.s00000981.activated.s00000715) AND 'merge.s00000730.activated >= merge.s00000730.activated) AND 'merge.s00000730.input.s00000709 >= merge.s00000730.input.s00000709) AND 'merge.s00000730.input.s00000737 >= merge.s00000730.input.s00000737) AND 'merge.s00000742.activated >= merge.s00000742.activated) AND 'process.s00000029##s00001135.input.s00001028 >= process.s00000029##s00001135.input.s00001028) AND 'process.s00000029##s00001135.output.s00000867 >= process.s00000029##s00001135.output.s00000867) AND 'process.s00000029##s00001135.outputCriterion.s00000704_omega >= process.s00000029##s00001135.outputCriterion.s00000704_omega))
benchmarks/service-tech/ibm-soundness/models/lib_A/A.s00000029__s00001148.lola.terminating.task1 0 → 100644
View file @ 4f283fdf
EF (((((((((((((((((((((((((((((((((((((((((((((((((((((((('sigma >= 1 AND 'alpha >= alpha) AND 'callToProcess.s00001009.inputCriterion.s00000700.used >= callToProcess.s00001009.inputCriterion.s00000700.used) AND 'callToProcess.s00001009.output.s00000713 >= callToProcess.s00001009.output.s00000713) AND 'callToProcess.s00001009.output.s00000849 >= callToProcess.s00001009.output.s00000849) AND 'callToProcess.s00001081.inputCriterion.s00000700.used >= callToProcess.s00001081.inputCriterion.s00000700.used) AND 'callToProcess.s00001081.output.s00000713 >= callToProcess.s00001081.output.s00000713) AND 'callToProcess.s00001081.output.s00000849 >= callToProcess.s00001081.output.s00000849) AND 'callToProcess.s00001098.input.s00000709 >= callToProcess.s00001098.input.s00000709) AND 'callToProcess.s00001098.input.s00000847 >= callToProcess.s00001098.input.s00000847) AND 'callToProcess.s00001098.inputCriterion.s00000700.used >= callToProcess.s00001098.inputCriterion.s00000700.used) AND 'callToProcess.s00001098.output.s00000713 >= callToProcess.s00001098.output.s00000713) AND 'callToProcess.s00001098.output.s00000849 >= callToProcess.s00001098.output.s00000849) AND 'callToProcess.s00001135.input.s00000709 >= callToProcess.s00001135.input.s00000709) AND 'callToProcess.s00001135.input.s00001028 >= callToProcess.s00001135.input.s00001028) AND 'callToProcess.s00001135.inputCriterion.s00000700.used >= callToProcess.s00001135.inputCriterion.s00000700.used) AND 'callToProcess.s00001135.output.s00000713 >= callToProcess.s00001135.output.s00000713) AND 'callToProcess.s00001135.output.s00000867 >= callToProcess.s00001135.output.s00000867) AND 'callToProcess.s00001135.output.s00001118 >= callToProcess.s00001135.output.s00001118) AND 'callToService.s00001157.input.s00000709 >= callToService.s00001157.input.s00000709) AND 'callToService.s00001157.inputCriterion.s00000700.used >= callToService.s00001157.inputCriterion.s00000700.used) AND 'callToService.s00001157.output.s00000713 >= callToService.s00001157.output.s00000713) AND 'callToService.s00001157.output.s00001027 >= callToService.s00001157.output.s00001027) AND 'callToService.s00001157.output.s00001029 >= callToService.s00001157.output.s00001029) AND 'callToTask.s00000887.input.s00000709 >= callToTask.s00000887.input.s00000709) AND 'callToTask.s00000887.input.s00000847 >= callToTask.s00000887.input.s00000847) AND 'callToTask.s00000887.inputCriterion.s00000858.used >= callToTask.s00000887.inputCriterion.s00000858.used) AND 'callToTask.s00000887.output.s00000713 >= callToTask.s00000887.output.s00000713) AND 'callToTask.s00000887.output.s00000849 >= callToTask.s00000887.output.s00000849) AND 'callToTask.s00000887.output.s00000867 >= callToTask.s00000887.output.s00000867) AND 'callToTask.s00001113.input.s00000709 >= callToTask.s00001113.input.s00000709) AND 'callToTask.s00001113.input.s00000847 >= callToTask.s00001113.input.s00000847) AND 'callToTask.s00001113.inputCriterion.s00000858.used >= callToTask.s00001113.inputCriterion.s00000858.used) AND 'callToTask.s00001113.output.s00000713 >= callToTask.s00001113.output.s00000713) AND 'callToTask.s00001113.output.s00000849 >= callToTask.s00001113.output.s00000849) AND 'callToTask.s00001155.inputCriterion.s00000700.used >= callToTask.s00001155.inputCriterion.s00000700.used) AND 'callToTask.s00001155.output.s00000713 >= callToTask.s00001155.output.s00000713) AND 'callToTask.s00001155.output.s00000848 >= callToTask.s00001155.output.s00000848) AND 'callToTask.s00001155.output.s00001029 >= callToTask.s00001155.output.s00001029) AND 'callToTask.s00001155.output.s00001145 >= callToTask.s00001155.output.s00001145) AND 'callToTask.s00001156.inputCriterion.s00000858.used >= callToTask.s00001156.inputCriterion.s00000858.used) AND 'callToTask.s00001156.output.s00000713 >= callToTask.s00001156.output.s00000713) AND 'callToTask.s00001156.output.s00000849 >= callToTask.s00001156.output.s00000849) AND 'decision.s00001149.activated >= decision.s00001149.activated) AND 'decision.s00001152.activated >= decision.s00001152.activated) AND 'endNode.s00000851.input.default >= endNode.s00000851.input.default) AND 'merge.s00000730.activated >= merge.s00000730.activated) AND 'merge.s00000730.input.s00000710 >= merge.s00000730.input.s00000710) AND 'merge.s00000730.input.s00000737 >= merge.s00000730.input.s00000737) AND 'merge.s00000742.activated >= merge.s00000742.activated) AND 'merge.s00000742.input.s00000710 >= merge.s00000742.input.s00000710) AND 'merge.s00000856.activated >= merge.s00000856.activated) AND 'process.s00000029##s00001148.input.s00001028 >= process.s00000029##s00001148.input.s00001028) AND 'process.s00000029##s00001148.output.s00000867 >= process.s00000029##s00001148.output.s00000867) AND 'process.s00000029##s00001148.output.s00001118 >= process.s00000029##s00001148.output.s00001118) AND 'process.s00000029##s00001148.outputCriterion.s00000704_omega >= process.s00000029##s00001148.outputCriterion.s00000704_omega))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment