Case Study: RoyalLoyal

Descripción del caso de estudio

RoyalLoyal [1] is the model of a software program that manages loyalty programs for third parties that want to offer their clients different types of bonuses. These awards or bonuses are in the form of points or additional services such as prices, a rental car more luxurious for the same price as a standard, best service in a airline flight, etc.. Any company wishing to offer these services could make it through these loyalty programs.

Figure 1 shows the UML class diagram of the system being described. In the context of model-driven software design (MDSD), this diagram represents a model at Platform Independent Model (PIM) abstraction level and shows no dependences on the programming language in which it will be implemented.

Figure 1 : Class diagram RoyalLoyal

The model central class is LoyaltyProgram. A system that runs a loyalty program contain only one instance of this class. On the other hand, a company that offers its customers join a loyalty program is represented by the class ProgramPartner . More than one company can enter the same program and hence customers entering the loyalty program can benefit from the services from any of the participating companies.

Each client of a program offered by a company can enter the loyalty program by obtaining a membership card. Objects of class Customer represent clients getting benefit from one (or more) program. A card of class CustomerCard is associated with a person. Most programs allow users to store bonus points. Each program decides how many points are generated for a certain purchase. These bonus points can be used to "buy" services from a company ProgramPartner that offers a loyalty program. The points are stored for each customer. To this end, each class Membership, which represents the association of a client to a program, has an object of class LoyaltyAccount storing the points.

In this case study the operation enroll(Customer) of class LoyaltyProgram will be described. Operation enroll enrolls the customer (only parameter of the operation) in the program LoyaltyProgram in which the operation is invoked. To this end, an association class Membership is created and all the attributes and associations of the association created are initialized.

Figure 2 shows the main sequence diagram. A new feature to the structures already described in the previous study cases PersonCar and Fibonacci, is the creation of new objects with messages of type Create: in particular an object of association class Membership and another object of class LoyaltyAccount.

Figure 2 : Sequence diagram of the operation enroll.

First, in the sequence diagram of the operation enroll, an association is created, the objet NewMB and the associtations Membership of both ends,LP and C are added with the methods LoyaltyProgram::addMembership(Membership) and Customer::addMembership(Membership). Next, both ends of the created object NewMB are initialized with the methods Membership::setParticipants(Customer) and Membership::setPrograms(LoyaltyProgram). The operation Customer::setCurrentLevel(ServiceLevel) sets the service level of the registration of C to the loyalty program LP.

Finally, the account where the operations and data of the association to the loyalty program are registered is created. The objet NewLA of class LoyaltyAccount is created with a message Create. After creating it, it is set as the account of the association to the loyalty program NewMB created with the first message Create. Afterwards, the attribute currentPoints is initialized with the operation LoyaltyAccount::setPoints(Int), the attribute number is initialized with the operation LoyaltyAccount::setAccountNumber(Int) and the atribute (association) transactions is set to be the empty set Set{} with the operation LoyaltyAccount::setTransactions(Transaction[*]).

Creating objects

The objective of this case study is to show the creation of objects by means of the UML messages Create Messages. A UML message Create Messages is a call for the creation of an object represented by a lifeline (an object of class Lifeline). A Create Message has in its attribute messageSort the literal createMessage. Following the generic schema of the transformation, a Maude rule is created for each message in the UML sequence diagram, a rule that specifies the behavior of the UML message in Maude.

Each object created in a sequence diagram, will have a unique identifier. To this end, in the state running Maude (the "soup of terms") there is a message that will have an identifier "fresh", stated as follows:

op next-Oid : Nat -> Msg [msg] .

The newly created object will have as identifier Oid the natural value that has the message next-Oid as parameter. For a value Nat to be able to be an object identifier it has been necessary to include the set of term of type Nat as a subset of Oid:

subsort Int < Oid .

Every time a rule Maude is generated as a consequence of a message Create Message, the unique identifier must be incremented:

} =>
{ [...]
next-Oid(NewOid:Integer + 1)
} .

