playing with tesla

Maude-2.7.1-osx/linear.maude

+***(
+
+    This file is part of the Maude 2 interpreter.
+
+    Copyright 1997-2006 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 Diophantine solver.
+***	Version 2.3.
+***
+
+fmod VECTOR{X :: DEFAULT} is
+  protecting (ARRAY * (sort Entry{X,Y} to Entry{Y},
+                       sort Array{X,Y} to Vector{Y})
+             ){Nat, X} .
+endfm
+
+fmod INDEX-PAIR is
+  protecting NAT .
+  sort IndexPair .
+  op _,_ : Nat Nat -> IndexPair [ctor] .
+endfm
+
+view IndexPair from TRIV to INDEX-PAIR is
+  sort Elt to IndexPair .
+endv
+
+fmod MATRIX{X :: DEFAULT} is
+  protecting (ARRAY * (sort Entry{X,Y} to Entry{Y},
+                       sort Array{X,Y} to Matrix{Y})
+             ){IndexPair, X} .
+endfm
+
+fmod INT-VECTOR is
+  protecting VECTOR{Int0} * (sort Entry{Int0} to IntVectorEntry,
+                             sort Vector{Int0} to IntVector,
+                             op empty to zeroVector) .
+endfm
+
+view IntVector from TRIV to INT-VECTOR is
+  sort Elt to IntVector .
+endv
+
+fmod INT-MATRIX is
+  protecting MATRIX{Int0} * (sort Entry{Int0} to IntMatrixEntry,
+                             sort Matrix{Int0} to IntMatrix,
+		              op empty to zeroMatrix) .
+endfm
+
+fmod DIOPHANTINE is
+  protecting STRING .
+  protecting INT-MATRIX .
+  protecting SET{IntVector} * (sort NeSet{IntVector} to NeIntVectorSet,
+                               sort Set{IntVector} to IntVectorSet,
+		               op _,_ : Set{IntVector} Set{IntVector} -> Set{IntVector} to
+                               (_,_) [prec 121 format (d d ni d)]) .
+
+  sort IntVectorSetPair .
+  op [_|_] : IntVectorSet IntVectorSet -> IntVectorSetPair [format (d n++i n ni n-- d)] .
+
+  op natSystemSolve : IntMatrix IntVector String -> IntVectorSetPair
+     [special (
+        id-hook MatrixOpSymbol		(natSystemSolve)
+        op-hook succSymbol		(s_ : Nat ~> NzNat)
+        op-hook minusSymbol		(-_ : NzNat ~> Int)
+        op-hook stringSymbol		(<Strings> : ~> Char)
+
+        op-hook emptyVectorSymbol	(zeroVector : ~> IntVector)
+        op-hook vectorEntrySymbol	(_|->_ : Nat Int ~> IntVectorEntry)
+        op-hook vectorSymbol		(_;_ : IntVector IntVector ~> IntVector)
+
+        op-hook emptyMatrixSymbol	(zeroMatrix : ~> IntMatrix)
+        op-hook matrixEntrySymbol	(_|->_ : IndexPair Int ~> IntMatrixEntry)
+        op-hook matrixSymbol		(_;_ : IntMatrix IntMatrix ~> IntMatrix)
+        op-hook indexPairSymbol		(_,_ : Nat Nat ~> IndexPair)
+
+        op-hook emptyVectorSetSymbol	(empty : ~> IntVectorSet)
+        op-hook vectorSetSymbol		(_,_ : IntVectorSet IntVectorSet ~> IntVectorSet)
+        op-hook vectorSetPairSymbol	([_|_] : IntVectorSet IntVectorSet ~> IntVectorSetPair))] .
+
+  op natSystemSolve : IntMatrix IntVector -> IntVectorSetPair .
+  eq natSystemSolve(M:IntMatrix, V:IntVector) = natSystemSolve(M:IntMatrix, V:IntVector, "") .
+endfm

Maude-2.7.1-osx/machine-int.maude

+***(
+
+    This file is part of the Maude 2 interpreter.
+
+    Copyright 1997-2006 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.
+
+)
+
+***
+***	Approximation of Maude 1.0 MachineInts.
+***	Version 2.3.
+***
+***	Note that 0 lives in MachineZero. Also using out of range
+***	integer constants may cause incorrect results. MACHINE-INT may
+***	be instanciated using a view that maps $nrBits to any power of
+***	2 that is >= 2.
+***
+
+fmod RENAMED-INT is
+  protecting INT * (
+    sort Zero to MachineZero,
+    sort NzNat to NzMachineNat,
+    sort Nat to MachineNat,
+    sort NzInt to NzMachineInt,
+    sort Int to MachineInt,
+
+    op s_ : Nat -> NzNat to $succ,
+    op sd : Nat Nat -> Nat to $sd,
+    op -_ : Int -> Int to $neg,
+    op _+_ : Int Int -> Int to $add,
+    op _-_ : Int Int -> Int to $sub,
+    op _*_ : NzInt NzInt -> NzInt to $mult,
+    op _quo_ : Int NzInt -> Int to $quo,
+    op _rem_ : Int NzInt -> Int to $rem,
+    op _^_ : Int Nat -> Int to $pow,
+
+    op abs : NzInt -> NzNat to $abs,
+    op gcd : NzInt Int -> NzNat to $gcd,
+    op lcm : NzInt NzInt -> NzNat to $lcm,
+    op min : NzInt NzInt -> NzInt to $min,
+    op max : NzInt NzInt -> NzInt to $max,
+
+    op _xor_ : Int Int -> Int to $xor,
+    op _>>_ : Int Nat -> Int to  $shr,
+    op _<<_ : Int Nat -> Int to $shl,
+
+    op _divides_ : NzInt Int -> Bool to $divides
+  ) .
+endfm
+
+fth BIT-WIDTH is
+  protecting RENAMED-INT .
+  op $nrBits : -> NzMachineNat .
+
+  var N : NzMachineNat .
+  eq $divides(2, $nrBits) = true [nonexec] .
+  ceq $divides(2, N) = true if $divides(N, $nrBits) /\ N > 1 [nonexec] .
+endfth
+
+view 32-BIT from BIT-WIDTH to RENAMED-INT is
+  op $nrBits to term 32 .
+endv
+
+view 64-BIT from BIT-WIDTH to RENAMED-INT is
+  op $nrBits to term 64 .
+endv
+
+fmod MACHINE-INT{X :: BIT-WIDTH} is
+***
+***	Note that operations
+***	  ~_   _&_  _|_   _<_  _<=_  _>_  _=>_
+***	are inherited unmodified.
+***
+  vars I J : MachineInt .
+  var K : NzMachineInt .
+
+  op $mask : -> NzMachineInt [memo] .
+  eq $mask = $sub($nrBits, 1) .
+
+  op $sign : -> NzMachineInt [memo] .
+  eq $sign = $pow(2, $mask) .
+
+  op maxMachineInt : -> NzMachineInt [memo] .
+  eq maxMachineInt = $sub($sign, 1) .
+
+  op minMachineInt : -> NzMachineInt [memo] .
+  eq minMachineInt = $neg($sign) .
+
+  op $wrap : MachineInt -> MachineInt .
+  eq $wrap(I) = (I & maxMachineInt) | $neg(I & $sign) .
+
+  op _+_ : MachineInt MachineInt -> MachineInt [assoc comm prec 33] .
+  eq I + J = $wrap($add(I, J)) .
+
+  op -_ : MachineInt -> MachineInt .
+  eq - I = $wrap($neg(I)) .
+
+  op _-_ : MachineInt MachineInt -> MachineInt [prec 33 gather (E e)] .
+  eq I - J = $wrap($sub(I, J)) .
+
+  op _*_ : MachineInt MachineInt -> MachineInt [assoc comm prec 31] .
+  eq I * J = $wrap($mult(I, J)) .
+
+  op _/_ : MachineInt NzMachineInt -> MachineInt [prec 31 gather (E e)] .
+  eq I / K = $wrap($quo(I, K)) .
+
+  op _%_ : MachineInt NzMachineInt -> MachineInt [prec 31 gather (E e)] .
+  eq I % K = $rem(I, K) .
+
+  op _^_ : MachineInt MachineInt -> MachineInt [prec 55 gather (E e)] .
+  eq I ^ J = $xor(I, J) .
+
+  op _>>_ : MachineInt MachineInt -> MachineInt [prec 35 gather (E e)] .
+  eq I >> J = $shr(I, ($mask & J)) .
+
+  op _<<_ : MachineInt MachineInt -> MachineInt [prec 35 gather (E e)] .
+  eq I << J = $wrap($shl(I, ($mask & J))) .
+endfm

Maude-2.7.1-osx/metaInterpreter.maude

+***(
+
+    This file is part of the Maude 2 interpreter.
+
+    Copyright 2009 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 meta-interpreters.
+***	Version 2.5.
+***
+
+mod META-INTERPRETER is
+  protecting META-LEVEL .
+  including CONFIGURATION .
+
+  op interpreter : Nat -> Oid .
+
+  op createInterpreter : Oid Oid -> Msg [ctor msg format (b o)] .
+  op createdInterpreter : Oid Oid Oid -> Msg [ctor msg format (m o)] .
+
+  op insertModule : Oid Oid Module -> Msg [ctor msg format (b o)] .
+  op insertedModule : Oid Oid -> Msg [ctor msg format (m o)] .
+
+  op showModule : Oid Oid Qid Bool -> Msg [ctor msg format (b o)] .
+  op showingModule : Oid Oid Module -> Msg [ctor msg format (m o)] .
+
+  op reduceTerm : Oid Oid Qid Term -> Msg [ctor msg format (b o)] .
+  op reducedTerm : Oid Oid Nat Term Sort -> Msg [ctor msg format (m o)] .
+
+  op rewriteTerm : Oid Oid Bound Qid Term -> Msg [ctor msg format (b o)] .
+  op rewroteTerm : Oid Oid Nat Term Sort -> Msg [ctor msg format (m o)] .
+
+  op frewriteTerm : Oid Oid Bound Nat Qid Term -> Msg [ctor msg format (b o)] .
+  op frewroteTerm : Oid Oid Nat Term Sort -> Msg [ctor msg format (m o)] .
+
+  op quit : Oid Oid -> Msg [ctor msg format (b o)] .
+  op bye : Oid Oid -> Msg [ctor msg format (m o)] .
+
+  op interpreterManager : -> Oid
+        [special (
+           id-hook InterpreterManagerSymbol
+           op-hook succSymbol			(s_ : Nat ~> NzNat)
+           op-hook interpreterOidSymbol		(interpreter : Nat ~> Oid)
+           op-hook createInterpreterMsg		(createInterpreter : Oid Oid ~> Msg)
+           op-hook createdInterpreterMsg	(createdInterpreter : Oid Oid Oid ~> Msg)
+           op-hook insertModuleMsg		(insertModule : Oid Oid Module ~> Msg)
+           op-hook insertedModuleMsg		(insertedModule : Oid Oid ~> Msg)
+           op-hook showModuleMsg		(showModule : Oid Oid Qid Bool ~> Msg)
+           op-hook showingModuleMsg		(showingModule : Oid Oid Module ~> Msg)
+           op-hook reduceTermMsg		(reduceTerm : Oid Oid Qid Term ~> Msg)
+           op-hook reducedTermMsg		(reducedTerm : Oid Oid Nat Term Sort ~> Msg)
+           op-hook rewriteTermMsg		(rewriteTerm : Oid Oid Bound Qid Term ~> Msg)
+           op-hook rewroteTermMsg		(rewroteTerm : Oid Oid Nat Term Sort ~> Msg)
+           op-hook frewriteTermMsg		(frewriteTerm : Oid Oid Bound Nat Qid Term ~> Msg)
+           op-hook frewroteTermMsg		(frewroteTerm : Oid Oid Nat Term Sort ~> Msg)
+           op-hook quitMsg			(quit : Oid Oid ~> Msg)
+           op-hook byeMsg			(bye : Oid Oid ~> Msg)
+           op-hook shareWith			(metaReduce : Module Term ~> ResultPair)
+        )] .
+endm

Maude-2.7.1-osx/model-checker.maude

+***(
+
+    This file is part of the Maude 2 interpreter.
+
+    Copyright 1997-2006 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.3.
+***
+
+fmod LTL is
+  protecting BOOL .
+  sort 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
+  including 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
+  protecting 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
+  protecting BOOL .
+  sorts State Prop .
+  op _|=_ : State Prop -> Bool [frozen] .
+endfm
+
+fmod MODEL-CHECKER is
+  protecting QID .
+  including SATISFACTION .
+  including LTL .
+  subsort Prop < Formula .
+
+  *** 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 [ctor] .
+  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

Maude-2.7.1-osx/smt.maude

+***(
+
+    This file is part of the Maude 2 interpreter.
+
+    Copyright 1997-2014 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.
+
+)
+
+***
+***	SMT bindings.
+***	Version alpha 104.
+***
+
+set include BOOL off .
+set include BOOLEAN off .
+
+fmod BOOLEAN is
+  sort Boolean .
+  op true : -> Boolean [special (id-hook SMT_Symbol (true))] .
+  op false : -> Boolean [special (id-hook SMT_Symbol (false))] .
+
+  op not_ : Boolean -> Boolean [prec 53 special (id-hook SMT_Symbol (not))] .
+  op _and_ : Boolean Boolean -> Boolean [gather (E e) prec 55 special (id-hook SMT_Symbol (and))] .
+  op _xor_ : Boolean Boolean -> Boolean [gather (E e) prec 57 special (id-hook SMT_Symbol (xor))] .
+  op _or_ : Boolean Boolean -> Boolean [gather (E e) prec 59 special (id-hook SMT_Symbol (or))] .
+  op _implies_ : Boolean Boolean -> Boolean [gather (e E) prec 61 special (id-hook SMT_Symbol (implies))] .
+
+  op _===_ : Boolean Boolean -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (===))] .
+  op _=/==_ : Boolean Boolean -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (=/==))] .
+  op _?_:_ : Boolean Boolean Boolean -> Boolean [gather (e e e) prec 71 special (id-hook SMT_Symbol (ite))] .
+endfm
+
+fmod INTEGER is
+  protecting BOOLEAN .
+  sort Integer .
+  op <Integers> : -> Integer [special (id-hook SMT_NumberSymbol (integers))] .
+
+  op -_ : Integer -> Integer [special (id-hook SMT_Symbol (-))] .
+  op _+_ : Integer Integer -> Integer [gather (E e) prec 33 special (id-hook SMT_Symbol (+))] .
+  op _*_ : Integer Integer -> Integer [gather (E e) prec 31 special (id-hook SMT_Symbol (*))] .
+  op _-_ : Integer Integer -> Integer [gather (E e) prec 33 special (id-hook SMT_Symbol (-))] .
+  op _div_ : Integer Integer -> Integer [gather (E e) prec 31 special (id-hook SMT_Symbol (div))] .
+  op _mod_ : Integer Integer -> Integer [gather (E e) prec 31 special (id-hook SMT_Symbol (mod))] .
+
+  op _<_ : Integer Integer -> Boolean [prec 37 special (id-hook SMT_Symbol (<))] .
+  op _<=_ : Integer Integer -> Boolean [prec 37 special (id-hook SMT_Symbol (<=))] .
+  op _>_ : Integer Integer -> Boolean [prec 37 special (id-hook SMT_Symbol (>))] .
+  op _>=_ : Integer Integer -> Boolean [prec 37 special (id-hook SMT_Symbol (>=))] .