NDRQL (Nondeterministic Rewriting Query Language) is a multiset query and update language executable in a term rewriting system.
Its most remarkable feature, besides non-standard approach to quantification
and introduction of fresh values, is
non-determinism — a query result is not uniquely determined by the database.
Arguably, this feature is very useful, e.g., in modelling user choices during
simulation or reachability analysis of a data-centric business process — the intended application of NDQRL. Query evaluation is implemented by converting
the query into a terminating term rewriting system and normalizing the initial term which encapsulates the current database. A normal form encapsulates a query result.
One can prove that NDQRL can express any relational algebra query.
This page makes available Maude implementatation of NDQRL's syntax and semantics in Maude rewriting language.
It also documents the implementation, as well as provides some example specification ready for simulation.
Syntax and semantics of NDRQL is defined in the Maude file QuerySemantics.maude
An example specification is contained in Bookings.maude.
NDQRL consists of several parts, and we present the language according to the division. NDQRL queries are proper Maude terms, and we present the language grammar using sorts and signatures of constructors.
Facts are term of sort Fact.
Facts can be thought of as reified instances of predicates (or rows in a database table, with a table name thrown in), and, accordingly, constructors of fact terms are like predicate names (or top level functors in Prolog).
It is assumed (though nowhere enforced) that the arguments of facts are terms in the “data signature” which does not contain any sort in the [Fact] kind, nor any other kind marking structural parts of queries and conditons.
Facts serve as components of quantification patterns in NDRQL, they are also by themselves DML queries (F as a query matches F in the database).
Databases on which NDQRL queries act are represented as multisets of facts of sort FactSet. Non-empty multisets of facts have sort NeFactSet. The subsort relation is defined by:
subsorts Fact < NeFactSet < FactSet .
i.e., every fact is a non-empty multiset of facts. Multisets of facts are constructed from facts with
op noneF : -> FactSet . op _o_ : FactSet FactSet -> FactSet [assoc comm id: noneF] . op _o_ : NeFactSet FactSet -> NeFactSet [ditto] .
i.e., noneF is an empty multiset, and _o_ is an associative and commutative multiset constructor with neutral element noneF.
A support for creation of fresh values is a common requirement: If identifiers for objects
are to provide unique identity across the whole history, the must not be reused (even if they are not present in the current active database domain).
We support creation of fresh values of nominal sorts only since freshness for non-nominal data types is problematic. A sort is nominal
if values of this sort
have no non-trivial algebraic or relational structure beside equality. To create fresh values, for each nominal sort Nom we have constructor
op {_}Nom : Nat -> Nom [ctor] .
which does not belong to the signature of data values
To make retrieval of fresh values similar to retrieval of data we use
fresh facts of sort FactN unrelated to Fact.
For each nominal sort Nom we have a single-argument constructor of the form
op CNom : Nom -> FactN [ctor] .
which wraps value {n}Nom such that for all m ≥ n, {m}Nom
was never used before. When fresh value of sort Nom is requested we
return {n}Nom and update the fresh fact to
CNom({n+1}Nom)
Fresh facts are combined into multisets of sort FactSetN.
Non-empty mulisets of fresh facts have sort NeFactSetN.
The subsort relation is given by
subsorts FactN < NeFactSetN < FactSetN .
i.e., a fresh fact is a non-empty multiset of fresh facts. Multisets of fresh facts are constructed from facts with operators
op noneFN : -> FactSetN . op _o_ : FactSetN FactSetN -> FactSetN [assoc comm id: noneFN] . op _o_ : NeFactSetN FactSetN -> NeFactSetN [ditto] .
i.e., _o_ is associative and commutative with identity
noneFN.
To facilitate updates (also bulk updates) of fresh facts needed in the semantics of DML queries, we define
the following function
op succ : FactN -> FactN . op refresh : FactSetN -> FactSetN . eq refresh(noneFN) = noneFN . eq refresh(fn:FactN o FnN:FactSetN) = succ(fn:FactN) o refresh(FnN:FactSetN) .
Function refresh simply applies succ to each element
of the multiset passed as an argument. Observe that we do not define (only declare)
the succ function. This is because we have to provide a
separate equation defining succ for each nominal sort Nom and
corresponding nominal value and fact constructors
{_}Nom and CNom (which are specification dependent),
even though the succ's definition will always follow the pattern
eq succ(CNom({N:Nat}Nom)) = CNom({s N:Nat}Nom)
where s : Nat -> Nat is a successor function. This is an unfortunate consequence
of Maude being the first order language which does not provide support for higher order functions.
Using parametrized modules would have allowed us to provide a single generic definition, but at
the cost of plenty of boilerplate (far more than just providing trivial equalities
for each nominal sort). Of course one can use metalevel to generate the equalities automatically.
Quantifiers in NDRQL quantify over patterns (of sort Pat) containing
non-ground multisets of facts and fresh facts marked
by modalities, which control retention of matched facts,
and wrap fresh facts.
Patterns can be preserving (of sort PatP),
semi-terminating (of sort PatST),
terminating (of sort PatT),
terminating & preserving (of sort PatTP), or neither.
The subsort relation is defined by
subsorts PatTP < PatT < PatST < Pat . subsorts PatTP < PatP < Pat .
Patterns are constructed with modalities
op [_]0 : NeFactSet -> PatST . op [_]? : NeFactSet -> PatTP . op [_]! : NeFactSet -> PatP . op [_]n : NeFactSetN -> Pat .
and associative and commutative, subsort overloaded operator _o_:
op _o_ : Pat Pat -> Pat [assoc comm] . op _o_ : PatT Pat -> PatT [ditto] . op _o_ : PatST Pat -> PatST [ditto] . op _o_ : PatP PatP -> PatP [ditto] . op _o_ : PatP PatTP -> PatTP [ditto] .
Thus, a terminating (resp. a semi-terminating) pattern has to contain at least one
fact wrapped with [_]? (resp. with either [_]? or [_]0).
A terminating and preserving pattern
consists of facts marked only with [_]? or [_]!, and it contains at least one fact wrapped with [_]?.
Directed equalities
vars F F' : NeFactSet . vars Fn Fn' : NeFactSetN . eq [ F ]0 o [ F' ]0 = [ F o F' ]0 . eq [ F ]? o [ F' ]? = [ F o F' ]? . eq [ F ]! o [ F' ]! = [ F o F' ]! . eq [ Fn ]n o [ Fn' ]n = [ Fn o Fn' ]n .
guarantee that fully reduced patterns have facts gathered in groups of the same modality.
The informal meaning of modalities is as follows:
[_]? can be considered at most once during quantifier evaluation, but they are not removed from the database.[_]0 are removed from the database when matched, but they are returned
if the computation branch this matching leads to is unsuccessful. Thus, the presence of facts marked by [_]0 in the pattern may not guarantee termination, unless one can prove that the formula under the quantifier is always successful.
[_]!
are always retained in the database.
[_]n wraps fresh facts.
The module SYNTAX-BASE defines some operators for extracting
parts of a pattern (i.e., fresh part, terminating and preserving, and so on).
They are very useful in the code implementing semantics of queries
The naming convention used below should be obvious:
ops get0 get? get! get!? get!?0 : Pat -> FactSet . op getn : Pat -> FactSetN . var P : Pat . var FnN : FactSetN . var fn : FactN . eq get0([ F ]0 o P) = F o get0(P) . eq get0([ F ]0) = F . eq get0(P) = noneF [owise] . eq get?([ F ]? o P) = F o get?(P) . eq get?([ F ]?) = F . eq get?(P) = noneF [owise] . eq get!([ F ]! o P) = F o get!(P) . eq get!([ F ]!) = F . eq get!(P) = noneF [owise] . eq getn([ Fn ]n o P) = Fn o getn(P) . eq getn([ Fn ]n) = Fn . eq getn(P) = noneFN [owise] . eq get!?(P) = get!(P) o get?(P) . eq get!?0(P) = get!(P) o get?(P) o get0(P) .
The sublanguage NDRQL(COND) of conditions
on finite multisets of facts is analogous
to first order logic with quantification restricted to the active domain.
Formulas of NDRQL(COND) are (generally non-ground) terms of sort Cond
constructed with (the definition of syntax of conditions is contained
in the module QUERY-SYNTAX).
ops False True : -> Cond .
op {_} : Bool -> Cond [strat (0)] .
op Not_ : Cond -> Cond .
ops _\/_ _/\_ : Cond Cond -> Cond [assoc comm] .
ops Exists_._ Forall_._ : PatTP Cond -> Cond .
Here _\/_ and _/\_
represent, respectively, disjunction and conjunction.
Exists_._ and Forall_._
are quantifiers, existential (∃) and universal (∀), respectively.
So, naively, exists [R(X, Y)]! o [P(Y)]? . Ψ(X, Y)
iff there exists a matching of R(X, Y) o P(Y)
with the current database such that Ψ(X, Y)
is satisfied (and actually for the particular pattern [R(X, Y)]! o [P(Y)]?
the naive explanation is correct). However the actual semantics described in the paper
and (as a Maude code) in the implementation section of this document
is more subtle, allowing for nondeterministic executions.
Constructor {_} wraps any boolean expression (term of sort Bool)
and makes it a condition. Thus, e.g., {X:Nat == Y:Nat} is a condition. It is defined
as lazy (with a strategy strat(0)) since otherwise non-ground subconditions
of the form {φ} would reduce inapproprietaly. Indeed,
Maude term X:Nat = Y:Nat reduces immediately to false
(there are no two equal natural numbers).
In first order logic we can define some of the logical connectives in terms of others. It turns out that the usual equivalences hold also for connectives in NDRQL(COND). Thus, to simplify the implementation of semantics we define (on the level of syntax):
var P : PatTP . vars C C' : Cond . eq True = Not False . eq C /\ C' = Not (Not C \/ Not C') . eq Forall P . C = Not (Exists P . Not C) .
The sublanguage NDRQL(DML) permits us to define basic DML operations on
multisets of facts which delete from and add some facts to the database.
One can think of them as generalized term rewriting rules.
Queries in NDRQL(DML) are terms of sort
DQuery.
Unfortunately, we cannot define NDRQL(DML) purely syntactically. Therefore
we also use a supersort NDQuery of DQuery for
“query” terms which conform to query syntax but are to general
to be always terminating. To define DQuery-terms we also need an
auxilliary sort DQueryS for “success assured queries”,
i.e., those queries in NDRQL(DML) which always execute successfully (i.e., they return something). Finally, to be able to factorise better the common code and avoid repetition, we define a common supersort
Query of both conditions in NDRQL(COND) and DML queries in NDRQL(DML).
The subsort relation is defined by:
subsorts Fact < DQueryS < DQuery < NDQuery . subsorts DQuery Cond < Query .
As implied by the subsort relation above, any fact is a “success assured DML query” (adding this fact to the database). More complex queries in NDRQL(DML) are constructed with the following function symbols (the Maude code is lifted from the module QUERY-SYNTAX). Their semantics
is informally defined with the bulletpoints below:
op Ok : -> DQueryS . op _=>_ : Cond NDQuery -> NDQuery . op _=>_ : Cond DQuery -> DQuery . op From_._ : Pat NDQuery -> NDQuery [prec 60] . op From_._ : PatT DQuery -> DQuery [prec 60] . op From_._ : PatST DQueryS -> DQuery [prec 60] . op _|>_ : NDQuery NDQuery -> NDQuery [assoc] . op _|>_ : DQuery DQuery -> DQuery [assoc] . op _|>_ : DQueryS DQuery -> DQueryS [assoc] . op _|>_ : DQuery DQueryS -> DQueryS [assoc] .
Ok is a “success assured DML query” doing nothing
(aside from successfully executing).ψ => Δ executes as Δ
if condition ψ holds and does nothing otherwise. Clearly, ψ => Δ
cannot be success assured since condition ψ can fail.
From Γ . Δ denotes iteration over facts in the database matching
Γ. At each iteration step σ(Δ) is executed, where
σ denotes the matching substitution. To guarantee termination, either
the pattern Γ has to be terminating or the pattern is only semiterminating,
but the query Δ is guaranteed to succeed.
Facts in the database matched with subpattern marked with [_]0
are removed from the database immediately, and they are not available to subqueries of
the current query (even to Δ). On the other hand facts added by the subquery
are not available to subqueries of the same DML query executed later.
Δ1 |> Δ2 executes first
Δ1, then Δ2.
If the query does not consume any facts (it contains only preserving and fresh patterns)
it amounts to adding to the database the union of what Δ1
and Δ2 would have added separately, but the immediacy of
fact deletion makes this operation potentially noncommutative (it is associative, though).
A specification is a (multi)-set of rewrite rules defined as “big business steps”
using a sequence of DML queries executed one after the other. More precisely,
a specification is a multiset (of sort QSpec) of business steps of
sort LDQuery (labelled DML query). The subsort relation is given by
subsort LDQuery < QSpec .
and multisets of business steps are constructed with
op EmptySpec : -> QSpec . op _ | _ : QSpec QSpec -> QSpec [assoc comm id: EmptySpec] .
Terms of sort LDQuery have one constructor:
op case : Qid NeDQSeq -> LDQuery .
The first argument is the step's label (where we use Maude's quoted identifiers for the purpose).
The second argument is a non-empty sequence of DML queries which are executed (in sequence) upon execution of
the given business step. Sequences of DML queries have sort DQSeq, non-empty ones have sort NeDQSeq
and the subsort relation is given by:
subsorts DQuery < NeDQSeq < DQSeq .and the sequences are constructed with operators
op Empty : -> DQSeq . op _;_ : DQSeq DQSeq -> DQSeq [assoc id: Empty] . op _;_ : NeDQSeq DQSeq -> NeDQSeq [ditto] . op _;_ : DQSeq NeDQSeq -> NeDQSeq [ditto] .
Operators related to specifications are defined in module QUERY-ALGEBRA.
In this section we will describe the remaining Maude code related (mostly) to semantics of queries (explaining the semantics along the way). The section is structured around Maude modules not described above.
For the description of modules QUERY-BASE, QUERY-SYNTAX and QUERY-ALGEBRA see the previous section.
VARIABLES — Helper functions to deal with lists of variables in terms
The module contains helper functions to deal with sets of metarepresentations of variables as well as to extract lists of metarepresentations of variables contained in metarepresentations of terms. In what follows we drop the “meta” part since whether we mean terms or their meta-representations should be clear from the context. Sets of variables are represented
simply as lists of terms (of sort TermList) from the META-LEVEL module. The functions below which expect list of variables (such as, e.g., Union or Insert) would not reduce when given as argument
a list of terms which contain anything but variables. This is why we define their codomains as having kind but not sort.
First, we have set operations “element of” (_In_),
“subset of” (_Sub_), Insert()
and Union() defined by the following, rather unsurprising code (note that
Insert() and Union() do not permit creation of duplicates):
op _In_ : Variable TermList -> Bool . op _Sub_ : TermList TermList -> [Bool] . op Insert : Variable TermList -> [TermList] . op Union : TermList TermList -> [TermList] . vars V V' : Variable . vars VV VV' : TermList . eq V In empty = false . eq V In (V, VV) = true . eq V In (V', VV) = V In VV [owise] . eq empty Sub VV = true . eq (V , VV) Sub VV' = (V In VV') and-then (VV Sub VV') . eq Insert(V, empty) = V . eq Insert(V, (V, VV)) = V, VV . eq Insert(V, (V', VV)) = V', Insert(V, VV) [owise] . eq Union(empty, VV) = VV . eq Union((V, VV), VV') = Union(VV, Insert(V, VV')) .
Next, there are two mutually recursive functions which extract set of variables occuring in a given term(s). We need VarL which returns variables occurring in a list
of terms in addition to the function Var we are really interested in in order to define what Var is on a term constructed with non-constant function symbol.
op Vars : Term -> TermList . op VarsL : TermList -> TermList . var C : Constant . var T : Term . var TL : TermList . var Q : Qid . var NTL : NeTermList . eq Vars(C) = empty . eq Vars(V) = V . eq VarsL(empty) = empty . eq VarsL((T, TL)) = Union(Vars(T), VarsL(TL)) . eq Vars(Q[NTL]) = VarsL(NTL) .
Finally, there is a function which returns length of a list of variables.
op Len : TermList -> [Nat] . eq Len(empty) = 0 . eq Len((V, VV)) = s Len(VV) .
IS-CLOSED — Functions related to checking if a query is closed
The module defines functions checking if a NDRQL query is closed.
Here closed?(Q) reduces to true if
query Q is closed and to false otherwise.
Term closed?(Q, VV) reduces to true
if Q becomes closed after variables in the list VV
are grounded in Q. Functions closed?() have the signature
op closed? : QSpec -> Bool . op closed? : Query -> Bool . op closed? : Query TermList -> Bool . op closed? : QSpec TermList -> Bool .
Remember that Query is the supersort of Cond
and DQuery.
To define the above functions we use two helpers: Function Vars()
extracting a set of variables occurring in the pattern:
op Vars : Pat -> TermList . eq Vars(P) = Vars(upTerm(P)) .
and function ext() which adds variables occurring in a pattern
to a set of variables:
op ext : Pat TermList -> TermList . eq ext(P, VV) = Union(Vars(P), VV) .
Two-argument closed?() functions are defined in an obvious way
in terms of the two-argument ones:
eq closed?(DQS) = closed?(DQS, empty) . eq closed?(QS) = closed?(QS, empty) .
Now we can define closedness for conditions (which reflect the fact that quantifiers are binding constructs):
eq closed?(False, VV) = true .
eq closed?({B}, VV) = Vars(upTerm({B})) Sub VV .
eq closed?(Not C, VV) = closed?(C, VV) .
eq closed?(C \/ C', VV) = closed?(C, VV) and closed?(C', VV) .
eq closed?(Exists Ptp . C, VV) = closed?(C, ext(Ptp, VV)) .
The closedness for DML queries (where From_._ operator is binding construct):
eq closed?(Ok, VV) = true . eq closed?(f, VV) = Vars(upTerm(f)) Sub VV . eq closed?(C => D, VV) = closed?(C, VV) and closed?(D, VV) . eq closed?(D |> D', VV) = closed?(D, VV) and closed?(D', VV) . eq closed?(From P . D, VV) = closed?(D, ext(P, VV)) .
And finally the closedness of specifications which contain no binding constructs:
eq closed?(Empty, VV) = true . eq closed?(EmptySpec, VV) = true . eq closed?(D ; DQS, VV) = closed?(D, VV) and closed?(DQS, VV) . eq closed?(case(Q, DQS) | QS, VV) = closed?(DQS, VV) and closed?(QS, VV) .
REWRITE-BASE — Base module for generated rewrite systemThis module defines basic constructors and sorts for the generated rewriting
system which executes the query. First of all, the terms which are rewritten have
the sort State and they are constructed with:
op new : FactSet FactSetN Bool -> State .
op {_,_} : Conf Stack -> State .
Here new(FS, FSn, B) is the state at the beginning of evaluation of
of a DML query, where FS is the current database, FSn
are the current fresh fact database (from which we take fresh values), and B
indicates if the execution of the previous DML query ended in success or not. Terms
of the form {C, S} describe intermediate states in the execution of a DML query,
where S is an execution stack used to recursively
evaluate the query and C stores intermediate results of the evaluation.
Terms of sort Conf are constructed with
op <_|_|_> : FactSet FactSetN FactSet -> Conf .
The first argument is the database of facts the query acts on, the second one is a multiset of fresh facts used to generate fresh values, and the last one is a multiset of facts added so far by the query execution. Those facts are added to the database only after the query execution ends, while facts removed from the database are removed immediately while the query executes.
Terms of sort Stack represent stacks of sort Frame with
subsort relation defined by
subsort Frame < Stack .
Stacks are constructed from frames with the following operators (stacks are effectively lists of frames):
op emptySt : -> Stack . op __ : Stack Stack -> Stack [assoc id: emptySt] .
Most constructors of frames are named after identifier of the corresponding subquery, and so they are declared dynamically during compilation. The only exceptions are the following:
op res : Bool -> Frame . op neg : -> Frame .
Constant neg is used when evaluating (negated) conditions — it negates the value of the subsequent frame.
Every frame is supposed to be, eventually, rewritten to either res(true) or res(false). In case of conditions it encodes whether the condition
is satisfied. In case of DML subqueries it encodes whether the execution was successful (res(true)) or not (res(false)).
Pairs of result frames next to one another get reduced by “oring” the wrapped booleans:
vars B B' : Bool . eq res(B) res(B') = res(B or B') .
Frames with names parametrized by the identifier of a subquery wrap local binding of variables. Additionally, frames related to evaluation of quantifiers or From_._
operator store iteration state represented as terms of sort LConf constructed with
op l : FactSet -> LConf . op l : FactSet Bool -> LConf . op l : FactSet Bool FactSet -> LConf .
The first argument in all the constructors above is a multiset of facts available for matching
(which changes as some facts are removed by (semi)terminating part of the pattern in each step).
The boolean argument is used when evaluating From_._ construct to indicate if the iteration was already successful (generated some new facts or Ok).
Finally, the last argument in a ternary constructor stores facts removed by the [_]0
pattern in case the computation branch is unsuccessful and the removed facts have to be returned to the database.
COMPILE-BASE — Helper functions related to generation of system module from queries
The module contains toolbox of functions which simplify generation of system module from queries. Most of the functions create values in the metalevel. It was found out
that constructing values directly, with the constructors from the META-TERM
module lead to unreadable, long and tedious code, so it was wothwhile to define even special functions which construct commonly used variables and constants on the metalevel.
First, there is a group of functions which generate metarepresentations of commonly used variables, constants and terms:
ops @true @false @B $true $false $B $B1 $B2 $noneF : -> Term . eq @true = 'res[$true] . eq @false = 'res[$false] . eq @B = 'res['B:Bool] . eq $noneF = 'noneF.FactSet . eq $true = 'true.Bool . eq $false = 'false.Bool . eq $B = 'B:Bool . eq $B1 = 'B1:Bool . eq $B2 = 'B2:Bool .
Next, we define functions fs() and fsn()
which, given a name return variable with this name and sort
FactSet or FactSetN, respectively.
We use those functions to define some more commonly used variables:
ops fs fsn : String -> Variable .
eq fs(S) = qid(S + ":FactSet") .
eq fsn(S) = qid(S + ":FactSetN") .
ops $F $F' $Fn $Ft $FN : -> Variable .
eq $F = fs("F") . eq $F' = fs("F'") . eq $Fn = fsn("Fn") .
eq $Ft = fs("Ft") . eq $FN = fs("FN") .
Most frames store values of variables in their arguments. They are of one of two forms
op [_,_,…,_]N : S1 S2 … Sn -> Frame . op [_,_,…,_|_]N : S1 S2 … Sn LConf -> Frame .
where N is an identifier of a subquery (or a subcondition) and
S1, S2, …, Sn is a sequence of sorts of variables the bindings of which are stored in the frame.
Thus, in order to construct the above declarations on the metalevel it is helpful to have the following functions two functions acception a list VV of (representations) of variables: args() which returns a string of the form "_,_,...,_" with as many underscores as there are variables in VV, and sorts() which returns a TypeList with sorts of variables in VV:
op args : Nat -> String . op args : TermList -> String . eq args(0) = "" . eq args(1) = "_" . eq args(s (s N)) = "_," + args(s N) . eq args(VV) = args(Len(VV)) . op sorts : TermList -> TypeList . eq sorts(empty) = nil . eq sorts((V, VV)) = getType(V) sorts(VV) .
Using the above functions one defines the following functions which construct names
of frame constructors (name() and sname() return names
of frame constructors of the form shown above, and sname() returns names of frames used in evaluating specifications):
op sname : Nat -> Qid .
ops name qName : Nat TermList -> Qid .
eq name(N, VV) = qid("[" + args(VV) + "]" + string(N, 10)) .
eq qName(N, VV) = qid("[" + args(VV) + "|_]" + string(N, 10)) .
eq sname(N) = qid("s" + string(N, 10)) .
Functions which return meta-representation of declarations of frame constructors, which use the above name creating functions are as follows:
op declSOp : Nat -> OpDecl . ops declOp declQOp : TermList Nat -> OpDecl . eq declOp(VV, N) = op name(N, VV) : sorts(VV) -> 'Frame [none] . . eq declQOp(VV, N) = op qName(N, VV) : sorts(VV) 'LConf -> 'Frame [none] . . eq declSOp(N) = op sname(N) : 'Bool -> 'Frame [none] . .
The meta-level frame constructors are needed when constructing meta-level representation of frame terms in meta-level representations of rules. To make expressions which construct such representations shorter we use the following operators:
op s : Nat Term -> Term .
op $ : Nat TermList -> Term .
op $ : Nat TermList Term -> Term .
eq s(N, T) = sname(N)[T] .
eq $(N, empty) = qid("[]" + string(N, 10) + ".Frame") .
eq $(N, VV) = name(N, VV)[VV] [owise] .
eq $(N, VV, T) = qName(N, VV)[VV, T] .
Rewrite rules we compile our queries into on the metalevel rewrite terms of sort
State. In those rules we need to match configuration term (of sort Conf) and the stack with one or two frames of particular shape at the top
of stack plus, possibly, the bottom of the stack). Accordingly we have the following
functions:
op %1 : Term Term -> Term .
op %2 : Term Term Term -> Term .
op %3 : Term Term Term Term -> Term .
eq %1(T, T') = '`{_`,_`}[T, T'] .
eq %2(T, T1, T2) = %1(T, '__[T1, T2]) .
eq %3(T, T1, T2, T3) = %1(T, '__[T1, T2, T3]) .
Meta-terms constructed with %1(), %2(), and %3()
are in most cases too general. Most rules abstract away the bottom of the stack
as a variable, and some of the rules do not need to match against the contents of configuration so they abstract the Conf term away as a variable.
Accordingly, we have the following functions:
op @ : Term -> Term .
op @2 : Term Term -> Term .
op @c : Term Term -> Term .
op @c2 : Term Term Term -> Term .
eq @(T) = %2('Cf:Conf, 'S:Stack, T) .
eq @2(T1, T2) = %3('Cf:Conf, 'S:Stack, T1, T2) .
eq @c(T, T') = %2(T, 'S:Stack, T') .
eq @c2(T, T1, T2) = %3(T, 'S:Stack, T1, T2) .
Finally, in rules which do need to match against configuration we have the following
function which shortens construction of metalevel representation of Conf
terms:
op c : Term Term Term -> Term .
eq c(T1, T2, T3) = qid("<_|_|_>")[T1, T2, T3] .
As before, we define some common specializations of the above helper:
ops cF cI cN : -> Term .
eq cF = c($F, $Fn, $FN) .
eq cI = c($F, $Fn, $noneF) .
eq cN = c('_o_[$F, $FN], $Fn, $noneF) .
COMPUTE-IDS — Computing identifiers of subqueries
A component of a frame name is the unique identifier of the subquery
related to the frame. The identifiers correspond to preorder numbering of the parse
tree of the query. We build the rewriting system corresponding to the query recursively
and hence, it is necessary to know at the calling function what will be the next
identifier available after recursive call. We could make recursively called function return
the next identifier as part of the returned value, but we decided that we get easier
to understand code if we define a separate function which computes the next identifier after
the supquery is processed. More precisely, assuming that N is the current
“next available identifier”, and Q is the subquery, then
next(N,Q) returns next available identifier after Q is processed.
Function next() is defined as follows:
var N : Nat . vars C C' : Cond . var Ptp : PatTP . var B : Bool .
var F : Fact . vars D D' : NDQuery . var P : Pat . var Q : Qid .
op next : Nat Query -> Nat .
eq next(N, False) = s N .
eq next(N, {B}) = s N .
eq next(N, Not C) = next(s N, C) .
eq next(N, Exists Ptp . C) = next(s N, C) .
eq next(N, C \/ C') = next(next(s N, C), C') .
eq next(N, Ok) = s N .
eq next(N, F) = s N .
eq next(N, C => D) = next(next(s N, D), C) .
eq next(N, D |> D') = next(next(s N, D'), D) .
eq next(N, From P . D) = next(s N, D) .
REC-MODULE — A “monad” for building system modules
Each subquery gives rise to both rewrite rules and declarations of corresponding frame constuctors (and possibly further recursive calls of the compiler). In order to simplify
building the system module which is the result of compilation of the query (or specification) we introduce a representation of meta-representation (of sort RecModule) of a module together with operations which allow to add equations,rewrite rules and declarations in a way which resembles writer-like monads (in, e.g., Haskell). Terms of sort RecModule are constructed with
op rec : Qid Qid OpDeclSet EquationSet RuleSet Nat -> RecModule .
The last argument is the smallest unused subquery identifier (to be used as part of corresponding frame name). The meaning of remaing arguments are best explained
by their sorts as well as the definition of a function which converts
RecModule term into SModule term (meta-representation of a system module):
op toModule : RecModule -> SModule .
eq toModule(rec(Q, Q', O, E, R, N)) = (mod Q is
including Q' .
sorts none .
none
O
none
E
R
endm) .
Initially (at the start of query compilation) the module contains no operator declarations,
equations nor rules, and the next subquery identifier is 0. The following operator constructs this initial term:
op initRec : Qid Qid -> RecModule . eq initRec(Q, Q') = rec(Q, Q', none, none, none, 0) .
During query compilation declarations, equalities and rewrite rules are added to
the RecModule term with operators
op _*_ : RecModule OpDeclSet -> RecModule . op _*_ : RecModule RuleSet -> RecModule . op _*_ : RecModule EquationSet -> RecModule . eq rec(Q, Q', O, E, R, N) * O' = rec(Q, Q', O O', E, R, N) . eq rec(Q, Q', O, E, R, N) * R' = rec(Q, Q', O, E, R R', N) . eq rec(Q, Q', O, E, R, N) * E' = rec(Q, Q', O, E E', R, N ) .
Finally, the “next subquery identifier” counter is updated and extracted with operators
op _+_ : RecModule Nat -> RecModule . eq rec(Q, Q', O, E, R, N) + M = rec(Q, Q', O, E, R, N + M) . op #_ : RecModule -> Nat . eq # rec(Q, Q', O, E, R, N) = N .
COMPILE-QUERY — Common base module for compiling all sublanguagesThis module contains further functions common to the compilation of all the query sublanguages. First, we have helper functions to convert parts of quantifier patterns with a given marking to matching patterns on the metalevel to match against the database (various get functions were defined in the SYNTAX-BASE module):
ops m! m!? m!?0 mn : Term Pat -> Term . eq m!(T, P) = '_o_[T, upTerm(get!(P))] . eq m!?(T, P) = '_o_[T, upTerm(get!?(P))] . eq m!?0(T, P) = '_o_[T, upTerm(get!?0(P))] . eq mn(T, P) = '_o_[T, upTerm(getn(P))] .
The first argument of the above functions will usually be a metarepresentation of a variable of sort FactSet or FactSetN to match “the rest of the database”
Next, for all binding constructs (quantifiers in conditions and From_._ operator, which for the sake of brevity we refer here simply as “quantifiers”) we need a function which decides when quantifier evaluation must stop, i.e., when there is no more submultisets of facts in the database matchable against the given quantification pattern. Such function is used in a conditional equation (actually, the only case where we use conditional equations and rules). The “end testing” functions
for quantifiers with pattern P have signatures of the form
op endN : FactSet S1 S2 … Sn -> Bool .
and they are defined with equations of the form
eq endN(FS o f, V1, V2, …, Vn) = true . eq endN(FS, V1, V2, …, Vn) = false [owise] .
where f := get!?0(P), and V1, V2, …, Vn are variables bound by both the quantifier and the surrounding context.
Since endN() is called with actual values of those
of variables V1, V2, …, Vn which are bound by the context (and so fixed for the time of quantifier evaluation) the rule where endN() returns true guarantees that also corresponding variables in the matching pattern are properly bound.
Finally, FS is a variable of sort
FactSet. Thus, quantifier evaluation must stop when endN(FS, V1, V2, …, Vn)=false.
Since endN() has signature and definition specific to a given quantifying subquery it cannot be defined prior to the compilation
of the query, and must instead be added to the constructed metalevel system module constructed during the compilation process. The following code is devoted to that purpose:
First, we have the function which creates end function's name from integer:
op eName : Nat -> Qid .
eq eName(N) = qid("end" + string(N, 10)) .
Then, there is the helper which creates an ending condition:
op eCond : Term TermList Nat -> Condition . eq eCond(T, VV, N) = (eName(N)[T, VV] = $false) .
Finally, we have the function which adds relevant declarations and defining equations to the constructed module (observe that we also declare with declQOp() the relevant frame):
op declQ : Pat TermList RecModule -> RecModule .
ceq declQ(P, VV, RM) = RM * declQOp(VV, N) * (
eq eName(N)[m!?0($F, P), VV] = $true [none] .
eq eName(N)[$F, VV] = $false [owise] .
) * (
op eName(N) : 'FactSet sorts(VV) -> 'Bool [none] .
) if N := (# RM) .
Next, we have the declaration of the main compilation function (for queries only, not specifications) together with the helper which has as the additional argument first unused
subquery identifier. The remaining arguments are: the (sub)query to be compiled, a list of variables bound by the context, and initial RecModule:
op compRec : Query TermList RecModule -> RecModule . op compRec : Query TermList RecModule Nat -> RecModule . eq compRec(Q, VV, RM) = compRec(Q, VV, RM, (# RM)) .
For a common purpose just declaring a simple frame storing bindings of a given list of variables and advancing the subquery identifier counter we have the following helper operator:
op _^_ : RecModule TermList -> RecModule . eq RM ^ VV = RM * declOp(VV, (# RM)) + 1 .
The following function is used when compiling the quantifier constructs
(either Exists P . Q or From P . Q). It creates declarations
of appropriate frame constructors and ending functions (through _^_ and declQ()) and it calls recursively compRec() function with
the subquery under quantifier (Q) and list of variables extended with
the new variables occurring in the quantification pattern P
(with function ext()):
op compQ : Query Pat TermList RecModule -> RecModule . eq compQ(Q, P, VV, RM) = compRec(Q, ext(P, VV), declQ(P, VV, RM) ^ VV) .
Finally the following function is used when compiling binary operators (i.e., expressions
Q1 \/ Q2, Q1 => Q2 and Q1 |> Q2):
op comp2 : Query Query TermList RecModule -> RecModule . eq comp2(Q1, Q2, VV, RM) = compRec(Q1, VV, compRec(Q2, VV, RM ^ VV)) .
Observe that in addition to calling functions such as compQ, comp2(), etc., we need to add specific equations and rules to the constructed rewriting system which actually evaluate the query.
COMPILE-COND — Compiling conditions
To understand the code below it is necessary to recall definitions of the
functions from the COMPILE-BASE module.
The present module contains definitions of function compRec
for compiling conditions. We will proceed by cases corresponding to constructors
of conditions.
First, we have condition false:
eq compRec(False, VV, RM, N) = (RM ^ VV) * (eq @($(N, VV)) = @(@false) [none] .) .
Thus we declare a simple frame constructors corresponding to the given occurrence of False which stores the bindings of variables from the context and we also declare the equality which actually evaluates False. The equation, if moved to object level would read:
eq {C:Conf, S:Stack [V1, V2, …, Vn]N} = {C:Conf, S:Stack res(false)} .
Next, we evaluate the embedded booleans
ceq compRec({B}, VV, RM, N) = (RM ^ VV) * (
eq @($(N, VV)) = @('res[T]) [none] .
) if '`{_`}[T] := upTerm({B}) .
Thus, the equality which evaluates the occurrence (identified by N) of a term {B} is as follows:
eq {C:Conf, S:Stack [V1, V2, … Vn]} = {C:Conf, S:stack res(B)} .
Observe that since variables contained in B must occur among
V1, V2, … Vn, it follows that
the equality is well defined and moreover B will evaluate fully to either
true or false.
Next we evaluate the subcondition of the form Not C:
eq compRec(Not C, VV, RM, N) = compRec(C, VV, RM ^ VV) * (
eq @($(N, VV)) = @2('neg.Frame, $(s N, VV)) [none] .
eq @2('neg.Frame, 'res[$B]) = @('res['not_[$B]]) [none] .
) .
Thus, the above code creates both the simple frame with identifier N
corresponding to Not C as well as a simple frame with identifier N + 1 corresponding to C. It also adds two equalities, the first of which
replaces the frame corresponding to Not C with frame not
and frame corresponding to C. The second one negates the result of evaluating the
frame corresponding to C. When rewritten in the object level the equations
read:
eq {C:Conf, S:Stack [V1, V2, …, Vn]N} = {C:Conf, S:Stack neg [V1, V2, …, Vn]N+1} .
Next there comes evaluation of disjunction:
eq compRec(C \/ C', VV, RM, N) = comp2(C', C, VV, RM) * (
eq @($(N, VV)) = @2($(s N, VV), $(next(s N, C), VV)) [none] .
eq @2($(s N, VV), @false) = @($(s N, VV)) [none] .
eq @2($(s N, VV), @true) = @(@true) [none] .
) .
Note that, in the code above, comp2() call adds definitions of three
(simple) frames: frame with identifier N corresponding to the disjunction,
frame with identifier N + 1 corresponding to C, and
frame with identifier next(N + 1, C) corresponding to C'.
Thus, the three equations added by the above code read when descended to object level (as before, N, N+1, next(N+1, C) are to be understood symbolically, as part of frame's name, and not as actual Maude terms):
eq {C:Conf, S:Stack [V1, V2, …, Vn]N} = {C:Conf, S:Stack [V1, V2, …, Vn]N+1 [V1, V2, …, Vn]next(N+1, C)} .
eq {C:Conf, S:Stack [V1, V2, …, Vn]N+1 res(false)} = {C:Conf, S:Stack [V1, V2, …, Vn]N+1} .
eq {C:Conf, S:Stack [V1, V2, …, Vn]N+1 res(true)} = {C:Conf, S:Stack res(true)} .
Thus, the first equality replaces the frame corresponding to C \/ C'
with frames corresponding to C and to C' (with C'
on top). The next two equations implement short-circuted implementation of evaluation of disjunction: first C' is evaluated, if true then C
is not evaluated and the result of conjunction is true. Otherwise, C is evaluated.
eq compRec((Exists P . C), VV, RM, N) = compQ(C, P, VV, RM) * (
eq @c(cF, $(N, VV)) = @c(cF, $(N, VV, 'l[$F])) [none] .
eq @2($(N, VV, 'l[$F]), @false) = @($(N, VV, 'l[$F])) [none] .
eq @2($(N, VV, 'l[$F]), @true) = @(@true) [none] .
ceq @($(N, VV, 'l[$F])) = @(@false) if eCond($F, VV, N) [none] .
) * (
rl @($(N, VV, 'l[m!?($F, P)]))
=> @2($(N, VV, 'l[m!($F, P)]), $(s N, ext(P, VV))) [label('Quant)] .
) .
The code above defines two: simple and complex (with additional arguments) frames for subformula Exists P . C with identifier N
and a simple frame with identifier N + 1 for C. In addition it defines four equations and and a rewrite rule which on the object level read as follows:
eq {< F:FactSet | Fn:FactSetN | FN:FactSet >, S:Stack [V1, V2, …, Vn]N}
= {< F:FactSet | Fn:FactSetN | FN:FactSet >, S:Stack [V1, V2, …, Vn | l(F:FactSet)]N} .
eq {C:Conf, S:Stack [V1, V2, …, Vn | l(F:FactSet)]N res(false)}
= {C:Conf, S:Stack [V1, V2, …, Vn | l(F:FactSet)]N} .
eq {C:Conf, S:Stack [V1, V2, …, Vn | l(F:FactSet)]N res(true)} = {C:Conf, S:Stack res(true)} .
ceq {C:Conf, S:Stack [V1, V2, …, Vn | l(F:FactSet)]N}
= {C:Conf, S:Stack res(false)} if endN(F:FactSet, V1, V2, …, Vn) = false .
rl [Quant] : {C:Conf, S:Stack [V1, V2, …, Vn | l(F:FactSet o P!?)]}
=> {C:Conf, S:Stack [V1, V2, …, Vn | l(F:FactSet o P!)] [V1, V2, …, Vn, W1, W2, …, Wm]N + 1} .
where P!? is the multiset of facts formed by the parts of P
marked by [_]! and [_]? and W1, …, Wm are variables of P not among V1, …, Vm.
COMPILE-DQUERY — Compiling DML queries
Here we describe definition of compRec() on DML queries. We consider each DML query in turn. First we have the code compiling Ok:
eq compRec(Ok, VV, RM, N) = (RM ^ VV) * (eq @($(N, VV)) = @(@true) [none] .) .
Thus, we add definition of a simple frame and the equation which on the object level reads
(Ok always succeeds):
eq {C:Conf, S:Stack [V1, V2, …, Vn]N} = {C:Conf, S:Stack res(true)} .
Next, we have code compiling fact occurrence:
eq compRec(f, VV, RM, N) = (RM ^ VV) * (
eq @c(cF, $(N, VV)) = @c(c($F, $Fn, '_o_[$FN, upTerm(f)]), @true) [none] .
) .
The fact is simply added to the multiset of new facts inside the Conf
term and the succeeds (by adding res(true) at the top of stack) as expressed by the equation added by the above code, which on the object level reads:
eq {< F | Fn | FN >, S:Stack [V1, V2, …, Vn]N} = {< F | Fn | FN o f >, S:Stack res(true)} .
Next, we have conditional. Using comp2() we create three frames: for the
conditional C => D (identifier N), the condition C
(identifier next(s N, D)), and conditionally executed
subquery D (identifier N + 1). We also add three equations:
eq compRec(C => D, VV, RM, N) = comp2(C, D, VV, RM) * (
eq @($(N, VV)) = @2($(s N, VV), $(next(s N, D), VV)) [none] .
eq @2($(s N, VV), @false) = @(@false) [none] .
eq @2($(s N, VV), @true) = @($(s N, VV)) [none] .
) .
The equations read as follows when translated into object level:
eq {C:Conf, S:Stack [V1, V2, …, Vn]N}
= {C:Conf, S:Stack [V1, V2, …, Vn]N + 1 [V1, V2, …, Vn]next(s N, D)} .
eq {C:Conf, S:Stack [V1, V2, …, Vn]N + 1 res(false)} = {C:Conf, S:Stack res(false)} .
eq {C:Conf, S:Stack [V1, V2, …, Vn]N + 1 res(true)} = {C:Conf, S:Stack [V1, V2, …, Vn]N + 1} .
Thus, we first evaluate the condition (placed on top of the stack).
If it evaluates as true, we evaluate the DML query. Otherwise we fail.
Next we deal with terms of the form D |> D'
which must be executed one after the other:
eq compRec(D |> D', VV, RM, N) = comp2(D, D', VV, RM) * (
eq @($(N, VV)) = @2($(s N, VV), $(next(s N, D'), VV)) [none] .
eq @2($(s N, VV), @B) = @2(@B, $(s N, VV)) [none] .
) .
Thus, we create frames for D |> D' (with identifier N),
for D' (with identifier N+1) and for
D (with identifier next(s N, D')).
We also add two equations which when translated to object level read:
eq {C:Conf, S:Stack [V1, V2, …, Vn]N}
= {C:Conf, S:Stack [V1, V2, …, Vn]N + 1 [V1, V2, …, Vn]next(s N, D')} .
eq {C:Conf, S:Stack [V1, V2, …, Vn]N + 1 res(B:Bool)} = {C:Conf, S:Stack res(B:Bool) [V1, V2, …, Vn]N + 1} .
Observe that after the frame corresponding to D' will be evaluated, we will
be left with two res() terms on the top of the stack (call them res(B) and res(B')). Then, another equation will cause those two frames to be replaced by res(B or B2).
Finally, we have the code compiling subqueries of the form From P . D:
eq compRec(From P . D, VV, RM, N) = compQ(D, P, VV, RM) * (
eq @c(cF, $(N, VV)) = @c(cF, $(N, VV, 'l[$F, $false])) [none] .
eq @c2(cF, $(N, VV, 'l[$F', $B, $Ft]), @false)
= @c(c('_o_[$F, $Ft], $Fn, $FN), $(N, VV, 'l['_o_[$F', $Ft], $B])) [none] .
eq @c2(cF, $(N, VV, 'l[$F', $B, $Ft]), @true) = @c(cF, $(N, VV, 'l[$F', $true])) [none] .
ceq @($(N, VV, 'l[$F', $B])) = @(@B) if eCond($F', VV, N) [none] .
) * (
rl @c(c(m!?0($F, P), mn($Fn, P), $FN), $(N, VV, 'l[m!?0($F', P), $B]))
=> @c2(c(m!?($F, P), '_o_[$Fn, 'refresh[upTerm(getn(P))]], $FN),
$(N, VV, 'l[m!($F', P), $B, upTerm(get0(P))]), $(s N, ext(P, VV))) [label('From)] .
) .
In order to understand what the above code does, first observe that frames
corresponding to From P . D have identifier N and the frame
corresponding to D has identifier N + 1. Then, observe that
equations and rules added by the above code read when moved to object level as:
eq {< F:FactSet | Fn:FactSetN | FN:FactSet >, S:Stack [V1, V2, …, Vn]N}
= {< F:FactSet | Fn:FactSetN | FN:FactSet >, S:Stack [V1, V2, …, Vn | l(F:FactSet, false)]N} .
eq {< F:FactSet | Fn:FactSetN | FN:FactSet >, S:Stack [V1, V2, …, Vn | l(F':FactSet, B:Bool, Ft:FactSet)]N res(false)}
= {< F:FactSet o Ft:FactSet | Fn:FactSetN | FN:FactSet >, S:Stack [V1, V2, …, Vn | l(F':FactSet o Ft:FactSet, B:Bool)]N} .
eq {C:Conf, S:Stack [V1, V2, …, Vn | l(F:FactSet, B:Bool, Ft:FactSet)]N res(true)}
= {C:Conf, S:Stack [V1, V2, …, Vn | l(F:FactSet, true)]N} .
ceq {C:Conf, S:Stack [V1, V2, …, Vn | l(F:FactSet, B:Bool)]N}
= {C:Conf, S:Stack res(B:Bool)} if endN(F:FactSet, V1, V2, …, Vn) = false .
rl [From] : {< P!?0 o F:FactSet | Fn o Pn | FN >, S:Stack [V1, V2, …, Vn | l(P!?0 o F':FactSet, B:Bool)]N}
=> {< P!? o F:FactSet | Fn o refresh(Pn) | FN >, S:Stack [V1, V2, …, Vn | l(P! o F':FactSet, B:Bool, P!)]N [V1, …, Vn, W1, … Wm]N+1} .
where P!?, Pn, etc. denotes the respectively marked part of P, and W1, …, Wm
are the variables in P not in V1, …, Vn.
COMPILE-SPEC — Compiling specificationsHere we describe functions which are used to compile specifications. The entrypoint of compilation is the following function:
op compile : QSpec Qid Qid -> SModule .
The first argument is the specification, the second the name of the module created as the result of compilation, finally, the third is the name of the module included in the compiled module. The compile() function is defined in terms of two helper functions:
op compRSpec : QSpec RecModule -> RecModule . op compRSeq : DQSeq RecModule -> RecModule . eq compile(QS, Q, Q') = toModule(compRSpec(QS, initRec(Q, Q'))) .
Functions compRSpec() and compRSeq recurse through
the structure of the specification. First, let us consider definition of compRSpec which compiles terms of sort QSpec:
eq compRSpec(EmptySpec, RM) = RM .
ceq compRSpec(case(Q, DQS) | QS, RM) = compRSpec(QS, compRSeq(DQS, RM * declSOp(# RM) * (
rl 'new[$F, $Fn, $true] => %2(cI, s(N, $false), $(N, empty)) [label(Q)] .
))) if N := (# RM) .
Recall that declSOp(N) adds declaration of the frame of the form
op sN : Bool -> Frame .
The boolean argument stores the result of execution of a given case. The rule added in the definition of compRSpec() when translated to object level reads as follows:
rl new(F:FactSet, Fn:FactSetN, true) => {< F:FactSet | Fn:FactSetN | noneF >, sN(false) []N} .
Note that only successful execution of a previous case (marked by boolean true in the argument of new() state) get to be rewritten further. The justification is that when searching for reachable states we want to avoid superfulous executions of useles (i.e., doing nothing) transitions, and we cut executions with such transitions early. Note that this also makes this system unsuitable for simple simulations with rewrite command since such execution is likely to stack quickly with unsuccessful transition. After execution of a rule we end with a state with an empty multiset of new facts and two frames on the stack: one, constructed with s(false) which corresponds to the current case and the other, a simple frame with empty set of variable bindings which corresponds to the first DML query in sequence inside the case.
Now we are ready do describe compilation of the sequence of DML queries. First we have the code which deals with empty sequence of DML queries which is the last recursive call of compRSeq(), and hence this code must deal with ending of the case execution:
ceq compRSeq(Empty, RM) = (RM + 1) * declOp(empty, # RM) * (
eq %2(cI, s(N, $B), $(N, empty)) = 'new[$F, $Fn, $B] [none] .
) if N := (# RM) .
There are two things to wonder about in the above code. The first is that it declares an empty simple frame (with declareOp) which is not really used. This is because this frame would be the initial frame for the computation of the next DML query, and previous recursive call assumes its existence. Secondly, the frame constructed with sN() is replaced after each DML query execution in sequence. Thus, N here is usually larger than at the beginning of the execution of the case. It will become clear after showing the rest of the code. The equality introduced above reads (after moving it to the object level):
eq {< F:FactSet | Fn:FactSetN | noneF >, sN(B:Bool) []N} = new(F:FactSet, Fn:FactSetN, B:Bool) .
Next we deal with a DML query in the sequence:
ceq compRSeq((D ; DQS), RM) = compRSeq(DQS, compRec(D, empty, RM * declSOp(N') * (
eq %2(cF, s(N, $B1), 'res[$B2]) = %2(cN, s(N', '_or_[$B1, $B2]), $(N', empty)) [none] .
))) if N := (# RM) /\ N' := next(N, D) .
Note that we declare here the next “s” - frame in the sequence (with declSOp()). The equation introduced here reads in the object level as follows:
eq {< F:FactSet | Fn:FactSetN | FN:FactSet >, sN(B1:Bool) res(B2:Bool)}
= {< F:FactSet o FN:FactSet | Fn:FactSetN | noneF >, snext(N, D)(B1:Bool or B2:Bool) []next(N, D)} .
The left-hand side corresponds to what the state looks like after the DML query is evaluated with the result of evaluation on top of the stack. Thus, for the case to succeed, we need at least one of the DML queries in the sequence to succeed.
Example specification (restaurant booking example from the paper) is contained in the file Bookings.maude. In order to run the example run Maude with a command
maude Bookings.maude
(the file also inputs QuerySemantics). Then, e.g., in order to check
if the state in which there exists a closed offer (and accepted associated booking) reachable in seven or
less business steps from the database
with no bookings and offers run the following command
(in Maude prompt):
red searchFinalized(7) .
We will now describle each module in Bookings.maude.
BOOKINGS-SYNTAXIn this module we define a syntactic part of the specification. More precisely, we define fact constructors and constants to describe the state of booking (including the token #):
sorts OState BState Rest Person Offer Book Url . op rest : Rest -> Fact . ops agent cust : Person -> Fact . op offer : Offer OState Rest Person -> Fact . op book : Book BState Offer Person -> Fact . op host : Book Person -> Fact . op prop : Book Url -> Fact . ops onHold available closed beingBooked : -> OState . ops drafting submitted canceled finalized accepted toBeValidated : -> BState . op # : Nat -> Fact .
We also define fresh facts and fresh object constructors:
op C : Offer -> FactN .
op C : Book -> FactN .
op C : Url -> FactN .
op C : Person -> FactN .
op {_}Offer : Nat -> Offer .
op {_}Book : Nat -> Book .
op {_}Url : Nat -> Url .
op {_}Person : Nat -> Person .
as well as the related cases of succ(_) function definition
(the function updates the fresh facts):
eq succ(C({N:Nat}Offer)) = C({s N:Nat}Offer) .
eq succ(C({N:Nat}Book)) = C({s N:Nat}Book) .
eq succ(C({N:Nat}Url)) = C({s N:Nat}Url) .
eq succ(C({N:Nat}Person)) = C({s N:Nat}Person) .
Finally, we define some constants to be used later in the specification of the business process:
*** restaurants ops r1 r2 r3 r4 : -> Rest . *** agents, customers and hosts ops a1 a2 a3 c1 c2 c3 c4 h1 h2 h3 h4 : -> Person . *** offers and bookings op o : -> Offer . op b : -> Book . op u : -> Url .
BOOKINGS-SPECThe module BOOKINGS-SPEC contains the actual definition of the business process. It
is also the module which is included in the generated module during compilation of the specification, so
it is important that it includes the REWRITE-BASE module.
We want to define a constant which reduces to a specification (for a future reference). The problem is
that the specification uses actual Maude variables, and in equations the set of variables on the right hand
side must be contained in the variables on the left hand side. To solve this problem we define a set of
constants which reduce to downTerm applied to metarepresentation of a variable. This is an ugly
hack but it works:
ops O1 O2 O3 : -> Offer .
ops B1 B2 B3 : -> Book .
ops A1 A2 A3 C1 C2 H1 H2 : -> Person .
ops R1 R2 : -> Rest .
ops U1 U2 : -> Url .
op N : -> Nat .
eq N = downTerm('N:Nat, 0) .
eq O1 = downTerm('O1:Offer, o) .
eq O2 = downTerm('O2:Offer, o) .
eq O3 = downTerm('O3:Offer, o) .
eq B1 = downTerm('B1:Book, b) .
eq B2 = downTerm('B2:Book, b) .
eq B3 = downTerm('B3:Book, b) .
eq A1 = downTerm('A1:Person, a1) .
eq A2 = downTerm('A2:Person, a1) .
eq A3 = downTerm('A3:Person, a1) .
eq C1 = downTerm('C1:Person, a1) .
eq C2 = downTerm('C2:Person, a1) .
eq H1 = downTerm('H1:Person, a1) .
eq H2 = downTerm('H2:Person, a1) .
eq R1 = downTerm('R1:Rest, r1) .
eq R2 = downTerm('R2:Rest, r1) .
eq U1 = downTerm('U1:Url, u) .
eq U2 = downTerm('U2:Url, u) .
Finally, we define a constant bookingSpec which stores the specification of the
business process:
op bookingSpec : -> QSpec .
eq bookingSpec
= case('newOffer,
From [#(s N)]0 o [C(O1)]n o [agent(A1)]? o [rest(R1)]! . (
(Forall [offer(O2, beingBooked, R2, A1)]? . False)
=> offer(O1, available, R1, A1)
|> (
From [offer(O3, available, R2, A1)]0 . offer(O3, onHold, R2, A1)
) |> #(N)
)
)
| case('resume,
From [#(s N) o offer(O1, onHold, R1, A1)]0 o [agent(A2)]? . (
(Forall [offer(O2, beingBooked, R2, A2)]? . False)
=> (
offer(O1, available, R1, A2)
|> (
From [offer(O2, available, R2, A2)]0 . offer(O2, onHold, R2, A2)
) |> #(N)
)
)
)
| case('newBooking,
From [#(s N) o offer(O1, available, R1, A1)]0 o [C(B1)]n o [cust(C1)]! . (
offer(O1, beingBooked, R1, A1)
|> book(B1, drafting, O1, C1)
|> #(N)
)
)
| case('closeOffer,
From [#(s N) o offer(O1, available, R1, A1)]0 . (
offer(O1, closed, R1, A1)
|> #(N)
)
)
| case('addHost0,
From [#(s N)]0 o [C(H1)]n o [book(B1, drafting, O1, C1)]! . (
host(B1, H1)
|> #(N)
)
)
| case('addHost1,
From [#(s N)]0 o [book(B1, drafting, O1, C1)]! o [host(B1 , H1)]? . (
(Forall [host(B1, H1)]? . False) => (
host(B1, H1)
|> #(N)
)
)
)
| case('submit,
From [#(s N) o book(B1, drafting, O1, C1)]0 . (
book(B1, submitted, O1, C1)
|> #(N)
)
)
| case('determineProposal,
From [#(s N) o book(B1, submitted, O1, C1)]0 o [C(U1)]n . (
prop(B1,U1)
|> book(B1,finalized,O1,C1)
|> (From [host(B1, H1)]0 . Ok)
|> #(N)
)
)
| case('reject,
From [#(s N) o book(B1, submitted, O1, C1) o offer(O1, beingBooked, R1, A1)]0 . (
book(B1, canceled, O1, C1)
|> offer(O1, available, R1, A1)
|> (From [host(B1, H1)]0 . Ok)
|> #(N)
)
)
| case('cancel,
From [#(s N) o book(B1, finalized, O1, C1) o offer(O1, beingBooked, R1, A1)]0 . (
book(B1, canceled, O1, C1)
|> offer(O1, available, R1, A1)
|> #(N)
)
)
| case('accept1,
From [#(s N) o book(B1, finalized, O1, C1) o offer(O1, beingBooked, R1, A1)]0 o [cust(C1)]? . (
(
Exists [
offer(O2, closed, R1, A2) o book(B2, accepted, O2, C1)
o offer(O3, closed, R1, A3) o book(B3, accepted, O3, C1)
]? . True
) => (
book(B1, accepted, O1, C1)
|> offer(O1, closed, R1, A1)
|> #(N)
)
)
)
| case('accept2,
From [#(s N) o book(B1, finalized, O1, C1)]0 o [offer(O1, beingBooked, R1, A1)]? . (
Not (
Exists [
offer(O2, closed, R1, A2) o book(B2, accepted, O2, C1)
o offer(O3, closed, R1, A3) o book(B3, accepted, O3, C1)
]? . True
) => (
book(B1, toBeValidated, O1, C1)
|> #(N)
)
)
)
| case('reject2,
From [#(s N) o book(B1, toBeValidated, O1, C1) o offer(O1, beingBooked, R1, A1)]0 . (
book(B1, canceled, O1, C1)
|> offer(O1, available, R1, A1)
|> #(N)
)
)
| case('confirm,
From [#(s N) o book(B1, toBeValidated, O1, C1) o offer(O1, beingBooked, R1, A1)]0 . (
book(B1, accepted, O1, C1)
|> offer(O1, closed, R1, A1)
|> #(N)
)
) .
EXPERIMENTSThe last module, EXPERIMENTS defines (as a convinience) checking if a state
where an offer is closed and a corresponding booking is accepted is reachable from a state with no offers
and bookings and a few predefined agents, restaurants, and customers.
First, we compile a specification (BSPEC is the name of compiled module):
op compSpec : -> SModule . eq compSpec = compile(bookingSpec, 'BSPEC, 'BOOKINGS-SPEC) .
The module defines 196 operators, 285 equations, and 83 rules.
First, we define an initial database, an initial multiset of fresh facts, and an initial state build from them:
op initDB : Nat -> FactSet .
op initDBN : -> FactSetN .
op initState : Nat -> State .
eq initDB(N:Nat) = agent(a1) o agent(a2) o cust(c1) o cust(c2) o rest(r1) o rest(r2) o #(N:Nat) .
eq initDBN = C({0}Offer) o C({0}Book) o C({0}Url) o C({0}Person) .
eq initState(N:Nat) = new(initDB(N:Nat), initDBN, true) .
The initial database (initDB) and state (initState) are parametrized with
an initial value of a token. Each business step consumes the token and decreases its parameter by 1. Thus
this parameter of initDB limits the depth of search measured in business steps.
Now we define a main operator in this module which performs the actual search:
op searchFinalized : Nat ~> ResultTriple? .
eq searchFinalized(N:Nat) = metaSearch(
compSpec,
upTerm(initState(N:Nat)),
upTerm(new(FS o offer(O1, closed, R1, A1) o book(B1, accepted, O1, C1), FSN, true)),
nil, '+, unbounded, 0
) .
Above O1, R1, A1, B1, C1 (imported from module BOOKINGS-SPEC)
and FS, FSN defined locally as
op FS : -> FactSet .
op FSN : -> FactSetN .
eq FS = downTerm('FS:FactSet, noneF) .
eq FSN = downTerm('FSN:FactSetN, noneFN) .
are variables defined as operators with metalevel operators (see the description of the previous module).
Reducing searchFinalized(7) yields the answer:
reduce in EXPERIMENTS : searchFinalized(7) .
rewrites: 525165 in 2528ms cpu (2535ms real) (207660 rewrites/second)
result ResultTriple: {'new['_o_['rest['r1.Rest],'rest['r2.Rest],'agent['a1.Person],'agent['a2.Person],'cust['c1.Person],'cust[
'c2.Person],'#['s_['0.Zero]],'prop['`{_`}Book['0.Zero],'`{_`}Url['0.Zero]],'offer['`{_`}Offer['0.Zero],'closed.OState,'r1.Rest,
'a1.Person],'book['`{_`}Book['0.Zero],'accepted.BState,'`{_`}Offer['0.Zero],'c1.Person]],'_o_['C['`{_`}Offer['s_['0.Zero]]],'C[
'`{_`}Book['s_['0.Zero]]],'C['`{_`}Url['s_['0.Zero]]],'C['`{_`}Person['0.Zero]]],'true.Bool],'State,
'A1:Person <- 'a1.Person ;
'B1:Book <- '`{_`}Book['0.Zero] ;
'C1:Person <- 'c1.Person ;
'FS:FactSet <- '_o_['rest['r1.Rest],'rest['r2.Rest],'agent['a1.Person],'agent['a2.Person],'cust['c1.Person],'cust['c2.Person],
'#['s_['0.Zero]],'prop['`{_`}Book['0.Zero],'`{_`}Url['0.Zero]]] ;
'FSN:FactSetN <- '_o_['C['`{_`}Offer['s_['0.Zero]]],'C['`{_`}Book['s_['0.Zero]]],'C['`{_`}Url['s_['0.Zero]]],'C['`{_`}Person[
'0.Zero]]] ;
'O1:Offer <- '`{_`}Offer['0.Zero] ;
'R1:Rest <- 'r1.Rest}