Maude Query Language is a implementation in a rewriting system Maude of a multiset query and DML language based on term matching, together with a simple simulation framework. Its intended application of this software is specification of data-centric business processes and their analysis through simulation and reachability analysis. The available files contain, apart from the core language implementation, a simple probabilistic simulation framework together with examples of its use.
mql/ folder). Change directory to mql/.
Run Maude interpreter from mql/. Inside Maude interpreter execute
in file.maudewhere
file.maude
is the file you want to load. Use the loaded modules. Each file in the source loads its dependencies. See below for the description of
contents of each of the available files.
Click on the corresponding header to view a source file:
FACT-SET defines general
sorts and constructors for multisets of facts as well as basic operators and
predicates (difference, inclusion and "element of").
Multisets of facts have sorts FactSet, and non-empty ones have sort
NeFactSet. Single facts (which are also multisets of facts) have sort
Fact. Constructors for facts are particular to each example and are not
defined here. Multisets of facts are constructed from facts using associative and
commutative union operator _o_ : FactSet FactSet ⟶ FactSet
which has an empty multiset of facts (constructed with empty : ⟶ FactSet)
as unit.
The module defines also the operator
unique : FactSet ⟶ FactSetwhich returns the multiset passed as argument with duplicate elements removed.
COND-SYNTAX defines the syntax of conditions (of sort
Cond). More precisely, True and False are conditions,B : Bool then {B} : Cond, C and C' are of sort Cond
then C and C', C or C', C implies C',
and not C are of sort Cond,FS : NeFactSet and C : Cond then
forall FS . C and exists FS . C
are of sort Cond,FS : NeFactSet then < FS > is
of sort Cond. Here < FS >
is equivalent to exists FS . True (though it is independently implemented).COND-SYNTAX defines function
closed? : Cond ⟶ Bool such that closed?(C) iff
condition C is closed.
EVAL-COND defines function
eval : FactSet Module Cond ⟶ [Bool]which provides semantics of conditions (
eval(FS, M, C) reduces to true iff C is closed and
FS ⊧ C in module M.
DML-SYNTAX{X :: RESULT} defines syntax of DML expressions
(of sort Dml{X}).
More precisely,
X$Result is a subsort of Dml{X}, i.e., any term of
sort X$Result is a DML expression (which evaluates to itself)D : Dml{X} and D' : Dml{X} then D & D'
is also a DML expression of sort Dml{X}. D & D'
evaluates to the union of results of D and D'.C : Cond and D : Dml{X} then
if C => D is a DML expression (which evaluates to the empty result
if C is not satisfied, and to whatever D evaluates to otherwise).FS : NeFactSet and D : Dml{X} then from FS : D
is a DML expression (for each matching of FS with the current database return
the respective evaluation of instantiation of D).DML-SYNTAX{X :: RESULT} defines function
closed? : Dml{X} ⟶ Bool such that closed?(D) iff
DML expression D is closed. The parameter of DML-SYNTAX{X :: RESULT}
is a theory which defines sort Result of objects DML expressions evaluate to
as well as operators
empty : ⟶ Result, _o_ : Result Result ⟶ Resultwhich correspond, respectively, to the empty result and composition (union) of results. Operator
_o_ is defined to be associative and commutative.
The theory has two instantiations (views from modules implementing it),
defined also in Query.maude:
FactSet and Addl. FactSet identifies sort Result
with FactSet, and operators _o_ and empty in theory with
the respective multiset constructors. Terms of sort Dml{FactSet} can be viewed as
queries. Addl identifies sort Result with the sort Addl.
Elements of the sort Addl are pairs of the form addl(ADD,DEL), where
ADD and DEL are multisets of facts (those to be added to and to be deleted
from the current database, respectively). Operators _o_ and empty
are implemented by componentwise application of respective constructors of multisets of facts.
EVAL-DML{X :: RESULT} defines function
eval : FactSet Module Dml{X} ⟶ X$Result
which provides semantics of DML expressions (if D is a closed DML expression then eval(FS, M, D)
reduces to the result of evaluation of D against multiset of facts FS in the context of module M).
REQUISITION-AND-PROCUREMENT contains definition of the data model
and two guards,TEST-REQUISITION-AND-PROCUREMENT contains definition of two example
multisets of facts against which the guards can be evaluated, as well as constants which reduce
to evaluations of instances of guards agains those two multisets. Thus, one can e.g., try Maude command
red in TEST-REQUISITION-AND-PROCUREMENT : test1 .
FRESH{X :: TRIV} which defines,
for the sort X$Elt, a subsort Fresh{X} marking a fresh value.
It also defines constructor for fresh values of sort Fresh{X}. Those fresh values are
constructed from natural numbers and the execution system should maintain the value of the
smallest natural not yet used to produce some fresh value. The second argument of this constructor is
a dummy of the same kind as the constructed fresh value. It provides the necessary hint to the Maude
interpreter, so that sorts and kinds of terms using fresh values can be correctly inferred.SAMPLE{X :: TRIV} defines function
sample : List{X} Nat Nat ⟶ Sample{X}
such that sample(L, K, N), where N is the first unused position in the sequence of random
numbers, reduces to a pair [L', N'], where L' is a K-element sample of a list L and N' is the revised first
unused position in the sequence of random numbers.
SAMPLE-FRESH{X :: TRIV} defines function
sampleFresh : List{X} Nat [X$Elt] Nat Nat ⟶ SampleFresh{X}.
Let N be the first unused position in the sequence of random numbers, and let M be the smallest natural number
not yet used to construct fresh value. Let Y be a dummy of sort X$Elt.
Then sample(L, K, Y, N, M), reduces to a triple [L', N', M'],
where
SET-TO-LIST{X :: TRIV} which defines the function
toList : Set{X} ⟶ List{X}
converting (non-deterministically!) a set into a list.TEST-SAMPLE defines tests for sampling values from a listTEST-FRESH defines tests for sampling values from a list with
the possibility of including fresh values (of sort Nominal
defined in the module TEST-NOMINAL).APPLY-ACTION-BASE defines an abstract framework for specifying the outcome of an action on a multiset of facts. Formally, actions (with labels of sort Action) are specified
by defining functions
def : Action ⟶ Dml{Addl},
pre : Action ⟶ Cond.
These functions assign to each action label, respectively, a DML expression,
and a condition. DML expressions of sort Dml{Addl} when evaluated return a pair
(of sort Addl) of multisets of facts, interpreted, respectively, as "facts to be added",
and "facts to be deleted".
Module
APPLY-ACTION-BASE does not define any constructors for the Action sort, and it
provides only signature but not definition of pre and def. Thus, both pre and def must be defined in the separate module which defines the actions.
APPLY-ACTION{X :: MINUS-PLUS} defines the function
exec : FactSet FactSet Action Module ⟶ FactSetwhich specifies the actual outcome of executing a given action. The theory
MINUS-PLUS defines a function
mp : FactSet FactSet FactSet ⟶ FactSetThere are two instances (views from the theory) of
MINUS-PLUS:
Mp-Multi and Mp-Unique. In the case of Mp-Multi,
mp(FS, DEL, ADD) evaluates to (FS - DEL) o ADD.
In the case of Mp-Unique, mp(FS, DEL, ADD) evaluates to
unique((unique(FS) - DEL) o ADD). In this case, even if FS,
DEL and ADD are multisets,
mp(FS, DEL, ADD) is duplicate-free. The occurence of the unique
operator directly applied to FS ensures that any fact in DEL
is removed from FS regardles of its multiplicity in FS and DEL
(remember that _-_ used here is a multiset difference).
Let M
be (the metarepresentation of) a module, let Ac be an action, and, finally,
let FS and IN be multisets of facts (representing, respectively, a current database
an argument to Ac).
Furthermore,
assume that FS ○ IN ⊧ pre(Ac) in M
(i.e., that the precondition of Ac is satisfied in FS ○ IN). Then the
term exec(FS, IN, Ac, M) reduces to the multiset mp(FS, DEL, ADD), where
addl(ADD, DEL) is the result of evaluating def(Ac) against
FS ○ IN. Thus, instanciating APPLY-ACTION with
Mp-Multi implies using multiset semantics, while
instanciating APPLY-ACTION with Mp-Unique implies that executing a DML-expression
has set semantics
(at least to some extent).
MINUS-PLUS
theory are instantiated only with Mp-Multi view.
SIMULATION-FRAMEWORK{X :: MINUS-PLUS} defines an abstract skeleton of a simulation framework. The parameter theory is used only to include
the correlated instantiation of APPLY-ACTION{X :: MINUS-PLUS} module.
Each simulation step updates not only a state of the system in the form of a multiset of
facts but also a simulation context (of sort SimulContext) which stores
all the auxialliary data necessery to perform simulation,
e.g., the last used position in the random number sequence, the last used fresh values, etc.
Each simulation step consists of (1) choosing an action, (2) choosing an input for this action, and
(3) executing the chosen action for a chosen input against a current database defining the state of the system. The last step is implemented with the function exec defined in the module APPLY-ACTION{X}. The first two steps are abstracted with functions
getNextAction : SimulContext ⟶ PairA, inp : Action SimulContext FactSet ⟶ Pair,where the last argument of inp is the current database (inputs of an action may depend on the current state of the system) and
PairA and Pair are sorts of pairs constructed with
[_,_] : FactSet SimulContext ⟶ Pair, [_,_] : Action SimulContext ⟶ PairA .Function
getNextAction returns a chosen action and a revised SimulContext, and
inp returns an input for the action given as a first argument, as well as revised SimulContext.
Module SIMULATION-FRAMEWORK{X :: MINUS-PLUS} defines only signatures of getNextAction and inp. Any instantiation
of this simulation framework must define those two functions as well as constructors of simulation context.
NEXT-STEP{X :: MINUS-PLUS} defines a single rewrite rule which starts the next simulation step and which complements the skeleton of a simulation framework defined in the module SIMULATION-FRAMEWORK{X :: MINUS-PLUS}. It was placed in the separate system module because the rest of the
simulation framework was purely equational (without rewrite rules). Note, however, that
functions getNextAction and inp may be defined either equationally
(as in SimExBooking.maude) or
with rewrite rules
(as in SimExBookingNP.maude) in a
instantiation of the simulation framework skeleton. BOOKING-FACTS defines sorts corresponding to entities appearing in the example, constructors of facts, and constants denoting
states of bookings and offers.BOOKING-VARS contains definitions of constants reducing to variables to be used
in the next module as logical variables inside condition or DML query terms. Each
such constant (of sort, say, S) is defined with the code of the form
op X : -> S . eq X = downTerm('X:S, a) .
where a is some constant of kind [S]. Such a constant X
reduces to X:S. The reason for using this convoluted construction is as follows:
We want to be able to use Maude's equations of the form
"op A = D ." where A is a constant, and D is a DML expression or condition. Unfortunately DML expressions and conditions are (usually) represented by non-ground terms, which means that such an equality would not compile (since variables of the right-hand side must include all the variables of the left-hand side). Amazingly, equations with constants on the right hand side which reduce to variables not occurring on the left hand side are accepted by Maude interpreter. Admittedly, this is an ugly hack, but it works, and working with non-ground terms outside rules and equations is ugly anyway since most operators work in an unexpected way with variables. E.g., X:S == Y:S reduces immediately to false whereas a programmer probably expected such an equality not to reduce at all
(since from the point of view of logic it is neither true nor false).
BOOKING-EXAMPLE defines all the actions and their preconditions used in the specification of "Restaurant Booking Application".SIMULATION-FRAMEWORK)
for the restaurant booking application. The two implementations differ in the method for picking the
next action and input facts. The present application uses probabilistic methods which yield
a linear simulation where at each step the next action and input for this action is sampled with functions from the
Sampling.maude. The
other implementation uses rewriting rules which allow exploration of the full range of possibilities. In both cases (probabilistic and non-probabilistic) there are actually two separate sub-implementations for comparison&emdash;one which
chooses input for the next action in a more targeted way (so that most of the precondition is satisfied and in most cases the chosen action actually executes) and the other one which chooses the next input more randomly. In the first case we get quicker progress, but at the price of not checking how our specification behaves with incorrect data. Returning to the probabilistic implementations, we have the following modules:
SIMULATION-CONTEXT
defines simulation context for the restaurant booking application, some helper functions
(such as the ones which extract from the database the lists of agents, bookings, and so on to be used when sampling the intput database for the next action) and function getNextAction
(see module SIMULATION-FRAMEWORK)
which chooses the next action by sampling a single action from the list of all actions defined for the restaurant booking application. The simulation context constructed with
[_,_|_] : Nat Nat List{Action} ⟶ SimulContext
stores, respectively, a first unused position in the sequence of natural numbers, first unused position in the sequence of fresh values, and a list of all considered actions. The module SIMULATION-CONTEXT
defines also a utility operator for constructing initial simulation contexts:
initContext : Nat ⟶ SimulContext.The sole argument is the initial position in the sequence of random numbers. Then
initContext(N) reduces to [N, 0 | actList], where
actList is the a list of all actions (without repetition) defined
in the BOOKING-EXAMPLE module
INP-DEF-TARGETED and INP-DEF-BLIND contain alternative definitions of function inp (see description of the module
SIMULATION-FRAMEWORK)
which, based on action label, the current simulation context and the current database returns input database for the given action execution.
Here arguments of input facts are either fresh or they are sampled from the values (of correct sort and meaning) in the current database using the functions defined in the
module SIMULATION-CONTEXT.
The difference between the two implementations is as follows:
inp defined in INP-DEF-TARGETED returns such input multisets of facts for a given action that most (if not all) of the action's precondition is satisfied.
E.g., for resume action it picks an an existing offer from those in the
onHold state (where only offers on hold can be resumed).inp defined in INP-DEF-BLIND draws input facts in a more "random" way, e.g., an offer for the resume action is drawn from
all offers, not just those in the onHold state.SIMULATION-FRAMEWORK)
for the restaurant booking application. Unlike
SimExBooking.maude
it does so without using probabilistic methods, instead relying purely on non-deterministic
(and non-confluent) rewriting. We have the following modules:
SIMULATION-CONTEXT-NONPROB defines simulation context
for the restaurant booking application and function getNextAction
(see module SIMULATION-FRAMEWORK)
which chooses the next action. Function getNextAction is defined through a rewrite rule which allows it to return any action non-deterministically chosen from the set of all actions (in the
restaurant booking application).
The simulation context constructed with
[_|_] : Nat List{Action} ⟶ SimulContext
stores, respectively, a first unused position in the sequence of fresh values and a list of all considered actions. The module defines also an auxilliary constructor used in the definition of one of the actions which requires multiple rewrites and storing partial results. Finally, the module defines
a utility operator for constructing initial simulation contexts:
initContext : ⟶ SimulContext.Here
initContext reduces to [0 | actSet], where
actSet is the set of all actions (without repetition).
INP-DEF-TARGETED-NONPROB and INP-DEF-BLIND-NONPROB contain alternative definitions of function inp (see description of the module
SIMULATION-FRAMEWORK)
expressed with rewrite rules (which provide non-determinism necessary for the
exploration of state space) instead of equations where a semblance of non-determinism
is provided by the use of pseudorandom functions as in the case of SimExBooking.maude. Again, the two
alternative modules correspond to a more (INP-DEF-TARGETED-NONPROB)
and less (INP-DEF-BLIND-NONPROB) targeted approaches to the generation of the
input facts, where in the more targeted approach we ensure that most (if not all)
preconditions are satisfied by design, whereas in the "blind" one we
allow generation of input facts for the given action which can
make the action's preconditions fail. The second approach is of course useful to ensure that
preconditions are specified as expected.
BOOKING-INIT-DATABASE defines constructors of values of sort
Person and Restaurant from natural numbers (h, a,
and c correspond to hosts, customers and agents, respectively):
c, a, h : Nat ⟶ Person, r : Nat ⟶ Restaurant,as well as function
initFact creating initial database
for tests:
initFact : Nat Nat Nat Nat ⟶ FactSet .Here
initFact(Nc, Na, Nr, Nh)
reduces to a multiset of facts containing, respectively, Nc,
Na, Nr, and Nh
facts of the form Cust(c(i)), Agent(a(i)), Host(h(i)), and
Rest(r(i)). Note that our specification does not include rules for creating new
customers, agents, hosts or restaurants, hence these must be provided in the initial database.
SIMUL-BASE-PROB and SIMUL-BASE-NONPROB define initial states
from which we start simulations. Choosing between one and the other module
decides if the simulation will be probabilistic or if it will use non-deterministic rewrite rules:
SIMUL-BASE-PROB provides initial state for probabilistic simulations with the function initState : Nat FactSet ⟶ State. The first argument is
the first position in the sequence of
random numbers to be used in the simulation. As the second argument we pass an initial database.
SIMUL-BASE-NONPROB defines a function
initState : FactSet ⟶ State which provides initial state for simulations
using non-deterministic rewrite rules. The argument is used to pass initial database.SIMUL-PROB-TARGETED, SIMUL-PROB-BLIND,
SIMUL-NONPROB-TARGETED, and SIMUL-NONPROB-BLIND
include combinations of modules SIMUL-BASE-PROB and
SIMUL-BASE-NONPROB with the respective definitions of inp
functions (see modules INP-DEF-TARGETED,
INP-DEF-BLIND,
INP-DEF-TARGETED-NONPROB
and INP-DEF-BLIND-NONPROB),
allowing us to perform simulations using respective implementations
of inp function.SIMUL-PROB-TARGETED module
using the following Maude command:
rew [m] in SIMUL-PROB-TARGETED : initState(N, FS) .where
m should be substituted with the number of required rewrite steps, N
with the initial position in the sequence of pseudorandom numbers, and FS with the initial database e.g.,
rew [30] in SIMUL-PROB-TARGETED : initState(0, initFact(3,3,3,5)) .As the result we obtain a term of sort
State representing the state of the system
after 30 rewrites, e.g. (the rewrites in the Maude's interpreter message below refer to all rewrites
including both applications of rewrite rules and equations),
rewrite [30] in SIMUL-PROB-TARGETED : initState(0, initFact(3,3,3,5)) . rewrites: 9539 in 41ms cpu (51ms real) (227987 rewrites/second) result State: state([358,6 | newOffer resume newBooking addHosts submit detProp cancel accept1 accept2 confirm closeOffer], mod 'SIMUL-BASE-PROB is including 'BOOL . including 'SIMULATION-CONTEXT . including 'NEXT-STEP{'Mp-Multi} . including 'BOOKING-INIT-DATABASE . sorts none . none op 'initState : 'Nat -> 'State [none] . none eq 'initState['N:Nat] = 'state['initContext['N:Nat], 'upModule[''SIMUL-BASE-PROB.Sort,'false.Bool], 'initFact.FactSet] [none] . none endm, Rest(r(1)) o Rest(r(2)) o Rest(r(3)) o Agent(a(1)) o Agent(a(2)) o Agent(a(3)) o Cust(c(1)) o Cust(c(2)) o Cust(c(3)) o Host(h(1)) o Host(h(2)) o Host(h(3)) o Host(h(4)) o Host(h(5)) o OState(${0,errorO}, closed) o OState(${3,errorO}, booking) o BState(${1,errorB}, accepted) o BState(${4,errorB}, finalized) o Prop(${1,errorB}, ${2,errorU}) o Prop(${4,errorB}, ${5,errorU}) o Offer(${0,errorO}, r(1), a(3)) o Offer(${3,errorO}, r(2), a(3)) o Booking(${1,errorB}, ${0,errorO}, c(1)) o Booking(${4,errorB}, ${3,errorO}, c(1)))To increase readability, in the listing above the database part of the state is coloured red, and simulation context is colored green. A more thorough examination of the specification requires reachability analysis. To perform reachability analysis one can use Maude's search command. For example, to see if the state with an accepted booking is reachable (i.e., if we can actually book a dinner with the specified procedure) with at most, say, 100 rewrite steps we could again use probabilistic methods with targeted inputs with the command
search [1, 100] in SIMUL-PROB-TARGETED : initState(0, initFact(3,3,3,5))
=>* state(SC:SimulContext, M:Module, FS:FactSet o BState(B:Booking, accepted)) .
yielding
Solution 1 (state 30) states: 31 rewrites: 8894 in 34ms cpu (34ms real) (259762 rewrites/second) SC:SimulContext --> [366,5 | newOffer resume newBooking addHosts submit detProp cancel accept1 accept2 confirm closeOffer] M:Module --> mod 'SIMUL-BASE-PROB is including 'BOOL . including 'SIMULATION-CONTEXT . including 'NEXT-STEP{'Mp-Multi} . including 'BOOKING-INIT-DATABASE . sorts none . none op 'initState : 'Nat -> 'State [none] . none eq 'initState['N:Nat] = 'state['initContext['N:Nat], 'upModule[''SIMUL-BASE-PROB.Sort, 'false.Bool],'initFact.FactSet] [none] . none endm FS:FactSet --> Rest(r(1)) o Rest(r(2)) o Rest(r(3)) o Agent(a(1)) o Agent(a(2)) o Agent(a(3)) o Cust(c(1)) o Cust(c(2)) o Cust(c(3)) o Host(h(1)) o Host(h(2)) o Host(h(3)) o Host(h(4)) o Host(h(5)) o OState(${0,errorO}, closed) o OState(${3,errorO},booking) o BState(${4,errorB}, submitted) o Prop(${1,errorB}, ${2,errorU}) o Offer(${0,errorO}, r(1), a(2)) o Offer(${3, errorO}, r(1), a(2)) o Booking(${1,errorB}, ${0,errorO}, c(3)) o Booking(${4,errorB}, ${3,errorO}, c(2)) B:Booking --> ${1,errorB}The intermediate steps can then be printed with the Maude command
show search graph .The example output is too long to be shown here. Alternatively, we could have used non-deterministic rewriting with targeted inputs with the command
search [1, 20] in SIMUL-NONPROB-TARGETED : initState(initFact(2,2,2,2))
=>* state(SC:SimulContext, M:Module, FS:FactSet o BState(B:Booking, accepted)) .
yielding
Solution 1 (state 195165) states: 195166 rewrites: 18340443 in 62056ms cpu (62072ms real) (295542 rewrites/second) SC:SimulContext --> [3 | newOffer, resume, closeOffer, newBooking, addHosts, submit, detProp, cancel, accept1, accept2, confirm] M:Module --> mod 'SIMUL-BASE-NONPROB is including 'BOOL . including 'SIMULATION-CONTEXT-NONPROB . including 'NEXT-STEP{'Mp-Multi} . including 'BOOKING-INIT-DATABASE . sorts none . none op 'initState : nil -> 'State [none] . none eq 'initState.State = 'state['initContext.SimulContext, 'upModule[''SIMUL-BASE-NONPROB.Sort,'false.Bool], 'initFact.FactSet] [none] . none endm FS:FactSet --> Rest(r(1)) o Rest(r(2)) o Agent(a(1)) o Agent(a(2)) o Cust(c(1)) o Cust(c(2)) o Host(h(1)) o Host(h(2)) o OState(${0,errorO}, closed) o Prop(${1,errorB}, ${2,errorU}) o Offer(${0,errorO}, r(1), a(1)) o Booking(${1,errorB}, ${0, errorO}, c(1)) B:Booking --> ${1,errorB}One should note the much longer execution time, despite the fact that we cheated here by execution the simultation with a much smaller initial database: two customers, agents, restaurants and hosts as opposed to three customers, agents and restaurants and five hosts used in the previous two examples.
There are several important remarks which must be made here:
We have performed some simple measurements of efficiency of the search procedure. More precisely, we measured duration and depth of the search, when checking reachability of the database where some booking is accepted, depending on the initial database and implementation. First we look upon probabilistic implementations. For both the blind and targeted strategy, as well as two initial databases:
- Since the probabilistic simulation uses probabilistic methods to choose the next action and its intput database, it follows that while non-empty result of Maude's search command means that the requested state is reachable within the given number of rewrite steps, the empty result does not indicate unreachability within the step limit. To get reasonable confidence try the simulation with several positions in the pseudorandom number sequence (and several seeds). A seed can be set by invoking Maude interpreter with option
-random-seed=K, whereKis the seed (default 0).- As remarked in the previous point, the probabilistic search procedure is non-reliable as far as negative answers are concerned. On the other hand, the execution of a probabilistic search procedure is linear, and this makes it both potentially more efficient, and easier to interpret than the one based on non-deterministic rewriting . One can think of our probabilistic rules as randomizing the plain rewrite command.
- One may observe that in case of non-deterministic rewriting based method the number of branches to be considered during the search procedure at the state where the next input set is computed depends on the size of database (which incrises during simulation as new fresh values are produced): linearly in case of rules which generate single facts of a given form, and, at the other extreme, exponentially when using rules generating multiple (and unbounded) number of facts for a given action (like, e.g., in case of
.addHosts). Since the size of the search tree can be approximated as bd, where d is the search depth and b is the average number of branches, it follows that the non-deterministic rewriting methods are practical only with either very small databases or very small search depths
initFact(3,3,3,5) and initFact(2,2,2,2) we run the search command, e.g.,
search [1, 3000] in SIMUL-PROB-TARGETED : initState(0, initFact(3,3,3,5))
=>* state(SC:SimulContext, M:Module, FS:FactSet o BState(B:Booking, accepted)) .
and we note the number of states used (which, in the case of deterministic rewrite rules equals the depth of search, i.e., number of rewrites necessary to reach the looked for state) and the duration of the search. The results are presented in the
tables below (the first column in each case is the initial position in the random number sequence):
| #n | Time [ms] | Depth |
| 0 | 33 | 31 |
| 100 | 111 | 95 |
| 200 | 115 | 85 |
| 300 | 177 | 119 |
| 400 | 85 | 81 |
| 500 | 78 | 72 |
| 600 | 60 | 65 |
| 700 | 58 | 57 |
| 800 | 110 | 79 |
| 900 | 102 | 71 |
| avg | 93 | 76 |
| std dev | 40 | 23 |
| #n | Time [ms] | Depth |
| 0 | 78 | 58 |
| 100 | 38 | 52 |
| 200 | 192 | 133 |
| 300 | 128 | 153 |
| 400 | 117 | 145 |
| 500 | 141 | 130 |
| 600 | 102 | 128 |
| 700 | 100 | 120 |
| 800 | 110 | 106 |
| 900 | 66 | 80 |
| avg | 107 | 110 |
| std dev | 42 | 36 |
| #n | Time [ms] | Depth |
| 0 | 5480 | 2635 |
| 100 | 5465 | 2638 |
| 200 | 5448 | 2631 |
| 300 | 5494 | 2622 |
| 400 | 5481 | 2614 |
| 500 | 5486 | 2606 |
| 600 | 5567 | 2599 |
| 700 | 5281 | 2591 |
| 800 | 47 | 60 |
| 900 | 5532 | 2576 |
| avg | 4928 | 2357 |
| std dev | 1717 | 807 |
| #n | Time [ms] | Depth |
| 0 | 216 | 174 |
| 100 | 1288 | 826 |
| 200 | 871 | 819 |
| 300 | 727 | 810 |
| 400 | 727 | 803 |
| 500 | 715 | 804 |
| 600 | 682 | 796 |
| 700 | 707 | 788 |
| 800 | 683 | 780 |
| 900 | 691 | 773 |
| avg | 731 | 737 |
| std dev | 259 | 199 |
As one can see (as could be reasonably expected) in case of targeted strategy neither the search time nor
the search depth seems to depend significantly on the size of the initial database.
On the other hand, for blind strategy not only the search time and depth is (in most cases, barring the luck, as in the
line at position 800) much larger, but it also dramatically depends on the initial database size.
This is understandable, since in the case of the blind strategy, inputs are chosen (mostly) blindly, that is,
with increasing size of the database, choosing input satisfying the precondition of a given action becomes less probable. This is only further aggravated by creation of new values. Conversly, in the case of
targeted strategy, the inputs are chosen almost always correctly (as long as it is possible at al), which
means that probability of (some) progress is not significantly reduced with the size of the database.
More precisely, the presence of many artifacts, slows their individual progress (since each action changes the state of only few of them). However, it is also more probable that some artifact reaches desired state
early in the simulation when there is not many of them.
Next we test non-probabilistic implementations. Here we perform only a single measurement for each combination of each of the two strategies with two selected initial databases.
| Data | Time [ms] | Depth |
initFact(2,2,2,2) | 56461 | 18 |
initFact(1,1,1,1) | 384 | 18 |
| Data | Time [ms] | Depth |
initFact(2,2,2,2) | 34715 | 20 |
initFact(1,1,1,1) | 596 | 20 |
As we see, there is no significant difference between blind and targeted strategy. However effecicency of both depend strongly on the size of the initial database, and both are extemaly ineffective compared to probablisitic method (which confirms the remark above).
Bartosz Zieliński (email: bzielinski@uni.lodz.pl, ORCID: 0000-0003-3534-6012),
Department of Mathematical Methods,
Faculty of Physics and Applied Informatics,
University of Łódź