--- The Maude Logical Bounded Model Checker Interface --- Author: Kyungmin Bae load model-checker **************************************** *** Basic Interface *** **************************************** fmod RULE-NAME is extending QID . sort RuleName . subsort Qid < RuleName . ops unlabeled deadlock : -> RuleName . endfm fmod SYMBOLIC-CHECKER is pr RULE-NAME . pr SATISFACTION . including LTL . subsort Prop < Formula . *** generic substitution for counter example sorts CEAssignment CESubstitution . subsort CEAssignment < CESubstitution . op _<-_ : Qid Universal -> CEAssignment [ctor poly (2) prec 63] . op none : -> CESubstitution . op _;_ : CESubstitution CESubstitution -> CESubstitution [ctor assoc comm id: none prec 65] . eq CA:CEAssignment ; CA:CEAssignment = CA:CEAssignment . *** transitions and results sorts Transition TransitionList ModelCheckResult . subsort Transition < TransitionList . subsort Bool < ModelCheckResult . op {_,_,_} : State CESubstitution RuleName -> Transition [ctor] . op nil : -> TransitionList [ctor] . op __ : TransitionList TransitionList -> TransitionList [ctor assoc id: nil format (d ni d)] . op prefix_loop_ : TransitionList TransitionList -> ModelCheckResult [ctor format(n n++i n ni i--)] . endfm ************************************************** *** Logical Model Checker on META-LEVEL *** ************************************************** --- core maude search function (using META-LEVEL) fmod BOUNDED-FOLDING-MODEL-CHECKER is pr RULE-NAME . pr META-LEVEL . pr SATISFACTION . including LTL . --- meta transition sorts MetaEdge MetaConf . op deadlock : -> MetaEdge [ctor] . op _/_ : RuleSet Substitution -> MetaEdge [ctor] . op <_> : State -> MetaConf [ctor] . op _|=>_ : MetaEdge State -> MetaConf [ctor] . --- propositions subsort Prop < Formula . op prop : Term -> Prop [ctor] . --- folding relation op _>=_ : State State -> Bool . op _~=_ : State State -> Bool . op _~_ : MetaEdge MetaEdge -> Bool . eq deadlock ~ deadlock = true . eq RS:RuleSet / S1:Substitution ~ RS:RuleSet / S2:Substitution = true . --- print state during model checking (debugging purpose) op prettyPrint : State ~> QidList . op prettyPrint : MetaEdge ~> QidList . --- transitions sort Transition TransitionList . subsort Transition < TransitionList . op {_,_} : State MetaEdge -> Transition [ctor] . op nil : -> TransitionList [ctor] . op __ : TransitionList TransitionList -> TransitionList [ctor assoc id: nil format (d ni d)] . --- model checking results sorts ModelCheckResult . subsort Bool < ModelCheckResult . op prefix_loop_ : TransitionList TransitionList -> ModelCheckResult [ctor format(n n++i n ni i--)] . --- bounded model checker report sort BoundedModelCheckReport . op result:_real:_bound:_complete:_ : ModelCheckResult Bool Nat Bool -> BoundedModelCheckReport [ctor] . --- model checker --- (InitState,Formula,SubsumptionFolding,Bound) op symbolicModelCheck : State Formula Bool Bound ~> BoundedModelCheckReport [special ( id-hook SymbolicModelCheckerSymbol --- temporal operators op-hook trueSymbol (True : ~> Formula) op-hook falseSymbol (False : ~> Formula) op-hook notSymbol (~_ : Formula ~> Formula) op-hook nextSymbol (O_ : Formula ~> Formula) op-hook andSymbol (_/\_ : Formula Formula ~> Formula) op-hook orSymbol (_\/_ : Formula Formula ~> Formula) op-hook untilSymbol (_U_ : Formula Formula ~> Formula) op-hook releaseSymbol (_R_ : Formula Formula ~> Formula) --- for Bound attribute op-hook succSymbol (s_ : Nat ~> NzNat) op-hook unboundedSymbol (unbounded : ~> Bound) --- state propositions op-hook satisfiesSymbol (_|=_ : State Formula ~> Bool) term-hook trueTerm (true) --- folding graph stuff op-hook subsumeFoldingRelSymbol (_>=_ : State State ~> Bool) op-hook renameFoldingRelSymbol (_~=_ : State State ~> Bool) op-hook compatibleTransSymbol (_~_ : MetaEdge MetaEdge ~> Bool) op-hook prettyPrintStateSymbol (prettyPrint : State ~> QidList) op-hook prettyPrintTransSymbol (prettyPrint : MetaEdge ~> QidList) --- meta graph op-hook metaStateSymbol (<_> : State ~> MetaConf) op-hook metaTransitionSymbol (_|=>_ : MetaEdge State ~> MetaConf) --- counterexamples term-hook falseTerm (false) term-hook deadlockTerm ((deadlock).MetaEdge) op-hook transitionSymbol ({_,_} : State MetaEdge ~> Transition) op-hook transitionListSymbol (__ : TransitionList TransitionList ~> TransitionList) op-hook nilTransitionListSymbol (nil : ~> TransitionList) op-hook counterexampleSymbol (prefix_loop_ : TransitionList TransitionList ~> ModelCheckResult) --- result report op-hook resultreportSymbol (result:_real:_bound:_complete:_ : ModelCheckResult Bool Nat Bool ~> BoundedModelCheckReport) )] . endfm **************************************** *** Full Maude Narrowing Connector *** **************************************** load full-maude27 fmod META-LMC-PARAMETERS is pr META-MODULE . op ##m## : ~> SModule [memo] . --- empty! the user module shoule define them. op ##f## : ~> TermList [memo] . var H : Header . var IL : ImportList . var SS : SortSet . var SSDS : SubsortDeclSet . var OPDS : OpDeclSet . var MAS : MembAxSet . var EQS : EquationSet . var RLS : RuleSet . vars T1 T2 : Term . var ATS : AttrSet . var COND : EqCondition . --- to handle the mismatch between Full & Core Maude --- due to some bugs, only used for getVarants and metaNarrow op trMod : SModule -> SModule [memo] . eq trMod(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = fmod H is IL sorts SS . SSDS OPDS MAS trEqs(EQS) endfm . eq trMod(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = mod H is IL sorts SS . SSDS OPDS MAS trEqs(EQS) RLS endm . op trEqs : EquationSet -> EquationSet . eq trEqs(eq T1 = T2 [metadata("variant") ATS] . EQS) = eq T1 = T2 [variant ATS] . trEqs(EQS) . eq trEqs(ceq T1 = T2 if COND [metadata("variant") ATS] . EQS) = ceq T1 = T2 if COND [variant ATS] . trEqs(EQS) . eq trEqs(EQS) = EQS [owise] . endfm fmod LMC-RESULT-SET is pr RESULT-CONTEXT-SET . sort StepResult StepResult? . subsort StepResult < StepResult? . op failure : -> StepResult? [ctor] . op {_,_,_/_} : Term Type Substitution RuleSet -> StepResult [ctor] . sort StepResultSet . subsort StepResult < StepResultSet . op empty : -> StepResultSet [ctor] . op _||_ : StepResultSet StepResultSet -> StepResultSet [ctor assoc comm id: empty prec 65] . eq X:StepResult || X:StepResult = X:StepResult . var M : Module . vars NextVar : Nat . vars S S' : Substitution . vars T TS CtTS : Term . var TL : TermList . var TP : Type . var R : Rule . var Tr : TraceNarrow . var B : Flags . vars Ct CtS : Context . var RTS : ResultContextSet . var SRS : StepResultSet . op to4Tuple : Module ResultContextSet -> StepResult . eq to4Tuple(M, empty ) = empty . eq to4Tuple(M, {T,TP,S,S',Ct,CtS,TS,CtTS,NextVar,Tr,B} | RTS ) = {CtTS, leastSort(M,CtTS), S .. S' / getRuleSet(Tr)} || to4Tuple(M, RTS) . op _|>_ : StepResult TermList -> StepResult . eq (empty).StepResult |> TL = (empty).StepResult . eq ({T,TP,S / R} || SRS) |> TL = {T,TP,S |> TL / R} || (SRS |> TL) . eq (failure || SRS ) |> TL = failure || (SRS |> TL) . op getRuleSet : TraceNarrow -> RuleSet . eq getRuleSet({T,S,TP,R} Tr) = R getRuleSet(Tr) . eq getRuleSet(nil) = none . sort VariantSet . subsort Variant < VariantSet . op emptyVariantSet : -> VariantSet [ctor] . op _#_ : VariantSet VariantSet -> VariantSet [ctor assoc comm id: emptyVariantSet prec 65 format (d d n d)] . eq X:Variant # X:Variant = X:Variant . endfm mod META-LMC-THEORY is pr LMC-RESULT-SET . pr META-LMC-PARAMETERS . pr BOUNDED-FOLDING-MODEL-CHECKER . vars T1 T2 ST ST' : Term . vars SUB SUB' : Substitution . var RS : RuleSet . var CD : Condition . var Q : Qid . var TP : Type . var SRS : StepResultSet . ops init mid : Term -> State [ctor] . --- functions ops next variant : Term -> StepResultSet . --- meta rules crl [init] : < init(ST) > => RS / SUB' |=> mid(getTerm(metaReduce((##m##),ST'))) if {ST',TP,SUB' / RS} || SRS := variant(ST) . crl [mid] : < mid(ST) > => RS / SUB' |=> mid(getTerm(metaReduce((##m##),ST'))) if {ST',TP,SUB' / RS} || SRS := next(ST) . endm fmod META-NARROWING-INTERFACE is pr META-LMC-PARAMETERS . pr LMC-RESULT-SET . pr META-NARROWING-SEARCH . var M : Module . var RS : RuleSet . vars T T1 T2 ST PT : Term . var TL : TermList . var C : Constant . var TP : Type . vars SUB SUB1 SUB2 : Substitution . vars NextVar NextVar' N : Nat . var VR : Variant . var VS : VariantSet . var SR : StepResult . var SRS : StepResultSet . op metaNarrow2 : Module Term -> StepResult . eq metaNarrow2(M,T) = to4Tuple(M,metaENarrowShowAll(M,T,1,full noStrategy BuiltIn-unify)) |> T . op metaGenVariant : Module Term -> VariantSet . eq metaGenVariant(M, T) = metaGenVariant(M, T, highestVar(T)) . op metaGenVariant : Module Term Nat -> VariantSet . eq metaGenVariant(M, T, NextVar) = metaGenVariant2(M, T, NextVar, 0) . op metaGenVariant2 : Module Term Nat Nat -> VariantSet . ceq metaGenVariant2(M, T, NextVar, N) = VR # metaGenVariant2(M,T,NextVar,s N) if VR := metaGetVariant(M,T,empty,NextVar,N) . eq metaGenVariant2(M, T, NextVar, N) = emptyVariantSet [owise] . --- variant narrowing prop instantiations. --- compute the PI-instantated states of the given state. --- StateSet PropSet -> StateSet op propSetInstSet : StepResultSet TermList ~> StepResultSet . eq propSetInstSet(SRS, (PT,TL)) = propSetInstSet(propInstSet(SRS, PT), TL) . eq propSetInstSet(SRS, empty) = SRS . --- StateSet Prop -> StateSet (trMod for genVariant) op propInstSet : StepResultSet Term ~> StepResultSet . eq propInstSet({ST,TP,SUB / RS} || SRS, PT) = filterPropVars({ST,TP,SUB / RS}, metaGenVariant(trMod(##m##), '_|=_[ST, PT])) || propInstSet(SRS, PT) . eq propInstSet(empty, PT) = empty . op filterPropVars : StepResult VariantSet ~> StepResultSet . eq filterPropVars({ST,TP,SUB / RS}, {T,SUB1,N} # VS) = if inst?(T) then {ST << SUB1,TP, SUB .. SUB1 / RS} else empty fi || filterPropVars({ST,TP,SUB / RS}, VS) . eq filterPropVars(SR, emptyVariantSet) = empty . --- TODO: by not filtering, we may allow more patterns that are not reduced --- to true/false. However, it easily generates spurious counter examples.. --- We may adopt this with abstract refinement techniques.. --- But with filtering, the |= equations should be total... op inst? : Term ~> Bool . eq inst?('true.Bool) = true . eq inst?('false.Bool) = true . eq inst?(T) = false [owise] . endfm mod META-SYMBOLIC-CONNECTOR is pr META-LMC-THEORY . pr BOUNDED-FOLDING-MODEL-CHECKER . pr META-NARROWING-INTERFACE . pr DECL-META-PRETTY-PRINT * (op addOps to addOpsSE, op addEqs to addEqsSE, op addSorts to addSortsSE) . var M : Module . vars T T' T1 T2 ST ST' PT CT : Term . var RN : RuleName . var RS : RuleSet . var TL : TermList . var V : Variable . var TP : Type . vars SUB SUB' SUB'' : Substitution . var B : Bool . var N : Nat . var D : Bound . var RT : ResultTriple . var RTS : ResultTripleSet . --- meta prop and state eq mid(ST) |= prop(PT) = getTerm(metaReduce((##m##), '_|=_[ST, PT])) == 'true.Bool . --- state folding eq init(ST) >= init(ST) = true . eq mid(ST) >= mid(ST') = metaMatch((##m##), ST, ST', nil, 0) :: Substitution . eq S1:State >= S2:State = false [owise] . --- renameing folding eq init(ST) ~= init(ST) = true . eq mid(ST) ~= mid(ST') = mid(ST) >= mid(ST') and-then mid(ST') >= mid(ST) . eq S1:State ~= S2:State = false [owise] . --- compute the next states --- TODO: keep both a state and a substitution for a counter example.. eq next(ST) = propSetInstSet(metaNarrow2(trMod(##m##), ST), ##f##) . eq variant(ST) = propSetInstSet({ST,leastSort((##m##),ST),none / none}, ##f##) . --- run LMC model check : State Formula -> Result op lmc-check : Term Term Bool Bound ~> BoundedModelCheckReport . ceq lmc-check(ST, PT, B, D) = symbolicModelCheck(init(ST), O tilde((##m##),PT), B, D) if sortLeq((##m##), leastSort((##m##),ST), 'State) /\ sortLeq((##m##), leastSort((##m##),PT), 'Formula) . --- meta formula op tilde : Module Term -> Formula . ceq tilde(M, PT) = prop(PT) if sortLeq(M,leastSort(M,PT),'Prop) . eq tilde(M, 'True.Formula) = True . eq tilde(M, 'False.Formula) = False . eq tilde(M, '~_[T]) = ~ tilde(M, T) . eq tilde(M, '_/\_[T, T']) = tilde(M, T) /\ tilde(M, T') . eq tilde(M, '_\/_[T, T']) = tilde(M, T) \/ tilde(M, T') . eq tilde(M, 'O_[T]) = O tilde(M, T) . eq tilde(M, '_U_[T, T']) = tilde(M, T) U tilde(M, T') . eq tilde(M, '_R_[T, T']) = tilde(M, T) R tilde(M, T') . --- pretty print (for debugging) eq prettyPrint(init(ST)) = eMetaPrettyPrint((##m##), ST) . eq prettyPrint(mid(ST)) = eMetaPrettyPrint((##m##), ST) . eq prettyPrint(RS / SUB) = ---eMetaPrettyPrint((##m##), RS) '/ prettyPrintSub(SUB) . op prettyPrintSub : Substitution -> QidList . eq prettyPrintSub(none) = 'none . eq prettyPrintSub(V <- T) = V '<- eMetaPrettyPrint((##m##),T) . eq prettyPrintSub(V <- T ; A:Assignment ; SUB) = V '<- eMetaPrettyPrint((##m##),T) '; prettyPrintSub(A:Assignment ; SUB) . endm ***************************************************** *** Full Maude Narrowing Connector (Condition) *** ***************************************************** --- NOTE: currently, only considering "T = true" mod META-LMC-COND-THEORY is pr META-LMC-THEORY . ops init mid : Term EqCondition -> State [ctor] . endm fmod META-NARROWING-COND-INTERFACE is pr META-NARROWING-INTERFACE . vars T T1 T2 ST PT : Term . var TL : TermList . var C : Constant . var CD : EqCondition . var RS : RuleSet . var TP : Type . vars SUB SUB1 SUB2 : Substitution . var N : Nat . var SR : StepResult . var SRS : StepResultSet . var VS : VariantSet . --- variant narrowing condition instantiations. --- StateSet EqCondition -> StateSet op condSetInstSet : StepResultSet EqCondition ~> StepResultSet . eq condSetInstSet(SRS, T = 'true.Bool /\ CD) = condSetInstSet(condInstSet(SRS, T), CD) . eq condSetInstSet(SRS, nil) = SRS . --- StateSet Prop -> StateSet op condInstSet : StepResultSet Term ~> StepResultSet . ceq condInstSet({ST,TP,SUB / RS} || SRS, T) = filterCondVars({ST,TP,SUB / RS}, VS) || condInstSet(SRS, T) if VS := metaGenVariant(trMod(##m##), T << SUB) . eq condInstSet(empty, T) = empty . --- only true instances (hence the conditions should be complete and FVP) op filterCondVars : StepResult VariantSet ~> StepResultSet . eq filterCondVars({ST,TP,SUB / RS}, {'true.Bool,SUB1,N} # VS) = {ST << SUB1, TP, SUB .. SUB1 / RS} || filterCondVars({ST,TP,SUB / RS}, VS) . eq filterCondVars(SR, VS) = empty [owise] . --- applying substitution to condition op _<<_ : EqCondition Substitution ~> EqCondition . eq (T1 = T2 /\ CD) << SUB = ((T1 << SUB) = (T2 << SUB)) /\ (CD << SUB) . eq (T1 := T2 /\ CD) << SUB = ((T1 << SUB) = (T2 << SUB)) /\ (CD << SUB) . eq (T : S:Sort /\ CD) << SUB = ((T << SUB) : S:Sort) /\ (CD << SUB) . eq nil << SUB = (nil).EqCondition . endfm mod META-SYMBOLIC-COND-CONNECTOR-BASE is pr META-LMC-COND-THEORY . pr META-SYMBOLIC-CONNECTOR . pr META-NARROWING-COND-INTERFACE . var M : Module . vars T T' T1 T2 ST ST' PT CT : Term . var TL : TermList . var V : Variable . var TP : Type . vars SUB SUB' SUB'' : Substitution . var B : Bool . var N : Nat . var D : Bound . var RT : ResultTriple . var RTS : ResultTripleSet . vars CD CD' : EqCondition . --- meta prop and state eq mid(ST,CD) |= prop(PT) = getTerm(metaReduce((##m##), '_|=_[ST, PT])) == 'true.Bool . --- with condition op lmc-check : Term Term EqCondition Bool Bound ~> BoundedModelCheckReport . ceq lmc-check(ST, PT, CD, B, D) = if CD == nil then symbolicModelCheck(init(ST), O tilde((##m##),PT), B, D) else symbolicModelCheck(init(ST,CD), O tilde((##m##),PT), B, D) fi if sortLeq((##m##), leastSort((##m##),ST), 'State) /\ sortLeq((##m##), leastSort((##m##),PT), 'Formula) . --- normalize conditions (modulo equation) --- NOTE: metaNormalize vs. metaReduce?? metaNormalize generates slightly --- more states for (state,condition) pairs if there exists equaltional --- abstraction, but it will be more correct since we do not worry about --- whether some variables is removed by such equations... op condNorm : EqCondition ~> EqCondition . eq condNorm(T = 'true.Bool /\ CD) = getTerm(metaNormalize((##m##),T)) = 'true.Bool /\ condNorm(CD) . eq condNorm(nil) = nil . --- pretty print (for debugging) eq prettyPrint(init(ST,CD)) = prettyPrint(init(ST)) '\n '\t eMetaPrettyPrint((##m##), CD) . eq prettyPrint(mid(ST,CD)) = prettyPrint(mid(ST)) '\n '\t eMetaPrettyPrint((##m##), CD) . endm --- Conditions are solved for generating states by variant narrowing mod META-SYMBOLIC-COND-CONNECTOR is pr META-SYMBOLIC-COND-CONNECTOR-BASE . var M : Module . vars T T' T1 T2 ST ST' PT CT : Term . var TL : TermList . var V : Variable . var TP : Type . vars SUB SUB' SUB'' : Substitution . var N : Nat . var SR : StepResult . var SRS : StepResultSet . vars CD CD' : EqCondition . var RS : RuleSet . --- meta rules crl [init-cond] : < init(ST,CD) > => RS / SUB' |=> mid(getTerm(metaReduce((##m##),ST')),condNorm(CD << SUB')) if {ST',TP,SUB' / RS} || SRS := variant(ST,CD) . crl [mid-cond] : < mid(ST,CD) > => RS / SUB' |=> mid(getTerm(metaReduce((##m##),ST')),condNorm(CD << SUB')) if {ST',TP,SUB' / RS} || SRS := next(ST,CD) . ops next variant : Term EqCondition -> StepResultSet . eq next(ST,CD) = propSetInstSet(condSetInstSet(metaNarrow2(trMod(##m##), ST),CD), ##f##) . eq variant(ST,CD) = propSetInstSet(condSetInstSet({ST,leastSort((##m##),ST),none / none},CD), ##f##) . --- condition should be already considered by variant narrowing eq mid(ST,CD) >= mid(ST',CD') = mid(ST) >= mid(ST') . eq mid(ST,CD) ~= mid(ST',CD') = mid(ST,CD) >= mid(ST',CD') and-then mid(ST',CD') >= mid(ST,CD) . endm --- Folding conditions C >= C' by checking C' => \rho(C) using variant narrowing mod META-SYMBOLIC-COND-CONNECTOR2 is pr META-SYMBOLIC-COND-CONNECTOR-BASE . vars T T' T1 T2 ST ST' PT CT : Term . var TL : TermList . var V : Variable . var TP : Type . vars SUB SUB' SUB'' : Substitution . var N : Nat . var B : Bool . var RS : RuleSet . var SR : StepResult . var SRS : StepResultSet . vars CD CD' : EqCondition . var VS : VariantSet . --- meta rules crl [init-cond] : < init(ST,CD) > => RS / SUB' |=> mid(getTerm(metaReduce((##m##),ST')),condNorm(CD << SUB')) if {ST',TP,SUB' / RS} || SRS := variant(ST) /\ condOK(CD << SUB') . crl [mid-cond] : < mid(ST,CD) > => RS / SUB' |=> mid(getTerm(metaReduce((##m##),ST')),condNorm(CD << SUB')) if {ST',TP,SUB' / RS} || SRS := next(ST) /\ condOK(CD << SUB') . --- Another method to check a condition. op condOK : EqCondition ~> Bool . eq condOK(T1 = 'true.Bool /\ CD) = if getTerm(metaReduce((##m##), T1)) == 'false.Bool then false else true fi and-then condOK(CD) . eq condOK(nil) = true . --- folding with conditions eq mid(ST,CD) >= mid(ST',CD') = condFold(ST, CD, ST', CD', 0) . eq mid(ST,CD) ~= mid(ST',CD') = mid(ST,CD) >= mid(ST',CD') and-then mid(ST',CD') >= mid(ST,CD) . op condFold : Term EqCondition Term EqCondition Nat -> Bool . ceq condFold(ST, CD, ST', CD', N) = implyOK(CD', CD << SUB) and-then condFold(ST, CD, ST', CD', s(N)) if SUB := metaMatch((##m##), ST, ST', nil, N) . eq condFold(ST, CD, ST', CD', 0) = false [owise] . eq condFold(ST, CD, ST', CD', s(N)) = true [owise] . --- check if the implecation (C1 /\ not C2) has no "true" solution op implyOK : EqCondition EqCondition ~> Bool . ceq implyOK(CD, CD') = implyOKsub(VS) if VS := metaGenVariant(trMod(##m##),'_and_[condList(CD,true), '_or_[condList(CD',false)]]) . op implyOKsub : VariantSet ~> Bool . ceq implyOKsub({T,SUB,N} # VS) = T' =/= 'true.Bool and-then implyOKsub(VS) if T' := getTerm(metaReduce((##m##),T)) . eq implyOKsub(emptyVariantSet) = true . op condList : EqCondition Bool ~> TermList . eq condList(T = 'true.Bool /\ CD, B) = if B then T else 'not_[T] fi, condList(CD, B) . eq condList(nil, B) = if B then 'true.Bool else 'false.Bool fi . endm ***************************************** *** Extending Full Maude *** ***************************************** --- REDEFINED fmod BANNER is pr STRING . op banner : -> String . eq banner = "Logical Model Checker January 10th 2012" . endfm fmod LMC-COMMANDS is inc COMMANDS . op lmc_|=_. : @Bubble@ @Bubble@ -> @Command@ [ctor] . op lfmc_|=_. : @Bubble@ @Bubble@ -> @Command@ [ctor] . endfm --- REDEFINED fmod FULL-MAUDE-SIGN is including VIEWS . inc LMC-COMMANDS . sort @Input@ . subsorts @Command@ @Module@ @View@ < @Input@ . endfm fmod META-PROP-SET is pr META-LEVEL . var M : Module . vars T T' : Term . op props : Module Term -> TermList . eq props(M, T) = #props(M, getTerm(metaReduce(M, T))) . op #props : Module Term -> TermList . --- Formula -> PropList . ceq #props(M, T) = T if sortLeq(M, leastSort(M, T), 'Prop) . eq #props(M, '~_[T]) = #props(M, T) . eq #props(M, '_/\_[T, T']) = #props(M, T), #props(M, T') . eq #props(M, '_\/_[T, T']) = #props(M, T), #props(M, T') . eq #props(M, 'O_[T]) = #props(M, T) . eq #props(M, '_U_[T, T']) = #props(M, T), #props(M, T') . eq #props(M, '_R_[T, T']) = #props(M, T), #props(M, T') . eq #props(M, T) = empty [owise] . endfm mod META-LMC-COUNTEREXAMPLE-TRANSFORMER is pr META-LMC-THEORY . pr META-LMC-COND-THEORY . pr BOUNDED-FOLDING-MODEL-CHECKER . vars Q F : Qid . var M : Module . var V : Variable . var C : Constant . var CD : Condition . vars T T' ST PT : Term . var TL : TermList . var TR : Transition . var TRL TRL' : TransitionList . var RS : RuleSet . var RN : RuleName . var AtS : AttrSet . var SUB : Substitution . var ME : MetaEdge . var D : Bound . vars B BC BR : Bool . var MR : ModelCheckResult . --- meta counterexample op transRes : ModelCheckResult -> Term . eq transRes(B) = upTerm(B:Bool) . eq transRes(prefix TRL loop TRL') = 'prefix_loop_[wrapTL('__,'nil.TransitionList,transTRs(TRL)), wrapTL('__,'nil.TransitionList,transTRs(TRL'))] . op transTRs : TransitionList -> TermList . eq transTRs(TR TRL) = transTR(TR), transTRs(TRL) . eq transTRs(nil) = empty . --- transition (including conditions) op transTR : Transition -> TermList . eq transTR({mid(ST), RS / SUB}) = '`{_`,_`,_`}[ST, wrapTL('_;_,'none.CESubstitution,transSUB(SUB)), upRuleName(getRuleName(RS))] . eq transTR({mid(ST), deadlock}) = '`{_`,_`,_`}[ST, 'none.CESubstitution, upRuleName(deadlock)] . eq transTR({init(ST), ME}) = empty . eq transTR({mid(ST,CD),ME}) = transTR({mid(ST),ME}) . eq transTR({init(ST,CD),ME}) = empty . --- substitution op transSUB : Substitution -> TermList . eq transSUB(none) = empty . eq transSUB(V <- T ; SUB) = '_<-_[qid("'" + string(getName(V)) + ".Qid"), T], transSUB(SUB) . op wrapTL : Qid Constant TermList -> Term . eq wrapTL(F, C, T) = T . eq wrapTL(F, C, (T,T',TL)) = F[T,T',TL] . eq wrapTL(F, C, empty) = C . op upRuleName : RuleName -> Constant . eq upRuleName(Q) = qid("'" + string(Q) + ".Qid") . eq upRuleName(RN) = upTerm(RN) [owise] . op getRuleName : RuleSet -> RuleName . eq getRuleName((rl T => T' [label(Q) AtS] .) RS) = Q . eq getRuleName((crl T => T' if CD [label(Q) AtS] .) RS) = Q . eq getRuleName(RS) = unlabeled [owise] . endm mod LMC-COMMAND-PROCESSING is pr COMMAND-PROCESSING . pr META-PROP-SET . vars T T1 T2 T3 T4 T5 T6 : Term . var TL TL1 : TermList . vars DB DB1 : Database . vars M U M1 M2 : Module . vars ME ME1 : ModuleExpression . vars B BC : Bool . var D : Bound . var CD : Condition . var QIL : QidList . vars VS VDS : OpDeclSet . vars QI QI' F V O : Qid . var TY : Type . var TDM : Tuple{Database,ModuleExpression} . var TMVB : [Tuple{Term,Module,Bool,OpDeclSet,Bound,Database}] . var RP : ResultPair . var RP? : [ResultPair] . --- command condition type op lmcCmdCond : Qid -> Type? . eq lmcCmdCond('lmc_|=_.) = 'Formula . eq lmcCmdCond('lfmc_|=_.) = 'Formula . eq lmcCmdCond(QI) = anyType [owise] . --- no condition --- process lmc commands op procLMCComd : Term ModuleExpression Database -> Tuple{Database,QidList} . --- no argument eq procLMCComd(QI, ME, DB) = if compiledModule(ME, DB) then procLMC(QI, empty, nil, unbounded, getFlatModule(ME,DB), getVars(ME,DB), DB) else procLMC(QI, empty, nil, unbounded, getFlatModule(modExp(evalModExp(ME,DB)), database(evalModExp(ME,DB))), getVars(modExp(evalModExp(ME,DB)), database(evalModExp(ME,DB))), database(evalModExp(ME,DB))) fi . --- there exist arguments ceq procLMCComd(F[TL], ME, DB) = if compiledModule(ME, DB) then procLMCComd(F, TL, getFlatModule(ME,DB), B, unbounded, getVars(ME,DB), DB, empty) else procLMCComd(F, TL, getFlatModule(modExp(evalModExp(ME,DB)), database(evalModExp(ME,DB))), B, unbounded, getVars(modExp(evalModExp(ME,DB)), database(evalModExp(ME,DB))), database(evalModExp(ME,DB)), empty) fi if B := included('META-MODULE, getImports(getTopModule(ME,DB)), DB) . ------------------------------------- --- parse arguments --- op procLMCComd : Qid TermList Module Bool Bound OpDeclSet Database TermList -> Tuple{Database,QidList} . eq procLMCComd(F, TL, unitError(QIL), B, D, VDS, DB, TL1) = << DB ; QIL >> . --- the first argument ceq procLMCComd(F, (T,TL), M, B, D, VDS, DB, empty) = if getModule(TMVB) :: Module and-then getTerm(TMVB) :: Term then procLMCComd(F, TL, getModule(TMVB), B, getBound(TMVB), getVars(TMVB), getDatabase(TMVB), getTerm(TMVB)) else << DB ; getMsg(getTerm(metaReduce(getModule(TMVB), getTerm(TMVB)))) >> fi if TMVB := solveBubblesRew(T, M, B, unbounded, VDS, DB) . --- "[1] in MOD :" --- intermediate arguments ceq procLMCComd(F, (T1,T2,TL), M, B, D, VDS, DB, TL1) = if T?:[Term] :: Term then procLMCComd(F, (T2,TL), M, B, D, VDS, DB, (TL1,T?:[Term])) else << DB ; getMsg(T?:[Term]) >> fi if T?:[Term] := solveBubbles(T1,M,B,VDS,DB) . --- the last argument (no condition) ceq procLMCComd(F, 'bubble[QI], M, B, D, VDS, DB, TL1) = if T?:[Term] :: Term then procLMC(F, (TL1,T?:[Term]), nil, D, M, VDS,DB) else << DB ; getMsg(T?:[Term]) >> fi if T?:[Term] := solveBubbles('bubble[QI],M,B,VDS,DB) . --- the last argument (may have condition) ceq procLMCComd(F, 'bubble['__[TL]], M, B, D, VDS, DB, TL1) = if T?:[Term] :: Term then procLMC(F, (TL1,T?:[Term]), nil, D, M, VDS,DB) else if lmcCmdCond(F) :: Type then parseLMCCondArg1(F,'bubble['__[TL]],lmcCmdCond(F),D,M,VDS,DB,TL1) else << DB ; getMsg(T?:[Term]) >> fi fi if T?:[Term] := solveBubbles('bubble['__[TL]], M, B, VDS, DB) . --- parse lmc command args: procLMCComd(BUBBLES,MOD,HasMetaLv?,HasCond?,...) op parseLMCCondArg1 : Qid Term Type Bound Module OpDeclSet Database TermList -> Tuple{Database,QidList} . op parseLMCCondArg2 : Qid Term Bound Module OpDeclSet Database TermList -> Tuple{Database,QidList} . --- the last argument (with condition) ceq parseLMCCondArg1(F, 'bubble['__[TL]], TY, D, M, VDS, DB, TL1) = if RP? :: ResultPair then parseLMCCondArg2(F, getTerm(RP?), D, M, VDS, DB, TL1) else << DB ; ('\r 'Error: '\o 'no 'parse 'for downQidList('__[TL,''..Qid]) '\n) >> fi if M1 := addOps( op '_s.t._. : TY '@Condition@ -> 'PatternCondition [prec(122)] . op '_such`that_. : TY '@Condition@ -> 'PatternCondition [prec(122)] ., addSorts('PatternCondition, addInfoConds(M))) /\ RP? := metaParse(M1, downQidList('__[TL,''..Qid]), 'PatternCondition) . --- parse conditions eq parseLMCCondArg2(F, QI[T1,T2], D, M, VDS, DB, TL1) = if QI == '_s.t._. or QI == '_such`that_. then procLMC(F, (TL1,T1), parseCond(T2,VDS), D, M, VDS, DB) else procLMC(F, (TL1,constsToVars(QI[T1,T2],VDS)), nil, D, M, VDS, DB) fi . eq parseLMCCondArg2(F, T, D, M, VDS, DB, TL1) = procLMC(F, (TL1,constsToVars(T,VDS)), nil, D, M, VDS, DB) [owise] . --- error handling eq getTerm({T, M, B, VDS, DB}) = T . eq getTerm(tupleTMBOBDerror(QIL)) = qidError(QIL) . eq getModule({T, M, B, VDS, DB}) = M . eq getModule(tupleTMBOBDerror(QIL)) = unitError(QIL) . eq getVars({T, M, B, VDS, DB}) = VDS . eq getVars(tupleTMBOBDerror(QIL)) = opDeclError(QIL) . eq getBool({T, M, B, VDS, DB}) = B . eq getBool(tupleTMBOBDerror(QIL)) = false . eq getDatabase({T, M, B, VDS, DB}) = DB . eq getDatabase(tupleTMBOBDerror(QIL)) = emptyDatabase . ------------------------------------- --- execute commands --- op procLMC : Qid TermList Condition Bound Module OpDeclSet Database -> Tuple{Database,QidList} . eq procLMC('lfmc_|=_., (T1,T2), CD, D, M, VDS, DB) = procLMCExec(T1, T2, CD, true, D, M, DB) . eq procLMC('lmc_|=_., (T1,T2), CD, D, M, VDS, DB) = procLMCExec(T1, T2, CD, false, D, M, DB) . op procLMCExec : Term Term Condition Bool Bound Module Database -> Tuple{Database,QidList} . ceq procLMCExec(T1, T2, CD, B, D, M, DB) = if RP? :: ResultPair then << DB ; printLMCInfo(M,B,T1,T2,CD) printLMCOutput(M,getTerm(RP?)) >> else << DB ; getMsg(getTerm(RP?)) >> fi if U := addEqs( (eq '##m##.Module = up(M) [none] . eq '##f##.TermList = upTerm(props(M,T2)) [none] .), upModule('META-SYMBOLIC-COND-CONNECTOR2, false)) /\ T3 := up(getTerm(metaReduce(M,T1))) /\ T4 := up(getTerm(metaReduce(M,T2))) /\ RP? := metaReduce(U, 'lmc-check[T3,T4,upTerm(CD),upTerm(B),upTerm(D)]) . op printLMCInfo : Module Bool Term Term Condition -> QidList . eq printLMCInfo(M, B, T1, T2, CD) = '\b 'logical (if B then 'folding else nil fi) 'model 'check 'in '\o eMetaPrettyPrint(getName(M)) '\b ': '\o '\n '\s '\s eMetaPrettyPrint(M,T1) '\b '\s '|= '\s '\o eMetaPrettyPrint(M,T2) (if CD == nil then nil else '\n '\b 'under 'the 'condition ': '\o '\n '\s '\s eMetaPrettyPrint(M,CD) fi) '\n . op printLMCOutput : Module Term -> QidList . eq printLMCOutput(M, 'result:_real:_bound:_complete:_[T1,T2,T3,T4]) = '\b 'result: '\o '\n '\s '\s (if T1 == 'true.Bool then if T4 == 'true.Bool then 'true '\s '`( 'complete 'with 'depth eMetaPrettyPrint(M,T3) '`) else 'no 'counterexample 'found 'within 'bound eMetaPrettyPrint(M,T3) fi else if T2 == 'true.Bool then nil else 'possibly 'spurious fi 'counterexample 'found 'at 'depth eMetaPrettyPrint(M,T3) '\n '\s '\s printLMCCE(M, T1) fi) '\n . eq printLMCOutput(M, T) = '\b 'error: '\o '\n '\s '\s 'model 'checker 'internal 'error '\n [owise] . op printLMCCE : Module Term -> QidList . ceq printLMCCE(M, T) = eMetaPrettyPrint(M, downTerm(getTerm(RP))) if RP := metaReduce(upModule('META-LMC-COUNTEREXAMPLE-TRANSFORMER,false), 'transRes[T]) . eq printLMCCE(M, T) = 'invalid 'counterexample 'term [owise] . endm mod LMC-DATABASE-HANDLING is inc DATABASE-HANDLING . pr LMC-COMMAND-PROCESSING . var Atts : AttributeSet . var X@DatabaseClass : DatabaseClass . var F : Qid . var O : Oid . var ME : ModuleExpression . var DB : Database . var TL : TermList . var T T' : Term . var QIL : QidList . crl [LMC] : < O : X@DatabaseClass | db : DB, input : (F[TL]), output : QIL, default : ME, Atts > => < O : X@DatabaseClass | db : getDatabase(procLMCComd(F[TL], ME, DB)), input : nilTermList, output : getQidList(procLMCComd(F[TL], ME, DB)), default : ME, Atts > if (F == 'lmc_|=_.) or-else (F == 'lfmc_|=_.) . endm mod LMC-FULL-MAUDE is pr FULL-MAUDE . pr LMC-DATABASE-HANDLING . endm set trace off . set break off . set profile off . loop init .