A Collection of ITP/OCL Examples

Coach-Company model

 In this example, borrowed from [Boronat, A., Ramos I., Carsí, J. Algebraic Semantics of Generic OCL Queries in the Eclipse Modeling Framework., 2006], we model a simple coach company. A coach has a specific number of seats and can be used for regular or private trips. In regular trips, the tickets are bought individually. In private trips, the whole coach is rented.

coach-company-example

Using OCL constraints we can further precise our model. In particular, we indicate that overbooking is not allowed in a regular trip.
The following script initialises an ITP/OCL session and loads the COACH class diagram, with the constraint about overbooking, in the ITP/OCL database:

loop init-ocl .

(create-class-diagram COACH .)
(insert-class COACH : Trip .)
(insert-class COACH : Coach .)
(insert-class COACH : Person .)
(insert-class COACH : PrivateTrip .)
(insert-class COACH : RegularTrip .)
(insert-subclass COACH : PrivateTrip -> Trip .)
(insert-subclass COACH : RegularTrip -> Trip .)
(insert-attr COACH : Trip (tripnr, Integer) .)
(insert-attr COACH : Coach (numberOfSeats, Integer) .)
(insert-attr COACH : Coach (id, Integer) .)
(insert-attr COACH : RegularTrip (availableSeats, Integer) .)
(insert-attr COACH : Person (name, String) .)
(insert-assoc COACH : Trip : trips : < * > <-> < 1 > : coach : Coach .)
(insert-assoc COACH : RegularTrip : trips : < * > <-> < * > : passengers : Person .)
(insert-invariant COACH : Coach :
((self:Coach #trips)->forAll(t:RegularTrip | ((t:RegularTrip #passengers)->size() <= ((t:RegularTrip #coach@) #numberOfSeats)))) .)

TWO DIFFERENT SNAPSHOTS

The object diagram COACH-1 below corresponds to a snapshot of the COACH class diagram.

coach1-snapshot

The following script loads the COACH-1 object diagram:

(create-object-diagram COACH : COACH-1 .)
(insert-object COACH-1 : Coach : coach1 .)
(insert-object COACH-1 : RegularTrip : trip1 .)
(insert-object COACH-1 : Person : person1 .)
(insert-object COACH-1 : Person : person2 .)
(insert-object COACH-1 : Person : person3 .)
(insert-attr-value COACH-1 : Coach : coach1 : id : Integer -> 1 .)
(insert-attr-value COACH-1 : Coach : coach1 : numberOfSeats : Integer -> 10 .)
(insert-attr-value COACH-1 : RegularTrip : trip1 : tripnr : Integer -> 1 .)
(insert-attr-value COACH-1 : RegularTrip : trip1 : availableSeats : Integer -> 9 .)
(insert-attr-value COACH-1 : Person : person1 : name : String -> "Peter" .)
(insert-attr-value COACH-1 : Person : person2 : name : String -> "John" .)
(insert-attr-value COACH-1 : Person : person3 : name : String -> "Mary" .)
(insert-link COACH-1 | RegularTrip : trips <-> coach : Coach | trip1 <-> coach1 .)
(insert-link COACH-1 | RegularTrip : trips <-> passengers : Person | trip1 <-> person1 .)
(insert-link COACH-1 | RegularTrip : trips <-> passengers : Person | trip1 <-> person2 .)

The snapshot COACH-1 clearly satisfies the contraint about overbooking. This can be automatically checked using the following script:

(check-invariants COACH : COACH-1 .)

The object diagram COACH-2 below corresponds to another snapshot of the COACH class diagram.

coach2-snapshot

The following script loads the COACH-2 object diagram:

(create-object-diagram COACH : COACH-2 .)
(insert-object COACH-2 : Coach : coach1 .)
(insert-object COACH-2 : RegularTrip : trip1 .)
(insert-object COACH-2 : Person : person1 .)
(insert-object COACH-2 : Person : person2 .)
(insert-object COACH-2 : Person : person3 .)
(insert-attr-value COACH-2 : Coach : coach1 : id : Integer -> 1 .)
(insert-attr-value COACH-2 : Coach : coach1 : numberOfSeats : Integer -> 2 .)
(insert-attr-value COACH-2 : RegularTrip : trip1 : tripnr : Integer -> 1 .)
(insert-attr-value COACH-2 : RegularTrip : trip1 : availableSeats : Integer -> 9 .)
(insert-attr-value COACH-2 : Person : person1 : name : String -> "Peter" .)
(insert-attr-value COACH-2 : Person : person2 : name : String -> "John" .)
(insert-attr-value COACH-2 : Person : person3 : name : String -> "Mary" .)
(insert-link COACH-2 | RegularTrip : trips <-> coach : Coach | trip1 <-> coach1 .)
(insert-link COACH-2 | RegularTrip : trips <-> passengers : Person | trip1 <-> person1 .)
(insert-link COACH-2 | RegularTrip : trips <-> passengers : Person | trip1 <-> person2 .)
(insert-link COACH-2 | RegularTrip : trips <-> passengers : Person | trip1 <-> person3 .)

The snapshot COACH-2 does not satisfy the contraint about overbooking. This can be automatically checked using the following script:

(check-invariants COACH : COACH-2 .)

You can download here the script of this example.

Flight model

In this example, borrowed from [Warmer, J., Kleppe, A. The Object Constraint Language, Second Edition: Getting Your Models Ready for MDA., Addison-Wesley, 2003], the association between class Flight and class Person, indicating that a certain group of persons are the passengers on a flight, has multiplicity many on the side of the Person class. :


flight-model-example

In reality, the number of passengers is restricted to the number of seats on the airplane that is associated with the flight. However, it is impossible to express this restriction in the diagram. In this example, the correct way to specify the multiplicity is to add to the diagram the corresponding OCL constrain.
The following script initialises an ITP/OCL session and loads the FLIGHT class diagram, with the constraint about limited seats, in the ITP/OCL database:

loop init-ocl .

(create-class-diagram FLIGHT .)
(insert-class FLIGHT : Flight .)
(insert-class FLIGHT : Person .)
(insert-class FLIGHT : Airplane .)
(insert-assoc FLIGHT : Flight : flights : < * > <-> < 1 > : plane : Airplane .)
(insert-assoc FLIGHT : Flight : flights : < * > <-> < * > : passengers : Person .)
(insert-attr FLIGHT : Flight (flightnr, Integer) .)
(insert-attr FLIGHT : Airplane (numberOfSeats, Integer) .)
(insert-attr FLIGHT : Person (name, String) .)
(insert-invariant FLIGHT : Flight :
(((self:Flight #passengers)->size()) <= ((self:Flight #plane@) #numberOfSeats)) .)

A SNAPSHOT

The object diagram FLIGHT-1 below corresponds to a snapshot of the FLIGHT class diagram.

fight-1-snapshot

The following script loads the FLIGHT-1 object diagram:

(create-object-diagram FLIGHT : FLIGHT-1 .)
(insert-object FLIGHT-1 : Flight : Flight1 .)
(insert-object FLIGHT-1 : Airplane : A-380 .)
(insert-object FLIGHT-1 : Person : Person1 .)
(insert-object FLIGHT-1 : Person : Person2 .)
(insert-object FLIGHT-1 : Person : Person3 .)
(insert-object FLIGHT-1 : Person : Person4 .)
(insert-link FLIGHT-1 | Flight : flights <-> plane : Airplane | Flight1 <-> A-380 .)
(insert-link FLIGHT-1 | Flight : flights <-> passengers : Person | Flight1 <-> Person1 .)
(insert-link FLIGHT-1 | Flight : flights <-> passengers : Person | Flight1 <-> Person2 .)
(insert-link FLIGHT-1 | Flight : flights <-> passengers : Person | Flight1 <-> Person3 .)
(insert-link FLIGHT-1 | Flight : flights <-> passengers : Person | Flight1 <-> Person4 .)
(insert-attr-value FLIGHT-1 : Flight : Flight1 : flightnr : Integer -> 3825 .)
(insert-attr-value FLIGHT-1 : Airplane : A-380 : numberOfSeats : Integer -> 300 .)
(insert-attr-value FLIGHT-1 : Person : Person1 : name : String -> "John" .)
(insert-attr-value FLIGHT-1 : Person : Person2 : name : String -> "Michael" .)
(insert-attr-value FLIGHT-1 : Person : Person3 : name : String -> "Raphael" .)
(insert-attr-value FLIGHT-1 : Person : Person4 : name : String -> "Mary" .)

The snapshot FLIGHT-1 clearly satisfies the contraint about limited seats. This can be automatically checked using the following script:

(check-invariants FLIGHT : FLIGHT-1 .)

You can download here the script of this example.

Royal and Loyal System

In this example, borrowed from [Warmer, J., Kleppe, A. The Object Constraint Language: Precise Modeling with UML., Addison-Wesley, 1999], we have modeled a computer system for a fictional company called Royal and Loyal (R&L). R&L handles loyalty programs for companies that offer their (good) customers various kinds of bonuses. Often, the extras take the form of bonus points or air miles, but other bonuses are possible as well: reduced rates, a larger car for the same price as a standard rental car, extra or better service on an airline, and so on. Anything a company is willing to offer can be a service rendered in a loyalty program.

royal-example

The central class in the model is LoyaltyProgram. A system that administers a single loyalty program will contain only one object of this class. A company that offers its customers a membership in a loyalty program is called a ProgramPartner. More than one company can enter into the same program. In that case, customers who enter the loyalty program can profit from services rendered by any of the participating companies.

Every customer of every program partner can enter the loyalty program by filling in a form and obtaining a membership card. The objects of class Customer represent the people who have entered the program. The membership card, represented by the class CustomerCard, is issued to one person. Card use is not checked, so the card could be used as a family or business card. Most loyalty programs allow customers to save bonus points. Each individual program partner decides when and how many bonus points are alloted for a certain purchase. Saved bonus can be used to "buy" specific services from one of the program partners. To account for the bonus points that are saved by a customer, every membership can be associated with a LoyaltyAccount.

Various transactions on this account are possible. First, there are transactions in which the customer obtain bonus points. These transactions are represented by a subclass of Transaction called Earning. Second, there are transactions in which the customer spends bonus points. In the model they are represented by instances of the Burning subclass of Transaction.

To administer different levels of service, the class ServiceLevel is introduced in the model. A service level is defined by the loyalty program and used for each membership.

The following script initialises an ITP/OCL session and loads the ROYAL-LOYAL class diagram in the ITP/OCL database:

loop init-ocl .

(create-class-diagram ROYAL&LOYAL .)
(insert-class ROYAL&LOYAL : LoyaltyProgram .)
(insert-class ROYAL&LOYAL : Customer .)
(insert-class ROYAL&LOYAL : CustomerCard .)
(insert-class ROYAL&LOYAL : Membership .)
(insert-class ROYAL&LOYAL : ServiceLevel .)
(insert-class ROYAL&LOYAL : ProgramPartner .)
(insert-class ROYAL&LOYAL : Service .)
(insert-class ROYAL&LOYAL : LoyaltyAccount .)
(insert-class ROYAL&LOYAL : Transaction .)
(insert-class ROYAL&LOYAL : Burning .)
(insert-class ROYAL&LOYAL : Earning .)

(insert-enum-class ROYAL&LOYAL : Color - silver gold .)

(insert-subclass ROYAL&LOYAL : Burning -> Transaction .)
(insert-subclass ROYAL&LOYAL : Earning -> Transaction .)

(insert-assoc ROYAL&LOYAL : LoyaltyProgram : program : < * > <-> < * > : customer : Customer .)
(insert-assoc ROYAL&LOYAL : Membership : membership : < * > <-> < 1 > : card : CustomerCard .)
(insert-assoc ROYAL&LOYAL : Customer : customer : < 1 > <-> < * > : cards : CustomerCard .)
(insert-assoc ROYAL&LOYAL : LoyaltyProgram : loyaltyprogram : < * > <-> < * > : servicelevel : ServiceLevel .)
(insert-assoc ROYAL&LOYAL : Membership : membership : < * > <-> < * > : loyaltyaccount : LoyaltyAccount .)
(insert-assoc ROYAL&LOYAL : LoyaltyProgram : loyaltyprogram : < * > <-> < * > : partners : ProgramPartner .)
(insert-assoc ROYAL&LOYAL : Service : deliveredServices : < * > <-> < * > : programpartner : ProgramPartner .)
(insert-assoc ROYAL&LOYAL : Transaction : transactions : < * > <-> < * > : service : Service .)
(insert-assoc ROYAL&LOYAL : ServiceLevel : actualLevel : < 1 > <-> < * > : membership : Membership .)
(insert-assoc ROYAL&LOYAL : CustomerCard : card : < * > <-> < * > : transactions : Transaction .)
(insert-assoc ROYAL&LOYAL : Transaction : transactions : < * > <-> < * > : loyaltyaccount : LoyaltyAccount .)

(insert-assoc-class ROYAL&LOYAL | LoyaltyProgram : program <-> customer : Customer | membership : Membership : membership .)

(insert-attr ROYAL&LOYAL : Customer (name, String) .)
(insert-attr ROYAL&LOYAL : Customer (title, String) .)
(insert-attr ROYAL&LOYAL : Customer (isMale, Boolean) .)
(insert-attr ROYAL&LOYAL : Customer (age, Integer) .)
(insert-attr ROYAL&LOYAL : CustomerCard (printedName, String) .)
(insert-attr ROYAL&LOYAL : CustomerCard (valid, Boolean) .)
(insert-attr ROYAL&LOYAL : CustomerCard (color, Color) .)
(insert-attr ROYAL&LOYAL : Service (condition, Boolean) .)
(insert-attr ROYAL&LOYAL : Service (pointsEarned, Integer) .)
(insert-attr ROYAL&LOYAL : Service (pointsBurned, Integer) .)
(insert-attr ROYAL&LOYAL : Service (description, String) .)
(insert-attr ROYAL&LOYAL : Transaction (points, Integer) .)
(insert-attr ROYAL&LOYAL : ServiceLevel (name, String) .)
(insert-attr ROYAL&LOYAL : ProgramPartner (numberOfCustomers, Integer) .)
(insert-attr ROYAL&LOYAL : LoyaltyAccount (points, Integer) .)

Putting Invariants on Attributes

In the R&L example, a reasonable invariant customerAge for every logalty program would be to demand that every customer who enters a loyalty program be of age.

(insert-invariant ROYAL&LOYAL : Customer : ((self:Customer #age) >= 18) .)

The object diagram ROYAL&LOYAL-1 below corresponds to a snapshot of the ROYAL&LOYAL class diagram.

inv1true

The following script loads the ROYAL&LOYAL-1 object diagram.

(create-object-diagram ROYAL&LOYAL : ROYAL&LOYAL-1 .)
(insert-object ROYAL&LOYAL-1 : Customer : Customer1 .)
(insert-object ROYAL&LOYAL-1 : Customer : Customer2 .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer1 : name : String -> "John-Smith" .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer2 : name : String -> "Mary-Poppins" .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer1 : title : String -> "Mr." .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer2 : title : String -> "Mrs." .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer1 : isMale : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer2 : isMale : Boolean -> false .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer1 : age : Integer -> 25 .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer2 : age : Integer -> 35 .)

The snapshot ROYAL&LOYAL-1 clearly satifies the constraint customerAge.

The object diagram ROYAL&LOYAL-2 below corresponds to another snapshot of the ROYAL&LOYAL class diagram. ROYAL&LOYAL-2, however, does not satisfy the constraint customerAge.

inv1false

The following script loads the ROYAL&LOYAL-2 object diagram.

(create-object-diagram ROYAL&LOYAL : ROYAL&LOYAL-2 .)
(insert-object ROYAL&LOYAL-2 : Customer : Customer1 .)
(insert-object ROYAL&LOYAL-2 : Customer : Customer2 .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer1 : name : String -> "John-Smith" .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer2 : name : String -> "Mary-Poppins" .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer1 : title : String -> "Mr." .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer2 : title : String -> "Mrs." .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer1 : isMale : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer2 : isMale : Boolean -> false .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer1 : age : Integer -> 15 .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer2 : age : Integer -> 35 .)

Putting Invariants on Associated Classes

You can put an invariant on attributes of objects of one class (as show in the preceding section) or on attributes of objects of associated classes, as shown next. In OCL, you can use the rolename to refer to the object on the other end of the association. For R&L, it would be useful to demand that the card and the customer related to a membership are related to each other; that is, a card issued for a membership is in the possesion of the customer who is mentioned in the membership.

(insert-invariant ROYAL&LOYAL : Membership :
(((self:Membership #card@) #customer@) = (self:Membership #customer@)) .)

This invariant sameCustomer literally means that the customer linked to the card object in a membership is the same object as the customer linked to the membership.

The object diagram ROYAL&LOYAL-1 below corresponds to a snapshot of the ROYAL&LOYAL class diagram.

inv2true

The following script loads the ROYAL&LOYAL-1 object diagram.

(create-object-diagram ROYAL&LOYAL : ROYAL&LOYAL-1 .)
(insert-object ROYAL&LOYAL-1 : LoyaltyProgram : Advantage .)
(insert-object ROYAL&LOYAL-1 : Membership : memb1 .)
(insert-object ROYAL&LOYAL-1 : Customer : customer1 .)
(insert-object ROYAL&LOYAL-1 : CustomerCard : card1 .)
(insert-object ROYAL&LOYAL-1 : ServiceLevel : s1 .)
(insert-attr-value ROYAL&LOYAL-1 : ServiceLevel : s1 : name : String -> "gold" .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer1 : name : String -> "John-Smith" .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer1 : title : String -> "Mr." .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer1 : isMale : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer1 : age : Integer -> 35 .)
(insert-attr-value ROYAL&LOYAL-1 : CustomerCard : card1 : valid : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-1 : CustomerCard : card1 : color : Color -> silver .)
(insert-attr-value ROYAL&LOYAL-1 : CustomerCard : card1 : printedName : String -> "Mr.John-Smith" .)
(insert-link ROYAL&LOYAL-1 | LoyaltyProgram : programs <-> participants : Customer | Advantage <-> customer1 .)
(insert-assoc-class-link ROYAL&LOYAL-1 | LoyaltyProgram : programs <-> participants : Customer | membership : Membership : membership | Advantage <-> customer1, memb1 .)
(insert-link ROYAL&LOYAL-1 | Customer : owner <-> cards : CustomerCard | customer1 <-> card1 .)
(insert-link ROYAL&LOYAL-1 | CustomerCard : card <-> membership : Membership | card1 <-> memb1 .)
(insert-link ROYAL&LOYAL-1 | ServiceLevel : actualLevel <-> membership : Membership | s1 <-> memb1 .)

The snapshot ROYAL&LOYAL-1 clearly satifies the constraint sameCustomer.

The object diagram ROYAL&LOYAL-2 below corresponds to another snapshot of the ROYAL&LOYAL class diagram. ROYAL&LOYAL-2, however, does not satisfy the constraint sameCustomer.

inv2false

The following script loads the ROYAL&LOYAL-2 object diagram.

(create-object-diagram ROYAL&LOYAL : ROYAL&LOYAL-2 .)
(insert-object ROYAL&LOYAL-2 : LoyaltyProgram : Advantage .)
(insert-object ROYAL&LOYAL-2 : Membership : memb2 .)
(insert-object ROYAL&LOYAL-2 : Customer : customer2 .)
(insert-object ROYAL&LOYAL-2 : CustomerCard : card2 .)
(insert-object ROYAL&LOYAL-2 : ServiceLevel : s1 .)
(insert-attr-value ROYAL&LOYAL-2 : ServiceLevel : s1 : name : String -> "gold" .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer2 : name : String -> "MaryPoppins" .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer2 : title : String -> "Mrs." .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer2 : isMale : Boolean -> false .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer2 : age : Integer -> 30 .)
(insert-attr-value ROYAL&LOYAL-2 : CustomerCard : card2 : valid : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-2 : CustomerCard : card2 : color : Color -> gold .)
(insert-attr-value ROYAL&LOYAL-2 : CustomerCard : card2 : printedName : String -> "MaryPoppins" .)
(insert-link ROYAL&LOYAL-2 | LoyaltyProgram : programs <-> participants : Customer | Advantage <-> customer2 .)
(insert-assoc-class-link ROYAL&LOYAL-2 | LoyaltyProgram : programs <-> participants : Customer | membership : Membership : membership | Advantage <-> customer2, memb2 .)
(insert-link ROYAL&LOYAL-2 | CustomerCard : card <-> membership : Membership | card2 <-> memb2 .)
(insert-link ROYAL&LOYAL-2 | ServiceLevel : actualLevel <-> membership : Membership | s1 <-> memb2 .)

Similarly, we can put an invariant on the attributes of associated classes:

(insert-invariant ROYAL&LOYAL : CustomerCard :
((self:CustomerCard #printedName) = ((self:CustomerCard #customer@) #title) #concat((self:CustomerCard #customer@) #name)) .)

This invariant rightPrintedName means that the attribute printedName in every instance of CustomerCard must be equal to the concatenation of the title and name attributes of the associated instance of Customer. If we check the previous snapshots, we find that rightPrintedName is fulfilled by ROYAL&LOYAL-1 but not by the ROYAL&LOYAL-2.

Dealing with Collections of Objects

Often the multiplicity of an association is greater than 1, thereby linking one object to a set of objects of the associated class. To deal with such a set, OCL has a number of operations called collection operations. For R&L, it would be useful to introduce the invariant numberServiceLevel that demands that in any loyalty program the number of service levels equals 2.

(insert-invariant ROYAL&LOYAL : LoyaltyProgram :
(((self:LoyaltyProgram #servicelevel)->size()) = 2) .)

The object diagram ROYAL&LOYAL-1 below corresponds to a snapshot of the ROYAL&LOYAL class diagram.

invtrue

The following script loads the ROYAL&LOYAL-1 object diagram.

(create-object-diagram ROYAL&LOYAL : ROYAL&LOYAL-1 .)
(insert-object ROYAL&LOYAL-1 : LoyaltyProgram : Advantage .)
(insert-object ROYAL&LOYAL-1 : ServiceLevel : s1 .)
(insert-object ROYAL&LOYAL-1 : ServiceLevel : s2 .)
(insert-attr-value ROYAL&LOYAL-1 : ServiceLevel : s1 : name : String -> "gold" .)
(insert-attr-value ROYAL&LOYAL-1 : ServiceLevel : s2 : name : String -> "silver" .)
(insert-link ROYAL&LOYAL-1 | LoyaltyProgram : program <-> levels : ServiceLevel | Advantage <-> s1 .)
(insert-link ROYAL&LOYAL-1 | LoyaltyProgram : program <-> levels : ServiceLevel | Advantage <-> s2 .)

The snapshot ROYAL&LOYAL-1 clearly satifies the constraint numberServiceLevel.

The object diagram ROYAL&LOYAL-2 below corresponds to another snapshot of the ROYAL&LOYAL class diagram. ROYAL&LOYAL-2, however, does not satisfy the constraint numberServiceLevel.

invfalse

(create-object-diagram ROYAL&LOYAL : ROYAL&LOYAL-2 .)
(insert-object ROYAL&LOYAL-2 : LoyaltyProgram : Advantage .)
(insert-object ROYAL&LOYAL-2 : ServiceLevel : s1 .)
(insert-object ROYAL&LOYAL-2 : ServiceLevel : s2 .)
(insert-attr-value ROYAL&LOYAL-2 : ServiceLevel : s1 : name : String -> "gold" .)
(insert-attr-value ROYAL&LOYAL-2 : ServiceLevel : s2 : name : String -> "silver" .)
(insert-link ROYAL&LOYAL-2 | LoyaltyProgram : program <-> levels : ServiceLevel | Advantage <-> s2 .)

Another invariant numberValidCard on the R&L model is that the number of valid cards for every customer must be equal to the number of programs the customer participates in.

(insert-invariant ROYAL&LOYAL : Customer :
((self:Customer #program)->size() = ((self:Customer #cards)->select(c:CustomerCard | (c:CustomerCard #valid) = true))->size()) .)

The object diagram ROYAL&LOYAL-1 below corresponds to a snapshot of the ROYAL&LOYAL class diagram.

inv1true

The following script loads the ROYAL&LOYAL-1 object diagram.

(create-object-diagram ROYAL&LOYAL : ROYAL&LOYAL-1 .)
(insert-object ROYAL&LOYAL-1 : LoyaltyProgram : Advantage .)
(insert-object ROYAL&LOYAL-1 : Membership : memb1 .)
(insert-object ROYAL&LOYAL-1 : Customer : customer1 .)
(insert-object ROYAL&LOYAL-1 : CustomerCard : card1 .)
(insert-object ROYAL&LOYAL-1 : ServiceLevel : s1 .)
(insert-object ROYAL&LOYAL-1 : ServiceLevel : s1 : name : String -> "gold" .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer1 : name : String -> "John-Smith" .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer1 : title : String -> "Mr." .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer1 : isMale : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-1 : Customer : customer1 : age : Integer -> 35 .)
(insert-attr-value ROYAL&LOYAL-1 : CustomerCard : card1 : valid : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-1 : CustomerCard : card1 : color : Color -> silver .)
(insert-attr-value ROYAL&LOYAL-1 : CustomerCard : card1 : printedName : String -> "Mr.John-Smith" .)
(insert-link ROYAL&LOYAL-1 | LoyaltyProgram : programs <-> participants : Customer | Advantage <-> customer1 .)
(insert-assoc-class-link ROYAL&LOYAL-1 | LoyaltyProgram : programs <-> participants : Customer | membership : Membership : membership | Advantage <-> customer1, memb1 .)
(insert-link ROYAL&LOYAL-1 | Customer : owner <-> cards : CustomerCard | customer1 <-> card1 .)
(insert-link ROYAL&LOYAL-1 | CustomerCard : card <-> membership : Membership | card1 <-> memb1 .) (insert-link ROYAL&LOYAL-1 | ServiceLevel : actualLevel <-> membership : Membership | s1 <-> memb1 .)

The snapshot ROYAL&LOYAL-1 clearly satifies the constraint numberValidCard.

The object diagram ROYAL&LOYAL-2 below corresponds to another snapshot of the ROYAL&LOYAL class diagram. ROYAL&LOYAL-2, however, does not satisfy the constraint numberValidCard.

inv1false

(create-object-diagram ROYAL&LOYAL : ROYAL&LOYAL-2 .)
(insert-object ROYAL&LOYAL-2 : LoyaltyProgram : Advantage .)
(insert-object ROYAL&LOYAL-2 : Membership : memb1 .)
(insert-object ROYAL&LOYAL-2 : Customer : customer1 .)
(insert-object ROYAL&LOYAL-2 : CustomerCard : card1 .)
(insert-object ROYAL&LOYAL-2 : CustomerCard : card3 .)
(insert-object ROYAL&LOYAL-2 : ServiceLevel : s1 .)
(insert-attr-value ROYAL&LOYAL-2 : ServiceLevel : s1 : name : String -> "gold" .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer1 : name : String -> "John-Smith" .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer1 : title : String -> "Mr." .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer1 : isMale : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-2 : Customer : customer1 : age : Integer -> 35 .)
(insert-attr-value ROYAL&LOYAL-2 : CustomerCard : card1 : valid : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-2 : CustomerCard : card1 : color : Color -> silver .)
(insert-attr-value ROYAL&LOYAL-2 : CustomerCard : card1 : printedName : String -> "Mr.John-Smith" .)
(insert-attr-value ROYAL&LOYAL-2 : CustomerCard : card3 : valid : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-2 : CustomerCard : card3 : color : Color -> gold .)
(insert-attr-value ROYAL&LOYAL-2 : CustomerCard : card3 : printedName : String -> "Mr.John-Smith" .)
(insert-link ROYAL&LOYAL-2 | LoyaltyProgram : programs <-> participants : Customer | Advantage <-> customer1 .)
(insert-assoc-class-link ROYAL&LOYAL-2 | LoyaltyProgram : programs <-> participants : Customer | membership : Membership : membership | Advantage <-> customer1, memb1 .)
(insert-link ROYAL&LOYAL-2 | Customer : owner <-> cards : CustomerCard | customer1 <-> card1 .)
(insert-link ROYAL&LOYAL-2 | Customer : owner <-> cards : CustomerCard | customer1 <-> card3 .)
(insert-link ROYAL&LOYAL-2 | CustomerCard : card <-> membership : Membership | card1 <-> memb1 .) (insert-link ROYAL&LOYAL-2 | ServiceLevel : actualLevel <-> membership : Memebership | s1 <-> memb1 .)

Also relevant for the R&L model is that, when none of the services offered in a LoyaltyProgram credits or debits the LoyaltyAccount instances, these instances are useless and should not be present. The following invariant uselessLoyaltyAccount states that when the LoyaltyProgram does not have the possibility for earning or burning points, the members of the LoyaltyProgram do not have LoyaltyAccounts; that is, the collection of LoyaltyAccounts associated with the Memberships must be empty.

(insert-invariant ROYAL&LOYAL : LoyaltyProgram :
((self:LoyaltyProgram #partners)->collect(p:ProgramPartner | p:ProgramPartner #deliveredServices))
->forAll(s:Service | (((s:Service #pointsEarned) = 0 and (s:Service #pointsBurned) = 0)
implies
(((self:LoyaltyProgram #membership)->collect(m:Membership | (m:Membership #loyaltyaccount)))->isEmpty()))) .)

The object diagram ROYAL&LOYAL-1 below corresponds to a snapshot of the ROYAL&LOYAL class diagram.

invtrue

The following script loads the ROYAL&LOYAL-1 object diagram.

(create-object-diagram ROYAL&LOYAL : ROYAL&LOYAL-1 .)
(insert-object ROYAL&LOYAL-1 : LoyaltyProgram : Advantage .)
(insert-object ROYAL&LOYAL-1 : Service : s1 .)
(insert-object ROYAL&LOYAL-1 : ProgramPartner : IBM .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s1 : condition : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s1 : pointsEarned : Integer -> 0 .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s1 : pointsBurned : Integer -> 0 .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s1 : description : String -> "discount" .)
(insert-attr-value ROYAL&LOYAL-1 : ProgramPartner : IBM : name : String -> "IBM" .)
(insert-attr-value ROYAL&LOYAL-1 : ProgramPartner : IBM : numberOfCustomers : Integer -> 500 .)
(insert-link ROYAL&LOYAL-1 | LoyaltyProgram : programs <-> partners : ProgramPartner | Advantage <-> IBM .)
(insert-link ROYAL&LOYAL-1 | Service : deliveredServices <-> partner : ProgramPartner | s1 <-> IBM .)

The snapshot ROYAL&LOYAL-1 clearly satifies the constraint uselessLoyaltyAccount.

The object diagram ROYAL&LOYAL-2 below corresponds to another snapshot of the ROYAL&LOYAL class diagram. ROYAL&LOYAL-2, however, does not satisfy the constraint uselessLoyaltyAccount.

invfalse

The following script loads the ROYAL&LOYAL-2 object diagram.

(create-object-diagram ROYAL&LOYAL : ROYAL&LOYAL-2 .)
(insert-object ROYAL&LOYAL-2 : LoyaltyProgram : Advantage .)
(insert-object ROYAL&LOYAL-2 : ProgramPartner : IBM .)
(insert-object ROYAL&LOYAL-2 : Service : s1 .)
(insert-object ROYAL&LOYAL-2 : ServiceLevel : s2 .)
(insert-object ROYAL&LOYAL-2 : CustomerCard : card1 .)
(insert-object ROYAL&LOYAL-2 : Customer : customer1 .)
(insert-attr-value ROYAL&LOYAL-2 : Service : s1 : condition : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-2 : Service : s1 : pointsEarned : Integer -> 0 .)
(insert-attr-value ROYAL&LOYAL-2 : Service : s1 : pointsBurned : Integer -> 0 .)
(insert-attr-value ROYAL&LOYAL-2 : Service : s1 : description : String -> "discount" .)
(insert-attr-value ROYAL&LOYAL-2 : ProgramPartner : IBM : name : String -> "IBM" .)
(insert-attr-value ROYAL&LOYAL-2 : ProgramPartner : IBM : numberOfCustomers : Integer -> 500 .)
(insert-link ROYAL&LOYAL-2 | LoyaltyProgram : programs <-> partners : ProgramPartner | Advantage <-> IBM .)
(insert-link ROYAL&LOYAL-2 | Service : deliveredServices <-> partner : ProgramPartner | s1 <-> IBM .)
(insert-object ROYAL&LOYAL-2 : Membership : memb3 .)
(insert-object ROYAL&LOYAL-2 : LoyaltyAccount : la1 .)
(insert-attr-value ROYAL&LOYAL-2 : LoyaltyAccount : la1 : points : Integer -> 30 .)
(insert-link ROYAL&LOYAL-2 | Membership : membership <-> account : LoyaltyAccount | memb3 <-> la1 .)
(insert-link ROYAL&LOYAL-2 | LoyaltyProgram : programs <-> membership : Membership | Advantage <-> memb3 .)
(insert-link ROYAL&LOYAL-2 | ServiceLevel : actualLevel <-> membership : Membership | s2 <-> memb3 .)
(insert-link ROYAL&LOYAL-2 | CustomerCard : card <-> membership : Membership | card1 <-> memb3 .)
(insert-link ROYAL&LOYAL-2 | Customer : customer <-> cards : CustomerCard | customer1 <-> card1 .)

Inheritance

The advantage of using inheritance is that an object using superclass instances need not know about the subclasses. But sometimes you want to use the subclasses. In the R&L example, the program partners want to limit by adding the invariant maximumPoints the number of bonus points they give away; they have set a maximum of 10,000 points to be burned for each partner.

(insert-invariant ROYAL&LOYAL : LoyaltyProgram :
(((((self:LoyaltyProgram #partners)->collect(p:ProgramPartner | p:ProgramPartner #deliveredServices))
->collect(s:Service | s:Service #transactions))->collect(bt:Burning | bt:Burning #points))->sum()) < 10000 .)

The object diagram ROYAL&LOYAL-1 below corresponds to a snapshot of the ROYAL&LOYAL class diagram.

invtrue

The following script loads the ROYAL&LOYAL-1 object diagram.

(insert-object ROYAL&LOYAL-1 : LoyaltyProgram : Advantage .)
(insert-object ROYAL&LOYAL-1 : ProgramPartner : IBM .)
(insert-object ROYAL&LOYAL-1 : ProgramPartner : Iberia .)
(insert-object ROYAL&LOYAL-1 : ProgramPartner : BP .)
(insert-object ROYAL&LOYAL-1 : Service : s1 .)
(insert-object ROYAL&LOYAL-1 : Service : s2 .)
(insert-object ROYAL&LOYAL-1 : Service : s3 .)
(insert-attr-value ROYAL&LOYAL-1 : LoyaltyProgram : Advantage : name : String -> "String" .)
(insert-attr-value ROYAL&LOYAL-1 : ProgramPartner : IBM : numberOfCustomers : Integer -> 500 .)
(insert-attr-value ROYAL&LOYAL-1 : ProgramPartner : Iberia : numberOfCustomers : Integer -> 300 .)
(insert-attr-value ROYAL&LOYAL-1 : ProgramPartner : BP : numberOfCustomers : Integer -> 1000 .)
(insert-attr-value ROYAL&LOYAL-1 : ProgramPartner : IBM : name : String -> "IBM" .)
(insert-attr-value ROYAL&LOYAL-1 : ProgramPartner : Iberia : name : String -> "Iberia" .)
(insert-attr-value ROYAL&LOYAL-1 : ProgramPartner : BP : name : String -> "BP" .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s1 : condition : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s2 : condition : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s3 : condition : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s1 : pointsEarned : Integer -> 500 .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s2 : pointsEarned : Integer -> 400 .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s3 : pointsEarned : Integer -> 500 .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s1 : pointsBurned : Integer -> 300 .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s2 : pointsBurned : Integer -> 400 .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s3 : pointsBurned : Integer -> 400 .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s1 : description : String -> "discount" .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s2 : description : String -> "flightPoints" .)
(insert-attr-value ROYAL&LOYAL-1 : Service : s3 : description : String -> "travelMiles" .)
(insert-attr-value ROYAL&LOYAL-1 : Transaction : b1 : points : Integer -> 300 .)
(insert-attr-value ROYAL&LOYAL-1 : Transaction : b2 : points : Integer -> 400 .)
(insert-attr-value ROYAL&LOYAL-1 : Transaction : b3 : points : Integer -> 400 .)
(insert-link ROYAL&LOYAL-1 | LoyaltyProgram : programs <-> partners : ProgramPartner | Advantage <-> IBM .)
(insert-link ROYAL&LOYAL-1 | LoyaltyProgram : programs <-> partners : ProgramPartner | Advantage <-> Iberia .)
(insert-link ROYAL&LOYAL-1 | LoyaltyProgram : programs <-> partners : ProgramPartner | Advantage <-> BP .)
(insert-link ROYAL&LOYAL-1 | Service : deliveredServices <-> partner : ProgramPartner | s1 <-> IBM .)
(insert-link ROYAL&LOYAL-1 | Service : deliveredServices <-> partner : ProgramPartner | s2 <-> Iberia .)
(insert-link ROYAL&LOYAL-1 | Service : deliveredServices <-> partner : ProgramPartner | s3 <-> BP .)
(insert-link ROYAL&LOYAL-1 | Transaction : transactions <-> generatedBy : Service | b1 <-> s1 .)
(insert-link ROYAL&LOYAL-1 | Transaction : transactions <-> generatedBy : Service | b2 <-> s2 .)
(insert-link ROYAL&LOYAL-1 | Transaction : transactions <-> generatedBy : Service | b3 <-> s3 .)

The snapshot ROYAL&LOYAL-1 clearly satifies the constraint maximumPoints.

The object diagram ROYAL&LOYAL-2 below corresponds to another snapshot of the ROYAL&LOYAL class diagram. ROYAL&LOYAL-2, however, does not satisfy the constraint maximumPoints.

invfalse

The script to load the ROYAL&LOYAL-2 object diagram is analogous to the script used to load ROYAL&LOYAL-1 except for the following commands:

(insert-attr-value ROYAL&LOYAL-2 : Transaction : b1 : points : Integer -> 3000 .)
(insert-attr-value ROYAL&LOYAL-2 : Transaction : b2 : points : Integer -> 4000 .)
(insert-attr-value ROYAL&LOYAL-2 : Transaction : b3 : points : Integer -> 4000 .)

Working with Enumerations

Sometimes an enumeration type is defined as an attribute type in a UML class model. An example can be found in the CustomerCard class, where the attribute color can have two values, either silver or gold. The following invariant colorCard states that the color of this card must match the service level of the membership.

(insert-invariant ROYAL&LOYAL : Membership :
((((self:Membership #actualLevel@) #name = "Silver") implies ((self:Membership #card@) #color = silver))
and
(((self:Membership #actualLevel@) #name = "Gold") implies ((self:Membership #card@) #color = gold))) .)

The object diagram ROYAL&LOYAL-1 below corresponds to a snapshot of the ROYAL&LOYAL class diagram.

invtrue

The following script loads the ROYAL&LOYAL-1 object diagram.

(create-object-diagram ROYAL&LOYAL : ROYAL&LOYAL-1 .)
(insert-object ROYAL&LOYAL-1 : ServiceLevel : level1 .)
(insert-object ROYAL&LOYAL-1 : ServiceLevel : level2 .)
(insert-object ROYAL&LOYAL-1 : CustomerCard : card1 .)
(insert-object ROYAL&LOYAL-1 : CustomerCard : card2 .)
(insert-object ROYAL&LOYAL-1 : Customer : customer1 .)
(insert-object ROYAL&LOYAL-1 : Customer : customer2 .)
(insert-attr-value ROYAL&LOYAL-1 : ServiceLevel : level1 : name : String -> "Gold" .)
(insert-attr-value ROYAL&LOYAL-1 : ServiceLevel : level2 : name : String -> "Silver" .)
(insert-object ROYAL&LOYAL-1 : Membership : memb1 .)
(insert-object ROYAL&LOYAL-1 : Membership : memb2 .)
(insert-link ROYAL&LOYAL-1 | ServiceLevel : currentLevel <-> membership : Membership | level1 <-> memb1 .)
(insert-link ROYAL&LOYAL-1 | ServiceLevel : currentLevel <-> membership : Membership | level2 <-> memb2 .)
(insert-link ROYAL&LOYAL-1 | CustomerCard : card <-> membership : Membership | card1 <-> memb1 .)
(insert-link ROYAL&LOYAL-1 | CustomerCard : card <-> membership : Membership | card2 <-> memb2 .)
(insert-attr-value ROYAL&LOYAL-1 : CustomerCard : card1 : valid : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-1 : CustomerCard : card1 : color : Color -> silver .)
(insert-attr-value ROYAL&LOYAL-1 : CustomerCard : card1 : printedName : String -> "Mr.John-Smith" .)
(insert-attr-value ROYAL&LOYAL-1 : CustomerCard : card1 : valid : Boolean -> true .)
(insert-attr-value ROYAL&LOYAL-1 : CustomerCard : card1 : color : Color -> gold .)
(insert-attr-value ROYAL&LOYAL-1 : CustomerCard : card1 : printedName : String -> "Mrs.MaryPoppins" .) (insert-link ROYAL&LOYAL-1 | Customer : customer <-> cards : CustomerCard | customer1 <-> card1 .)
(insert-link ROYAL&LOYAL-1 | Customer : customer <-> cards : CustomerCard | customer2 <-> card2 .)
The snapshot ROYAL&LOYAL-1 clearly satifies the constraint colorCard.

The object diagram ROYAL&LOYAL-2 below corresponds to another snapshot of the ROYAL&LOYAL class diagram. ROYAL&LOYAL-2, however, does not satisfy the constraint colorCard.

invfalse

The script to load the ROYAL&LOYAL-2 object diagram is analogous to the script used to load ROYAL&LOYAL-1 except for the following command:

(insert-attr-value ROYAL&LOYAL-2 : CustomerCard : card1 : color : Color -> silver .)


You can download here the script of this example.

The Company Model

In this example we have modeled a company with employees, departments, and projects. A department can have any number of employees working for it and can control any number of projects. An employee can work in one or more departments and can participate on any number of projects. Each project is controlled by one department and can have any number of employees working on it. The example is borrowed from [Buettner, F. USE quick tour].

company-example

The following script initialises an ITP/OCL session and loads the COMPANY class diagram in the ITP/OCL database:


loop init-ocl .
(create-class-diagram COMPANY .)
(insert-class COMPANY : Employee .)
(insert-class COMPANY : Department .)
(insert-class COMPANY : Project .)
(insert-attr COMPANY : Employee (name, String) .)
(insert-attr COMPANY : Employee (salary, Integer) .)
(insert-attr COMPANY : Department (name, String) .)
(insert-attr COMPANY : Department (location, String) .)
(insert-attr COMPANY : Department (budget, Integer) .)
(insert-attr COMPANY : Project (name, String) .)
(insert-attr COMPANY : Project (budget, Integer) .)
(insert-assoc COMPANY : Employee : employee : < * > <-> < 1,* > : department : Department .)
(insert-assoc COMPANY : Employee : employee : < * > <-> < * > : project : Project .)
(insert-assoc COMPANY : Department : department : < 1 > <-> < * > : project : Project .)

The following OCL invariants add reasonable constraints to the COMPANY model, which however could not be specified using only diagrams.

  • The number of employees working in a department must be greater or equal to the number of projects controlled by the department.
    (insert-invariant COMPANY : Department : (self:Department #employee)->size() >= (self:Department #project)->size() .)
  • Employees get a higher salary when they work on more projects.
    (insert-invariant COMPANY :: ((Employee #allInstances)->forAll(e1:Employee | ((Employee #allInstances)->forAll(e2:Employee | (((e1:Employee #project)->size() > (e2:Employee #project)->size()) implies ((e1:Employee #salary) > (e2:Employee #salary))))))) .)
  • The budget of a project must not exceed the budget of the controlling department.
    (insert-invariant COMPANY : Project : ((self:Project #budget) <= (self:Project #department@) #budget) .)
  • Employees working on a project must also work in the controlling department.
    (insert-invariant COMPANY : Project : (((self:Project #department@)#employee)->includesAll(self:Project #employee)) .)

TWO BASIC SNAPSHOTS

As an example, consider the following snapshot COMPANY-1 of the class diagram COMPANY . Clearly, it fulfills all the invariants except for the one implicitely stated in the multiplicity of the WorksIn> association: the employees john and frank do not work for any department.

company1-snapshot

The following script loads the COMPANY-1 object diagram:

(create-object-diagram COMPANY : COMPANY-1 .)
(insert-object COMPANY-1 : Department : cs .)
(insert-attr-value COMPANY-1 : Department : cs : name : String -> "Computer Science" .)
(insert-attr-value COMPANY-1 : Department : cs : location : String -> "Bremen" .)
(insert-attr-value COMPANY-1 : Department : cs : budget : Integer -> 10000 .)
(insert-object COMPANY-1 : Employee : john .)
(insert-attr-value COMPANY-1 : Employee : john : name : String -> "John" .)
(insert-attr-value COMPANY-1 : Employee : john : salary : Integer -> 4000 .)
(insert-object COMPANY-1 : Employee : frank .)
(insert-attr-value COMPANY-1 : Employee : frank : name : String -> "Frank" .)
(insert-attr-value COMPANY-1 : Employee : frank : salary : Integer -> 4500 .)

When we type in the command:

(check-invariants COMPANY : COMPANY-1 .)

we obtain the expected negative result. It is easy to modify our snapshot so as to obtain a different result: for instance, if we assigned john and frank to the cs department, all the invariants are fulfilled.

company1WithLinks-snapshot

The following script assigns john and frank to the cs department.

(insert-link COMPANY-1 | Employee : employee <-> department : Department | john <-> cs .)
(insert-link COMPANY-1 | Employee : employee <-> department : Department | frank <-> cs .)

A MORE COMPLEX SNAPSHOT

Consider now the following snapshot COMPANY-2 of the class diagramCOMPANY

company2-snapshot

The following script loads the COMPANY-2 object diagram:

(create-object-diagram COMPANY : COMPANY-2 .)
(insert-object COMPANY-2 : Department : cs .)
(insert-attr-value COMPANY-2 : Department : cs : name : String -> "Computer Science" .)
(insert-attr-value COMPANY-2 : Department : cs : location : String -> "Bremen" .)
(insert-attr-value COMPANY-2 : Department : cs : budget : Integer -> 10000 .)
(insert-object COMPANY-2 : Employee : john .)
(insert-attr-value COMPANY-2 : Employee : john : name : String -> "John" .)
(insert-attr-value COMPANY-2 : Employee : john : salary : Integer -> 4000 .)
(insert-object COMPANY-2 : Employee : frank .)
(insert-attr-value COMPANY-2 : Employee : frank : name : String -> "Frank" .)
(insert-attr-value COMPANY-2 : Employee : frank : salary : Integer -> 4500 .)

(insert-link COMPANY-2 | Employee : employee <-> department : Department | john <-> cs .)
(insert-link COMPANY-2 | Employee : employee <-> department : Department | frank <-> cs .)

(insert-object COMPANY-2 : Project : research .)
(insert-attr-value COMPANY-2 : Project : research : name : String -> "Research" .)
(insert-attr-value COMPANY-2 : Project : research : budget : Integer -> 12000 .)
(insert-object COMPANY-2 : Project : teaching .)
(insert-attr-value COMPANY-2 : Project : teaching : name : String -> "Validating UML" .)
(insert-attr-value COMPANY-2 : Project : teaching : budget : Integer -> 3000 .)
(insert-link COMPANY-2 | Department : department <-> project : Project | cs <-> research .)
(insert-link COMPANY-2 | Department : department <-> project : Project | cs <-> teaching .)
(insert-link COMPANY-2 | Employee : employee <-> project : Project | frank <-> research .)
(insert-link COMPANY-2 | Employee : employee <-> project : Project | frank <-> teaching .)
(insert-link COMPANY-2 | Employee : employee <-> project : Project | john <-> research .)

Notice that COMPANY-2 fulfills all the constraints except for the one about projects' budget, because the budget of the research project exceeds indeed the budget of its controling department. When we type in the command:

(check-invariants COMPANY : COMPANY-2 .)

we obtain the expected negative result.

You can download here the script of this example.

Manuel Clavel and