The object created must be stored in the operation execution context. The operation context will own the parameters of the operation and the local variables to the UML sequence diagram. A created object will be stored, therefore, as an argument of the context. The name of the attribute of the pair will be assigned by the user as a name of the lifeline created. In the case of the first message in the sequence diagram shown in Figure 2, the name of the argument will be NewMB. In the Maude rule that specifies the message createMembership() a new pair arg(NewMB, NewOid) is added to the list of pairs of the right hand side (RHS) context.

The rule of Code 1 corresponds to the code generated for message createMembership of the sequence diagram shown in Figure 2. The newly created object NewOid : Membership is added to the state in the Maude execution, that is, to the soup of terms, as it appears in th rule right hand side (RHS).

Code 1 : Output generated from the message createMembership.

Running the case study

To build a trace of the study case "Royal and Loyal", an initial state will be proposed from which a call to method LoyaltyProgram::enroll(Customer) will be done.

Code 2 : Initial state of the case study.

In the Code 2 the initial state for this study case is defined as a constant of type Configuration. This term of type Configuration is made up of a multiset of objects. The object SilverAndGold of type LoyaltyProgram, represents a loyalty program with the same name that the object identifier and with levels Silver and Gold. In the other hand, there are three clients: tony, paul and jane, all of them without associations to any loyalty program. The object identifiers used are Maude constants of type Oid.

Code 3 : Initial state with the call operator to the operation enroll.

With the following Maude call:

rew in ROYAL-LOYAL-VALIDATION-TEST : [ init-state-ready ] .

the rewrite of the initial state that calls to the operation LoyaltyProgram::enroll(Customer) is made (Code 3). The ouput is:

Code 4 : Resulting state of the rewriting process.

As two objects have been created, the value of the operator next-Oid is 3 (natural), the identifier that would correspond to the object created next. The loyalty program "SilverAndGold" has now in its attribute Membership the object of association to the program 1 of type Membership. In a similar way, the client tony (of type Customer) has in its attribute Membership the object 1 of type Membership. On the other hand, an object of type LoyaltyAccount has been created, with identifier 2, that represents the points account of the association created with identifier 1. All the attributes have been correctly initialized.

The following invariants have been defined:

Code 5 : Loyalty account points must be positive.

In Code 5 it is specified as a constraint that the attribute currentPoints of aech object of type LoyaltyAccount corresponding to an association Membership to a loyalty program, must be positive. It is also included the possibility that the points may not be initialized or that the account has not been created for the association. Those cases can happen in the initialization process.

Code 6 : Association levels.

In Code 6 it is specified that all the levels of an association to a loyalty program must be possible in that program, that is, the level of an association must be offered by the program it belongs to. The select operation will filter the values null in the associations Membership that are being created and whose levels have not been stablished yet.

Code 7 : Identifiers of user accounts must be unique.

In Code 7 it is specified the invariant that stablishes that the number of a loyalty account of an association Membership is unique, that is, there can not be two accounts with the same number.

All diagrams implied in the definition of enroll

In addition to the figures 1 and 2, below we show those sequence diagrams describing all the operations involved in the operation enroll.

Figure 3 : Sequence diagram of the operation Customer::AddMembership.

Figure 4 : Sequence diagram of the operation LoyaltyAccount::AddMembership.

Figure 5 : Sequence diagram of the operation LoyaltyAccount::SetAccountNumber.

Figure 6 : Sequence diagram of the operation LoyaltyAccount::SetMembership.

Figure 7 : Sequence diagram of the operation LoyaltyAccount::SetPoints.

Figure 8 : Sequence diagram of the operation LoyaltyAccount::SetTransactions.

Figure 9 : Sequence diagram of the operation LoyaltyProgram::IncLastAccNmb.

Figure 10 : Sequence diagram of the operation Membership::SetAccount.

Figure 11 : Sequence diagram of the operation Membership::SetCurrentLevel.

Figure 13 : Sequence diagram of the operation Membership::SetPrograms.


  • [1] J. Warmer and A. Kleppe. The Object Constraint Language: Getting Your Models Ready for MDA. Addison-Wesley Logman Publishing Co., USA, 2 edition, 2003.


    Maude codes
    Papyrus project

    Last modification: 3rd September, 2013