Previous Version of Maude-SE

About Maude SE
Getting started
How to Cite
Download
1. Supported Version
SMT Interface
1. Full Maude Interface
  1. Search Command
  2. Usage
2. Core Maude Interface
  1. Core Maude Functions
  2. Usage
Examples

About Maude SE

Maude SE is a rewriting modulo SMT extension of Maude at C++ level. It provides a Maude user interface to specify an SMT formula with equations and rules and can generate a set of concrete assignments when the formula is satisfied. Currently supported SMT solvers are Z3, Yices2, CVC4, and dReal.

Get started now Paper

Maude-SE is an SMT extension of Maude that tightly integrates Maude and SMT solvers with extra functionality. It extends the original Maude-SMT at core Maude level. In addition to the existing SMT solving capability of Maude, the tool provides three additional features that are not currently supported by Maude but that are very useful for rewriting modulo SMT:

building satisfying assignments by SMT solving,
simplifying formulas using the underlying SMT solver, and
dealing with non-linear arithmetic formulas.

Maude-SE can analyze nontrivial systems that cannot be dealt with by the previous Maude-SMT implementation.

There are three versions of Maude SE (i.e., Z3, Yices2, CVC4), depending on an underlying SMT solver it uses.

Getting started

To use Maude SE, please follow the instructions below:

Download one of the zip files from here (e.g., maude-se-z3.tar.gz).

Extract the zip file to somewhere you want.

# you can see `smt-check.maude` at the top directory.
$ tar -xvzf maude-se-z3.tar.gz && cd maude-se-z3

Load or include smt-check.maude in your own module.

How to Cite

To cite our paper, use the following bibtex format or refer to the google scholar.

@article{yu2020maude,
  title={Maude-SE: A tight integration of Maude and SMT solvers},
  author={Yu, Geunyeol and Bae, Kyungmin},
  journal={Rewriting Logic and its Applications},
  pages={220},
  year={2020}
}

Download

Maude-SE currently supports three major SMT solvers: Z3, Yices2 (a variation of Yices solver Yices2-mcsat), and CVC4. Maude-SE with Z3, Yices2-mcsat, and CVC4 support quantifier free nonlinear theories as well as linear theories, while Yices only supports linear ones. We will going to support dReal SMT solver (dReal3 and dReal4) in the future.

Supported Version

#	Name	Files
1	maude-se-z3	[MacOS][Ubuntu]
2	maude-se-yices2	[MacOS][Ubuntu]
3	maude-se-yices2-mcsat	[MacOS][Ubuntu]
4	maude-se-cvc4	[MacOS][Ubuntu]
5	maude-se-dreal4

Currently, we support Maude-SE executables for Linux 64 bits only. We will provide executables for MacOS later.

SMT Interface

Full Maude Interface

The Full Maude interface of Maude SE provides smt-search2 command for symbolic reachability analysis.

Search Command

Given an initial state t, a goal pattern u, and a goal condition cond, the following command searches for n states that are reachable within m rewrite steps from the initial state t, match the goal pattern u, and satisfy the goal condition cond.

(smt-search2 [n, m] in M : t =>* u such that cond.)

Usage

To see the usage of this command, refer to the Maude-SE paper for more details. For the simple usage of the command, see the full/robot.maude example.

Core Maude Interface

The main functionality of the Maude SE is implemented in the predefined functional module SMT-CHECK which also contains signatures for both SMT formulas and their solutions.

The interface contains two main functions in the module SMT-CHECK:

smtCheck for checking the satisfiability of an SMT formula, and
simplifyFormula for simplifying the formula.

Core Maude Functions

op smtCheck : BooleanExpr -> SmtCheckResult .
eq smtCheck(BE:BooleanExpr) = smtCheck(BE:BooleanExpr, false) .
op smtCheck : BooleanExpr Bool -> SmtCheckResult [special ... )] .
op simplifyFormula : BooleanExpr -> BooleanExpr [special ... )] .
op simplifyFormula : IntegerExpr -> IntegerExpr [special ... )] .
op simplifyFormula : RealExpr -> RealExpr [special ... )] .

Usage

To see the usages of these functions, see gcd.maude and robot.maude examples.

Examples

