Strategies are necessary for controlling the execution of rules that are not terminating, or that do not satisfy the admissibility conditions discussed in Section 5.3. A simple but interesting strategy may be one that allows us to execute a given sequence of rules, that is, to accomplish sequentially a series of actions from a particular initial state. We introduce in this section such a generic strategy and illustrate its use by applying it for executing the systems specified in Sections 15.2 and 15.5. Dealing with strategies may become cumbersome, since we need to handle terms and modules at different levels of reflection, and expressions may become quite hard to read and handle. We show in this section how the upModule and upTerm functions and the down command introduced in Section 14.4 can help in alleviating this difficulty.
A strategy is represented as a sequence of rule applications. We
instantiate the predefined module LIST with pairs formed by
a rule label representing the rule to be applied, and a substitution
to partially instantiate the variables in such a rule before its
application. The pairs are obtained using the generic tuple
construction described in Section 14.3.1. Thus, to get the
module expression LIST{Tuple{Qid, Substitution}}, given
the predefined view Qid and the parameterized view
Tuple, that we have already used in the partial functions
example of Section 14.3.2, we only need to define a
view Substitution from TRIV to META-LEVEL.
(view Substitution from TRIV to META-LEVEL is
sort Elt to Substitution .
endv)
This construction is put to work in the module REW-SEQ below. The operator rewSeq in this module takes the metarepresentation of a module, the metarepresentation of a term, and a list of pairs (each formed by a rule label and a substitution); the term obtained in this way is rewritten by applying the given rules sequentially, using in their applications their corresponding partial substitutions.
(mod REW-SEQ is
including META-LEVEL .
protecting LIST{Tuple{Qid, Substitution}} .
var M : Module .
var T : Term .
var L : Qid .
var S : Substitution .
var LLS : List{Tuple{Qid, Substitution}} .
op rewSeq :
Module Term List{Tuple{Qid, Substitution}} -> [Term] .
rl [seq] : rewSeq(M, T, (L, S) LLS)
=> rewSeq(M,
getTerm(metaXapply(M, T, L, S, 0, unbounded, 0)), LLS) .
rl [seq] : rewSeq(M, T, nil) => T .
endm)
The rules to be applied here are part of the module given as first argument. The strategy starts with the term given as initial state, which is replaced in each recursive call by the term representing the state obtained after the application of the next rule in the sequence (see Section 11.4.4). When all the rules have been applied, thus reaching the empty list as third argument, the current state is returned as the resulting final state.
We illustrate the use of the rewSeq strategy by applying a sequence of rules on a configuration of the rent-a-car system specified in Section 15.2. Let RENT-A-CAR-STORE be the name of the module containing the specification of such a system, and let StoreConf be a configuration of objects defined in the following module.
(fmod RENT-A-CAR-STORE-TEST is
pr RENT-A-CAR-STORE .
op StoreConf : -> Configuration [memo] .
eq StoreConf
= < 'C1 : Customer | cash : 5000, debt : 0, suspended : false >
< 'C2 : Customer | cash : 5000, debt : 0, suspended : false >
< 'A1 : EconomyCar | available : true, rate : 100 >
< 'A3 : MidSizeCar | available : true, rate : 150 >
< 'A5 : FullSizeCar | available : true, rate : 200 >
< 'C : Calendar | date : 0 > .
endfm)
The StoreConf configuration consists of two clients C1 and C2, three cars A1, A3 and A5, and a calendar object C. Now, let StoreStrat be a sequence of pairs (rule label - substitution) that defines the strategy declared in the following module as a sequence of actions:
(fmod REW-SEQ-TEST is
pr REW-SEQ .
op StoreStrat : -> List{Tuple{Qid, Substitution}} [memo] .
eq StoreStrat
= ('car-rental,
'U:Oid <- ''C1.Qid ; *** size car A3 for 2 days
'I:Oid <- ''A3.Qid ;
'NumDays:Int <- 's_^2['0.Zero] ;
'A:Oid <- ''a0.Qid)
('new-day, none) *** two days pass
('new-day, none)
('on-date-car-return, none) *** car A3 is returned
('new-day, none)
('car-rental, *** client C1 rents the full
'U:Oid <- ''C1.Qid ; *** size car A5 for 1 day
'I:Oid <- ''A5.Qid ;
'NumDays:Int <- 's_^1['0.Zero] ;
'A:Oid <- ''a1.Qid)
('new-day, none) *** two days pass
('new-day, none)
('late-car-return, none) *** car A5 is returned
('new-day, none)
('suspend-late-payers, none) *** client C1 is suspended
('new-day, none)
('new-day, none)
('pay-debt, *** client C1 pays 100$
'Amnt:Int <- 's_^100['0.Zero]) .
endfm)
Comments on the righthand side of the code above explain the sequence of rules defining the strategy. Basically, the execution trace specified consists of client C1 renting two cars, one of which is returned on time and the other one is returned late. After the second car is returned, the client is suspended for being late in his payments. The client then pays part of his debt. Note how the passage of time is modeled by the application of the rule new-day.
Now, in order to execute the system specifications using this strategy, we just need to use rewSeq to apply the given rules sequentially, using their corresponding partial substitutions in their applications. Note how the first two arguments are metarepresented with the upModule and upTerm functions, since they need to be the metarepresentations of the actual module and term, respectively.
Maude> (down RENT-A-CAR-STORE :
rew rewSeq(upModule(RENT-A-CAR-STORE-TEST),
upTerm(RENT-A-CAR-STORE-TEST, StoreConf),
StoreStrat) .)
result Configuration :
< 'C : Calendar | date : 8 >
< 'C1 : Customer | suspended : true, debt : 140, cash : 4400 >
< 'C2 : Customer | suspended : false, debt : 0, cash : 5000 >
< 'A1 : EconomyCar | rate : 100, available : true >
< 'A3 : MidSizeCar | rate : 150, available : true >
< 'A5 : FullSizeCar | rate : 200, available : true >
We can see in this configuration that eight days have passed, after which the client
C1 is suspended. The client C1 has paid a total of
(= 2 
150 + 200 + 100), and has still a debt of
(= 200 + 20 % 200 
100).
The same strategy can be used to execute the extended specification in Section 15.5, contained in a module named EXTENDED-RENT-A-CAR-STORE. First, we define a module with an initial configuration ExtStoreConf.
(fmod EXTENDED-RENT-A-CAR-STORE-TEST is
pr EXTENDED-RENT-A-CAR-STORE .
op ExtStoreConf : -> Configuration [memo] .
eq ExtStoreConf
= < 'S : Store |
discounts :
(((Staff, EconomyCar), 20),
((Staff, MidSizeCar), 30),
((Staff, FullSizeCar), 40),
((OccasionalCust, EconomyCar), 0),
((OccasionalCust, MidSizeCar), 0),
((OccasionalCust, FullSizeCar), 0),
((PreferredCust, EconomyCar), 10),
((PreferredCust, MidSizeCar), 15),
((PreferredCust, FullSizeCar), 20)),
payments : empty, penalty : 0,
threshold : 1000, suspended : empty,
rates : ((EconomyCar, 100),
(MidSizeCar, 150),
(FullSizeCar, 200)),
customers : ('C1, 'C2),
cars : ('A1, 'A3, 'A5),
rentals : empty, calendar : 'C >
< 'C1 : Staff | cash : 5000, debt : 0 >
< 'C2 : OccasionalCust | cash : 5000, debt : 0 >
< 'A1 : EconomyCar | available : true >
< 'A3 : MidSizeCar | available : true >
< 'A5 : FullSizeCar | available : true >
< 'C : Calendar | date : 0 > .
endfm)
Now we execute a command completely analogous to the previous one,
obtaining a resulting state that shows how, after eight days, client
C1 has paid 
, and has a debt of 
.
Maude> (down EXTENDED-RENT-A-CAR-STORE :
rew rewSeq(upModule(EXTENDED-RENT-A-CAR-STORE),
upTerm(EXTENDED-RENT-A-CAR-STORE, ExtStoreConf),
StoreStrat) .)
result Configuration :
< 'A1 : EconomyCar | available : true >
< 'A3 : MidSizeCar | available : true >
< 'A5 : FullSizeCar | available : true >
< 'C : Calendar | date : 8 >
< 'C1 : Staff | cash : 4500, debt : 60 >
< 'C2 : OccasionalCust | cash : 5000, debt : 0 >
< 'S : Store | calendar : 'C,
cars : ('A1, 'A3, 'A5),
customers : ('C1, 'C2),
discounts : (((OccasionalCust, EconomyCar), 0),
((OccasionalCust, FullSizeCar), 0),
((OccasionalCust, MidSizeCar), 0),
((PreferredCust, EconomyCar), 10),
((PreferredCust, FullSizeCar), 20),
((PreferredCust, MidSizeCar), 15),
((Staff, EconomyCar), 20),
((Staff, FullSizeCar), 40),
((Staff, MidSizeCar), 30)),
payments : ('C1, 500),
penalty : 0,
rates : ((EconomyCar, 100),
(FullSizeCar, 200),
(MidSizeCar, 150)),
rentals : empty,
suspended : 'C1,
threshold : 1000 >