diff --git a/contrib/tools/lmc.md/lgraph-search.md b/contrib/tools/lmc.md/lgraph-search.md index 19d25c41..07257724 100644 --- a/contrib/tools/lmc.md/lgraph-search.md +++ b/contrib/tools/lmc.md/lgraph-search.md @@ -3,9 +3,6 @@ Labelled Graph Search and Analysis Here is a labelled graph search algorithm and its instantiation to narrowing. -Abstract Graph Search Algorithms --------------------------------- - ```maude sload ../meta/narrowing.maude sload ../meta/cterms.maude @@ -16,96 +13,65 @@ sload lmc.maude set include BOOL off . ``` -### Data Structures +Data Structures +--------------- -Sort `LabeledGraph` is an edge-labelled graph between `Node`s. +### Node Maps + +Sort `NodeMap` can store a natural-number indexed set of nodes which support `fold`ing. +Insertion returns the `NodeId`, which can either be a new natural number or an old natural number with an associated `fold`. ```maude -fmod LABELED-GRAPH is +fmod FOLDING-NODEMAP is + protecting NAT . + protecting EXT-BOOL . +``` + +Natural numbers can be interpreted as `NodeId`s, which makes it possible to refer to nodes more compactly. - sorts Node NeNodeSet NodeSet . - ------------------------------ - subsort Node < NeNodeSet < NodeSet . +```maude + sorts NodeId Node NeNodeSet NodeSet . + ------------------------------------- + subsort Nat < NodeId < Node < NeNodeSet < NodeSet . - --- TODO: change variables N, N' to ND, ND' - vars N N' : Node . vars NeNS NeNS' : NeNodeSet . + vars N N' : Nat . vars NID NID' : NodeId . + vars ND ND' : Node . vars NeNS NeNS' NeNS'' : NeNodeSet . vars NS NS' : NodeSet . op .NodeSet : -> NodeSet . op _;_ : NodeSet NodeSet -> NodeSet [assoc comm id: .NodeSet] . op _;_ : NodeSet NeNodeSet -> NeNodeSet [ditto] . ------------------------------------------------------ eq NeNS ; NeNS = NeNS . - - sorts Label LabeledEdge NeLabeledGraph LabeledGraph . - subsorts LabeledEdge < NeLabeledGraph < LabeledGraph . - ------------------------------------------------------ - var L : Label . var NeLG : NeLabeledGraph . - - op .LabeledGraph : -> LabeledGraph . - op __ : LabeledGraph LabeledGraph -> LabeledGraph [assoc comm id: .LabeledGraph prec 55 format(d n d)] . - op __ : NeLabeledGraph LabeledGraph -> NeLabeledGraph [ditto] . - -------------------------------------------------------------------------- - eq NeLG NeLG = NeLG . - - op _-[_]->_ : Node Label Node -> LabeledEdge [prec 50] . - -------------------------------------------------------- - - sorts Transition NeTransitionSet TransitionSet . - ------------------------------------------------ - subsorts Transition < NeTransitionSet < TransitionSet . - - var TS : TransitionSet . vars NeTS NeTS' : NeTransitionSet . - - op .TransitionSet : -> TransitionSet . - op _,_ : TransitionSet TransitionSet -> TransitionSet [assoc comm id: .TransitionSet] . - op _,_ : NeTransitionSet TransitionSet -> NeTransitionSet [ditto] . - ------------------------------------------------------------------------------ - eq NeTS , NeTS = NeTS . - - op <_,_> : Label Node -> Transition . - op _->_ : Node TransitionSet -> LabeledGraph [prec 50] . - --------------------------------------------------------- - eq N -> .TransitionSet = .LabeledGraph . - eq N -> < L , N' > = N -[ L ]-> N' . - eq N -> NeTS , NeTS' = N -> NeTS N -> NeTS' . -endfm ``` -### Folding Search Command +A `Fold` is a "witness" that a specified node is less general than another node. +The user can specify the equations for `fold` to allow subsumption when possible. ```maude -fmod GRAPH-FOLDING-SEARCH is - protecting NAT . - protecting EXT-BOOL . - protecting BOUND . - extending LABELED-GRAPH . + sort Fold NeFoldSet FoldSet . + ----------------------------- + subsort Fold < NeFoldSet < FoldSet . - vars D D' : Depth . var B : Bound . - vars NS NS' NS'' : NodeSet . vars NeNS NeNS' NeNS'' : NeNodeSet . - vars N N' N'' : Nat . var NID NID' NID'' : NodeId . vars ND ND' : Node . - var L : Label . vars LG LG' LG'' LG''' : LabeledGraph . vars NeLG NeLG' : NeLabeledGraph . - - sort Fold . - ----------- vars F F' : Fold . var F? : [Fold] . op .Fold : -> Fold . - op fold : Node Node -> [Fold] . - -------------------------------- - eq fold(ND, ND) = .Fold . + -------------------- - op step : Node -> [TransitionSet] . - ----------------------------------- + op .FoldSet : -> FoldSet . + op __ : FoldSet FoldSet -> FoldSet [assoc comm id: .FoldSet] . + op __ : FoldSet NeFoldSet -> NeFoldSet [ditto] . + ------------------------------------------------------ + eq F F = F . - op all-step : NodeSet -> [LabeledGraph] . - ----------------------------------------- - eq all-step(ND) = ND -> step(ND) . - eq all-step(.NodeSet) = .LabeledGraph . - eq all-step(NeNS ; NeNS') = all-step(NeNS) all-step(NeNS') . + op fold : NodeSet Node -> [FoldSet] . + ------------------------------------- + eq fold(.NodeSet , ND') = .Fold . + eq fold(ND , ND) = .Fold . + ceq fold(ND ; NeNS , ND') = F F' if F := fold(ND, ND') + /\ F' := fold(NeNS, ND') . - sort NodeId . - ------------- - subsorts Nat < NodeId < Node . + op _[_] : Nat Fold -> NodeId [right id: .Fold prec 20] . + -------------------------------------------------------- --- TODO: add operator _~=_ for NodeSet equality --- TODO: extract this and common functionality from bae-symbolic branch @@ -130,10 +96,12 @@ fmod GRAPH-FOLDING-SEARCH is op isEmpty? : NodeSet -> [Bool] . --------------------------------- eq isEmpty?(.NodeSet) = true . +``` - op _[_] : Nat Fold -> NodeId [right id: .Fold prec 20] . - -------------------------------------------------------- +A `NodeMap` is a lookup table of `Nat |-> Node`, which supports a lookup `_[_]` and `insert` operation. +The insert operation is aware of the user defined `Fold`s, and will not create new entries for new nodes that are less general than existing ones. +```maude sorts NodeAlias NeNodeMap NodeMap NodeMap? . -------------------------------------------- subsorts NodeAlias < NeNodeMap < NodeMap . @@ -143,23 +111,24 @@ fmod GRAPH-FOLDING-SEARCH is op _|->_ : Nat Node -> NodeAlias [prec 55] . -------------------------------------------- - op .NodeMap : -> NodeMap . - op __ : NeNodeMap NodeMap -> NeNodeMap [assoc id: .NodeMap prec 60 format(d n d)] . - op __ : NodeMap NodeMap -> NodeMap [ditto] . - ------------------------------------------------ + op .NodeMap : -> NodeMap . + op __ : NeNodeMap NodeMap -> NeNodeMap [assoc id: .NodeMap prec 60 format(d n d)] . + op __ : NodeMap NodeMap -> NodeMap [ditto] . + ------------------------------------------------------ eq NeNM NeNM = NeNM . op nodes : NodeMap -> [NodeSet] . --------------------------------- eq nodes(.NodeMap) = .NodeSet . - eq nodes(N |-> NID) = .NodeSet . - eq nodes(N |-> ND) = ND . + eq nodes(N |-> ND) = if ND :: NodeId then .NodeSet else ND fi . eq nodes(NeNM NeNM') = nodes(NeNM) ; nodes(NeNM') . op _[_] : NodeMap NodeSet -> [NodeSet] . ---------------------------------------- eq (NID |-> ND NM) [ NID' ] = if NID == NID' then ND else NM [ NID' ] fi . + eq .NodeMap [ NS ] = .NodeSet . + eq NM [ .NodeSet ] = .NodeSet . eq NM [ NeNS ; NeNS' ] = (NM [ NeNS ]) ; (NM [ NeNS' ]) . @@ -176,7 +145,54 @@ fmod GRAPH-FOLDING-SEARCH is else #insert(N |-> ND, NM N' |-> ND', NM') fi if F? := fold(ND, ND') . +``` + +We can also ask for all nodes which intersect with a given `NodeSet`. +```maude + op intersects-with : NodeMap NodeSet -> [NodeSet] . + --------------------------------------------------- + eq intersects-with(.NodeMap, NS) = .NodeSet . + eq intersects-with(NM, .NodeSet) = .NodeSet . + + eq intersects-with(N |-> ND NM , NeNS) = if intersect(ND, NeNS) =/= .NodeSet then N else .NodeSet fi ; intersects-with(NM, NeNS) . +endfm +``` + +### Folding Edge-labeled Graphs + +Sort `LabeledGraph` is an edge-labelled graph between `Node`s. +The `Label` used is left abstract. + +```maude +fmod FOLDING-LABELED-GRAPH is + protecting FOLDING-NODEMAP . + + var N : Nat . vars NID NID' NID'' : NodeId . vars ND ND' : Node . + vars NeNS NeNS' : NeNodeSet . var NS NS' NS'' : NodeSet . + vars NM NM' NM'' : NodeMap . + + sorts Label LabeledEdge NeLabeledGraph LabeledGraph . + ----------------------------------------------------- + subsorts LabeledEdge < NeLabeledGraph < LabeledGraph . + + var L : Label . var LG : LabeledGraph . vars NeLG NeLG' : NeLabeledGraph . + + op .LabeledGraph : -> LabeledGraph . + op __ : LabeledGraph LabeledGraph -> LabeledGraph [assoc comm id: .LabeledGraph prec 55 format(d n d)] . + op __ : NeLabeledGraph LabeledGraph -> NeLabeledGraph [ditto] . + -------------------------------------------------------------------------- + eq NeLG NeLG = NeLG . + + op _-[_]->_ : Node Label Node -> LabeledEdge [prec 50] . + -------------------------------------------------------- +``` + +A `FoldedLabeledGraph` will use the `NodeMap` to store nodes, instead of directly storing them as nodes. +This will allow for "folding" the graph when a certain node is subsumed by another. +In the data structure `FoldedLabeledGraph?`, we additionally maintain a `frontier` of nodes which have not been explored for successor states yet. + +```maude sorts FoldedLabeledGraph FoldedLabeledGraph? . ---------------------------------------------- subsort FoldedLabeledGraph < FoldedLabeledGraph? . @@ -219,6 +235,83 @@ fmod GRAPH-FOLDING-SEARCH is op flgraph : NodeSet -> FoldedLabeledGraph? . --------------------------------------------- eq flgraph(NS) = insert(NS, .FoldedLabeledGraph) . +endfm +``` + +Folding Graph Searches +---------------------- + +Over these data-structures, we can define abstract graph-search algorithms. + +### Single search step + +```maude +fmod FOLDING-LABELED-GRAPH-STEP is + protecting FOLDING-LABELED-GRAPH . + + vars N N' : Nat . vars ND ND' : Node . + vars NS : NodeSet . vars NeNS NeNS' : NeNodeSet . var NM : NodeMap . + var L : Label . var LG : LabeledGraph . var FLG : FoldedLabeledGraph . +``` + +A `Transition` can be used to represent a set of outgoing edges from a given `Node` compactly. + +```maude + sorts Transition NeTransitionSet TransitionSet . + ------------------------------------------------ + subsorts Transition < NeTransitionSet < TransitionSet . + + var T : Transition . vars NeTS NeTS' : NeTransitionSet . + + op .TransitionSet : -> TransitionSet . + op _,_ : TransitionSet TransitionSet -> TransitionSet [assoc comm id: .TransitionSet] . + op _,_ : NeTransitionSet TransitionSet -> NeTransitionSet [ditto] . + ------------------------------------------------------------------------------ + eq NeTS , NeTS = NeTS . + + op <_,_> : Label Node -> Transition . + op _->_ : Node TransitionSet -> LabeledGraph [prec 50] . + --------------------------------------------------------- + eq ND -> .TransitionSet = .LabeledGraph . + eq ND -> < L , ND' > = ND -[ L ]-> ND' . + eq ND -> NeTS , NeTS' = ND -> NeTS ND -> NeTS' . + + op nodes : TransitionSet -> [NodeSet] . + --------------------------------------- + eq nodes(.TransitionSet) = .NodeSet . + eq nodes(< L , ND >) = ND . + eq nodes((NeTS , NeTS')) = nodes(NeTS) ; nodes(NeTS') . +``` + +The following are system-specific (user-specified). + +- `step` *must* return the complete set of outgoing edges (`TransitionSet`). +- `prune` *may* optionally be instantiated to prune given transitions generated by `step` (note the fallback `owise` case). + +**TODO**: `step` loses information about *which* `Node` resulted in each `Transition`. + +```maude + op step : NodeSet -> [TransitionSet] . + -------------------------------------- + eq step(.NodeSet) = .TransitionSet . + eq step(NeNS ; NeNS') = step(NeNS) , step(NeNS') . + + op prune : TransitionSet -> [TransitionSet] . + --------------------------------------------- + eq prune(T) = T [owise] . + eq prune(.TransitionSet) = .TransitionSet . + eq prune(NeTS , NeTS') = prune(NeTS) , prune(NeTS') . +``` + +- `all-step` will generate the labeled graph associated with doing a single step on a set of initial nodes. +- `extend` uses all the above functionality to explore the existing frontier of the current `FoldedLabeledGraph?`. + +```maude + op all-step : NodeSet -> [LabeledGraph] . + ----------------------------------------- + eq all-step(ND) = ND -> step(ND) . + eq all-step(.NodeSet) = .LabeledGraph . + eq all-step(NeNS ; NeNS') = all-step(NeNS) all-step(NeNS') . op extend : NodeSet -> [FoldedLabeledGraph?] . op extend : FoldedLabeledGraph? -> [FoldedLabeledGraph?] . @@ -230,29 +323,38 @@ fmod GRAPH-FOLDING-SEARCH is endfm ``` -### Graph Analysis +### Full graph analysis + +After the user has instantiated the abstract graph search machinery, various analysis are provided. ```maude -fmod GRAPH-ANALYSIS is - protecting GRAPH-FOLDING-SEARCH . - protecting EXT-BOOL . +fmod FOLDING-LABELED-GRAPH-SEARCH is + protecting FOLDING-LABELED-GRAPH-STEP . + protecting BOUND . var N : Nat . var B : Bound . vars NS NS' : NodeSet . var NeNS NeNS' : NeNodeSet . var FLG : FoldedLabeledGraph . var FLG? : FoldedLabeledGraph? . +``` +`bfs` allows doing a (possible bounded) breadth-first search from a specified set of nodes. + +```maude op bfs : NodeSet -> [FoldedLabeledGraph] . op bfs : NodeSet Bound -> [FoldedLabeledGraph] . - op #bfs : Bound FoldedLabeledGraph -> [FoldedLabeledGraph] . - ------------------------------------------------------------ + op #bfs : Bound FoldedLabeledGraph -> [FoldedLabeledGraph] [memo] . + ------------------------------------------------------------------- eq bfs(NS) = bfs(NS, unbounded) . eq bfs(NS, B) = #bfs(B, flgraph(NS)) . eq #bfs(B, FLG) = FLG . eq #bfs(0, FLG?) = FLG? . eq #bfs(B, FLG | NeNS) = #bfs(decrement(B), extend(FLG | NeNS)) . +``` - --- TODO: uniform command language (to perform multiple computations). +`invariant` will check that a given `NodeSet` is invariant by extending it with one step and checking subsumption of the new nodes into the original set. + +```maude op invariant : NodeSet -> [Bool] . ---------------------------------- eq invariant(NS) = nodes(extend(NS)) <= NS . @@ -280,37 +382,60 @@ Instantiation to Narrowing ### Common Narrowing +The above algorithms are abstract, but must be instantiated to a particular problem type. +Here, they are instantiated it to two theories of interest for Maude: narrowing and narrowing modulo $T$. + +The parameters are instantiated as follows: + +- A `Label` is a tuple of the rule identifier enabling the transition, and the substitution used to take the rule. +- A `Node` is a Maude meta-level `Term`, taking a `step` means calling out to Maude's meta-level narrowing functionality. +- A `Fold` is a substitution which enables subsumption, and Maude's meta-level matching functionality is used to compute folds. + +**TODO**: Support partial folds? + Would need a pattern like `T /\ not (T_1 \/ ... \/ T_i)` for `T_1 \/ ... \/ T_i` the folded component. + ```maude fmod NARROWING-GRAPH-COMMON is protecting NARROWING . protecting RENAME-METAVARS . protecting SUBSTITUTION-SET . - extending GRAPH-FOLDING-SEARCH . + extending FOLDING-LABELED-GRAPH-SEARCH . extending META-LMC-PARAMETERS . - vars T T' : Term . var M : Module . - var SUB : Substitution . var SUBS : SubstitutionSet . - vars NSR NSR' : NarrowStepResult . var NSRS : NarrowStepResults . var RL : Qid . + vars T T' : Term . var NeTS : NeTermSet . var M : Module . var SUB : Substitution . var TYPE : Type . + vars NSR NSR' : NarrowStepResult . var NeNSRS : NeNarrowStepResults . var NSRS : NarrowStepResults . var RL : Qid . op label : Qid Substitution -> Label . -------------------------------------- op transition : NarrowStepResults -> [TransitionSet] . ------------------------------------------------------ - eq transition({RL : T , SUB }) = < label(RL, SUB) , state(T) > . - eq transition(.NarrowStepResults) = .TransitionSet . - eq transition(NSR || NSR' || NSRS) = transition(NSR) , transition(NSR') , transition(NSRS) . + ceq transition({RL : T , SUB }) = prune(< label(RL, SUB) , state(T') >) if { T' , TYPE } := metaReduce(#M, T) . + eq transition(.NarrowStepResults) = .TransitionSet . + eq transition(NSR || NeNSRS) = transition(NSR) , transition(NeNSRS) . - op state : Term -> Node . - op fold : Substitution -> Fold . - --------------------------------- - eq step(state(T)) = transition(narrowSteps(#M, T)) . + op fold : SubstitutionSet -> Fold . + ----------------------------------- ceq fold(state(T), state(T')) = fold(SUB) if SUB := metaMatch(#M, T', T, nil, 0) . + + op state : Term -> Node . + ------------------------- + eq step(state(T)) = transition(narrowSteps(#M, T)) . + + op states : TermSet -> NodeSet . + -------------------------------- + eq states(.TermSet) = .NodeSet . + eq states(T) = state(T) . + eq states(T | NeTS) = state(T) ; states(NeTS) . endfm ``` ### Unconditional Narrowing +For unconditional narrowing, we additionally define: + +- `intersect` should assume empty intersection if there are no variant unifiers between the states. + ```maude fmod NARROWING-GRAPH is including NARROWING-GRAPH-COMMON . @@ -324,15 +449,25 @@ endfm ### Conditional Narrowing +For conditional narrowing, we additionally define: + +- `prune` can opportunistically remove states where the constraint is exactly the identified false term. +- `fold` must also take the side-condition into account to ensure subsumption, and can look through multiple matching subsumptions on the term to do so. +- `implies?` is supplied by the user and should check that the models of the first condition are contained in those of the second. +- `intersect` can assume no intersection only if there are no variant unifiers on the *state* component, not taking into account the *constraint*. + ```maude fmod CONDITIONAL-NARROWING-GRAPH is including NARROWING-GRAPH-COMMON + META-CONDITIONAL-LMC-PARAMETERS . - vars ND ND' : Node . vars T T' C C' : Term . var F : Fold . + vars ND ND' : Node . vars T T' C C' : Term . var F : Fold . var L : Label . vars Q RL : Qid . var SUB : Substitution . var SUB? : Substitution? . var N : Nat . vars NSR NSR' : NarrowStepResult . var NSRS : NarrowStepResults . + ceq prune(< L , state(Q[T, C]) >) = .TransitionSet if Q = #cTerm /\ C = #cFalse . + --------------------------------------------------------------------------------- + ceq fold(ND, ND') = F if F := foldAny(ND, ND', 0) . --------------------------------------------------- @@ -342,15 +477,12 @@ fmod CONDITIONAL-NARROWING-GRAPH is if state(Q[T , C ]) := ND /\ Q == #cTerm /\ state(Q[T' , C']) := ND' /\ Q == #cTerm /\ SUB := metaMatch(#M, T', T, nil, N) . -``` - -- `implies?` is supplied by the user and should check that the models of the first condition are contained in those of the second. -```maude - --- TODO: Measure performance of this with `memo` on `implies?` vs not. - --- Probably theory specific, maybe best to leave the choice of `memo` to each individual theory. op implies? : Term Term -> [Bool] . ----------------------------------- + eq implies?(C, C) = true . + ceq implies?(C, C') = true if C' = #cTrue . + ceq implies?(C, C') = true if C = #cFalse . ceq intersect(state(Q[T,C]), state(Q[T',C'])) = .NodeSet if Q = #cTerm /\ noUnifier := metaVariantDisjointUnify(#M, renameTmpVar(#M, T) =? renameTmpVar(#M, T'), empty, 0, 0) . diff --git a/tests/tools/lmc/Makefile.am b/tests/tools/lmc/Makefile.am index f474b7a6..2a3c3342 100644 --- a/tests/tools/lmc/Makefile.am +++ b/tests/tools/lmc/Makefile.am @@ -5,6 +5,7 @@ TESTS = \ bank-account.maude \ lgraph-search.maude \ lmc.maude \ + thermostat.maude \ token.maude RESULT_FILES = \ @@ -12,6 +13,7 @@ RESULT_FILES = \ bank-account.expected \ lgraph-search.expected \ lmc.expected \ + thermostat.expected \ token.expected EXTRA_DIST = $(TESTS) $(RESULT_FILES) diff --git a/tests/tools/lmc/bakery.expected b/tests/tools/lmc/bakery.expected index ca5a8afd..afce3eb7 100644 --- a/tests/tools/lmc/bakery.expected +++ b/tests/tools/lmc/bakery.expected @@ -12,12 +12,12 @@ rewrites: 5 result Bool: true ========================================== reduce in BAKERY-NARROWING-GRAPH : step(state(conf2Idle)) . -rewrites: 12 +rewrites: 15 result Transition: < label('wake, none),state('_;_;_['s.NzNat,'0.Name,'__[ '`[_`]['idle.ModeIdle],'`[_`]['wait['0.Name]]]]) > ========================================== reduce in BAKERY-NARROWING-GRAPH : step(state(confManyWait)) . -rewrites: 18 +rewrites: 23 result NeTransitionSet: < label('crit, 'PWS:ProcWaitSet <- '__['@1:ProcWaitSet,'`[_`]['wait['0.Name]]]),state( '_;_;_['0.Name,'0.Name,'__['@1:ProcWaitSet,'`[_`]['crit['0.Name]]]]) >,< @@ -26,7 +26,7 @@ result NeTransitionSet: < label('crit, '_;_;_['s.NzNat,'0.Name,'__['@1:ProcWaitSet,'`[_`]['wait['0.Name]]]]) > ========================================== reduce in BAKERY-NARROWING-GRAPH : step(state(confBad)) . -rewrites: 35 +rewrites: 52 result NeTransitionSet: < label('crit, 'M:Name <- '@4:Name ; 'N:Name <- '@3:Name ; @@ -74,7 +74,7 @@ result Fold: fold( 'Y:Name <- '__['s.NzNat,'V1:Name]) ========================================== reduce in BAKERY-NARROWING-GRAPH : bfs(state(conf2Idle), 2) . -rewrites: 124 +rewrites: 132 result FoldedLabeledGraph?: (0 -[label('wake, none)]-> 2 2 -[label('crit, none)]-> 4 2 -[label('wake, none)]-> 6) @@ -90,7 +90,7 @@ result FoldedLabeledGraph?: (0 -[label('wake, none)]-> 2 | 4 ; 6 ========================================== reduce in BAKERY-NARROWING-GRAPH : bfs(state(confManyWait), 2) . -rewrites: 349 +rewrites: 369 result FoldedLabeledGraph?: (0 -[label('crit, 'PWS:ProcWaitSet <- '__['@1:ProcWaitSet,'`[_`]['wait['0.Name]]])]-> 2 0 -[label('wake, @@ -124,7 +124,7 @@ result FoldedLabeledGraph?: (0 -[label('crit, | 6 ; 8 ; 10 ; 12 ; 14 ========================================== reduce in BAKERY-NARROWING-GRAPH : state(conf2Idle) =>[10]state(confBad) . -rewrites: 8186 +rewrites: 8251 result [Bool]: (0 -[label('wake, none)]-> 2 2 -[label('crit, none)]-> 4 2 -[label('wake, none)]-> 6 @@ -197,7 +197,7 @@ result [Bool]: (0 -[label('wake, none)]-> 2 'N:Name]],'`[_`]['crit['M:Name]],'PS:ProcSet]]) ========================================== reduce in BAKERY-NARROWING-GRAPH : state(confManyWait) =>[10]state(confBad) . -rewrites: 2635 +rewrites: 2655 result [Bool]: not isEmpty?(state('_;_;_['0.Name,'0.Name,'__['@1:ProcWaitSet, '`[_`]['crit['0.Name]],'`[_`]['crit['0.Name]]]])) or-else extend((0 -[ label('crit, @@ -261,7 +261,7 @@ result NeNodeSet: state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode, ========================================== reduce in BAKERY-FVP-CONDITIONAL-NARROWING-GRAPH : (state(inj(1)) ; state(inj( 2))) =>* state(inj(9)) . -rewrites: 4197 +rewrites: 3846 result [Bool]: not isEmpty?(intersect(state('_st_['<_`,_`,_`,_>['@1:Mode, '0.Nat,'crit.Mode,'@2:Nat],'tt.TrueLit`{Bool`}]), state('_st_[ '<_`,_`,_`,_>['crit.Mode,'X2:Nat,'crit.Mode,'X3:Nat],'tt.TrueLit`{Bool`}])) @@ -305,7 +305,11 @@ result [Bool]: not isEmpty?(intersect(state('_st_['<_`,_`,_`,_>['@1:Mode, 'PC:Mode <- 'wait.NcMode ; 'QNC:NcMode <- '@2:NcMode ; 'Y1:Nat <- '@1:Nat ; - 'Y2:Nat <- '@3:Nat)]-> 9 + 'Y2:Nat <- '@3:Nat)]-> 0[fold( + 'PC:Mode <- 'crit.Mode ; + 'QNC:NcMode <- '@2:NcMode ; + 'Y1:Nat <- '@1:Nat ; + 'Y2:Nat <- '@3:Nat)] 0 -[label('p2_sleep, 'PC:Mode <- '@1:Mode ; 'QNC:NcMode <- 'sleep.NcMode ; @@ -375,16 +379,15 @@ result [Bool]: not isEmpty?(intersect(state('_st_['<_`,_`,_`,_>['@1:Mode, 'PNC:NcMode <- '@1:NcMode ; 'QC:Mode <- 'wait.NcMode ; 'X1:Nat <- '@2:Nat ; - 'X2:Nat <- '@3:Nat)]-> 15[fold( - '@1:Mode <- '@1:NcMode ; - '@2:Nat <- '@2:Nat ; - '@3:Nat <- '@3:Nat)]) + 'X2:Nat <- '@3:Nat)]-> 1[fold( + 'PNC:NcMode <- '@1:NcMode ; + 'QC:Mode <- 'crit.Mode ; + 'X1:Nat <- '@2:Nat ; + 'X2:Nat <- '@3:Nat)]) | 0 |-> state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat], 'tt.TrueLit`{Bool`}]) 1 |-> state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat], 'tt.TrueLit`{Bool`}]) -9 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'@1:Nat,'@2:NcMode,'@3:Nat],'_?=_[ - 'true.Bool,'_<=_['@1:Nat,'@3:Nat]]]) 13 |-> state('_st_['<_`,_`,_`,_>['@1:Mode,'0.Nat,'crit.Mode,'@2:Nat], 'tt.TrueLit`{Bool`}]) 15 |-> state('_st_['<_`,_`,_`,_>['@1:Mode,'@2:Nat,'crit.Mode,'@3:Nat],'_?=_[ @@ -394,12 +397,12 @@ result [Bool]: not isEmpty?(intersect(state('_st_['<_`,_`,_`,_>['@1:Mode, 21 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'@1:Nat,'@2:Mode,'@3:Nat],'_?=_[ 'true.Bool,'_<=_['@1:Nat,'@3:Nat]]]) | 30 -| 9 ; 13 ; 15 ; 19 ; 21) =>[decrement(unbounded)]state('_st_['<_`,_`,_`,_>[ +| 13 ; 15 ; 19 ; 21) =>[decrement(unbounded)]state('_st_['<_`,_`,_`,_>[ 'crit.Mode,'X2:Nat,'crit.Mode,'X3:Nat],'tt.TrueLit`{Bool`}]) ========================================== reduce in BAKERY-FVP-CONDITIONAL-NARROWING-GRAPH : bfs(state(inj(1)) ; state( inj(2)), 2) . -rewrites: 9926 +rewrites: 3482 result FoldedLabeledGraph?: (0 -[label('p1_crit, 'PC:Mode <- 'crit.Mode ; 'QNC:NcMode <- '@2:NcMode ; @@ -431,7 +434,11 @@ result FoldedLabeledGraph?: (0 -[label('p1_crit, 'PC:Mode <- 'wait.NcMode ; 'QNC:NcMode <- '@2:NcMode ; 'Y1:Nat <- '@1:Nat ; - 'Y2:Nat <- '@3:Nat)]-> 9 + 'Y2:Nat <- '@3:Nat)]-> 0[fold( + 'PC:Mode <- 'crit.Mode ; + 'QNC:NcMode <- '@2:NcMode ; + 'Y1:Nat <- '@1:Nat ; + 'Y2:Nat <- '@3:Nat)] 0 -[label('p2_sleep, 'PC:Mode <- '@1:Mode ; 'QNC:NcMode <- 'sleep.NcMode ; @@ -501,65 +508,11 @@ result FoldedLabeledGraph?: (0 -[label('p1_crit, 'PNC:NcMode <- '@1:NcMode ; 'QC:Mode <- 'wait.NcMode ; 'X1:Nat <- '@2:Nat ; - 'X2:Nat <- '@3:Nat)]-> 15[fold( - '@1:Mode <- '@1:NcMode ; - '@2:Nat <- '@2:Nat ; - '@3:Nat <- '@3:Nat)] -9 -[label('p1_crit, - '@1:Nat <- '%2:Nat ; - '@2:NcMode <- '%1:NcMode ; - '@3:Nat <- '_+_['%2:Nat,'%3:Nat])]-> 0[fold( - 'PC:Mode <- 'sleep.NcMode ; - 'QNC:NcMode <- '%1:NcMode ; - 'Y1:Nat <- '0.Nat ; - 'Y2:Nat <- '_+_['%2:Nat,'%3:Nat])] -9 -[label('p1_crit, - '@1:Nat <- '@1:Nat ; - '@2:NcMode <- '@2:NcMode ; - '@3:Nat <- '@3:Nat)]-> 83[fold( - '@1:Nat <- '@1:Nat ; - '@2:Mode <- '@2:NcMode ; - '@3:Nat <- '@3:Nat)] -9 -[label('p1_crit, - '@1:Nat <- '_+_['%2:Nat,'%3:NzNat] ; - '@2:NcMode <- '%1:NcMode ; - '@3:Nat <- '%2:Nat)]-> 85[fold( - '%1:Mode <- '%1:NcMode ; - '%2:Nat <- '%2:Nat)] -9 -[label('p2_sleep, - '@1:Nat <- '%1:Nat ; - '@2:NcMode <- 'sleep.NcMode ; - '@3:Nat <- '_+_['%1:Nat,'%2:Nat])]-> 0[fold( - 'PC:Mode <- 'crit.Mode ; - 'QNC:NcMode <- 'wait.NcMode ; - 'Y1:Nat <- '%1:Nat ; - 'Y2:Nat <- '_+_['1.NzNat,'%1:Nat])] -9 -[label('p2_sleep, - '@1:Nat <- '@1:Nat ; - '@2:NcMode <- 'sleep.NcMode ; - '@3:Nat <- '@2:Nat)]-> 95 -9 -[label('p2_sleep, - '@1:Nat <- '_+_['%1:Nat,'%2:NzNat] ; - '@2:NcMode <- 'sleep.NcMode ; - '@3:Nat <- '%1:Nat)]-> 97 -9 -[label('p2_wait1, - '@1:Nat <- '0.Nat ; - '@2:NcMode <- 'wait.NcMode ; - '@3:Nat <- '%1:Nat)]-> 13[fold( - '@1:Mode <- 'crit.Mode ; - '@2:Nat <- '%1:Nat)] -9 -[label('p2_wait2, - '@1:Nat <- '%1:Nat ; - '@2:NcMode <- 'wait.NcMode ; - '@3:Nat <- '_+_['%1:Nat,'%2:Nat])]-> 59 -9 -[label('p2_wait2, - '@1:Nat <- '@1:Nat ; - '@2:NcMode <- 'wait.NcMode ; - '@3:Nat <- '@2:Nat)]-> 61 -9 -[label('p2_wait2, - '@1:Nat <- '_+_['%1:Nat,'%2:NzNat] ; - '@2:NcMode <- 'wait.NcMode ; - '@3:Nat <- '%1:Nat)]-> 63 + 'X2:Nat <- '@3:Nat)]-> 1[fold( + 'PNC:NcMode <- '@1:NcMode ; + 'QC:Mode <- 'crit.Mode ; + 'X1:Nat <- '@2:Nat ; + 'X2:Nat <- '@3:Nat)] 13 -[label('p1_crit, '@1:Mode <- 'crit.Mode ; '@2:Nat <- '@1:Nat)]-> 1[fold( @@ -591,14 +544,14 @@ result FoldedLabeledGraph?: (0 -[label('p1_crit, 'QNC:NcMode <- 'sleep.NcMode ; 'Y1:Nat <- '0.Nat ; 'Y2:Nat <- '0.Nat)] -15 -[label('p1_crit, - '@1:Mode <- 'crit.Mode ; - '@2:Nat <- '%1:Nat ; - '@3:Nat <- '_+_['%1:Nat,'%2:Nat])]-> 41 15 -[label('p1_crit, '@1:Mode <- 'crit.Mode ; '@2:Nat <- '@1:Nat ; - '@3:Nat <- '@2:Nat)]-> 43 + '@3:Nat <- '@2:Nat)]-> 1[fold( + 'PNC:NcMode <- 'sleep.NcMode ; + 'QC:Mode <- 'crit.Mode ; + 'X1:Nat <- '0.Nat ; + 'X2:Nat <- '@2:Nat)] 15 -[label('p1_crit, '@1:Mode <- 'crit.Mode ; '@2:Nat <- '_+_['%1:Nat,'%2:NzNat] ; @@ -607,14 +560,14 @@ result FoldedLabeledGraph?: (0 -[label('p1_crit, 'QC:Mode <- 'crit.Mode ; 'X1:Nat <- '0.Nat ; 'X2:Nat <- '%1:Nat)] -15 -[label('p1_sleep, - '@1:Mode <- 'sleep.NcMode ; - '@2:Nat <- '%1:Nat ; - '@3:Nat <- '_+_['%1:Nat,'%2:Nat])]-> 47 15 -[label('p1_sleep, '@1:Mode <- 'sleep.NcMode ; '@2:Nat <- '@1:Nat ; - '@3:Nat <- '@2:Nat)]-> 49 + '@3:Nat <- '@2:Nat)]-> 1[fold( + 'PNC:NcMode <- 'wait.NcMode ; + 'QC:Mode <- 'crit.Mode ; + 'X1:Nat <- '_+_['1.NzNat,'@2:Nat] ; + 'X2:Nat <- '@2:Nat)] 15 -[label('p1_sleep, '@1:Mode <- 'sleep.NcMode ; '@2:Nat <- '_+_['%1:Nat,'%2:NzNat] ; @@ -629,10 +582,6 @@ result FoldedLabeledGraph?: (0 -[label('p1_crit, '@3:Nat <- '0.Nat)]-> 19[fold( '@1:Nat <- '%1:NzNat ; '@2:Mode <- 'crit.Mode)] -15 -[label('p1_wait1, - '@1:Mode <- 'wait.NcMode ; - '@2:Nat <- '0.Nat ; - '@3:Nat <- '0.Nat)]-> 55 15 -[label('p1_wait1, '@1:Mode <- 'wait.NcMode ; '@2:Nat <- '@1:Nat ; @@ -640,22 +589,10 @@ result FoldedLabeledGraph?: (0 -[label('p1_crit, '@1:Mode <- 'crit.Mode ; '@2:Nat <- '@1:Nat ; '@3:Nat <- '0.Nat)] -15 -[label('p1_wait2, - '@1:Mode <- 'wait.NcMode ; - '@2:Nat <- '%1:Nat ; - '@3:Nat <- '_+_['%1:Nat,'%2:Nat])]-> 59 15 -[label('p1_wait2, '@1:Mode <- 'wait.NcMode ; '@2:Nat <- '@1:Nat ; - '@3:Nat <- '@2:Nat)]-> 61 -15 -[label('p1_wait2, - '@1:Mode <- 'wait.NcMode ; - '@2:Nat <- '_+_['%1:Nat,'%2:NzNat] ; - '@3:Nat <- '%1:Nat)]-> 63 -15 -[label('p2_crit, - '@1:Mode <- '%1:Mode ; - '@2:Nat <- '%2:Nat ; - '@3:Nat <- '_+_['%2:Nat,'%3:Nat])]-> 65 + '@3:Nat <- '@2:Nat)]-> 53 15 -[label('p2_crit, '@1:Mode <- '%1:Mode ; '@2:Nat <- '_+_['%2:Nat,'%3:NzNat] ; @@ -667,7 +604,11 @@ result FoldedLabeledGraph?: (0 -[label('p1_crit, 15 -[label('p2_crit, '@1:Mode <- '@1:Mode ; '@2:Nat <- '@2:Nat ; - '@3:Nat <- '@3:Nat)]-> 69 + '@3:Nat <- '@3:Nat)]-> 0[fold( + 'PC:Mode <- '@1:Mode ; + 'QNC:NcMode <- 'sleep.NcMode ; + 'Y1:Nat <- '@2:Nat ; + 'Y2:Nat <- '0.Nat)] 19 -[label('p1_crit, '@1:Nat <- '@1:Nat ; '@2:Mode <- '@2:Mode)]-> 1[fold( @@ -711,11 +652,11 @@ result FoldedLabeledGraph?: (0 -[label('p1_crit, 21 -[label('p1_crit, '@1:Nat <- '@1:Nat ; '@2:Mode <- '@2:Mode ; - '@3:Nat <- '@3:Nat)]-> 83 -21 -[label('p1_crit, - '@1:Nat <- '_+_['%2:Nat,'%3:NzNat] ; - '@2:Mode <- '%1:Mode ; - '@3:Nat <- '%2:Nat)]-> 85 + '@3:Nat <- '@3:Nat)]-> 1[fold( + 'PNC:NcMode <- 'sleep.NcMode ; + 'QC:Mode <- '@2:Mode ; + 'X1:Nat <- '0.Nat ; + 'X2:Nat <- '@3:Nat)] 21 -[label('p2_crit, '@1:Nat <- '%1:Nat ; '@2:Mode <- 'crit.Mode ; @@ -727,13 +668,11 @@ result FoldedLabeledGraph?: (0 -[label('p1_crit, 21 -[label('p2_crit, '@1:Nat <- '@1:Nat ; '@2:Mode <- 'crit.Mode ; - '@3:Nat <- '@2:Nat)]-> 89 -21 -[label('p2_crit, - '@1:Nat <- '_+_['%1:Nat,'%2:NzNat] ; - '@2:Mode <- 'crit.Mode ; - '@3:Nat <- '%1:Nat)]-> 65[fold( - '%1:Mode <- 'crit.Mode ; - '%2:Nat <- '_+_['%1:Nat,'%2:NzNat])] + '@3:Nat <- '@2:Nat)]-> 0[fold( + 'PC:Mode <- 'crit.Mode ; + 'QNC:NcMode <- 'sleep.NcMode ; + 'Y1:Nat <- '@1:Nat ; + 'Y2:Nat <- '0.Nat)] 21 -[label('p2_sleep, '@1:Nat <- '%1:Nat ; '@2:Mode <- 'sleep.NcMode ; @@ -745,35 +684,25 @@ result FoldedLabeledGraph?: (0 -[label('p1_crit, 21 -[label('p2_sleep, '@1:Nat <- '@1:Nat ; '@2:Mode <- 'sleep.NcMode ; - '@3:Nat <- '@2:Nat)]-> 95 -21 -[label('p2_sleep, - '@1:Nat <- '_+_['%1:Nat,'%2:NzNat] ; - '@2:Mode <- 'sleep.NcMode ; - '@3:Nat <- '%1:Nat)]-> 97 + '@3:Nat <- '@2:Nat)]-> 0[fold( + 'PC:Mode <- 'crit.Mode ; + 'QNC:NcMode <- 'wait.NcMode ; + 'Y1:Nat <- '@1:Nat ; + 'Y2:Nat <- '_+_['1.NzNat,'@1:Nat])] 21 -[label('p2_wait1, '@1:Nat <- '0.Nat ; '@2:Mode <- 'wait.NcMode ; '@3:Nat <- '%1:Nat)]-> 13[fold( '@1:Mode <- 'crit.Mode ; '@2:Nat <- '%1:Nat)] -21 -[label('p2_wait2, - '@1:Nat <- '%1:Nat ; - '@2:Mode <- 'wait.NcMode ; - '@3:Nat <- '_+_['%1:Nat,'%2:Nat])]-> 59 21 -[label('p2_wait2, '@1:Nat <- '@1:Nat ; '@2:Mode <- 'wait.NcMode ; - '@3:Nat <- '@2:Nat)]-> 61 -21 -[label('p2_wait2, - '@1:Nat <- '_+_['%1:Nat,'%2:NzNat] ; - '@2:Mode <- 'wait.NcMode ; - '@3:Nat <- '%1:Nat)]-> 63) + '@3:Nat <- '@2:Nat)]-> 53) | 0 |-> state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat], 'tt.TrueLit`{Bool`}]) 1 |-> state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat], 'tt.TrueLit`{Bool`}]) -9 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'@1:Nat,'@2:NcMode,'@3:Nat],'_?=_[ - 'true.Bool,'_<=_['@1:Nat,'@3:Nat]]]) 13 |-> state('_st_['<_`,_`,_`,_>['@1:Mode,'0.Nat,'crit.Mode,'@2:Nat], 'tt.TrueLit`{Bool`}]) 15 |-> state('_st_['<_`,_`,_`,_>['@1:Mode,'@2:Nat,'crit.Mode,'@3:Nat],'_?=_[ @@ -782,379 +711,24 @@ result FoldedLabeledGraph?: (0 -[label('p1_crit, 'tt.TrueLit`{Bool`}]) 21 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'@1:Nat,'@2:Mode,'@3:Nat],'_?=_[ 'true.Bool,'_<=_['@1:Nat,'@3:Nat]]]) -41 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'_+_['%1:Nat, - '%2:Nat]],'ff.FalseLit`{Bool`}]) -43 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'@2:Nat], - '_?=_['true.Bool,'_<_['@2:Nat,'@1:Nat]]]) -47 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'%1:Nat,'%2:Nat], - 'crit.Mode,'_+_['%1:Nat,'%2:Nat]],'ff.FalseLit`{Bool`}]) -49 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@2:Nat], - 'crit.Mode,'@2:Nat],'_?=_['true.Bool,'_<_['@2:Nat,'@1:Nat]]]) -55 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'0.Nat,'crit.Mode,'0.Nat], - 'ff.FalseLit`{Bool`}]) -59 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'%1:Nat,'crit.Mode,'_+_['%1:Nat, - '%2:Nat]],'ff.FalseLit`{Bool`}]) -61 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'@1:Nat,'crit.Mode,'@2:Nat],'_/\_[ +53 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'@1:Nat,'crit.Mode,'@2:Nat],'_/\_[ '_?=_['true.Bool,'_<=_['@1:Nat,'@2:Nat]],'_?=_['true.Bool,'_<_['@2:Nat, '@1:Nat]]]]) -63 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['%1:Nat,'%2:NzNat],'crit.Mode, - '%1:Nat],'ff.FalseLit`{Bool`}]) -65 |-> state('_st_['<_`,_`,_`,_>['%1:Mode,'%2:Nat,'sleep.NcMode,'0.Nat], - 'ff.FalseLit`{Bool`}]) -69 |-> state('_st_['<_`,_`,_`,_>['@1:Mode,'@2:Nat,'sleep.NcMode,'0.Nat],'_?=_[ - 'true.Bool,'_<_['@3:Nat,'@2:Nat]]]) -83 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'@2:Mode,'@3:Nat],'_?=_[ - 'true.Bool,'_<=_['@1:Nat,'@3:Nat]]]) -85 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'%1:Mode,'%2:Nat], - 'ff.FalseLit`{Bool`}]) -89 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'@1:Nat,'sleep.NcMode,'0.Nat], - '_?=_['true.Bool,'_<=_['@1:Nat,'@2:Nat]]]) -95 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'@1:Nat,'wait.NcMode,'_+_['1.NzNat, - '@1:Nat]],'_?=_['true.Bool,'_<=_['@1:Nat,'@2:Nat]]]) -97 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['%1:Nat,'%2:NzNat], - 'wait.NcMode,'_+_['1.NzNat,'%1:Nat,'%2:NzNat]],'ff.FalseLit`{Bool`}]) -| 126 -| 41 ; 43 ; 47 ; 49 ; 55 ; 59 ; 61 ; 63 ; 65 ; 69 ; 83 ; 85 ; 89 ; 95 ; 97 +| 84 +| 53 ========================================== reduce in BAKERY-FVP-CONDITIONAL-NARROWING-GRAPH : state(inj(4)) =>* state(inj( 9)) . -rewrites: 20702 -result [Bool]: not isEmpty?(intersect(state('_st_['<_`,_`,_`,_>['crit.Mode, - '1.NzNat,'crit.Mode,'_+_['1.NzNat,'1.NzNat]],'ff.FalseLit`{Bool`}]), state( - '_st_['<_`,_`,_`,_>['crit.Mode,'X2:Nat,'crit.Mode,'X3:Nat], - 'tt.TrueLit`{Bool`}])) ; intersect(state('_st_['<_`,_`,_`,_>['crit.Mode, - 'X2:Nat,'crit.Mode,'X3:Nat],'tt.TrueLit`{Bool`}]), state('_st_[ - '<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat],'crit.Mode,'_+_['1.NzNat, - '1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}])) ; intersect(state('_st_[ - '<_`,_`,_`,_>['crit.Mode,'X2:Nat,'crit.Mode,'X3:Nat],'tt.TrueLit`{Bool`}]), - state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], - 'crit.Mode,'_+_['1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]))) or-else extend( - (0 -[label('p1_sleep, - 'X0:Nat <- '@1:Nat ; - 'X1:Nat <- '@2:Nat)]-> 2 -0 -[label('p2_sleep, - 'X0:Nat <- '@1:Nat ; - 'X1:Nat <- '@2:Nat)]-> 4 -2 -[label('p1_wait1, - '@2:Nat <- '0.Nat)]-> 12 -2 -[label('p1_wait2, - '@2:Nat <- '@1:Nat)]-> 14 -2 -[label('p2_sleep, - '@2:Nat <- '@1:Nat)]-> 16 -4 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 6 -4 -[label('p2_wait1, - '@1:Nat <- '0.Nat)]-> 8 -4 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 10 -6 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 38 -6 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 40 -8 -[label('p1_sleep, none)]-> 26 -8 -[label('p2_crit, none)]-> 0[fold( - 'X0:Nat <- '0.Nat ; - 'X1:Nat <- '0.Nat)] -10 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 30 -10 -[label('p2_crit, - '@1:Nat <- '@1:Nat)]-> 32 -12 -[label('p1_crit, none)]-> 0[fold( - 'X0:Nat <- '0.Nat ; - 'X1:Nat <- '0.Nat)] -12 -[label('p2_sleep, none)]-> 20 -14 -[label('p1_crit, - '@1:Nat <- '@1:Nat)]-> 22 -14 -[label('p2_sleep, - '@1:Nat <- '@1:Nat)]-> 24 -16 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 34 -16 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 36 -20 -[label('p1_crit, none)]-> 42 -20 -[label('p2_wait2, none)]-> 44 -22 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 58 -22 -[label('p2_sleep, - '@1:Nat <- '@1:Nat)]-> 54[fold( - '@1:Nat <- '0.Nat)] -24 -[label('p1_crit, - '@1:Nat <- '@1:Nat)]-> 46 -24 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 48 -26 -[label('p1_wait2, none)]-> 56[fold( - '@1:Nat <- '0.Nat)] -26 -[label('p2_crit, none)]-> 68 -30 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 56 -30 -[label('p2_crit, - '@1:Nat <- '@1:Nat)]-> 72[fold( - '@1:Nat <- '_+_['1.NzNat,'@1:Nat])] -32 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 58[fold( - '@1:Nat <- '0.Nat)] -32 -[label('p2_sleep, - '@1:Nat <- '@1:Nat)]-> 64 -34 -[label('p1_crit, - '@1:Nat <- '@1:Nat)]-> 50 -34 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 48 -36 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 48 -36 -[label('p2_crit, - '@1:Nat <- '@1:Nat)]-> 72 -38 -[label('p1_crit, - '@1:Nat <- '@1:Nat)]-> 54 -38 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 56 -40 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 56 -40 -[label('p2_crit, - '@1:Nat <- '@1:Nat)]-> 80) -| 0 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'X0:Nat,'sleep.NcMode,'X1:Nat], - 'tt.TrueLit`{Bool`}]) -2 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@2:Nat], - 'sleep.NcMode,'@2:Nat],'tt.TrueLit`{Bool`}]) -4 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'@1:Nat,'wait.NcMode,'_+_[ - '1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) -6 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], - 'wait.NcMode,'_+_['1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) -8 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'1.NzNat], - 'tt.TrueLit`{Bool`}]) -10 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'@1:Nat,'crit.Mode,'_+_[ - '1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -12 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'1.NzNat,'sleep.NcMode,'0.Nat], - 'tt.TrueLit`{Bool`}]) -14 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat], - 'sleep.NcMode,'@1:Nat],'ff.FalseLit`{Bool`}]) -16 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat], - 'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) -20 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'1.NzNat,'wait.NcMode,'_+_[ - '1.NzNat,'1.NzNat]],'tt.TrueLit`{Bool`}]) -22 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'sleep.NcMode,'@1:Nat], - 'ff.FalseLit`{Bool`}]) -24 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat], - 'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -26 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat], - 'crit.Mode,'1.NzNat],'tt.TrueLit`{Bool`}]) -30 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], - 'crit.Mode,'_+_['1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -32 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'@1:Nat,'sleep.NcMode,'0.Nat], - 'ff.FalseLit`{Bool`}]) -34 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat], - 'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) -36 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat], - 'crit.Mode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -38 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], - 'wait.NcMode,'_+_['1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -40 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], - 'crit.Mode,'_+_['1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) -42 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_[ - '1.NzNat,'1.NzNat]],'tt.TrueLit`{Bool`}]) -44 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'1.NzNat,'crit.Mode,'_+_['1.NzNat, - '1.NzNat]],'ff.FalseLit`{Bool`}]) -46 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_[ - '1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -48 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat],'crit.Mode, - '_+_['1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -50 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_[ - '1.NzNat,'1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) -54 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_[ - '1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -56 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], - 'crit.Mode,'_+_['1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -58 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat], - 'sleep.NcMode,'@1:Nat],'ff.FalseLit`{Bool`}]) -64 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'@1:Nat,'wait.NcMode,'_+_[ - '1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -68 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat], - 'sleep.NcMode,'0.Nat],'tt.TrueLit`{Bool`}]) -72 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat], - 'sleep.NcMode,'0.Nat],'ff.FalseLit`{Bool`}]) -80 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], - 'sleep.NcMode,'0.Nat],'tt.TrueLit`{Bool`}]) -| 81 -| 42 ; 44 ; 46 ; 48 ; 50 ; 54 ; 56 ; 58 ; 64 ; 68 ; 72 ; 80) =>[decrement( - unbounded)]state('_st_['<_`,_`,_`,_>['crit.Mode,'X2:Nat,'crit.Mode, - 'X3:Nat],'tt.TrueLit`{Bool`}]) +rewrites: 11640 +result Bool: false ========================================== reduce in BAKERY-FVP-CONDITIONAL-NARROWING-GRAPH : nodes(bfs(state(inj(4)))) <= (state(inj(1)) ; state(inj(2))) . -rewrites: 38110 -result [Bool]: ((((((((((((((((((((((((((((((((((((((state('_st_['<_`,_`,_`,_>[ - 'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat],'wait.NcMode,'_+_['1.NzNat, - '@1:Nat]],'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode, - 'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}])) - and-then state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat, - '@1:Nat],'sleep.NcMode,'0.Nat],'tt.TrueLit`{Bool`}]) <= (state('_st_[ - '<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; - state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat], - 'tt.TrueLit`{Bool`}]))) and-then state('_st_['<_`,_`,_`,_>['wait.NcMode, - '_+_['1.NzNat,'1.NzNat,'@1:Nat],'crit.Mode,'_+_['1.NzNat,'@1:Nat]], - 'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat, - 'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>[ - 'PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then - state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], - 'crit.Mode,'_+_['1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) <= (state('_st_[ - '<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; - state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat], - 'tt.TrueLit`{Bool`}]))) and-then state('_st_['<_`,_`,_`,_>['wait.NcMode, - '_+_['1.NzNat,'@2:Nat],'sleep.NcMode,'@2:Nat],'tt.TrueLit`{Bool`}]) <= ( - state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat], - 'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat, - 'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then state('_st_[ - '<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat],'wait.NcMode,'_+_[ - '1.NzNat,'1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) <= (state('_st_[ - '<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; - state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat], - 'tt.TrueLit`{Bool`}]))) and-then state('_st_['<_`,_`,_`,_>['wait.NcMode, - '_+_['1.NzNat,'@1:Nat],'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]], - 'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat, - 'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>[ - 'PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then - state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat], - 'sleep.NcMode,'@1:Nat],'ff.FalseLit`{Bool`}]) <= (state('_st_[ - '<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; - state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat], - 'tt.TrueLit`{Bool`}]))) and-then state('_st_['<_`,_`,_`,_>['wait.NcMode, - '_+_['1.NzNat,'@1:Nat],'sleep.NcMode,'0.Nat],'ff.FalseLit`{Bool`}]) <= ( - state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat], - 'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat, - 'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then state('_st_[ - '<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat],'crit.Mode,'_+_['1.NzNat, - '1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>[ - 'PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat], - 'sleep.NcMode,'0.Nat],'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>[ - 'PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat], - 'crit.Mode,'1.NzNat],'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>[ - 'PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['sleep.NcMode,'X0:Nat,'sleep.NcMode, - 'X1:Nat],'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode, - 'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['sleep.NcMode,'@1:Nat,'wait.NcMode,'_+_[ - '1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>[ - 'PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['sleep.NcMode,'@1:Nat,'wait.NcMode,'_+_[ - '1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>[ - 'PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['sleep.NcMode,'@1:Nat,'sleep.NcMode, - '0.Nat],'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode, - 'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['sleep.NcMode,'@1:Nat,'crit.Mode,'_+_[ - '1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>[ - 'PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_[ - '1.NzNat,'1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) <= (state('_st_[ - '<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; - state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat], - 'tt.TrueLit`{Bool`}]))) and-then state('_st_['<_`,_`,_`,_>['sleep.NcMode, - '0.Nat,'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) - <= (state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat], - 'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat, - 'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then state('_st_[ - '<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_['1.NzNat,'@1:Nat]], - 'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat, - 'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>[ - 'PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then - state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_['1.NzNat, - '1.NzNat]],'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode, - 'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'sleep.NcMode, - '@1:Nat],'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode, - 'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'_+_[ - '1.NzNat,'1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) <= (state('_st_[ - '<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; - state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat], - 'tt.TrueLit`{Bool`}]))) and-then state('_st_['<_`,_`,_`,_>['sleep.NcMode, - '0.Nat,'crit.Mode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) - <= (state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat], - 'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat, - 'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then state('_st_[ - '<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'_+_['1.NzNat,'@1:Nat]], - 'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat, - 'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>[ - 'PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then - state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'_+_['1.NzNat, - '1.NzNat]],'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode, - 'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'_+_[ - '1.NzNat,'1.NzNat]],'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>[ - 'PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode, - '1.NzNat],'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode, - 'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat, - '@1:Nat],'wait.NcMode,'_+_['1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) <= ( - state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat], - 'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat, - 'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then state('_st_[ - '<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat,'@1:Nat],'sleep.NcMode, - '0.Nat],'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode, - 'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat, - '@1:Nat],'crit.Mode,'_+_['1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) <= ( - state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat], - 'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat, - 'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then state('_st_[ - '<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat],'wait.NcMode,'_+_['1.NzNat, - '1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>[ - 'PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat], - 'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) <= ( - state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat], - 'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat, - 'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then state('_st_[ - '<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat],'sleep.NcMode,'@1:Nat], - 'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat, - 'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>[ - 'PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then - state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat],'sleep.NcMode, - '0.Nat],'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode, - 'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat], - 'crit.Mode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) <= ( - state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat], - 'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat, - 'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then state('_st_[ - '<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat],'sleep.NcMode,'0.Nat], - 'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:Nat, - 'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_['<_`,_`,_`,_>[ - 'PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) and-then - state('_st_['<_`,_`,_`,_>['crit.Mode,'1.NzNat,'wait.NcMode,'_+_['1.NzNat, - '1.NzNat]],'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode, - 'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['crit.Mode,'1.NzNat,'sleep.NcMode, - '0.Nat],'tt.TrueLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>['PC:Mode, - 'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}]))) - and-then state('_st_['<_`,_`,_`,_>['crit.Mode,'1.NzNat,'crit.Mode,'_+_[ - '1.NzNat,'1.NzNat]],'ff.FalseLit`{Bool`}]) <= (state('_st_['<_`,_`,_`,_>[ - 'PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat],'tt.TrueLit`{Bool`}]) ; state('_st_[ - '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat],'tt.TrueLit`{Bool`}])) +rewrites: 6641 +result Bool: true ========================================== reduce in BAKERY-FVP-CONDITIONAL-NARROWING-GRAPH : bfs(state(inj(4))) . -rewrites: 37948 +rewrites: 11 result FoldedLabeledGraph: (0 -[label('p1_sleep, 'X0:Nat <- '@1:Nat ; 'X1:Nat <- '@2:Nat)]-> 2 @@ -1162,201 +736,70 @@ result FoldedLabeledGraph: (0 -[label('p1_sleep, 'X0:Nat <- '@1:Nat ; 'X1:Nat <- '@2:Nat)]-> 4 2 -[label('p1_wait1, - '@2:Nat <- '0.Nat)]-> 12 -2 -[label('p1_wait2, - '@2:Nat <- '@1:Nat)]-> 14 + '@2:Nat <- '0.Nat)]-> 10 2 -[label('p2_sleep, - '@2:Nat <- '@1:Nat)]-> 16 + '@2:Nat <- '@1:Nat)]-> 12 4 -[label('p1_sleep, '@1:Nat <- '@1:Nat)]-> 6 4 -[label('p2_wait1, '@1:Nat <- '0.Nat)]-> 8 -4 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 10 -6 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 38 6 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 40 -8 -[label('p1_sleep, none)]-> 26 + '@1:Nat <- '@1:Nat)]-> 24 +8 -[label('p1_sleep, none)]-> 18 8 -[label('p2_crit, none)]-> 0[fold( 'X0:Nat <- '0.Nat ; 'X1:Nat <- '0.Nat)] -10 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 30 -10 -[label('p2_crit, - '@1:Nat <- '@1:Nat)]-> 32 -12 -[label('p1_crit, none)]-> 0[fold( +10 -[label('p1_crit, none)]-> 0[fold( 'X0:Nat <- '0.Nat ; 'X1:Nat <- '0.Nat)] -12 -[label('p2_sleep, none)]-> 20 -14 -[label('p1_crit, +10 -[label('p2_sleep, none)]-> 16 +12 -[label('p1_wait2, '@1:Nat <- '@1:Nat)]-> 22 -14 -[label('p2_sleep, - '@1:Nat <- '@1:Nat)]-> 24 -16 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 34 -16 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 36 -20 -[label('p1_crit, none)]-> 42 -20 -[label('p2_wait2, none)]-> 44 -22 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 58 -22 -[label('p2_sleep, - '@1:Nat <- '@1:Nat)]-> 54[fold( - '@1:Nat <- '0.Nat)] -24 -[label('p1_crit, - '@1:Nat <- '@1:Nat)]-> 46 -24 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 48 -26 -[label('p1_wait2, none)]-> 56[fold( - '@1:Nat <- '0.Nat)] -26 -[label('p2_crit, none)]-> 68 -30 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 56 -30 -[label('p2_crit, - '@1:Nat <- '@1:Nat)]-> 72[fold( - '@1:Nat <- '_+_['1.NzNat,'@1:Nat])] -32 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 58[fold( - '@1:Nat <- '0.Nat)] -32 -[label('p2_sleep, - '@1:Nat <- '@1:Nat)]-> 64 -34 -[label('p1_crit, - '@1:Nat <- '@1:Nat)]-> 50 -34 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 48 -36 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 48 -36 -[label('p2_crit, - '@1:Nat <- '@1:Nat)]-> 72 -38 -[label('p1_crit, - '@1:Nat <- '@1:Nat)]-> 54 -38 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 56 -40 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 56 -40 -[label('p2_crit, - '@1:Nat <- '@1:Nat)]-> 80 -42 -[label('p1_sleep, none)]-> 6[fold( +16 -[label('p1_crit, none)]-> 26 +18 -[label('p2_crit, none)]-> 30 +22 -[label('p1_crit, + '@1:Nat <- '@1:Nat)]-> 28 +24 -[label('p2_crit, + '@1:Nat <- '@1:Nat)]-> 32 +26 -[label('p1_sleep, none)]-> 6[fold( '@1:Nat <- '1.NzNat)] -42 -[label('p2_wait1, none)]-> 96 -42 -[label('p2_wait2, none)]-> 82 -44 -[label('p1_crit, none)]-> 82 -44 -[label('p2_crit, none)]-> 14[fold( - '@1:Nat <- '0.Nat)] -46 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 100[fold( - '@1:Nat <- '_+_['1.NzNat,'@1:Nat])] -46 -[label('p2_wait1, - '@1:Nat <- '@1:Nat)]-> 86 -46 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 86 -48 -[label('p1_crit, - '@1:Nat <- '@1:Nat)]-> 86 -48 -[label('p2_crit, - '@1:Nat <- '@1:Nat)]-> 88 -50 -[label('p1_sleep, +26 -[label('p2_wait1, none)]-> 36 +28 -[label('p1_sleep, '@1:Nat <- '@1:Nat)]-> 6[fold( '@1:Nat <- '_+_['1.NzNat,'@1:Nat])] -50 -[label('p2_wait1, - '@1:Nat <- '@1:Nat)]-> 114 -50 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 86 -54 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 100 -54 -[label('p2_wait1, - '@1:Nat <- '@1:Nat)]-> 90 -54 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 90 -56 -[label('p1_crit, - '@1:Nat <- '@1:Nat)]-> 90 -56 -[label('p2_crit, - '@1:Nat <- '@1:Nat)]-> 88[fold( - '@1:Nat <- '_+_['1.NzNat,'@1:Nat])] -58 -[label('p1_wait1, - '@1:Nat <- '0.Nat)]-> 14[fold( - '@1:Nat <- '0.Nat)] -58 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 14 -58 -[label('p2_sleep, - '@1:Nat <- '@1:Nat)]-> 134 -64 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 100 -64 -[label('p2_wait1, - '@1:Nat <- '0.Nat)]-> 10[fold( - '@1:Nat <- '0.Nat)] -64 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 10 -68 -[label('p1_wait1, none)]-> 124 -68 -[label('p1_wait2, none)]-> 88[fold( - '@1:Nat <- '1.NzNat)] -68 -[label('p2_sleep, none)]-> 16[fold( - '@1:Nat <- '1.NzNat)] -72 -[label('p1_wait1, - '@1:Nat <- '@1:Nat)]-> 88 -72 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 88 -72 -[label('p2_sleep, - '@1:Nat <- '@1:Nat)]-> 134 -80 -[label('p1_wait1, - '@1:Nat <- '@1:Nat)]-> 142 -80 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 88[fold( - '@1:Nat <- '_+_['1.NzNat,'@1:Nat])] -80 -[label('p2_sleep, - '@1:Nat <- '@1:Nat)]-> 16[fold( - '@1:Nat <- '_+_['1.NzNat,'@1:Nat])] -82 -[label('p1_sleep, none)]-> 30[fold( +28 -[label('p2_wait1, + '@1:Nat <- '@1:Nat)]-> 40 +30 -[label('p1_wait1, none)]-> 42 +30 -[label('p2_sleep, none)]-> 12[fold( '@1:Nat <- '1.NzNat)] -82 -[label('p2_crit, none)]-> 22[fold( - '@1:Nat <- '0.Nat)] -86 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 30[fold( +32 -[label('p1_wait1, + '@1:Nat <- '@1:Nat)]-> 46 +32 -[label('p2_sleep, + '@1:Nat <- '@1:Nat)]-> 12[fold( '@1:Nat <- '_+_['1.NzNat,'@1:Nat])] -86 -[label('p2_crit, - '@1:Nat <- '@1:Nat)]-> 22[fold( - '@1:Nat <- '0.Nat)] -88 -[label('p1_crit, - '@1:Nat <- '@1:Nat)]-> 22[fold( - '@1:Nat <- '0.Nat)] -88 -[label('p2_sleep, - '@1:Nat <- '@1:Nat)]-> 24 -90 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 30 -90 -[label('p2_crit, - '@1:Nat <- '@1:Nat)]-> 22[fold( - '@1:Nat <- '0.Nat)] -96 -[label('p1_sleep, none)]-> 40[fold( +36 -[label('p1_sleep, none)]-> 24[fold( '@1:Nat <- '1.NzNat)] -96 -[label('p2_crit, none)]-> 0[fold( +36 -[label('p2_crit, none)]-> 0[fold( 'X0:Nat <- '0.Nat ; 'X1:Nat <- '0.Nat)] -100 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 38 -100 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 30 -114 -[label('p1_sleep, - '@1:Nat <- '@1:Nat)]-> 40[fold( +40 -[label('p1_sleep, + '@1:Nat <- '@1:Nat)]-> 24[fold( '@1:Nat <- '_+_['1.NzNat,'@1:Nat])] -114 -[label('p2_crit, +40 -[label('p2_crit, '@1:Nat <- '@1:Nat)]-> 0[fold( 'X0:Nat <- '0.Nat ; 'X1:Nat <- '0.Nat)] -124 -[label('p1_crit, none)]-> 0[fold( +42 -[label('p1_crit, none)]-> 0[fold( 'X0:Nat <- '0.Nat ; 'X1:Nat <- '0.Nat)] -124 -[label('p2_sleep, none)]-> 34[fold( +42 -[label('p2_sleep, none)]-> 22[fold( '@1:Nat <- '1.NzNat)] -134 -[label('p1_wait2, - '@1:Nat <- '@1:Nat)]-> 24 -134 -[label('p2_wait2, - '@1:Nat <- '@1:Nat)]-> 36 -142 -[label('p1_crit, +46 -[label('p1_crit, '@1:Nat <- '@1:Nat)]-> 0[fold( 'X0:Nat <- '0.Nat ; 'X1:Nat <- '0.Nat)] -142 -[label('p2_sleep, - '@1:Nat <- '@1:Nat)]-> 34[fold( +46 -[label('p2_sleep, + '@1:Nat <- '@1:Nat)]-> 22[fold( '@1:Nat <- '_+_['1.NzNat,'@1:Nat])]) | 0 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'X0:Nat,'sleep.NcMode,'X1:Nat], 'tt.TrueLit`{Bool`}]) @@ -1368,83 +811,39 @@ result FoldedLabeledGraph: (0 -[label('p1_sleep, 'wait.NcMode,'_+_['1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) 8 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'1.NzNat], 'tt.TrueLit`{Bool`}]) -10 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'@1:Nat,'crit.Mode,'_+_[ - '1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -12 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'1.NzNat,'sleep.NcMode,'0.Nat], +10 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'1.NzNat,'sleep.NcMode,'0.Nat], 'tt.TrueLit`{Bool`}]) -14 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat], - 'sleep.NcMode,'@1:Nat],'ff.FalseLit`{Bool`}]) -16 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat], +12 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat], 'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) -20 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'1.NzNat,'wait.NcMode,'_+_[ +16 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'1.NzNat,'wait.NcMode,'_+_[ '1.NzNat,'1.NzNat]],'tt.TrueLit`{Bool`}]) -22 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'sleep.NcMode,'@1:Nat], - 'ff.FalseLit`{Bool`}]) -24 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat], - 'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -26 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat], +18 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat], 'crit.Mode,'1.NzNat],'tt.TrueLit`{Bool`}]) -30 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], - 'crit.Mode,'_+_['1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -32 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'@1:Nat,'sleep.NcMode,'0.Nat], - 'ff.FalseLit`{Bool`}]) -34 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat], +22 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat], 'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) -36 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat], - 'crit.Mode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -38 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], - 'wait.NcMode,'_+_['1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -40 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], +24 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], 'crit.Mode,'_+_['1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) -42 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_[ +26 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_[ '1.NzNat,'1.NzNat]],'tt.TrueLit`{Bool`}]) -44 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'1.NzNat,'crit.Mode,'_+_['1.NzNat, - '1.NzNat]],'ff.FalseLit`{Bool`}]) -46 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_[ - '1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -48 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat],'crit.Mode, - '_+_['1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -50 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_[ +28 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_[ '1.NzNat,'1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) -54 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'wait.NcMode,'_+_[ - '1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -56 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], - 'crit.Mode,'_+_['1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -58 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat], - 'sleep.NcMode,'@1:Nat],'ff.FalseLit`{Bool`}]) -64 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'@1:Nat,'wait.NcMode,'_+_[ - '1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -68 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat], +30 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat], 'sleep.NcMode,'0.Nat],'tt.TrueLit`{Bool`}]) -72 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat], - 'sleep.NcMode,'0.Nat],'ff.FalseLit`{Bool`}]) -80 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], +32 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], 'sleep.NcMode,'0.Nat],'tt.TrueLit`{Bool`}]) -82 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'_+_['1.NzNat, - '1.NzNat]],'ff.FalseLit`{Bool`}]) -86 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'_+_['1.NzNat, - '1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -88 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'@1:Nat], - 'sleep.NcMode,'0.Nat],'ff.FalseLit`{Bool`}]) -90 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'_+_['1.NzNat, - '@1:Nat]],'ff.FalseLit`{Bool`}]) -96 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'_+_['1.NzNat, +36 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'_+_['1.NzNat, '1.NzNat]],'tt.TrueLit`{Bool`}]) -100 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], - 'wait.NcMode,'_+_['1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -114 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'_+_[ - '1.NzNat,'1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) -124 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat], +40 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'crit.Mode,'_+_['1.NzNat, + '1.NzNat,'@1:Nat]],'tt.TrueLit`{Bool`}]) +42 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat], 'sleep.NcMode,'0.Nat],'tt.TrueLit`{Bool`}]) -134 |-> state('_st_['<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat], - 'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat]],'ff.FalseLit`{Bool`}]) -142 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], +46 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat,'1.NzNat,'@1:Nat], 'sleep.NcMode,'0.Nat],'tt.TrueLit`{Bool`}]) -| 187 +| 65 ========================================== reduce in BAKERY-FVP-CONDITIONAL-NARROWING-GRAPH : (state(inj(5)) ; state(inj( 6))) =>* state(inj(9)) . -rewrites: 3932 +rewrites: 3181 result [Bool]: not isEmpty?(intersect(state('_st_['<_`,_`,_`,_>['@1:Mode, '@2:NzNat,'crit.Mode,'@3:Nat],'_?=_['true.Bool,'_<_['@3:Nat,'@2:NzNat]]]), state('_st_['<_`,_`,_`,_>['crit.Mode,'X2:Nat,'crit.Mode,'X3:Nat], @@ -1478,7 +877,11 @@ result [Bool]: not isEmpty?(intersect(state('_st_['<_`,_`,_`,_>['@1:Mode, 'PC:Mode <- 'wait.NcMode ; 'QNC:NcMode <- '@2:NcMode ; 'Y1:NzNat <- '@1:NzNat ; - 'Y2:Nat <- '@3:Nat)]-> 9 + 'Y2:Nat <- '@3:Nat)]-> 0[fold( + 'PC:Mode <- 'crit.Mode ; + 'QNC:NcMode <- '@2:NcMode ; + 'Y1:NzNat <- '@1:NzNat ; + 'Y2:Nat <- '@3:Nat)] 0 -[label('p2_sleep, 'PC:Mode <- '@1:Mode ; 'QNC:NcMode <- 'sleep.NcMode ; @@ -1534,25 +937,25 @@ result [Bool]: not isEmpty?(intersect(state('_st_['<_`,_`,_`,_>['@1:Mode, 'PNC:NcMode <- '@1:NcMode ; 'QC:Mode <- 'wait.NcMode ; 'X1:Nat <- '@2:Nat ; - 'X2:NzNat <- '@3:NzNat)]-> 25) + 'X2:NzNat <- '@3:NzNat)]-> 1[fold( + 'PNC:NcMode <- '@1:NcMode ; + 'QC:Mode <- 'crit.Mode ; + 'X1:Nat <- '@2:Nat ; + 'X2:NzNat <- '@3:NzNat)]) | 0 |-> state('_st_['<_`,_`,_`,_>['PC:Mode,'Y1:NzNat,'QNC:NcMode,'Y2:Nat], 'tt.TrueLit`{Bool`}]) 1 |-> state('_st_['<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:NzNat], 'tt.TrueLit`{Bool`}]) 3 |-> state('_st_['<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'@2:NcMode,'@3:Nat], 'tt.TrueLit`{Bool`}]) -9 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'@1:NzNat,'@2:NcMode,'@3:Nat],'_?=_[ - 'true.Bool,'_<=_['@1:NzNat,'@3:Nat]]]) 13 |-> state('_st_['<_`,_`,_`,_>['@1:Mode,'@2:NzNat,'crit.Mode,'@3:Nat],'_?=_[ 'true.Bool,'_<_['@3:Nat,'@2:NzNat]]]) 17 |-> state('_st_['<_`,_`,_`,_>['crit.Mode,'@1:Nat,'@2:Mode,'@3:NzNat],'_?=_[ 'true.Bool,'_<=_['@1:Nat,'@3:NzNat]]]) 19 |-> state('_st_['<_`,_`,_`,_>['@1:NcMode,'@2:Nat,'sleep.NcMode,'0.Nat], 'tt.TrueLit`{Bool`}]) -25 |-> state('_st_['<_`,_`,_`,_>['@1:NcMode,'@2:Nat,'crit.Mode,'@3:NzNat], - '_?=_['true.Bool,'_<_['@3:NzNat,'@2:Nat]]]) | 26 -| 3 ; 9 ; 13 ; 17 ; 19 ; 25) =>[decrement(unbounded)]state('_st_['<_`,_`,_`,_>[ +| 3 ; 13 ; 17 ; 19) =>[decrement(unbounded)]state('_st_['<_`,_`,_`,_>[ 'crit.Mode,'X2:Nat,'crit.Mode,'X3:Nat],'tt.TrueLit`{Bool`}]) Warning: sort declarations for operator resolveNames failed preregularity check on 6 out of 48 sort tuples. First such tuple is (Type). @@ -1602,15 +1005,15 @@ reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : wellFormed(#M, init(9)) . rewrites: 3 result Bool: true ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : step(states(0)) . -rewrites: 19 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : step(state(init(0))) . +rewrites: 23 result NeTransitionSet: < label('p1_sleep, none),state('<_`,_`,_`,_>[ 'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'1.NzNat],'wait.NcMode,'_+_['1.NzNat, '1.NzNat]]) >,< label('p2_wait2, none),state('<_`,_`,_`,_>['sleep.NcMode, '_+_['1.NzNat,'1.NzNat,'1.NzNat],'crit.Mode,'_+_['1.NzNat,'1.NzNat]]) > ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : step(states(1)) . -rewrites: 45 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : step(state(init(1))) . +rewrites: 68 result NeTransitionSet: < label('p1_sleep, 'PNC:NcMode <- 'sleep.NcMode ; 'QC:Mode <- '@2:Mode ; @@ -1648,8 +1051,8 @@ result NeTransitionSet: < label('p1_sleep, 'X2:Nat <- '@2:Nat),state('<_`,_`,_`,_>['@1:NcMode,'_+_['@2:Nat,'@3:NzNat], 'crit.Mode,'@2:Nat]) > ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : step(states(2)) . -rewrites: 45 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : step(state(init(2))) . +rewrites: 68 result NeTransitionSet: < label('p1_crit, 'PC:Mode <- 'crit.Mode ; 'QNC:NcMode <- '@2:NcMode ; @@ -1687,24 +1090,26 @@ result NeTransitionSet: < label('p1_crit, 'Y2:Nat <- '@2:Nat),state('<_`,_`,_`,_>['@1:Mode,'_+_['@2:Nat,'@3:NzNat], 'crit.Mode,'@2:Nat]) > ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : step(states(3)) . -rewrites: 19 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : step(state(init(3))) . +rewrites: 23 result NeTransitionSet: < label('p1_sleep, 'X0:Nat <- '@1:Nat),state('<_`,_`,_`,_>['wait.NcMode,'_+_['1.NzNat,'@1:Nat], 'sleep.NcMode,'@1:Nat]) >,< label('p2_sleep, 'X0:Nat <- '@1:Nat),state('<_`,_`,_`,_>['sleep.NcMode,'@1:Nat,'wait.NcMode, '_+_['1.NzNat,'@1:Nat]]) > ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : states(3) <= states(1 ; 2) . -rewrites: 12 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : state(init(3)) <= states(init(1) | + init(2)) . +rewrites: 10 result Bool: true ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : states(1) <= states(1 ; 2) . -rewrites: 13 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : state(init(1)) <= states(init(1) | + init(2)) . +rewrites: 10 result Bool: true ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : states(2) <= states(1) . -rewrites: 7 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : state(init(2)) <= state(init(1)) . +rewrites: 5 result [Bool]: state('<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat]) <= state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat]) ========================================== @@ -1791,8 +1196,8 @@ reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : intersect(state('<_`,_`,_`,_>[ rewrites: 293 result NodeSet: .NodeSet ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : bfs(states(1)) . -rewrites: 519 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : bfs(state(init(1))) . +rewrites: 571 result FoldedLabeledGraph: (0 -[label('p1_sleep, 'PNC:NcMode <- 'sleep.NcMode ; 'QC:Mode <- '@2:Mode ; @@ -1909,8 +1314,8 @@ result FoldedLabeledGraph: (0 -[label('p1_sleep, 6 |-> state('<_`,_`,_`,_>['crit.Mode,'@2:Nat,'@1:Mode,'_+_['@2:Nat,'@3:Nat]]) | 33 ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : bfs(states(2)) . -rewrites: 515 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : bfs(state(init(2))) . +rewrites: 567 result FoldedLabeledGraph: (0 -[label('p1_crit, 'PC:Mode <- 'crit.Mode ; 'QNC:NcMode <- '@2:NcMode ; @@ -2028,8 +1433,8 @@ result FoldedLabeledGraph: (0 -[label('p1_crit, '@2:Nat]) | 33 ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : bfs(states(3)) . -rewrites: 3981 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : bfs(state(init(3))) . +rewrites: 4063 result FoldedLabeledGraph: (0 -[label('p1_sleep, 'X0:Nat <- '@1:Nat)]-> 2 0 -[label('p2_sleep, @@ -2131,8 +1536,8 @@ result FoldedLabeledGraph: (0 -[label('p1_sleep, 'sleep.NcMode,'0.Nat]) | 65 ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : bfs(states(1 ; 2)) . -rewrites: 1338 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : bfs(states(init(1) | init(2))) . +rewrites: 1443 result FoldedLabeledGraph: (0 -[label('p1_crit, 'PC:Mode <- 'crit.Mode ; 'QNC:NcMode <- '@2:NcMode ; @@ -2376,20 +1781,20 @@ result FoldedLabeledGraph: (0 -[label('p1_crit, 21 |-> state('<_`,_`,_`,_>['crit.Mode,'@2:Nat,'@1:Mode,'_+_['@2:Nat,'@3:Nat]]) | 66 ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(states(1))) . -rewrites: 525 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(state(init(1)))) . +rewrites: 21 result NeNodeSet: state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat]) ; state('<_`,_`,_`,_>['crit.Mode,'@1:Nat,'@2:Mode,'0.Nat]) ; state( '<_`,_`,_`,_>['crit.Mode,'@2:Nat,'@1:Mode,'_+_['@2:Nat,'@3:Nat]]) ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(states(2))) . -rewrites: 521 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(state(init(2)))) . +rewrites: 21 result NeNodeSet: state('<_`,_`,_`,_>['@1:Mode,'0.Nat,'crit.Mode,'@2:Nat]) ; state('<_`,_`,_`,_>['@1:Mode,'_+_['@2:Nat,'@3:NzNat],'crit.Mode,'@2:Nat]) ; state('<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat]) ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(states(3))) . -rewrites: 4019 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(state(init(3)))) . +rewrites: 85 result NeNodeSet: state('<_`,_`,_`,_>['crit.Mode,'1.NzNat,'sleep.NcMode, '0.Nat]) ; state('<_`,_`,_`,_>['crit.Mode,'1.NzNat,'wait.NcMode,'_+_[ '1.NzNat,'1.NzNat]]) ; state('<_`,_`,_`,_>['crit.Mode,'_+_['1.NzNat, @@ -2415,8 +1820,9 @@ result NeNodeSet: state('<_`,_`,_`,_>['crit.Mode,'1.NzNat,'sleep.NcMode, 'wait.NcMode,'_+_['1.NzNat,'1.NzNat,'@1:Nat],'wait.NcMode,'_+_['1.NzNat, '@1:Nat]]) ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(states(1 ; 2))) . -rewrites: 1350 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(states(init(1) | init( + 2)))) . +rewrites: 47 result NeNodeSet: state('<_`,_`,_`,_>['@1:Mode,'0.Nat,'crit.Mode,'@2:Nat]) ; state('<_`,_`,_`,_>['@1:Mode,'_+_['@2:Nat,'@3:NzNat],'crit.Mode,'@2:Nat]) ; state('<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat]) ; state( @@ -2424,38 +1830,39 @@ result NeNodeSet: state('<_`,_`,_`,_>['@1:Mode,'0.Nat,'crit.Mode,'@2:Nat]) ; 'crit.Mode,'@1:Nat,'@2:Mode,'0.Nat]) ; state('<_`,_`,_`,_>['crit.Mode, '@2:Nat,'@1:Mode,'_+_['@2:Nat,'@3:Nat]]) ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(states(1 ; 2))) <= ( - nodes(bfs(states(1))) ; nodes(bfs(states(2)))) . -rewrites: 2469 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(states(init(1) | init( + 2)))) <= (nodes(bfs(state(init(1)))) ; nodes(bfs(state(init(2))))) . +rewrites: 160 result Bool: true ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : (nodes(bfs(states(1))) ; nodes(bfs( - states(2)))) <= nodes(bfs(states(1 ; 2))) . -rewrites: 2469 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : (nodes(bfs(state(init(1)))) ; + nodes(bfs(state(init(2))))) <= nodes(bfs(states(init(1) | init(2)))) . +rewrites: 160 result Bool: true ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : states(3) <= states(1 ; 2) . -rewrites: 12 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : state(init(3)) <= states(init(1) | + init(2)) . +rewrites: 10 result Bool: true ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : states(3) <= nodes(bfs(states(1 ; - 2))) . -rewrites: 1363 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : state(init(3)) <= nodes(bfs(states( + init(1) | init(2)))) . +rewrites: 59 result Bool: true ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : states(1 ; 2) <= nodes(extend( - states(1 ; 2))) . -rewrites: 489 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : states(init(1) | init(2)) <= nodes( + extend(states(init(1) | init(2)))) . +rewrites: 548 result Bool: true ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : states(1 ; 2) <= nodes(bfs(states(1 - ; 2))) . -rewrites: 1373 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : states(init(1) | init(2)) <= nodes( + bfs(states(init(1) | init(2)))) . +rewrites: 70 result Bool: true ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(extend(states(1 ; 2))) <= - states(1 ; 2) . -rewrites: 477 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(extend(states(init(1) | init( + 2)))) <= states(init(1) | init(2)) . +rewrites: 536 result [Bool]: ((((state('<_`,_`,_`,_>['crit.Mode,'@2:Nat,'@1:Mode,'_+_[ '@2:Nat,'@3:Nat]]) <= (state('<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode, 'Y2:Nat]) ; state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat])) @@ -2474,14 +1881,15 @@ result [Bool]: ((((state('<_`,_`,_`,_>['crit.Mode,'@2:Nat,'@1:Mode,'_+_[ '@2:Nat]) <= (state('<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat]) ; state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat])) ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(extend(states(1 ; 2))) <= - nodes(bfs(states(1 ; 2))) . -rewrites: 1884 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(extend(states(init(1) | init( + 2)))) <= nodes(bfs(states(init(1) | init(2)))) . +rewrites: 641 result Bool: true ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(extend(states(5 ; 6 ; 7 ; - 8))) <= states(5 ; 6 ; 7 ; 8) . -rewrites: 532 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(extend(states(init(5) | init( + 6) | init(7) | init(8)))) <= states(init(5) | init(6) | init(7) | init(8)) + . +rewrites: 586 result [Bool]: (((((state('<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'@2:NcMode, '@3:Nat]) <= (state('<_`,_`,_`,_>['PC:Mode,'Y1:NzNat,'QNC:NcMode,'Y2:Nat]) ; state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:NzNat]) ; state( @@ -2518,13 +1926,14 @@ result [Bool]: (((((state('<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'@2:NcMode, '<_`,_`,_`,_>['QC:Mode,'Y1:NzNat,'wait.NcMode,'Y2:Nat]) ; state( '<_`,_`,_`,_>['wait.NcMode,'Y1:Nat,'QC:Mode,'Y2:NzNat])) ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(states(3))) <= states(1 ; - 2) . -rewrites: 4170 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(state(init(3)))) <= + states(init(1) | init(2)) . +rewrites: 235 result Bool: true ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : invariant(states(1 ; 2)) . -rewrites: 478 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : invariant(states(init(1) | init( + 2))) . +rewrites: 537 result [Bool]: ((((state('<_`,_`,_`,_>['crit.Mode,'@2:Nat,'@1:Mode,'_+_[ '@2:Nat,'@3:Nat]]) <= (state('<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode, 'Y2:Nat]) ; state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat])) @@ -2543,8 +1952,9 @@ result [Bool]: ((((state('<_`,_`,_`,_>['crit.Mode,'@2:Nat,'@1:Mode,'_+_[ '@2:Nat]) <= (state('<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat]) ; state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat])) ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : invariant(states(4 ; 5 ; 6)) . -rewrites: 643 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : invariant(states(init(4) | init(5) + | init(6))) . +rewrites: 705 result [Bool]: (((((state('<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'@2:NcMode, '@3:Nat]) <= (state('<_`,_`,_`,_>['PC:Mode,'Y1:NzNat,'QNC:NcMode,'Y2:Nat]) ; state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:NzNat]) ; state( @@ -2574,8 +1984,9 @@ result [Bool]: (((((state('<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'@2:NcMode, '<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:NzNat]) ; state( '<_`,_`,_`,_>['sleep.NcMode,'X0:Nat,'sleep.NcMode,'X1:Nat])) ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : invariant(states(5 ; 6 ; 7 ; 8)) . -rewrites: 533 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : invariant(states(init(5) | init(6) + | init(7) | init(8))) . +rewrites: 587 result [Bool]: (((((state('<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'@2:NcMode, '@3:Nat]) <= (state('<_`,_`,_`,_>['PC:Mode,'Y1:NzNat,'QNC:NcMode,'Y2:Nat]) ; state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:NzNat]) ; state( @@ -2612,9 +2023,9 @@ result [Bool]: (((((state('<_`,_`,_`,_>['sleep.NcMode,'0.Nat,'@2:NcMode, '<_`,_`,_`,_>['QC:Mode,'Y1:NzNat,'wait.NcMode,'Y2:Nat]) ; state( '<_`,_`,_`,_>['wait.NcMode,'Y1:Nat,'QC:Mode,'Y2:NzNat])) ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(states(1 ; 2))) <= - states(1 ; 2) . -rewrites: 1361 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : nodes(bfs(states(init(1) | init( + 2)))) <= states(init(1) | init(2)) . +rewrites: 58 result [Bool]: ((((state('<_`,_`,_`,_>['crit.Mode,'@2:Nat,'@1:Mode,'_+_[ '@2:Nat,'@3:Nat]]) <= (state('<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode, 'Y2:Nat]) ; state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat])) @@ -2633,9 +2044,9 @@ result [Bool]: ((((state('<_`,_`,_`,_>['crit.Mode,'@2:Nat,'@1:Mode,'_+_[ '@2:Nat]) <= (state('<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat]) ; state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat])) ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : check states(3) stable in states(1 - ; 2) . -rewrites: 487 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : check state(init(3)) stable in + states(init(1) | init(2)) . +rewrites: 545 result [Bool]: ((((state('<_`,_`,_`,_>['crit.Mode,'@2:Nat,'@1:Mode,'_+_[ '@2:Nat,'@3:Nat]]) <= (state('<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode, 'Y2:Nat]) ; state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat])) @@ -2654,12 +2065,13 @@ result [Bool]: ((((state('<_`,_`,_`,_>['crit.Mode,'@2:Nat,'@1:Mode,'_+_[ '@2:Nat]) <= (state('<_`,_`,_`,_>['PC:Mode,'Y1:Nat,'QNC:NcMode,'Y2:Nat]) ; state('<_`,_`,_`,_>['PNC:NcMode,'X1:Nat,'QC:Mode,'X2:Nat])) ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : states(3) =>* states(9) . -rewrites: 9029 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : state(init(3)) =>* state(init(9)) . +rewrites: 9110 result Bool: false ========================================== -reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : states(1 ; 2) =>* states(9) . -rewrites: 3480 +reduce in BAKERY-FVP-CTOR-NARROWING-GRAPH : states(init(1) | init(2)) =>* + state(init(9)) . +rewrites: 3526 result [Bool]: not isEmpty?(intersect(state('<_`,_`,_`,_>['@1:Mode,'0.Nat, 'crit.Mode,'@2:Nat]), state('<_`,_`,_`,_>['crit.Mode,'X2:Nat,'crit.Mode, 'X3:Nat])) ; intersect(state('<_`,_`,_`,_>['@1:Mode,'_+_['@2:Nat, diff --git a/tests/tools/lmc/bakery.maude b/tests/tools/lmc/bakery.maude index 2406c078..00db5893 100644 --- a/tests/tools/lmc/bakery.maude +++ b/tests/tools/lmc/bakery.maude @@ -4,7 +4,7 @@ load ../../../contrib/systems/bakery.maude load ../../../contrib/tools/lmc/lgraph-search.maude fmod RENAMED-NARROWING-GRAPH is - including ( NARROWING-GRAPH + GRAPH-ANALYSIS ) + including NARROWING-GRAPH * ( sort Nat to NatP , sort NzNat to NzNatP ) . @@ -63,16 +63,7 @@ reduce state(confManyWait) =>[10] state(confBad) . fmod FVP-BAKERY-INIT is protecting META-TERM . protecting UNCONDITIONALIZE-FVP-BOOL . - including CONDITIONAL-NARROWING-GRAPH + GRAPH-ANALYSIS . - - var N : Nat . vars NeNS NeNS' : NeNodeSet . - - op states : NodeSet -> [NodeSet] . - ---------------------------------- - eq states(N) = state(init(N)) . - - eq states(.NodeSet) = .NodeSet . - eq states(NeNS ; NeNS') = states(NeNS) ; states(NeNS') . + including CONDITIONAL-NARROWING-GRAPH + FOLDING-LABELED-GRAPH-SEARCH . op init : Nat -> [Term] . ------------------------- @@ -132,7 +123,7 @@ reduce (state(inj(5)) ; state(inj(6))) =>* state(inj(9)) . mod BAKERY-FVP-CTOR-NARROWING-GRAPH is protecting FVP-BAKERY-INIT . - including NARROWING-GRAPH + GRAPH-ANALYSIS . + extending NARROWING-GRAPH + FOLDING-LABELED-GRAPH-SEARCH . eq #M = upModule('BAKERY-FVP-CTOR, true) . endm @@ -160,14 +151,14 @@ reduce wellFormed(#M, init(7)) . reduce wellFormed(#M, init(8)) . reduce wellFormed(#M, init(9)) . -reduce step(states(0)) . -reduce step(states(1)) . -reduce step(states(2)) . -reduce step(states(3)) . +reduce step(state(init(0))) . +reduce step(state(init(1))) . +reduce step(state(init(2))) . +reduce step(state(init(3))) . -reduce states(3) <= states(1 ; 2) . -reduce states(1) <= states(1 ; 2) . -reduce states(2) <= states(1) . +reduce state(init(3)) <= states(init(1) | init(2)) . +reduce state(init(1)) <= states(init(1) | init(2)) . +reduce state(init(2)) <= state(init(1)) . reduce state('wait.NcMode) <= state('PC:Mode) . reduce state('_+_['1.NzNat,'V3:Nat]) <= state('Y1:NzNat) . @@ -202,37 +193,37 @@ reduce intersect( state('<_`,_`,_`,_>['V1:Mode,'0.Nat,'crit.Mode,'V2:Nat]) ) . --- both initial states yield finite state-graphs -reduce bfs(states(1)) . -reduce bfs(states(2)) . -reduce bfs(states(3)) . -reduce bfs(states(1 ; 2)) . - -reduce nodes(bfs(states(1))) . -reduce nodes(bfs(states(2))) . -reduce nodes(bfs(states(3))) . -reduce nodes(bfs(states(1 ; 2))) . - -reduce nodes(bfs(states(1 ; 2))) <= (nodes(bfs(states(1))) ; nodes(bfs(states(2)))) . -reduce (nodes(bfs(states(1))) ; nodes(bfs(states(2)))) <= nodes(bfs(states(1 ; 2))) . - -reduce states(3) <= (states(1 ; 2)) . -reduce states(3) <= nodes(bfs(states(1 ; 2))) . -reduce (states(1 ; 2)) <= nodes(extend(states(1 ; 2))) . -reduce (states(1 ; 2)) <= nodes(bfs(states(1 ; 2))) . -reduce nodes(extend(states(1 ; 2))) <= states(1 ; 2) . -reduce nodes(extend(states(1 ; 2))) <= nodes(bfs(states(1 ; 2))) . -reduce nodes(extend(states(5 ; 6 ; 7 ; 8))) <= states(5 ; 6 ; 7 ; 8) . +reduce bfs(state(init(1))) . +reduce bfs(state(init(2))) . +reduce bfs(state(init(3))) . +reduce bfs(states(init(1) | init(2))) . + +reduce nodes(bfs(state(init(1)))) . +reduce nodes(bfs(state(init(2)))) . +reduce nodes(bfs(state(init(3)))) . +reduce nodes(bfs(states(init(1) | init(2)))) . + +reduce nodes(bfs(states(init(1) | init(2)))) <= (nodes(bfs(state(init(1)))) ; nodes(bfs(state(init(2))))) . +reduce (nodes(bfs(state(init(1)))) ; nodes(bfs(state(init(2))))) <= nodes(bfs(states(init(1) | init(2)))) . + +reduce state(init(3)) <= states(init(1) | init(2)) . +reduce state(init(3)) <= nodes(bfs(states(init(1) | init(2)))) . +reduce states(init(1) | init(2)) <= nodes(extend(states(init(1) | init(2)))) . +reduce states(init(1) | init(2)) <= nodes(bfs(states(init(1) | init(2)))) . +reduce nodes(extend(states(init(1) | init(2)))) <= states(init(1) | init(2)) . +reduce nodes(extend(states(init(1) | init(2)))) <= nodes(bfs(states(init(1) | init(2)))) . +reduce nodes(extend(states(init(5) | init(6) | init(7) | init(8)))) <= states(init(5) | init(6) | init(7) | init(8)) . --- state init(3) stays within init(1) ; init(2) -reduce nodes(bfs(states(3))) <= (states(1 ; 2)) . +reduce nodes(bfs(state(init(3)))) <= states(init(1) | init(2)) . --- even though in general init(1) ; init(2) is *not* an invariant -reduce invariant(states(1 ; 2)) . -reduce invariant(states(4 ; 5 ; 6)) . -reduce invariant(states(5 ; 6 ; 7 ; 8)) . -reduce nodes(bfs(states(1 ; 2))) <= (states(1 ; 2)) . -reduce check states(3) stable in states(1 ; 2) . +reduce invariant(states(init(1) | init(2))) . +reduce invariant(states(init(4) | init(5) | init(6))) . +reduce invariant(states(init(5) | init(6) | init(7) | init(8))) . +reduce nodes(bfs(states(init(1) | init(2)))) <= states(init(1) | init(2)) . +reduce check state(init(3)) stable in states(init(1) | init(2)) . --- state 3 never reaches the bad state 9, but states 1 ; 2 can -reduce states(3) =>* states(9) . -reduce states(1 ; 2) =>* states(9) . +reduce state(init(3)) =>* state(init(9)) . +reduce states(init(1) | init(2)) =>* state(init(9)) . diff --git a/tests/tools/lmc/bank-account.expected b/tests/tools/lmc/bank-account.expected index 19ff3671..26e31123 100644 --- a/tests/tools/lmc/bank-account.expected +++ b/tests/tools/lmc/bank-account.expected @@ -228,7 +228,7 @@ rewrites: 6 result Bool: true ========================================== reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : bfs(state(cinit(0))) . -rewrites: 150 +rewrites: 177 result FoldedLabeledGraph: (0 -[label('deposit, 'C:Form`{Bool`} <- '@4:Form`{Bool`} ; 'MSGS:MsgConf <- '@3:MsgConf ; @@ -278,39 +278,27 @@ result FoldedLabeledGraph: (0 -[label('deposit, | 11 ========================================== reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : bfs(state(cinit(1)), 1) . -rewrites: 1069 +rewrites: 875 result FoldedLabeledGraph?: (0 -[label('deposit, - 'MSGS:MsgConf <- '%1:MsgConf ; - 'N:Nat <- '%2:Nat ; - 'X:Nat <- '_+_['%2:Nat,'%3:NzNat])]-> 2 -0 -[label('deposit, 'MSGS:MsgConf <- '%1:MsgConf ; 'N:Nat <- '_+_['%2:Nat,'%3:Nat] ; - 'X:Nat <- '%2:Nat)]-> 4 + 'X:Nat <- '%2:Nat)]-> 2 0 -[label('deposit, 'MSGS:MsgConf <- '@3:MsgConf ; 'N:Nat <- '@1:Nat ; - 'X:Nat <- '@2:Nat)]-> 6 + 'X:Nat <- '@2:Nat)]-> 4 0 -[label('doWithdrawal1, 'MSGS:MsgConf <- '_`,_['%1:MsgConf,'withdraw['_+_['%2:Nat,'%3:Nat]]] ; 'N:Nat <- '_+_['%2:Nat,'%3:Nat,'%4:Nat] ; - 'X:Nat <- '%2:Nat)]-> 4[fold( + 'X:Nat <- '%2:Nat)]-> 2[fold( '%1:MsgConf <- '%1:MsgConf ; '%2:Nat <- '0.Nat ; '%3:Nat <- '%4:Nat ; '%4:Nat <- '0.Nat)] -0 -[label('doWithdrawal2, - 'MSGS:MsgConf <- '_`,_['%4:MsgConf,'withdraw['%1:Nat]] ; - 'N:Nat <- '_+_['%1:Nat,'%2:Nat] ; - 'X:Nat <- '_+_['%1:Nat,'%2:Nat,'%3:NzNat])]-> 2[fold( - '%1:MsgConf <- '%4:MsgConf ; - '%2:Nat <- '%2:Nat ; - '%3:NzNat <- '%3:NzNat ; - '%4:Nat <- '0.Nat)] 0 -[label('doWithdrawal2, 'MSGS:MsgConf <- '_`,_['%4:MsgConf,'withdraw['%1:Nat]] ; 'N:Nat <- '_+_['%1:Nat,'%2:Nat,'%3:Nat] ; - 'X:Nat <- '_+_['%1:Nat,'%2:Nat])]-> 4[fold( + 'X:Nat <- '_+_['%1:Nat,'%2:Nat])]-> 2[fold( '%1:MsgConf <- '%4:MsgConf ; '%2:Nat <- '%2:Nat ; '%3:Nat <- '0.Nat ; @@ -318,70 +306,63 @@ result FoldedLabeledGraph?: (0 -[label('deposit, 0 -[label('doWithdrawal2, 'MSGS:MsgConf <- '_`,_['@4:MsgConf,'withdraw['@1:Nat]] ; 'N:Nat <- '_+_['@3:Nat,'@1:Nat] ; - 'X:Nat <- '_+_['@2:Nat,'@1:Nat])]-> 14 + 'X:Nat <- '_+_['@2:Nat,'@1:Nat])]-> 10 0 -[label('initWithdrawal, 'MSGS:MsgConf <- '%2:MsgConf ; 'N:Nat <- '_+_['%1:Nat,'%3:Nat,'%4:Nat] ; - 'X:Nat <- '%1:Nat)]-> 4[fold( + 'X:Nat <- '%1:Nat)]-> 2[fold( '%1:MsgConf <- '_`,_['%2:MsgConf,'withdraw['%3:Nat]] ; '%2:Nat <- '_+_['%1:Nat,'%3:Nat] ; '%3:Nat <- '0.Nat ; '%4:Nat <- '%4:Nat)] -0 -[label('overdraft, - 'MSGS:MsgConf <- '_`,_['%1:MsgConf,'withdraw['_+_['1.NzNat,'%2:Nat,'%3:Nat]]] - ; - 'N:Nat <- '%2:Nat ; - 'X:Nat <- '_+_['%2:Nat,'%4:NzNat])]-> 18 0 -[label('overdraft, 'MSGS:MsgConf <- '_`,_['%1:MsgConf,'withdraw['_+_['1.NzNat,'%2:Nat,'%3:Nat, '%4:Nat]]] ; 'N:Nat <- '_+_['%2:Nat,'%3:Nat] ; - 'X:Nat <- '%2:Nat)]-> 20 + 'X:Nat <- '%2:Nat)]-> 14 0 -[label('overdraft, 'MSGS:MsgConf <- '_`,_['@2:MsgConf,'withdraw['_+_['1.NzNat,'@3:Nat,'@4:Nat]]] ; 'N:Nat <- '@3:Nat ; - 'X:Nat <- '@1:Nat)]-> 22) + 'X:Nat <- '@1:Nat)]-> 16) | 0 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['N:Nat,'X:Nat,'false.Bool], 'MSGS:MsgConf],'_?=_['true.Bool,'_<=_['X:Nat,'N:Nat]]]) -2 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['_+_['%2:Nat,'%4:Nat],'_+_[ - '%2:Nat,'%3:NzNat],'false.Bool],'%1:MsgConf],'ff.FalseLit`{Bool`}]) -4 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['_+_['%2:Nat,'%3:Nat, +2 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['_+_['%2:Nat,'%3:Nat, '%4:Nat],'%2:Nat,'false.Bool],'%1:MsgConf],'tt.TrueLit`{Bool`}]) -6 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['_+_['@1:Nat,'@4:Nat], +4 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['_+_['@1:Nat,'@4:Nat], '@2:Nat,'false.Bool],'@3:MsgConf],'_?=_['true.Bool,'_<=_['@2:Nat, '@1:Nat]]]) -14 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['@3:Nat,'@2:Nat, +10 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['@3:Nat,'@2:Nat, 'false.Bool],'@4:MsgConf],'_?=_['true.Bool,'_<=_['_+_['@2:Nat,'@1:Nat], '_+_['@3:Nat,'@1:Nat]]]]) -18 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['%2:Nat,'_+_['%2:Nat, - '%4:NzNat],'true.Bool],'%1:MsgConf],'ff.FalseLit`{Bool`}]) -20 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['_+_['%2:Nat,'%3:Nat], +14 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['_+_['%2:Nat,'%3:Nat], '%2:Nat,'true.Bool],'%1:MsgConf],'tt.TrueLit`{Bool`}]) -22 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['@3:Nat,'@1:Nat,'true.Bool], +16 |-> state('_st_['_#_['<`bal:_pend:_overdraft:_>['@3:Nat,'@1:Nat,'true.Bool], '@2:MsgConf],'_?=_['true.Bool,'_<=_['@1:Nat,'@3:Nat]]]) -| 23 -| 2 ; 4 ; 6 ; 14 ; 18 ; 20 ; 22 +| 17 +| 2 ; 4 ; 10 ; 14 ; 16 ========================================== reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : state(pred(1)) <= state(pred( 0)) . rewrites: 8 result Bool: true ========================================== -reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : states(1) <= states(0) . -rewrites: 14 +reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : state(cinit(1)) <= state(cinit( + 0)) . +rewrites: 12 result Bool: true ========================================== -reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : states(1) <= states(2) . -rewrites: 16 +reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : state(cinit(1)) <= state(cinit( + 2)) . +rewrites: 14 result [Bool]: state('_st_['_#_['<`bal:_pend:_overdraft:_>['N:Nat,'X:Nat, 'false.Bool],'MSGS:MsgConf],'_?=_['true.Bool,'_<=_['X:Nat,'N:Nat]]]) <= state('_st_['_#_['<`bal:_pend:_overdraft:_>['N:Nat,'X:Nat,'true.Bool], 'MSGS:MsgConf],'C:Form`{Bool`}]) ========================================== -reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : intersect(states(0), states(2)) - . -rewrites: 285 +reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : intersect(state(cinit(0)), + state(cinit(2))) . +rewrites: 283 result NodeSet: .NodeSet ========================================== reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : implies?(pred(0), pred(0)) . @@ -389,25 +370,26 @@ rewrites: 2 result Bool: true ========================================== reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : implies?(pred(0), pred(1)) . -rewrites: 13 +rewrites: 15 result Bool: false ========================================== reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : implies?(pred(1), pred(2)) . -rewrites: 13 -result Bool: false +rewrites: 14 +result Bool: true ========================================== -reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : invariant(states(0)) . -rewrites: 146 +reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : invariant(state(cinit(0))) . +rewrites: 176 result [Bool]: state('_st_['_#_['<`bal:_pend:_overdraft:_>['@4:Nat,'@1:Nat, 'true.Bool],'@3:MsgConf],'@2:Form`{Bool`}]) <= state('_st_['_#_[ '<`bal:_pend:_overdraft:_>['N:Nat,'X:Nat,'false.Bool],'MSGS:MsgConf], 'C:Form`{Bool`}]) ========================================== -reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : invariant(states(2)) . -rewrites: 29 +reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : invariant(state(cinit(2))) . +rewrites: 30 result Bool: true ========================================== -reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : invariant(states(0 ; 2)) . -rewrites: 190 +reduce in BANK-ACCOUNT-CTOR-UNCONDITIONALIZED : invariant(state(cinit(0)) ; + state(cinit(2))) . +rewrites: 218 result Bool: true Bye. diff --git a/tests/tools/lmc/bank-account.maude b/tests/tools/lmc/bank-account.maude index 41130e25..1d9e7b42 100644 --- a/tests/tools/lmc/bank-account.maude +++ b/tests/tools/lmc/bank-account.maude @@ -8,7 +8,7 @@ load ../../../contrib/tools/meta/narrowing.maude --- ============================= mod BANK-ACCOUNT-INIT-STATES is - extending CONDITIONAL-NARROWING-GRAPH + GRAPH-ANALYSIS . + extending CONDITIONAL-NARROWING-GRAPH + FOLDING-LABELED-GRAPH-SEARCH . protecting UNCONDITIONALIZE-FVP-BOOL . var N : Nat . vars NeNS NeNS' : NeNodeSet . vars T T' : Term . @@ -56,13 +56,6 @@ mod BANK-ACCOUNT-INIT-STATES is -------------------------------- eq sub(0) = ('MSGS:MsgConf <- '@1:MsgConf ; 'N:Nat <- '_+_['@2:Nat,'@3:Nat,'debts['@1:MsgConf]] ; 'X:Nat <- 'debts['@1:MsgConf]) . eq sub(1) = ('MSGS:MsgConf <- '@3:MsgConf ; 'N:Nat <- '_+_['@1:Nat,'@4:Nat] ; 'X:Nat <- '@2:Nat) . - - op states : NodeSet -> [NodeSet] . - ---------------------------------- - eq states(.NodeSet) = .NodeSet . - eq states(NeNS ; NeNS') = states(NeNS) ; states(NeNS') . - - eq states(N) = state(cinit(N)) . endm --- Module BANK-ACCOUNT-UNCONDITIONALIZED @@ -125,19 +118,19 @@ reduce wellFormed(#M, cinit(7)) . reduce bfs(state(cinit(0))) . reduce bfs(state(cinit(1)), 1) . -reduce state(pred(1)) <= state(pred(0)) . -reduce states(1) <= states(0) . -reduce states(1) <= states(2) . +reduce state(pred(1)) <= state(pred(0)) . +reduce state(cinit(1)) <= state(cinit(0)) . +reduce state(cinit(1)) <= state(cinit(2)) . -reduce intersect(states(0), states(2)) . +reduce intersect(state(cinit(0)), state(cinit(2))) . reduce implies?(pred(0), pred(0)) . reduce implies?(pred(0), pred(1)) . reduce implies?(pred(1), pred(2)) . -reduce invariant(states(0)) . -reduce invariant(states(2)) . -reduce invariant(states(0 ; 2)) . +reduce invariant(state(cinit(0))) . +reduce invariant(state(cinit(2))) . +reduce invariant(state(cinit(0)) ; state(cinit(2))) . --- ; --- proving that `states(1)` is an invariant --- ; reduce invariant(states(1)) . diff --git a/tests/tools/lmc/lgraph-search.expected b/tests/tools/lmc/lgraph-search.expected index 039d300b..74b1c25b 100644 --- a/tests/tools/lmc/lgraph-search.expected +++ b/tests/tools/lmc/lgraph-search.expected @@ -28,7 +28,7 @@ result Fold: < ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : fold(E, D) . rewrites: 0 -result [Fold]: fold(E, D) +result [FoldSet]: fold(E, D) ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : B <= (A ; B ; C) . rewrites: 4 @@ -146,8 +146,8 @@ reduce in GRAPH-FOLDING-SEARCH-TEST : (0 |-> A 1 |-> B 2 |-> F 3 |-> G)[7] . -rewrites: 12 -result [Bound,NodeSet]: .NodeMap[7] +rewrites: 13 +result NodeSet: .NodeSet ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : (0 |-> A 1 |-> B @@ -160,8 +160,8 @@ reduce in GRAPH-FOLDING-SEARCH-TEST : (0 |-> A 1 |-> B 2 |-> F 3 |-> G)[2 ; 3 ; 7] . -rewrites: 35 -result [Bound,NodeSet]: F ; G ; .NodeMap[7] +rewrites: 36 +result NeNodeSet: F ; G ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : insert(3 |-> A, .NodeMap) . rewrites: 2 @@ -188,6 +188,43 @@ result NodeMap?: {4 |-> A 1 |-> D 5 |-> E,5,5} ========================================== +reduce in GRAPH-FOLDING-SEARCH-TEST : nodes(.NodeMap) . +rewrites: 1 +result NodeSet: .NodeSet +========================================== +reduce in GRAPH-FOLDING-SEARCH-TEST : nodes(0 |-> A +1 |-> B +2 |-> F) . +rewrites: 11 +result NeNodeSet: A ; B ; F +========================================== +reduce in GRAPH-FOLDING-SEARCH-TEST : intersects-with(0 |-> A +1 |-> B +2 |-> E, C ; D) . +rewrites: 101 +result NeNodeSet: 1 ; 2 +========================================== +reduce in GRAPH-FOLDING-SEARCH-TEST : intersects-with(1 |-> B +2 |-> E, C) . +rewrites: 34 +result NzNat: 1 +========================================== +reduce in GRAPH-FOLDING-SEARCH-TEST : intersects-with(0 |-> A +2 |-> E, C) . +rewrites: 41 +result NodeSet: .NodeSet +========================================== +reduce in GRAPH-FOLDING-SEARCH-TEST : intersects-with(0 |-> A +1 |-> B +2 |-> E, A ; C) . +rewrites: 101 +result NeNodeSet: 0 ; 1 +========================================== +reduce in GRAPH-FOLDING-SEARCH-TEST : intersects-with(1 |-> B +2 |-> E, D) . +rewrites: 34 +result NzNat: 2 +========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : insert(.NodeSet, .FoldedLabeledGraph) . rewrites: 2 result FoldedLabeledGraph: .LabeledGraph @@ -472,21 +509,21 @@ reduce in GRAPH-FOLDING-SEARCH-TEST : nodes(.LabeledGraph | 0 |-> A | 1 | 0) . -rewrites: 2 +rewrites: 4 result Node: A ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : nodes(extend(.LabeledGraph | 0 |-> A | 1 | 0)) . -rewrites: 64 +rewrites: 70 result NeNodeSet: A ; B ; D ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : nodes(extend(extend(.LabeledGraph | 0 |-> A | 1 | 0))) . -rewrites: 164 +rewrites: 174 result NeNodeSet: A ; B ; C ; D ; G ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : nodes(extend(.LabeledGraph @@ -495,12 +532,12 @@ reduce in GRAPH-FOLDING-SEARCH-TEST : nodes(extend(.LabeledGraph 2 |-> C | 3 | 0 ; 1 ; 2)) . -rewrites: 136 +rewrites: 144 result NeNodeSet: A ; B ; C ; D ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : nodes(extend(insert(A ; B ; C, .FoldedLabeledGraph))) . -rewrites: 161 +rewrites: 169 result NeNodeSet: A ; B ; C ; D ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : frontier(.FoldedLabeledGraph) . @@ -576,7 +613,7 @@ result FoldedLabeledGraph: (0 -[x]-> 2 | 17 ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : bfs(A, unbounded) == bfs(A) . -rewrites: 508 +rewrites: 16 result Bool: true ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : bfs(C, 1) . @@ -729,15 +766,15 @@ rewrites: 9 result Bool: true ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : invariant(E) . -rewrites: 30 +rewrites: 32 result Bool: true ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : invariant(A ; B ; C) . -rewrites: 174 +rewrites: 182 result Bool: false ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : invariant(A ; B ; C ; D ; E ; F ; G) . -rewrites: 570 +rewrites: 584 result Bool: true ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : check .NodeSet stable in .NodeSet . @@ -749,7 +786,7 @@ rewrites: 3 result Bool: false ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : check A stable in A . -rewrites: 82 +rewrites: 88 result Bool: false ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : check A ; B stable in A . @@ -757,12 +794,12 @@ rewrites: 6 result Bool: false ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : check A ; B ; C stable in A ; B ; C . -rewrites: 192 +rewrites: 200 result Bool: false ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : check A ; B ; C stable in A ; B ; C ; D ; E ; F ; G . -rewrites: 588 +rewrites: 602 result Bool: true ========================================== reduce in GRAPH-FOLDING-SEARCH-TEST : A =>* A . diff --git a/tests/tools/lmc/lgraph-search.maude b/tests/tools/lmc/lgraph-search.maude index dbbf0b97..86010164 100644 --- a/tests/tools/lmc/lgraph-search.maude +++ b/tests/tools/lmc/lgraph-search.maude @@ -1,6 +1,5 @@ set show timing off . -load ../../../contrib/systems/token.maude load ../../../contrib/tools/lmc/lgraph-search.maude --- Testing Harnesses @@ -10,7 +9,7 @@ load ../../../contrib/tools/lmc/lgraph-search.maude --- -------------- fmod GRAPH-FOLDING-SEARCH-TEST is - extending GRAPH-ANALYSIS . + extending FOLDING-LABELED-GRAPH-SEARCH . ops A B C D E F G : -> Node . ops x y z : -> Label . @@ -93,6 +92,16 @@ reduce insert( 3 |-> D , 2 |-> E ) . reduce insert( 2 |-> D , 4 |-> A 1 |-> D ) . reduce insert( 5 |-> E , 4 |-> A 1 |-> D ) . +reduce nodes(.NodeMap) . +reduce nodes(0 |-> A 1 |-> B 2 |-> F) . + +reduce intersects-with( 0 |-> A 1 |-> B 2 |-> E , C ; D ) . +reduce intersects-with( 1 |-> B 2 |-> E , C ) . +reduce intersects-with( 0 |-> A 2 |-> E , C ) . + +reduce intersects-with( 0 |-> A 1 |-> B 2 |-> E , A ; C ) . +reduce intersects-with( 1 |-> B 2 |-> E , D ) . + reduce insert( .NodeSet , .FoldedLabeledGraph) . reduce insert( A ; B ; C , .FoldedLabeledGraph) . reduce insert( A ; B ; C ; D ; E ; F ; G, .FoldedLabeledGraph) . @@ -135,8 +144,9 @@ reduce frontier(extend(E)) . reduce frontier(extend(A ; B ; C)) . reduce frontier(extend(A ; B ; C ; D ; E ; F ; G)) . ---- Test Module GRAPH-ANALYSIS ---- -------------------------- + +--- Test Module FOLDING-LABELED-GRAPH-SEARCH +--- ---------------------------------------- reduce bfs(A, 0) . reduce bfs(A, 1) . diff --git a/tests/tools/lmc/thermostat.expected b/tests/tools/lmc/thermostat.expected new file mode 100644 index 00000000..30f20588 --- /dev/null +++ b/tests/tools/lmc/thermostat.expected @@ -0,0 +1,389 @@ +Warning: sort declarations for operator resolveNames failed preregularity check + on 6 out of 48 sort tuples. First such tuple is (Type). +Warning: sort declarations for operator resolveNames failed preregularity check + on 1 out of 26 sort tuples. First such tuple is (NullDeclSet). +Warning: ctor declarations for associative operator __ are conflict on 138 out + of 17576 sort triples. First such triple is (ModuleDeclSet, SortDeclSet, + SortDeclSet). +========================================== +reduce in THERMOSTAT-INT-NARROWING-GRAPH : wellFormed(#M) . +rewrites: 121 +result Bool: (true).Bool +========================================== +reduce in THERMOSTAT-INT-NARROWING-GRAPH : wellFormed(#M, goodConf) . +rewrites: 26 +result Bool: (true).Bool +========================================== +reduce in THERMOSTAT-INT-NARROWING-GRAPH : wellFormed(#M, badConf) . +rewrites: 26 +result Bool: (true).Bool +========================================== +reduce in THERMOSTAT-INT-NARROWING-GRAPH : bfs(state(goodConf), 2) . +rewrites: 31916 +result FoldedLabeledGraph?: (0 -[label('inmode-off, + 'T:Int <- '%1:Int ; + 'TMP:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'%2:Nat])]-> 2 +0 -[label('inmode-off, + 'T:Int <- '@1:Int ; + 'TMP:Int <- '@2:Int)]-> 4 +0 -[label('inmode-off, + 'T:Int <- '@1:Int ; + 'TMP:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 6 +0 -[label('inmode-off, + 'T:Int <- '@1:Int ; + 'TMP:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat])]-> 8 +0 -[label('inmode-off, + 'T:Int <- '@1:Int ; + 'TMP:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat])]-> 10 +0 -[label('inmode-off, + 'T:Int <- '@1:Int ; + 'TMP:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat])]-> 12 +0 -[label('inmode-off, + 'T:Int <- '@1:Int ; + 'TMP:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat])]-> 14 +0 -[label('inmode-off, + 'T:Int <- '@1:Int ; + 'TMP:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 16 +0 -[label('turning-on, + 'T:Int <- '%1:Int ; + 'TMP:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'%2:Nat])]-> 18 +0 -[label('turning-on, + 'T:Int <- '@1:Int ; + 'TMP:Int <- '@2:Int)]-> 20 +0 -[label('turning-on, + 'T:Int <- '@1:Int ; + 'TMP:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 22 +0 -[label('turning-on, + 'T:Int <- '@1:Int ; + 'TMP:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 24 +0 -[label('turning-on, + 'T:Int <- '@1:Int ; + 'TMP:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 26 +2 -[label('tick, + '%1:Int <- '%1:Int ; + '%2:Nat <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'%2:Nat])]-> 28 +2 -[label('tick, + '%1:Int <- '@1:Int ; + '%2:Nat <- '@2:Nat)]-> 30 +2 -[label('tick, + '%1:Int <- '@1:Int ; + '%2:Nat <- '_+_['1.NzNat,'1.NzNat,'1.NzNat])]-> 32 +2 -[label('tick, + '%1:Int <- '@1:Int ; + '%2:Nat <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 34 +2 -[label('tick, + '%1:Int <- '@1:Int ; + '%2:Nat <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 36 +2 -[label('tick, + '%1:Int <- '@1:Int ; + '%2:Nat <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 38 +2 -[label('tick, + '%1:Int <- '@1:Int ; + '%2:Nat <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat])]-> 40 +2 -[label('tick, + '%1:Int <- '@1:Int ; + '%2:Nat <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat])]-> 42 +4 -[label('tick, + '@1:Int <- '%1:Int ; + '@2:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'%2:Nat])]-> 30[fold( + '@1:Int <- '%1:Int ; + '@2:Nat <- '%2:Nat)] +4 -[label('tick, + '@1:Int <- '%1:Int ; + '@2:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 32[ + fold( + '@1:Int <- '%1:Int)] +4 -[label('tick, + '@1:Int <- '%1:Int ; + '@2:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat])]-> 34[fold( + '@1:Int <- '%1:Int)] +4 -[label('tick, + '@1:Int <- '%1:Int ; + '@2:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat])]-> 36[fold( + '@1:Int <- '%1:Int)] +4 -[label('tick, + '@1:Int <- '%1:Int ; + '@2:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat])]-> 38[fold( + '@1:Int <- '%1:Int)] +4 -[label('tick, + '@1:Int <- '%1:Int ; + '@2:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat])]-> 40[fold( + '@1:Int <- '%1:Int)] +4 -[label('tick, + '@1:Int <- '%1:Int ; + '@2:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 42[fold( + '@1:Int <- '%1:Int)] +4 -[label('tick, + '@1:Int <- '@1:Int ; + '@2:Int <- '@2:Int)]-> 58 +4 -[label('tick, + '@1:Int <- '@1:Int ; + '@2:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'@2:Nat])]-> + 28[fold( + '%1:Int <- '@1:Int ; + '%2:Nat <- '@2:Nat)] +6 -[label('tick, + '@1:Int <- '@1:Int)]-> 32 +8 -[label('tick, + '@1:Int <- '@1:Int)]-> 34 +10 -[label('tick, + '@1:Int <- '@1:Int)]-> 36 +12 -[label('tick, + '@1:Int <- '@1:Int)]-> 38 +14 -[label('tick, + '@1:Int <- '@1:Int)]-> 40 +16 -[label('tick, + '@1:Int <- '@1:Int)]-> 42 +18 -[label('tick, + '%2:Nat <- '0.Nat)]-> 76 +18 -[label('tick, + '%2:Nat <- '1.NzNat)]-> 80 +18 -[label('tick, + '%2:Nat <- '@1:Nat)]-> 78[fold( + '%1:Nat <- '@1:Nat)] +18 -[label('tick, + '%2:Nat <- '_+_['1.NzNat,'1.NzNat])]-> 82 +20 -[label('tick, + '@2:Int <- '@1:Int)]-> 74 +20 -[label('tick, + '@2:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 76 +20 -[label('tick, + '@2:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'%1:Nat])]-> 78 +20 -[label('tick, + '@2:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 80 +20 -[label('tick, + '@2:Int <- '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat])]-> 82 +22 -[label('tick, none)]-> 76 +24 -[label('tick, none)]-> 80 +26 -[label('tick, none)]-> 82) +| 0 |-> state('_st_['`{_`,_`,_`}['T:Int,'TMP:Int,'off.Mode],'_/\_['_?=_['_<=_[ + 'min.Int,'TMP:Int],'true.Bool],'_?=_['_<=_['TMP:Int,'max.Int], + 'true.Bool]]]) +2 |-> state('_st_['<_`,_`,_>['%1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'%2:Nat], + 'off.InMode],'_/\_['_?=_['true.Bool,'_<=_['%2:Nat,'_+_['1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat]]],'_?=_['false.Bool, + '_<_['%2:Nat,'_+_['1.NzNat,'1.NzNat,'1.NzNat]]]]]) +4 |-> state('_st_['<_`,_`,_>['@1:Int,'@2:Int,'off.InMode],'_/\_['_?=_[ + 'true.Bool,'_<=_['@2:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat]]],'_?=_['true.Bool,'_<=_[ + '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat],'@2:Int]],'_?=_['false.Bool,'_<_['@2:Int,'_+_[ + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat]]]]]) +6 |-> state('_st_['<_`,_`,_>['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat],'off.InMode],'tt.TrueLit`{Bool`}]) +8 |-> state('_st_['<_`,_`,_>['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat],'off.InMode],'tt.TrueLit`{Bool`}]) +10 |-> state('_st_['<_`,_`,_>['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat],'off.InMode],'tt.TrueLit`{Bool`}]) +12 |-> state('_st_['<_`,_`,_>['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'off.InMode],'tt.TrueLit`{Bool`}]) +14 |-> state('_st_['<_`,_`,_>['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'off.InMode], + 'tt.TrueLit`{Bool`}]) +16 |-> state('_st_['<_`,_`,_>['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'off.InMode], + 'tt.TrueLit`{Bool`}]) +18 |-> state('_st_['<_`,_`,_>['_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'_+_[ + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'%2:Nat],'delay['on.InMode]],'_/\_['_?=_['true.Bool, + '_<=_['%2:Nat,'_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat]]],'_?=_['true.Bool,'_<_['%2:Nat,'_+_['1.NzNat,'1.NzNat, + '1.NzNat]]]]]) +20 |-> state('_st_['<_`,_`,_>['_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat], + '@2:Int,'delay['on.InMode]],'_/\_['_?=_['true.Bool,'_<=_['@2:Int,'_+_[ + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat]]],'_?=_['true.Bool,'_<=_['_+_['1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat], + '@2:Int]],'_?=_['true.Bool,'_<_['@2:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat]]]]]) +22 |-> state('_st_['<_`,_`,_>['_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'_+_[ + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat],'delay['on.InMode]],'tt.TrueLit`{Bool`}]) +24 |-> state('_st_['<_`,_`,_>['_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'_+_[ + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat],'delay['on.InMode]],'tt.TrueLit`{Bool`}]) +26 |-> state('_st_['<_`,_`,_>['_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'_+_[ + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'delay['on.InMode]], + 'tt.TrueLit`{Bool`}]) +28 |-> state('_st_['`{_`,_`,_`}['%1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'%2:Nat], + 'off.InMode],'_?=_['true.Bool,'_<=_['%2:Nat,'_+_['1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat]]]]) +30 |-> state('_st_['`{_`,_`,_`}['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'@2:Nat],'off.InMode],'_/\_['_?=_[ + 'true.Bool,'_<=_['@2:Nat,'_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat]]],'_?=_['false.Bool,'_<_['@2:Nat,'_+_['1.NzNat, + '1.NzNat,'1.NzNat]]]]]) +32 |-> state('_st_['`{_`,_`,_`}['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat], + 'off.InMode],'tt.TrueLit`{Bool`}]) +34 |-> state('_st_['`{_`,_`,_`}['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat], + 'off.InMode],'tt.TrueLit`{Bool`}]) +36 |-> state('_st_['`{_`,_`,_`}['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat],'off.InMode],'tt.TrueLit`{Bool`}]) +38 |-> state('_st_['`{_`,_`,_`}['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat],'off.InMode],'tt.TrueLit`{Bool`}]) +40 |-> state('_st_['`{_`,_`,_`}['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat],'off.InMode],'tt.TrueLit`{Bool`}]) +42 |-> state('_st_['`{_`,_`,_`}['@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'off.InMode],'tt.TrueLit`{Bool`}]) +58 |-> state('_st_['`{_`,_`,_`}['@1:Int,'_+_['@2:Int,'-_['_+_['1.NzNat, + '1.NzNat,'1.NzNat]]],'off.InMode],'_/\_['_?=_['true.Bool,'_<=_['@2:Int, + '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat]]],'_?=_['true.Bool,'_<=_['_+_['1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat],'@2:Int]],'_?=_['false.Bool,'_<_['@2:Int,'_+_['1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat]]]]]) +74 |-> state('_st_['`{_`,_`,_`}['_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'_+_[ + '@1:Int,'-_['1.NzNat]],'delay['on.InMode]],'_/\_['_?=_['true.Bool,'_<=_[ + '@1:Int,'_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat]]],'_?=_['true.Bool,'_<=_['_+_[ + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat],'@1:Int]],'_?=_['true.Bool,'_<_['@1:Int,'_+_['1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat]]]]]) +76 |-> state('_st_['`{_`,_`,_`}['_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'_+_[ + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat],'delay['on.InMode]],'tt.TrueLit`{Bool`}]) +78 |-> state('_st_['`{_`,_`,_`}['_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'_+_[ + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'%1:Nat],'delay['on.InMode]],'_/\_['_?=_['true.Bool,'_<=_['%1:Nat, + '_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat]]],'_?=_['true.Bool,'_<_['%1:Nat,'_+_['1.NzNat,'1.NzNat, + '1.NzNat]]]]]) +80 |-> state('_st_['`{_`,_`,_`}['_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'_+_[ + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat],'delay['on.InMode]],'tt.TrueLit`{Bool`}]) +82 |-> state('_st_['`{_`,_`,_`}['_+_['1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat],'_+_[ + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat,'1.NzNat, + '1.NzNat,'1.NzNat,'1.NzNat],'delay['on.InMode]],'tt.TrueLit`{Bool`}]) +| 97 +| 28 ; 30 ; 32 ; 34 ; 36 ; 38 ; 40 ; 42 ; 58 ; 74 ; 76 ; 78 ; 80 ; 82 +========================================== +reduce in THERMOSTAT-INT-NARROWING-GRAPH : state(goodConf) =>[5]state(badConf) + . +rewrites: 607 +result [Bool]: not isEmpty?(intersect(state('_st_['`{_`,_`,_`}['T:Int,'TMP:Int, + 'M:Mode],'~_['_/\_['_?=_['_<=_['min.Int,'TMP:Int],'true.Bool],'_?=_['_<=_[ + 'TMP:Int,'max.Int],'true.Bool]]]]), state('_st_['`{_`,_`,_`}['T:Int, + 'TMP:Int,'off.Mode],'_/\_['_?=_['_<=_['min.Int,'TMP:Int],'true.Bool],'_?=_[ + '_<=_['TMP:Int,'max.Int],'true.Bool]]]))) or-else extend(state('_st_[ + '`{_`,_`,_`}['T:Int,'TMP:Int,'off.Mode],'_/\_['_?=_['_<=_['min.Int, + 'TMP:Int],'true.Bool],'_?=_['_<=_['TMP:Int,'max.Int],'true.Bool]]])) =>[ + decrement(5)]state('_st_['`{_`,_`,_`}['T:Int,'TMP:Int,'M:Mode],'~_['_/\_[ + '_?=_['_<=_['min.Int,'TMP:Int],'true.Bool],'_?=_['_<=_['TMP:Int,'max.Int], + 'true.Bool]]]]) +Bye. diff --git a/tests/tools/lmc/thermostat.maude b/tests/tools/lmc/thermostat.maude new file mode 100644 index 00000000..f2a9d5a7 --- /dev/null +++ b/tests/tools/lmc/thermostat.maude @@ -0,0 +1,103 @@ +load ../../../contrib/systems/thermostat.maude +load ../../../contrib/tools/lmc/lgraph-search.maude +load ../../../contrib/tools/meta/variables.maude + +set include BOOL off . + +--- ### Thermostat Search Instantiation + +mod THERMOSTAT-COMMON-INIT is + protecting META-TERM . + protecting RENAME-METAVARS . + extending CONDITIONAL-NARROWING-GRAPH + FOLDING-LABELED-GRAPH-SEARCH . + + vars TIME TMP TMP' TMP'' T C : Term . + vars RL Q : Qid . var SUB : Substitution . + + op #nSort : -> Qid . + op #nTrue : -> Qid . + -------------------- + +--- In all cases, the top-sort of the Thermostat parameterized module will be `Conf`, which we instantiate here. + + eq #tSort = 'Conf . + ------------------- + +--- Operators `lt`, `le`, `min`, `max`, and `inRange` are macros for specifying meta-level side-conditions compactly/easily for this theory. + + ops lt le : Term Term -> [Term] . + --------------------------------- + eq lt(TMP, TMP') = '_?=_[ '_<_[TMP, TMP'], #nTrue] . + eq le(TMP, TMP') = '_?=_['_<=_[TMP, TMP'], #nTrue] . + + ops min max : -> Term . + ----------------------- + eq min = qid("min." + string(#nSort)) . + eq max = qid("max." + string(#nSort)) . + + op inRange : Term Term Term -> [Term] . + --------------------------------------- + eq inRange(TMP, TMP', TMP'') = #cConjunct[le(TMP', TMP), le(TMP, TMP'')] . + +--- These states capture "good" and "bad" states for the thermostat; `goodConf` has the temperature within bounds, while `badConf` has the temperature out of bounds. + + op goodConf : -> [Term] . + op badConf : -> [Term] . + ------------------------- + eq goodConf = #cTerm['`{_`,_`,_`}[qid("T:" + string(#nSort)) , qid("TMP:" + string(#nSort)) , 'off.Mode ], inRange(qid("TMP:" + string(#nSort)), min, max)] . + eq badConf = #cTerm['`{_`,_`,_`}[qid("T:" + string(#nSort)) , qid("TMP:" + string(#nSort)) , 'M:Mode ], '~_[inRange(qid("TMP:" + string(#nSort)), min, max)]] . + +--- **TODO**: Move this equation to somewhere more generic. +--- In order to take advantage of our ability to prune infeasible states, we extend the definition of `prune` to check if the side-condition is unsatisfiable. +--- For a specific theory, one can specify `isUnsat` so that it simplifies to `true` if you can prove infeasibility. + + ceq prune(< label(RL, SUB) , state(Q[T, C]) >) = .TransitionSet if Q = #cTerm /\ isUnsat(C) . + --------------------------------------------------------------------------------------------- + + op isUnsat : Term -> [Bool] . + ----------------------------- +endm + +--- ### Thermostat Search modulo FVP-INT + +--- By importing `UNCONDITIONALIZE-FVP-BOOL`, we already have the relevant instantiation for the `FVP-BOOL` side-condition theory. +--- In addition, we tell the tool that the top sort in the original theory `#MO` is `Conf`. + +mod THERMOSTAT-INT-NARROWING-GRAPH is + extending THERMOSTAT-COMMON-INIT . + extending UNCONDITIONALIZE-FVP-BOOL . + + var T : Term . var TS : TermSet . vars NeTS NeTS' : NeTermSet . + vars V V' : Variant . var VS : VariantSet . + var N : Nat . var P : Parent . var B : Bool . var SUB : Substitution . + + eq #nSort = 'Int . + eq #nTrue = 'true.Bool . + ------------------------ + + eq #MO = upModule('THERMOSTAT-INT-COMFORTABLE, true) . + ------------------------------------------------------ + +--- Here we check that a given constraint `isUnsat` by generating variants and checking whether they are all false or exactly a renaming. +--- **TODO**: Invoke varsat. + + ceq isUnsat(T) = false if T == #cTrue . + ceq isUnsat(T) = true if T == #cFalse . + ceq isUnsat(T) = filterFalse(TS) == .TermSet if not T == #cTrue /\ not T == #cFalse + /\ TS := getTerms(filterRenaming(variants(#M, renameTmpVar(#M, T)))) . + ------------------------------------------------------------------------------------------------------------------- + + op filterFalse : TermSet -> [TermSet] . + --------------------------------------- + eq filterFalse(T) = if T == #cFalse then .TermSet else T fi . + + eq filterFalse(.TermSet) = .TermSet . + eq filterFalse(NeTS | NeTS') = filterFalse(NeTS) | filterFalse(NeTS') . +endm + +reduce wellFormed(#M) . +reduce wellFormed(#M, goodConf) . +reduce wellFormed(#M, badConf) . + +reduce bfs(state(goodConf), 2) . +reduce state(goodConf) =>[5] state(badConf) . diff --git a/tests/tools/lmc/token.expected b/tests/tools/lmc/token.expected index 22fae4ec..a6d9a094 100644 --- a/tests/tools/lmc/token.expected +++ b/tests/tools/lmc/token.expected @@ -32,12 +32,12 @@ rewrites: 3 result Bool: true ========================================== reduce in NARROW-SEARCH-2TOKEN : step(state(init(0))) . -rewrites: 11 +rewrites: 14 result Transition: < label('a-enter, none),state('`{_`}['__['`[_`,crit`][ 'a.Name],'`[_`,wait`]['b.Name]]]) > ========================================== reduce in NARROW-SEARCH-2TOKEN : step(state(init(1))) . -rewrites: 18 +rewrites: 23 result NeTransitionSet: < label('a-enter, 'T:Token <- '$.Token),state('`{_`}['__['`[_`,crit`]['a.Name],'`[_`,wait`][ 'b.Name]]]) >,< label('b-enter, @@ -45,17 +45,17 @@ result NeTransitionSet: < label('a-enter, 'a.Name]]]) > ========================================== reduce in NARROW-SEARCH-2TOKEN : step(state(init(2))) . -rewrites: 11 +rewrites: 14 result Transition: < label('b-exit, none),state('`{_`}['__['$.Token, '`[_`,wait`]['a.Name],'`[_`,wait`]['b.Name]]]) > ========================================== reduce in NARROW-SEARCH-2TOKEN : step(state(init(3))) . -rewrites: 11 +rewrites: 14 result Transition: < label('a-exit, none),state('`{_`}['__['*.Token, '`[_`,wait`]['a.Name],'`[_`,wait`]['b.Name]]]) > ========================================== reduce in NARROW-SEARCH-2TOKEN : step(state(init(4))) . -rewrites: 29 +rewrites: 41 result NeTransitionSet: < label('a-enter, 'T':Token <- '$.Token ; 'T:Token <- '@1:Token),state('`{_`}['__['@1:Token,'`[_`,crit`]['a.Name], @@ -71,7 +71,7 @@ result NeTransitionSet: < label('a-enter, '`[_`,wait`]['a.Name]]]) > ========================================== reduce in NARROW-SEARCH-2TOKEN : step(state(init(5))) . -rewrites: 22 +rewrites: 32 result NeTransitionSet: < label('a-enter, 'P:Proc <- '@1:Proc),state('`{_`}['__['@1:Proc,'`[_`,crit`]['a.Name]]]) >,< label('a-exit, @@ -81,7 +81,7 @@ result NeTransitionSet: < label('a-enter, '`[_`,wait`]['a.Name],'`[_`,wait`]['b.Name]]]) > ========================================== reduce in NARROW-SEARCH-2TOKEN : step(state(init(6))) . -rewrites: 22 +rewrites: 32 result NeTransitionSet: < label('a-exit, 'P:Proc <- '`[_`,crit`]['a.Name]),state('`{_`}['__['*.Token,'*.Token, '`[_`,wait`]['a.Name],'`[_`,wait`]['a.Name]]]) >,< label('b-enter, @@ -91,7 +91,7 @@ result NeTransitionSet: < label('a-exit, '`[_`,wait`]['a.Name],'`[_`,wait`]['b.Name]]]) > ========================================== reduce in NARROW-SEARCH-2TOKEN : step(state(init(7))) . -rewrites: 29 +rewrites: 41 result NeTransitionSet: < label('a-enter, 'P:Proc <- '@1:Proc ; 'T:Token <- '$.Token),state('`{_`}['__['@1:Proc,'`[_`,crit`]['a.Name]]]) >,< @@ -117,13 +117,13 @@ result Fold: fold( ========================================== reduce in NARROW-SEARCH-2TOKEN : fold(state(init(0)), state(init(6))) . rewrites: 4 -result [Fold]: fold(state('`{_`}['__['$.Token,'`[_`,wait`]['a.Name], +result [FoldSet]: fold(state('`{_`}['__['$.Token,'`[_`,wait`]['a.Name], '`[_`,wait`]['b.Name]]]), state('`{_`}['__['*.Token,'P:Proc,'`[_`,wait`][ 'a.Name]]])) ========================================== reduce in NARROW-SEARCH-2TOKEN : fold(state(init(1)), state(init(6))) . rewrites: 4 -result [Fold]: fold(state('`{_`}['__['T:Token,'`[_`,wait`]['a.Name], +result [FoldSet]: fold(state('`{_`}['__['T:Token,'`[_`,wait`]['a.Name], '`[_`,wait`]['b.Name]]]), state('`{_`}['__['*.Token,'P:Proc,'`[_`,wait`][ 'a.Name]]])) ========================================== @@ -133,7 +133,7 @@ result Fold: fold( 'P:Proc <- '`[_`,wait`]['b.Name]) ========================================== reduce in NARROW-SEARCH-2TOKEN : bfs(state(init(0))) . -rewrites: 194 +rewrites: 206 result FoldedLabeledGraph: (0 -[label('a-enter, none)]-> 2 2 -[label('a-exit, none)]-> 4 4 -[label('b-enter, none)]-> 6 @@ -146,7 +146,7 @@ result FoldedLabeledGraph: (0 -[label('a-enter, none)]-> 2 | 9 ========================================== reduce in NARROW-SEARCH-2TOKEN : bfs(state(init(1))) . -rewrites: 156 +rewrites: 167 result FoldedLabeledGraph: (0 -[label('a-enter, 'T:Token <- '$.Token)]-> 2 0 -[label('b-enter, @@ -162,7 +162,7 @@ result FoldedLabeledGraph: (0 -[label('a-enter, | 9 ========================================== reduce in NARROW-SEARCH-2TOKEN : bfs(state(init(2))) . -rewrites: 196 +rewrites: 208 result FoldedLabeledGraph: (0 -[label('b-exit, none)]-> 2 2 -[label('a-enter, none)]-> 4 4 -[label('a-exit, none)]-> 6 @@ -174,7 +174,7 @@ result FoldedLabeledGraph: (0 -[label('b-exit, none)]-> 2 | 9 ========================================== reduce in NARROW-SEARCH-2TOKEN : bfs(state(init(3))) . -rewrites: 196 +rewrites: 208 result FoldedLabeledGraph: (0 -[label('a-exit, none)]-> 2 2 -[label('b-enter, none)]-> 4 4 -[label('b-exit, none)]-> 6 @@ -186,7 +186,7 @@ result FoldedLabeledGraph: (0 -[label('a-exit, none)]-> 2 | 9 ========================================== reduce in NARROW-SEARCH-2TOKEN : bfs(state(init(4))) . -rewrites: 406 +rewrites: 433 result FoldedLabeledGraph: (0 -[label('a-enter, 'T':Token <- '$.Token ; 'T:Token <- '@1:Token)]-> 2 @@ -223,7 +223,7 @@ result FoldedLabeledGraph: (0 -[label('a-enter, | 21 ========================================== reduce in NARROW-SEARCH-2TOKEN : bfs(state(init(5))) . -rewrites: 1348 +rewrites: 1398 result FoldedLabeledGraph: (0 -[label('a-enter, 'P:Proc <- '@1:Proc)]-> 2 0 -[label('a-exit, @@ -273,7 +273,7 @@ result FoldedLabeledGraph: (0 -[label('a-enter, | 35 ========================================== reduce in NARROW-SEARCH-2TOKEN : bfs(state(init(6))) . -rewrites: 1518 +rewrites: 1566 result FoldedLabeledGraph: (0 -[label('a-exit, 'P:Proc <- '`[_`,crit`]['a.Name])]-> 2 0 -[label('b-enter, @@ -316,7 +316,7 @@ result FoldedLabeledGraph: (0 -[label('a-exit, | 35 ========================================== reduce in NARROW-SEARCH-2TOKEN : bfs(state(init(7))) . -rewrites: 901 +rewrites: 942 result FoldedLabeledGraph: (0 -[label('a-enter, 'P:Proc <- '@1:Proc ; 'T:Token <- '$.Token)]-> 2 @@ -377,7 +377,7 @@ result FoldedLabeledGraph: (0 -[label('a-enter, | 31 ========================================== reduce in NARROW-SEARCH-2TOKEN : bfs(state(init(7))) . -rewrites: 901 +rewrites: 9 result FoldedLabeledGraph: (0 -[label('a-enter, 'P:Proc <- '@1:Proc ; 'T:Token <- '$.Token)]-> 2 @@ -439,6 +439,6 @@ result FoldedLabeledGraph: (0 -[label('a-enter, ========================================== reduce in NARROW-SEARCH-2TOKEN : check state(init(0)) stable in state(init(1)) ; state(init(2)) ; state(init(3)) . -rewrites: 252 +rewrites: 269 result Bool: true Bye. diff --git a/tests/tools/lmc/token.maude b/tests/tools/lmc/token.maude index 121edaf6..bb2ee3e2 100644 --- a/tests/tools/lmc/token.maude +++ b/tests/tools/lmc/token.maude @@ -9,7 +9,7 @@ load ../../../contrib/tools/meta/narrowing.maude mod NARROW-SEARCH-2TOKEN is protecting 2TOKEN . - including NARROWING-GRAPH + GRAPH-ANALYSIS . + including NARROWING-GRAPH + FOLDING-LABELED-GRAPH-SEARCH . eq #M = upModule('2TOKEN, true) .