We provide three examples: robot-full.maude, gcd.maude, and robot.maude.

Full Maude Robot

(omod ROBOT-DYNAMICS is
  pr REAL .
  inc CONFIGURATION .

  sort Vector .
  op `[_`,_`] : Real Real -> Vector [ctor] .
  sorts RobotTraceItem RobotTrace .
  subsort Vector < RobotTraceItem < RobotTrace .
  op ==`(_:_`)==> : Vector Real -> RobotTraceItem [ctor] .
  op __ : RobotTrace RobotTrace -> RobotTrace [ctor assoc] .
  class Robot | pos : Vector, vel : Vector, acc : Vector, clock : Real, trace : RobotTrace .
  sort State .
  op r : -> Oid [ctor] .
  subsort Configuration < State .

  vars O : Oid .
  vars PX VX AX PY VY AY PX' VX' AX' PY' VY' AY' T T' TAU : Real .
  var ATTS : AttributeSet .
  var TRACE : RobotTrace .

  crl [move]:
      < O : Robot | pos  : [PX,  PY], 
                       vel  : [VX,  VY],
			acc : [AX, AY],
                       clock : T,
                       trace : TRACE >
   => < O : Robot | pos  : [PX', PY'], 
                       vel  : [VX', VY'],
                       clock : T + TAU, 
                       trace : TRACE ==([VX', VY'] : T + TAU)==> [PX', PY'] >
   if VX' = VX + AX * TAU
   /\ VY' = VY + AY * TAU
   /\ PX' = 1/2 * AX * TAU * TAU + VX * TAU + PX
   /\ PY' = 1/2 * AY * TAU * TAU + VY * TAU + PY 
   /\ TAU >= 0/1 = true [nonexec] . 

  crl [accX]:
      < O : Robot | acc : [AX,  AY] >
   => < O : Robot | acc : [AX', AY] >
   if AY = 0/1 [nonexec] .

  crl [accY]:
      < O : Robot | acc : [AX, AY] >
   => < O : Robot | acc : [AX, AY'] >
   if AX = 0/1 [nonexec] . 
endom)

(smt-search2 [1] 
    < r : Robot | pos  : [0/1, 0/1],
                   vel  : [0/1, 0/1],
                   acc  : [0/1, 0/1],
                   clock : 0/1,
		   trace : [0/1, 0/1] >
  =>*
    < r : Robot | pos  : [10/1, 10/1] > .)

To run the full-maude robot example using Z3 binding of Maude SE, go to the top directory (where the exectuable is placed) and type the following command:

$ ./maude-se-z3 examples/full/robot.maude

GCD

mod GCD is
  protecting INTEGER-EXPR .
  pr SMT-CHECK .
  pr META-LEVEL .
    
  ops a b : -> SMTVarId [ctor] .

  sort GcdResult .
  op gcd : IntegerExpr IntegerExpr -> GcdResult [ctor] .
  op ret : IntegerExpr -> GcdResult [ctor] .


  sort State .
  op {_,_} : BooleanExpr GcdResult -> State [ctor] .

  vars CONST CONST' : BooleanExpr .
  vars X Y : IntegerExpr .
  var SS : SatAssignmentSet .

  crl {CONST, gcd(X, Y)} => {simplifyFormula(CONST'), gcd(X - Y, Y)}
  if CONST' := CONST and (X > Y) === (true).Boolean / smtCheck(CONST', false) .

  crl {CONST, gcd(X, Y)} => {simplifyFormula(CONST'), gcd(X, Y - X)}
  if CONST' := CONST and (X < Y) === (true).Boolean / smtCheck(CONST', false) .

  crl {CONST, gcd(X, Y)} => {simplifyFormula(CONST'), ret(X)}
  if CONST' := CONST and (X === Y) === (true).Boolean / smtCheck(CONST', false) .
endm

search [1] {true, gcd(i(a), i(b))} =>* {CONST, ret(NN:IntegerExpr)} such that
CONST' := CONST and i(a) + i(b) === 27 and NN:IntegerExpr === 3
/\ smtCheck(CONST') = (true).Bool .

To run the GCD example using Z3 binding of Maude SE, go to top directory (whre the executable is placed) and type the following command:

$ ./maude-se-z3 examples/gcd.maude

Robot

mod ROBOT is
  pr REAL-EXPR .
  inc CONFIGURATION .
    
  sort Robot .
  subsort Robot < Cid .
  op Robot : -> Robot [ctor format(! o)] .
    
  op pos`:_ : Vector -> Attribute [ctor gather(&)] .
  op vel`:_ : Vector -> Attribute [ctor gather(&)] .
  op acc`:_ : Vector -> Attribute [ctor gather(&)] .
  op time`:_ : RealExpr -> Attribute [ctor gather(&)] .
    
  sort Vector .
  op [_,_] : RealExpr RealExpr -> Vector [ctor] .
endm
    
    
mod ROBOT-DYNAMICS is
  pr ROBOT .
  pr SMT-CHECK .
  inc NAT .
  pr META-LEVEL .
    
  sort State .
  subsort Nat < SMTVarId .
  op {_,_,_} : BooleanExpr Nat Configuration -> State [ctor] .
    
  var N : Nat .
  vars O : Oid .
  vars CONST CONST' : BooleanExpr .
  vars PX VX AX PY VY AY PX' VX' AX' PY' VY' AY' T T' TAU : RealExpr .
  var ATTS : AttributeSet .
    
  crl [move]:
  {CONST, N, 
    < O : C:Robot | pos  : [PX,  PY], 
                    vel  : [VX,  VY],
                    acc  : [AX,  AY],  
                    time : T, ATTS >}
    => {CONST', N + 5, 
    < O : C:Robot | pos  : [PX', PY'], 
                    vel  : [VX', VY'],
                    acc  : [AX,  AY], 
                    time : T + TAU, ATTS >}
    if TAU := r(N)
    /\ [PX', PY'] := [r(N + 1), r(N + 2)]
    /\ [VX', VY'] := [r(N + 3), r(N + 4)]
    /\ CONST' := simplifyFormula(CONST and TAU >= toReal(0)
            and VX' === VX + AX * TAU
            and VY' === VY + AY * TAU
            and PX' === 1/2 * AX * TAU * TAU + VX * TAU + PX
            and PY' === 1/2 * AY * TAU * TAU + VY * TAU + PY) 
    /\ smtCheck(CONST') .
    
  crl [accX]:
    {CONST,  N,   < O : C:Robot | acc : [AX,  AY], ATTS >}
    => 
    {CONST', s N, < O : C:Robot | acc : [AX', AY], ATTS >}
    if AX' := r(N)
    /\ CONST' := simplifyFormula(CONST and AY === toReal(0))
    /\ smtCheck(CONST') .
    
  crl [accY]:
    {CONST,  N,   < O : C:Robot | acc : [AX, AY],  ATTS >}
    => 
    {CONST', s N, < O : C:Robot | acc : [AX, AY'], ATTS >}
    if AY' := r(N)
    /\ CONST' := simplifyFormula(CONST and AX === toReal(0)) 
    /\ smtCheck(CONST') .
endm
    
mod ROBOT-ANALYSIS is
  inc ROBOT-DYNAMICS .
    
  var N : Nat .
  vars CONST : BooleanExpr .
  vars PX VX AX PY VY AY T : RealExpr .
  var SS : SatAssignmentSet .
  var OBJ : Object .
  var ATTS : AttributeSet .
    
  op r : -> Oid [ctor] .
endm
      
search [1] 
{true,  0, 
 < r : Robot | pos  : [toReal(0), toReal(0)],
               vel  : [toReal(0), toReal(0)],
               acc  : [toReal(0), toReal(0)],
               time : toReal(0) >}
=>*
{CONST,  N, 
 < r : Robot | pos  : [PX, PY], ATTS >} such that
{SS} := smtCheck(CONST and PX === 10/1 and PY === 10/1, true) .

To run the robot example using Z3 binding of Maude SE, go to top directory (whre the executable is placed) and type the following command:

$ ./maude-se-z3 examples/robot.maude

Previous Version of Maude-SE

Table of contents

About Maude SE

Getting started

How to Cite

Download

Supported Version

SMT Interface

Full Maude Interface

Search Command

Usage

Core Maude Interface

Core Maude Functions

Usage

Examples

Full Maude Robot

GCD

Robot