***( This file is part of the Maude 2 interpreter. Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA. ) *** *** Maude LTL satisfiability solver and model checker. *** Version 2.0. *** fmod LTL is sorts Prop Formula . subsort Prop < Formula . *** primitive LTL operators ops True False : -> Formula [ctor format (g o)] . op ~_ : Formula -> Formula [ctor prec 53 format (r o d)] . op _/\_ : Formula Formula -> Formula [comm ctor gather (E e) prec 55 format (d r o d)] . op _\/_ : Formula Formula -> Formula [comm ctor gather (E e) prec 59 format (d r o d)] . op O_ : Formula -> Formula [ctor prec 53 format (r o d)] . op _U_ : Formula Formula -> Formula [ctor prec 63 format (d r o d)] . op _R_ : Formula Formula -> Formula [ctor prec 63 format (d r o d)] . *** defined LTL operators op _->_ : Formula Formula -> Formula [gather (e E) prec 65 format (d r o d)] . op _<->_ : Formula Formula -> Formula [prec 65 format (d r o d)] . op <>_ : Formula -> Formula [prec 53 format (r o d)] . op []_ : Formula -> Formula [prec 53 format (r d o d)] . op _W_ : Formula Formula -> Formula [prec 63 format (d r o d)] . op _|->_ : Formula Formula -> Formula [prec 63 format (d r o d)] . *** leads-to op _=>_ : Formula Formula -> Formula [gather (e E) prec 65 format (d r o d)] . op _<=>_ : Formula Formula -> Formula [prec 65 format (d r o d)] . vars f g : Formula . eq f -> g = ~ f \/ g . eq f <-> g = (f -> g) /\ (g -> f) . eq <> f = True U f . eq [] f = False R f . eq f W g = (f U g) \/ [] f . eq f |-> g = [](f -> (<> g)) . eq f => g = [] (f -> g) . eq f <=> g = [] (f <-> g) . *** negative normal form eq ~ True = False . eq ~ False = True . eq ~ ~ f = f . eq ~ (f \/ g) = ~ f /\ ~ g . eq ~ (f /\ g) = ~ f \/ ~ g . eq ~ O f = O ~ f . eq ~(f U g) = (~ f) R (~ g) . eq ~(f R g) = (~ f) U (~ g) . endfm fmod LTL-SIMPLIFIER is inc LTL . *** The simplifier is based on: *** Kousha Etessami and Gerard J. Holzman, *** "Optimizing Buchi Automata", p153-167, CONCUR 2000, LNCS 1877. *** We use the Maude sort system to do much of the work. sorts TrueFormula FalseFormula PureFormula PE-Formula PU-Formula . subsort TrueFormula FalseFormula < PureFormula < PE-Formula PU-Formula < Formula . op True : -> TrueFormula [ctor ditto] . op False : -> FalseFormula [ctor ditto] . op _/\_ : PE-Formula PE-Formula -> PE-Formula [ctor ditto] . op _/\_ : PU-Formula PU-Formula -> PU-Formula [ctor ditto] . op _/\_ : PureFormula PureFormula -> PureFormula [ctor ditto] . op _\/_ : PE-Formula PE-Formula -> PE-Formula [ctor ditto] . op _\/_ : PU-Formula PU-Formula -> PU-Formula [ctor ditto] . op _\/_ : PureFormula PureFormula -> PureFormula [ctor ditto] . op O_ : PE-Formula -> PE-Formula [ctor ditto] . op O_ : PU-Formula -> PU-Formula [ctor ditto] . op O_ : PureFormula -> PureFormula [ctor ditto] . op _U_ : PE-Formula PE-Formula -> PE-Formula [ctor ditto] . op _U_ : PU-Formula PU-Formula -> PU-Formula [ctor ditto] . op _U_ : PureFormula PureFormula -> PureFormula [ctor ditto] . op _U_ : TrueFormula Formula -> PE-Formula [ctor ditto] . op _U_ : TrueFormula PU-Formula -> PureFormula [ctor ditto] . op _R_ : PE-Formula PE-Formula -> PE-Formula [ctor ditto] . op _R_ : PU-Formula PU-Formula -> PU-Formula [ctor ditto] . op _R_ : PureFormula PureFormula -> PureFormula [ctor ditto] . op _R_ : FalseFormula Formula -> PU-Formula [ctor ditto] . op _R_ : FalseFormula PE-Formula -> PureFormula [ctor ditto] . vars p q r s : Formula . var pe : PE-Formula . var pu : PU-Formula . var pr : PureFormula . *** Rules 1, 2 and 3; each with its dual. eq (p U r) /\ (q U r) = (p /\ q) U r . eq (p R r) \/ (q R r) = (p \/ q) R r . eq (p U q) \/ (p U r) = p U (q \/ r) . eq (p R q) /\ (p R r) = p R (q /\ r) . eq True U (p U q) = True U q . eq False R (p R q) = False R q . *** Rules 4 and 5 do most of the work. eq p U pe = pe . eq p R pu = pu . *** An extra rule in the same style. eq O pr = pr . *** We also use the rules from: *** Fabio Somenzi and Roderick Bloem, *** "Efficient Buchi Automata from LTL Formulae", *** p247-263, CAV 2000, LNCS 1633. *** that are not subsumed by the previous system. *** Four pairs of duals. eq O p /\ O q = O (p /\ q) . eq O p \/ O q = O (p \/ q) . eq O p U O q = O (p U q) . eq O p R O q = O (p R q) . eq True U O p = O (True U p) . eq False R O p = O (False R p) . eq (False R (True U p)) \/ (False R (True U q)) = False R (True U (p \/ q)) . eq (True U (False R p)) /\ (True U (False R q)) = True U (False R (p /\ q)) . *** <= relation on formula op _<=_ : Formula Formula -> Bool [prec 75] . eq p <= p = true . eq False <= p = true . eq p <= True = true . ceq p <= (q /\ r) = true if (p <= q) /\ (p <= r) . ceq p <= (q \/ r) = true if p <= q . ceq (p /\ q) <= r = true if p <= r . ceq (p \/ q) <= r = true if (p <= r) /\ (q <= r) . ceq p <= (q U r) = true if p <= r . ceq (p R q) <= r = true if q <= r . ceq (p U q) <= r = true if (p <= r) /\ (q <= r) . ceq p <= (q R r) = true if (p <= q) /\ (p <= r) . ceq (p U q) <= (r U s) = true if (p <= r) /\ (q <= s) . ceq (p R q) <= (r R s) = true if (p <= r) /\ (q <= s) . *** condition rules depending on <= relation ceq p /\ q = p if p <= q . ceq p \/ q = q if p <= q . ceq p /\ q = False if p <= ~ q . ceq p \/ q = True if ~ p <= q . ceq p U q = q if p <= q . ceq p R q = q if q <= p . ceq p U q = True U q if p =/= True /\ ~ q <= p . ceq p R q = False R q if p =/= False /\ q <= ~ p . ceq p U (q U r) = q U r if p <= q . ceq p R (q R r) = q R r if q <= p . endfm fmod SAT-SOLVER is inc LTL . *** formula lists and results sorts FormulaList SatSolveResult TautCheckResult . subsort Formula < FormulaList . subsort Bool < SatSolveResult TautCheckResult . op nil : -> FormulaList [ctor] . op _;_ : FormulaList FormulaList -> FormulaList [ctor assoc id: nil] . op model : FormulaList FormulaList -> SatSolveResult [ctor] . op satSolve : Formula ~> SatSolveResult [special ( id-hook SatSolverSymbol 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) op-hook formulaListSymbol (_;_ : FormulaList FormulaList ~> FormulaList) op-hook nilFormulaListSymbol (nil : ~> FormulaList) op-hook modelSymbol (model : FormulaList FormulaList ~> SatSolveResult) term-hook falseTerm (false) )] . op counterexample : FormulaList FormulaList -> TautCheckResult [ctor] . op tautCheck : Formula ~> TautCheckResult . op $invert : SatSolveResult -> TautCheckResult . var F : Formula . vars L C : FormulaList . eq tautCheck(F) = $invert(satSolve(~ F)) . eq $invert(false) = true . eq $invert(model(L, C)) = counterexample(L, C) . endfm fmod SATISFACTION is pr LTL . sort State . op _|=_ : State Formula ~> Bool . endfm fmod MODEL-CHECKER is pr QID . inc SATISFACTION . *** transitions and results sorts RuleName Transition TransitionList ModelCheckResult . subsort Qid < RuleName . subsort Transition < TransitionList . subsort Bool < ModelCheckResult . ops unlabeled deadlock : -> RuleName . op {_,_} : State RuleName -> Transition . op nil : -> TransitionList [ctor] . op __ : TransitionList TransitionList -> TransitionList [ctor assoc id: nil] . op counterexample : TransitionList TransitionList -> ModelCheckResult [ctor] . op modelCheck : State Formula ~> ModelCheckResult [special ( id-hook ModelCheckerSymbol 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) op-hook satisfiesSymbol (_|=_ : State Formula ~> Bool) op-hook qidSymbol ( : ~> Qid) op-hook unlabeledSymbol (unlabeled : ~> RuleName) op-hook deadlockSymbol (deadlock : ~> RuleName) op-hook transitionSymbol ({_,_} : State RuleName ~> Transition) op-hook transitionListSymbol (__ : TransitionList TransitionList ~> TransitionList) op-hook nilTransitionListSymbol (nil : ~> TransitionList) op-hook counterexampleSymbol (counterexample : TransitionList TransitionList ~> ModelCheckResult) term-hook trueTerm (true) )] . endfm