# Example-Driven Modeling Using Clafer

Examples for the paper Example-Driven Modeling Using Clafer.

The model compiles and instantiates with Clafer/ClaferIG v0.4.2 (revised on 2015-10-20).

“We learn by example and by direct experience because there are real limits to the adequacy of verbal instruction.” –Malcolm Gladwell

# Points

We are trying to make:

• systematically using explicit examples for eliciting, modeling, verifying, and validating complex business knowledge
• model = examples + abstractions
• assumption: people can formulate simple abstractions directly (common sense)
• assumption: experts drop down to concrete examples to clarify difficult, exceptional, and corner-cases(cog-psy)
• different kinds of examples are useful, most notably:
• partial examples that naturally express person’s partial view of the world,
• near-miss, negative examples that show constraint violations
• contrasting examples that show alternative cases
• Clafer is a lightweight structural modeling language which naturally supports EDM with the following language features:
• support for untyped and partially typed examples
• support for specializing and extending both the examples and abstractions (easy extension + constraints can be used in both)
• examples and abstractions are easily expressed and can be easily mixed in the same model
• both examples and abstractions look the same in syntax and have unified semantics
• examples are by default partial
• full support of the reasoner - this makes the model playable: constraints can be checked and full completions of partial examples can be automatically generated.
• we’d like to show types of modeling scenarios and how they are supported by Clafer

# Scenario

Business domain modeling and requirements elicitation for a “Room Booking Software”.

Participants: Alice (SME), Bob (BA), Charlie (BA)

## Session 1: Bob and Alice

ALICE: Members of our organization often book rooms for meetings. Each meeting is organized by a chair and has at least one other participant. Each room has a maximum capacity it can hold. Depending on the room different equipment is available.

BOB: Please, give me examples of meetings and rooms.

ALICE: The mid-year review meeting always takes place in June. It is organized by Steven, our chair, and is held in the meeting room C. The room provides a whiteboard and audio-conferencing equipment to include online participants. Another example is an on-demand meeting organized within work hours. Joanna, a team-leader, sometimes meets other team members in room D. They use a whiteboard and have no online participants.

BOB writes down the examples, learns the domain and abstracts concepts to come up with a model.

Examples:

midYearReview : Meeting
month -> June
[ chair = Steven ]
[ room = C ]
Steven : Member
C : Room

(using redefinition would be)

midYearReview : Meeting
month -> June
chair -> Steven
room -> C
[ some onlineParticipant ]

Steven : Member

C : Room
whiteboard
audioConferencing
ondemandMeeting : Meeting
[ chair = Joanna ]
[ room = D ]
Joanna : Member
D : Room

(using redefinition would be)

ondemandMeeting : Meeting
chair -> Joanna
[ no onlineParticipant ]
room -> D

Joanna : Member

D : Room
whiteboard

Abstractions:

