Maude-help mailing list

[Francisco Duran <duran AT lcc.uma.es>]

Hi Alexandre,

My apologies!

I was working on it, but things got complicated. In FM2.1 built-in modules were 
handled in a special way, they were recognized and left to Core Maude to handle 
them. For FM2.1.1 I tried to handle all modules in a similar way, so that they 
are handled like any other module. Now I believe this was a wrong decision, and 
this is why my answer was taken so long.

You could use the model checker entering the files in model-checker.maude as 
Full Maude modules (like in the attached file). However, in this way it is much 
more inefficient (in time and memory). I'm working on an alternative, but it's 
taking more than I expected.

Paco



Alexandre Rademaker wrote:

> Hello Team,
>
> Please, someone could help me? My question below about Model Checking in 
> Full Maude is still open!
>
> Thanks for all,
> Alexandre Rademaker
>
> -------- Original Message --------
> Subject: Full Maude 2.1.1 and Model Checker
> Date: Tue, 26 Oct 2004 13:18:29 -0200
> From: Alexandre Rademaker 
> <rademake AT eml.cc>
> Reply-To: 
> rademake AT eml.cc
> To: 
> maude-help AT maude.cs.uiuc.edu
>
> How can I use the Model Checker in Full-Maude?
>
> After removing the comment in line 124 of Full-Maude file I am
> not able to import the Model Checker modules in others Modules in Full
> Maude database. Example:
>
> (omod S-VER-PCB is
>  inc MODEL-CHECKER .
>  subsort Configuration < State .
>  ...
> endom)
>
> In the Full-Maude 2.1 one could extend the equation:
>
>   op builtIns : -> ModNameSet .
>   eq builtIns
>     = 'TRUTH-VALUE . ...
>
> and add references for MODEL-CHECKER modules at Core Maude database,
> but in the current version of Full-Maude it seems to me that the
> operator builtIns was removed! So, since the Model Checker modules are
> load in Core Maude, how can I use the Core Maude Modules in
> Full-Maude?
>
> Best regards,
> Alexandre Rademaker
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help
***(

    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)

set trace on .
trace include FULL-MAUDE .
set trace select on .
trace select metaParse .

(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)

eof

(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            (<Qids> : ~> 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)