Wiki
Clone wikiCafeOBJ / OSEK / contents / index-e / backup / 20_Systemservices / 5_Even_Controt
Event control
Registration of events
Observation which returns a set of registered events:
#!python module DECLARED-EVENT { imports { ex(OBSERVATION2EVENTS) } signature { op declaredEvent : -> Observation2Events } }
Registration of events:
#!python module DECLARE-EVENT { imports { ex(REGISTRATION) ex(DECLARE) ex(INTERFACE) } signature { op DeclareEvent : Event -> Registration } axioms { vars C : System vars E : Event eq state(DeclareEvent(E)(C)) = declare(E)(state(C)) . } }
Transitions
Raising events:
#!python module OCCUR { imports { ex(RAISE) pr(EXTENDED) } signature { op occur : Extended Mask -> Raise } axioms { vars C : State vars T : Extended vars M : Mask eq owner(event(occur(T,M))) = T . eq mask(event(occur(T,M))) = M . } }
Clearing events:
#!python module REMOVE { imports { ex(CLEAR) pr(EXTENDED) pr(CURRENT) } signature { op remove : Extended Mask -> Clear } axioms { vars C : State vars T : Extended vars M : Mask eq owner(event(remove(T,M))) = T . eq mask(event(remove(T,M))) = M . cq (current(C) = owner(event(remove(T,M)))) = true if pre(remove(T,M),C) . } }
System services
SetEvent:
#!python module SET-EVENT { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(EVENT-COMPOSITION) pr(OCCUR) pr(RELEASE) pr(SUSPENDED) pr(ISR) pr(CURRENT) pr(OCCURRENCE) pr(WAITING-MASK) pr(NORMAL) pr(API-ERROR) } signature { op SetEvent : Extended Mask -> SystemService } axioms { vars C : System vars X : Extended vars M : Mask cq pre(occur(X,M)(state(C))) = true if pre(SetEvent(X,M)(C)) . cq occurrence(X(state(C)) > 0 = true if pre(SetEvent(X,M)(C)) . cq isExtended(X) = true if pre(SetEvent(X,M)(C)) . cq not(suspended(X)(state(C))) = true if pre(SetEvent(X,M)(C)) . cq (isISR(current(state(C))) or isTask(current(state(C)))) = true if pre(SetEvent(X,M)(C)) . cq state(SetEvent(X,M)(C)) = release(X),occur(X,M)(state(C))) if pre(SetEvent(X,M)(C) and waiting(X)(state(C)) and mask(X)(state(C)) == M . cq state(SetEvent(X,M)(C)) = occur(X,M)(state(C)) if pre(SetEvent(X,M)(C) and (~(waiting(X)(state(C))) or mask(X)(state(C)) =/= M) . cq status(SetEvent(X,M)(C)) = E-OK if pre(SetEvent(X,M)(C) . cq status(SetEvent(X,M)(C)) = E-OS-ID if occurrence(X(state(C)) == 0 . cq status(SetEvent(X,M)(C)) = E-OS-ACCESS if not(isExtended(X)) . cq status(SetEvent(X,M)(C)) = E-OS-STATE if suspended(X)(state(C)) . } }
ClearEvent:
#!python module CLEAR-EVENT { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(EVENT-COMPOSITION) pr(REMOVE) pr(SUSPENDED) pr(ISR) pr(CURRENT) pr(NORMAL) pr(API-ERROR) } signature { op ClearEvent : Mask -> SystemService } axioms { vars C : System vars M : Mask cq pre(remove(current(state(C)),M)(state(C)) = true if pre(ClearEvent(M)(C)) . cq state(ClearEvent(M)(C)) = remove(current(state(C)),M)(state(C)) if pre(ClearEvent(M)(C) . cq status(ClearEvent(M)(C)) = E-OK if pre(ClearEvent(M)(C) . cq status(ClearEvent(M)(C)) = E-OS-ACCESS if isTask(current(state(C))) andnot(isExtended(current(state(C)))) . cq status(ClearEvent(M)(C)) = E-OS-CALLEVEL if isISR(current(state(C))) . } }
GetEvent:
#!python module GET-EVENT { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(RESULT-MASK-STATE) pr(WAITING-MASK) pr(SUSPENDED) pr(OCCURRENCE) pr(NORMAL) pr(API-ERROR) } signature { op GetEvent : Extended -> SystemService } axioms { vars C : System vars X : Extended cq occurrence(X(state(C)) > 0 = true if pre(GetEvent(X)(C)) . cq isExtended(X) and not(suspended(X)(state(C))) true if pre(GetEvent(X)(C) . eq state(GetEvent(X)(C)) = state(C) . cq maskState,result(GetEvent(X)(C))) = mask(X)(state(C)) if pre(GetEvent(X)(C) . cq status(GetEvent(X)(C)) = E-OK if pre(GetEvent(X)(C) . cq status(GetEvent(X)(C)) = E-OS-ID if occurrence(X(state(C)) == 0 . cq status(GetEvent(X)(C)) = E-OS-ACCESS if not(isExtended(X)) . cq status(GetEvent(X)(C)) = E-OS-STATE if suspended(X)(state(C)) . } }
WaitEvent:
#!python module WAIT-EVENT { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(WAIT) pr(RELEASE) pr(RAISED) pr(ISR) pr(EVENT-COMPOSITION) pr(CURRENT) pr(NORMAL) pr(API-ERROR) } signature { op WaitEvent : Mask -> SystemService } axioms { vars C : System vars X : Extended vars M : Mask cq pre(wait(current(state(C)),M)(state(C)) = true if pre(WaitEvent(M)(C) . cq state(WaitEvent(M)(C)) = release(current(state(C))),wait(current(state(C)),M)(state(C))) if pre(WaitEvent(M)(C) and comp(current(state(C)),M) @ raised(state(C)) . cq state(WaitEvent(M)(C)) = wait(current(state(C)),M)(state(C)) if pre(WaitEvent(M)(C) andnot(comp(current(state(C)),M) @ raised(state(C))) . cq status(WaitEvent(M)(C)) = E-OK if pre(WaitEvent(M)(C) . cq status(WaitEvent(M)(C)) = E-OS-ACCESS if isTask(current(state(C))) andnot(isExtended(current(state(C)))) . cq status(WaitEvent(M)(C)) = E-OS-RESOURCE if occupied(current(state(C)))(state(C)) =/= nil . cq status(WaitEvent(M)(C)) = E-OS-CALLEVEL if isISR(current(state(C))) . } }
Updated