• Bob also makes reasonable assumptions about the numbers of participants and online participants and their relation to room capacity. Also no members can be both a participant and onlineParticipant at the same time.*
abstract Meeting
chair -> Member
[ this not in participant.dref ]
[ this not in onlineParticipant.dref ]
participant -> Member +
onlineParticipant -> Member *
room -> Room
[ this.capacity >= # participant + 1 ]
time -> integer
whiteboard -> Whiteboard
rep -> Rep
enum Month = June | July
abstract Member

BOB: So we have 3 main concepts: Meeting, Room, Member. The participants are on-site members or join remotely. There is one distinguished member: the chair. I assume there must be at least one participant other than a chair to call a meeting. I also assume that the chair is not part of the list of participants and that online participants do not count for room capacity calculation.

ALICE: Yes, these assumptions are correct.

BOB: I have one question. Are all types of the equipment available in each meeting room? For example, can there be a meeting room without audioConferencing equipment?

ALICE: Well, each room provides either a traditional or an electronic whiteboard. All other equipment is optional (such as projectors and computers). Only if the meeting includes remote participants, must the room offer at least audio-conferencing equipment.

BOB: Aha, an important constraint must be added!

Bob adds the constraint [ some onlineParticipant => room.audioConferencing ] to the Meeting.

abstract Room
capacity -> integer
num -> integer
or whiteboard ?
electronic
projector ?
computer ?
audioConferencing ?

Next, Bob verifies his model.

Bob creates a few Members, who could chair or participate in meetings in addition to Steven and Joanna.

Al : Member
Ben : Member
Carl : Member
Dennise : Member
Ed : Member
Fran : Member
Georgia : Member
Hellen : Member

Next, Bob generates a series of completions of his model.

One completion is shown below.

June
July
Al
Ben
Carl
Dennise
Ed
Fran
Georgia
Hellen
midYearReview
month = June
chair$1 = Steven participant$1 = Ed
participant$2 = Ben participant$3 = Joanna
onlineParticipant = Hellen
room$1 = C Steven C capacity$1 = 12
whiteboard$1 traditional audioConferencing ondemandMeeting chair$2 = Joanna
participant$4 = Ben participant$5 = Al
room$2 = D Joanna D capacity$2 = 13
whiteboard$2 electronic For each generated completion, Bob asks Alice to confirm whether the completion is valid or invalid. ALICE: all examples I’ve seen are correct. BOB: can you think of an invalid example? ALICE: For example, say Al invites Ben, Carl, Ed, Fran, and Hellen into a small room E with capacity 4. Al also invites Dennise and Fran to participate online. The room E does not have audio conferencing equipment. Such a situation should not be allowed. BOB: let’s see whether it is allowed by our model so far. Bob constructs a negative example and attempts to instantiate the model. badMeeting : Meeting [ chair = Al ] [ room = E ] E : Room [ capacity = 4 ] Clafer Instance Generator responds: No more instances found. Try increasing scope to get more instances. The following set of constraints cannot be satisfied in the current scope. 1) onlineParticipant = Dennise, Fran (line 36, column 6) 2) no audioConferencing (line 41, column 6) 3) some onlineParticipant => room.audioConferencing (line 10, column 7) 4) participant = Ben, Carl, Ed, Fran, Hellen (line 33, column 4) 5) this.capacity >= # participant + 1 (line 9, column 11) Altering the following constraints produced the following near-miss example: 1) removed participant = Ben, Carl, Ed, Fran, Hellen 2) removed onlineParticipant = Dennise, Fran E capacity = 4 whiteboard traditional projector Al Ben Carl Dennise Ed Fran Georgia Hellen badMeeting chair = Al participant = Hellen room = E BOB: IG reported that constraints 1)-5) are mutually contradicting. Actually, constraints 1)-3) are mutually contradicting as well as constraints 4) and 5). IG removed one constraint from each group (UnSAT Core) to produce a near-miss instance. The resulting near-miss example shows that there cannot be any online participants and that Ben, Carl, Ed, Fran, Hellen cannot participate because that exceeds room’s capacity. ## Session 2: Charlie and Alice The first session between Alice and Charlie goes as follows. ALICE: We need to keep track of bookings to ensure that rooms and people are not double-booked. Recently, for example, Sue, the head of research, had scheduled two meetings at the same day at 10am. CHARLIE: How did that happen? ALICE: First, she organized a meeting at 10am. The other meeting was organized by Sam also at 10am. Sue somehow understood that Sam wanted to attend her meeting and confirmed her attendance at Sam’s meeting. It wasn’t the first time that miscommunication happened. CHARLIE: I see. So how does Sue deal with conflicting meetings? ALICE: In several ways. First, she may cancel one of the meetings. Alternatively, she confirms only one of the meetings while keeping the other one unconfirmed. She can also confirm the two meetings but they cannot overlap. Sometimes she combines the two meetings into one if the topics are similar. Each employee should have a daily agenda of meetings. Based on that they should be able to confirm or decline each meeting. CHARLIE: That’s quite complex. I think I understand… Charlie writes down the possible ways of scheduling meetings. CD+ abstract Agenda mt -> Meeting * SueAgenda : Agenda m1 -> M1 ? m2 -> M2 ? M1 : Meeting ? M2 : Meeting ? [ time = 10 ] completion CD+->c1 SueAgenda_c1 : Agenda m1 -> M1_c1 m2 -> M2_c1 0 M1_c1 : Meeting 1 M2_c1 : Meeting 0 [ time = 10 ] completion CD+->c2 SueAgenda_c2 : Agenda m1 -> M1_c2 m2 -> M2_c2 ? M1_c2 : Meeting 1 [ time = 11 ] M2_c2 : Meeting ? [ time = 10 ] completion c1->c4 and c2->c4 SueAgenda_c4 : Agenda m1 -> M1_c4 M1_c4 : Meeting 1 [ time = 10 ] M2_c4 : Meeting 0 [ time = 10 ] completion c2->c6 SueAgenda_c6 : Agenda m1 -> M1_c6 m2 -> M2_c6 M1_c6 : Meeting [ time = 11 ] M2_c6 : Meeting [ time = 10 ] completion CD+->c3 SueAgenda6 m1 -> M1_6 m2 -> M2_6 M1_6 : Meeting 1 M2_6 : Meeting 1 time -> 10 M12_6 : M1, M2 ## Session 3: Bob and Alice The second session between Alice and Bob goes as follows. ALICE: Each meeting is organized by a chair who is responsible for booking the room. Chair also notifies other participants about the meeting. Rooms have different equipment, and obviously, different numbers. CD I Sue : Member SM : Meeting [ chair = Sue ] BOB: Let’s understand a concrete meeting. Could you please give me an example of room booking? What equipment is used? ALICE: Sure. For example, Sue organizes meetings for her research group. They use an electronic whiteboard, as it simplifies sharing notes online. Bob writes down the example Bob I SM_BobI : Meeting [ chair = Sue ] [ room = R_BobI ] R_BobI : Room enum Whiteboard = Electronic | Traditional BOB: Perfect. Do all rooms have an electronic whiteboard? ALICE: No. All rooms have a traditional whiteboard, but only some rooms offer the electronic one. Bob completes the example Bob II SM_BobII : Meeting [ chair = Sue ] [ room = R_BobII ] R_BobII : ERoom abstract ERoom : Room ## Session 4: Charlie and Alice The second session between Alice and Charlie goes as follows. ALICE: As you may know, each meeting is organized by a chair. BOB: Right, such as Sue. Alice, how often are the meetings scheduled? Can you give me a concrete example? ALICE: For example, Sue organizes weekly meetings at 10am. They discuss progress done on research projects. Charlie writes down the example Charlie SM_Charlie : Meeting [ chair = Sue ] [ rep = Weekly ] [ time = 10 ] enum Rep = Daily | Weekly Based on the partial examples Bob and Charlie create an example that merges their knowledge. The partial object diagram is a combination of Charlie’s example and Bob’s refined example. Fortunately, there are no conflicts in the merged example. CD II SM_CDII : Meeting [ chair = Sue ] [ rep = Weekly ] [ time = 10 ] [ room = R_BobII ] ## Session 5: Bob, Charlie, and Alice There is, however, still one unknown: the room number num where Sue meets her group. The two BAs propose a class diagram that provides an abstraction for meetings. Abstractions generalize information to improve understanding of a set of examples. The BAs were able to construct the class diagram only after consolidating their partial knowledge. OD SM_OD : Meeting [ chair = Sue ] [ rep = Weekly ] [ time = 10 ] [ room = R_OD ] R_OD : ERoom [ num = 200 ] BOB, CHARLIE: Is the final combined example valid? ALICE: Yes, it seems valid; however, I am not sure since our model is already quite complex. Could you please show me a complete instantiation? BOB: Sure. Bob generates a few completions of the integrated example. Hellen Sue Electronic Traditional Daily Weekly SM_OD chair = Sue participant = Hellen room = R_OD time = 10 whiteboard$1 = Electronic
rep = Weekly
R_OD
capacity = 21
num = 200
whiteboard\$2
electronic

ALICE: That looks great!