Kĩ thuật lập trình - Lecture 11: Specifying systems – state diag’s & ocl

Ivan MarsicRutgers UniversityLECTURE 11: Specifying Systems – State Diag’s & OCL1TopicsUML State Machine DiagramsState Activities: Entry, Do, and Exit ActivitiesComposite States and Nested StatesConcurrencyUML Object Constraint Language (OCL)OCL SyntaxOCL Constraints and Contracts2State Machine Diagram:Basic NotationDelistedListing plannedTradedinitial-listingtradebankruptcy, merger, acquisition, States of Stock_iinitial stateindicated byterminal stateindicated byeventtransitionThese are not states:They are only labels that indicate the actual initial/terminal states3UML Diagrams Differ from FSMsModularization of statesConcurrent behaviorsState activities4States of Stock_itradetradetradetradetradetradetradetradeBuySellHoldTradedBuySellHoldListing plannedDelistedDelistedListing plannedTradedinitial-listingtradebankruptcy, merger, acquisition, composite statesub-states:(based on analyst recommendations)5States of Stock_iDelistedIPO plannedTradedinitial-listingtradebankruptcy, acquisition, merger, TradedIPO plannedDelistedtradetradetradetradetradetradetradetradeBuySellHoldinitial-listingbankruptcy, acquisition, merger, IPO = initial public offeringcomposite statenestedstate6State Activities:Entry, Do, and Exit Activitiesmatchedcompletion transitioncancel,rejectviewtradeExecutedArchivedCancelledsubmitdataentryInPreparation Pendingdo: check_price & supply [buy] check_price & demand [sell]States of a Trading Order“do”stateactivity(order placed and waiting for the specified market conditions)7timer-expired /signal-reset,set numOfAttemps := 0User leaves without succeeding or blockingautoLockInterval-expired /Auto-locking feature not shown!State Diagram for Controller[ Recall Section 2.7.4: Test Coverage and Code Coverage ]invalid-key [numOfAttemps  maxNumOfAttempts] / signal-failureinvalid-key / signal-failureinvalid-key[numOfAttemps  maxNumOfAttempts] / sound-alarmBlockedLockedAcceptingvalid-key / signal-successvalid-key / signal-success,set numOfAttemps := 0UnlockedNote how the object responds differently to the same event (invalid-key in Accepting state), depending on which events preceded itHow state diagram motivates you to consider alternative usage scenarios and provides “crutches”:8invalid-key [numOfAttemps  maxNumOfAttempts] / signal-failureinvalid-key / signal-failureinvalid-key[numOfAttemps  maxNumOfAttempts] / sound-alarmautoLockInterval-expired /timer-expired /signal-reset,set numOfAttemps := 0BlockedLocked Acceptingentry: start timerdo: countdownvalid-key / signal-successvalid-key / signal-success Unlockedentry: start timerdo: countdownState Diagram for ControllerNeed “entry” and “do” state activities for countdown timers9State “Accepting” RefinedAcceptinginvalid-key / signal-failureinvalid-key /sound-alarmtimer-expired /signal-reset,set numOfAttemps := 0valid-key / signal-successvalid-key / signal-successinvalid-key / signal-failureinvalid-key / signal-failureTwoMaxNumOfAttemptsOnevalid-key / signal-successOr, get rid of state “Accepting” and introduce state “Zero” 10Problem: States of a Hotel Roommake-reservation /arrive /depart /VacantOccupiedReservedProblem: but a guest may be occupying the room while it is reserved by a future guest!? or the room may be vacantwhile reserved by a future guest!? need a notion of time (“timing diagram”)11Problem: States of a Hotel RoomVacantReservedTime [days]OccupiedReservedby guest BC make-reservation C arrive C departReservedby guest CA arriveA departB make-reservationB arriveB departStates12Problem: States of a Hotel RoomVacantReservedTime [days]OccupiedReservedby guest BC make-reservation C arrive C departReservedby guest CA arriveA departB make-reservationB arriveB departWhat state? What if the guest is late? – “Holding” state? What if the room is overbooked? What when it is being cleaned?Issue: state transitions are weird—”Reserved” is a future state but transitioned to by a current event!13Object:Reservation tableObject:Room occupancyProblem: States of a Hotel RoomVacantReservedTime [days]OccupiedReservedby guest BC make-reservationReservedby guest CA arriveA departB make-reservationAvailablecurrent timeSOLUTION:Introduce a new object!reservefreeObjects send messages that change states14Problem: States of a Hotel RoomVacantReservedTime [days]Occupied C arrive C departA arriveA departB arriveB departAvailablecurrent timeObject 2:Reservation tableObject 1:Room occupancyWe need two objects:One tracks room’s current state (occupancy)and the other its future state (reservation)15OCL: Object Constraint LanguageOCL is used in UML diagrams towrite constraints in class diagramsguard conditions in state and activity diagramsbased on Boolean logicBoolean expressions (“OCL constraints”) used to state facts about elements of UML diagramsThe implementation must ensure that the constraints always hold true16Basic OCL Types and Operations*TypeValuesOperationsBooleantrue, falseand, or, xor, not, implies, if-then-elseInteger1, 48, 3, 84967, *, , , /, abs()Real0.5, 3.14159265, 1.e+5*, , , /, floor()String'With more exploration comes more text.'concat(), size(), substring()17OCL: Types of Navigation Class_A– attribute1– attribute2– (a) Local attribute(b) Directly related class(c) Indirectly related class Class_A Class_B**assocBAassocAB Class_A Class_B** Class_C**assocBAassocABassocCBassocBCWithin Class_A:self.attribute2Within Class_A:self.assocABWithin Class_A:self.assocAB.assocBC18Accessing Collections in OCL*OCL NotationMeaningEXAMPLE OPERATIONS ON ALL OCL COLLECTIONSc->size()Returns the number of elements in the collection c.c->isEmpty()Returns true if c has no elements, false otherwise.c1->includesAll(c2)Returns true if every element of c2 is found in c1.c1->excludesAll(c2)Returns true if no element of c2 is found in c1.c->forAll(var | expr)Returns true if the Boolean expression expr true for all elements in c. As an element is being evaluated, it is bound to the variable var, which can be used in expr. This implements universal quantification .c->forAll(var1, var2 | expr)Same as above, except that expr is evaluated for every possible pair of elements from c, including the cases where the pair consists of the same element.c->exists(var | expr)Returns true if there exists at least one element in c for which expr is true. This implements existential quantification .c->isUnique(var | expr)Returns true if expr evaluates to a different value when applied to every element of c.c->select(expr)Returns a collection that contains only the elements of c for which expr is true.EXAMPLE OPERATIONS SPECIFIC TO OCL SETSs1->intersection(s2)Returns the set of the elements found in s1 and also in s2.s1->union(s2)Returns the set of the elements found either s1 or s2.s->excluding(x)Returns the set s without object x.EXAMPLE OPERATION SPECIFIC TO OCL SEQUENCESseq->first()Returns the object that is the first element in the sequence seq.19OCL Constraints and ContractsA contract specifies constraints on the class state that must be valid always or at certain times, such as before or after an operation is invokedThree types of constraints in OCL: invariants, preconditions, and postconditionsAn invariant must always evaluate to true for all instance objects of a class, regardless of what operation is invoked and in what orderapplies to a class attributeA precondition is a predicate that is checked before an operation is executedapplies to a specific operation; used to validate input parametersA postcondition is a predicate that must be true after an operation is executedalso applies to a specific operation; describes how the object’s state was changed by an operation20Example Constraints (1)Invariant: the maximum allowed number of failed attempts at disarming the lock must be a positive integercontext Controller inv: self.getMaxNumOfAttempts() > 0Precondition: to execute enterKey() the number of failed attempts must be less than the maximum allowed numbercontext Controller::enterKey(k : Key) : boolean pre: self.getNumOfAttempts()  self.getMaxNumOfAttempts()21Example Constraints (2)The postconditions for enterKey() are(Poc1) a failed attempt is recorded(Poc2) if the number of failed attempts reached the maximum allowed, the system blocks and the alarm bell blurtsReformulate (Poc1) to:(Poc1) if the key is not element of the set of valid keys, then the counter of failed attempts after exiting from enterKey() must be by one greater than before entering enterKey() context Controller::enterKey(k : Key) : Boolean-- postcondition (Poc1):post: let allValidKeys : Set = self.checker.validKeys() if allValidKeys.exists(vk | k = vk) then getNumOfAttempts() = getNumOfAttempts()@pre else getNumOfAttempts() = getNumOfAttempts()@pre + 1-- postcondition (Poc2):post: getNumOfAttempts() >= getMaxNumOfAttempts() implies self.isBlocked() and self.alarmCtrl.isOn()22xUnit / JUnit assert_*_()Verification is usually done using the assert_*_() methods that define the expected state and raise errors if the actual state differs == (2 * 2));assertEquals(expected, actual);assertNull(Object object);etc.23TLA+ Specification[closed, unlit][open, lit][closed, lit]turnLightOff(?)unlock(valid key)unlock(valid key)locklock,unlock(invalid key)lock,unlock(invalid key)MAIN CONFUSION:What is this state diagram representing?The state of _what_ object?24