Wiki
Clone wikiCafeOBJ / OSEK / contents / index-e / backup / 20_Systemservices / 6_Alarms
Alarm
Registration of alarms
Registration of alarms:
#!python module DECLARE-ALARM { imports { ex(REGISTRATION) ex(DECLARE) ex(INTERFACE) } signature { op DeclareAlarm : Alarm -> Registration } axioms { vars C : System vars A : Alarm eq state(DeclareAlarm(A)(C)) = declare(A)(state(C)) . } }
Observations
Observation of declared alarm:
#!python module DECLARED-ALARM { imports { ex(OBSERVATION2ALARMS) } signature { op declaredAlarm : -> Observation2Alarms } }
Observation of cycles:
#!python module CYCLE { imports { ex(OBSERVATION2NAT) pr(ALARM) } signature { op cycle : Alarm -> Observation2Nat } }
Observation of deadline:
#!python module DEADLINE { imports { ex(OBSERVATION2NAT) pr(ALARM) } signature { op deadline : Alarm -> Observation2Nat } }
Observation of remainder:
#!python module REMAINDER { imports { ex(OBSERVATION2INT) } signature { op remainder : -> Observation2Int } }
Observation of now:
#!python module NOW { imports { ex(OBSERVATION2NAT) pr(ALARM) } signature { op now : Alarm -> Observation2Nat } }
Observation of used-alarm:
#!python module USED-ALARM { imports { ex(OBSERVATION2ALARMS) } signature { op usedAlarm : -> Observation2Alarms } }
Transitions
Cancel alarms:
#!python module CANCEL { imports { ex(TRANSITION) pr(USED-ALARM) } signature { op cancel : Alarm -> Transition } axioms { vars C : State vars A : Alarm cq A @ usedAlarm(C) = true if pre(cancel(A)(C)) . eq usedAlarm(cancel(A)(C)) = usedAlarm(C) \ A . eq rev(usedAlarm,cancel(A)) = true . } }
Expiration of alarms:
#!python module EXPIRE { imports { pr(COMPLEMENT) ex(TRANSITION) pr(ASSIGNMENT) pr(NOW) pr(DEADLINE) } signature { op expire : Alarm -> Transition } axioms { vars C : State vars A : Alarm cq expire(A)(C) = alarm2Transition(A)(C) if now(A)(C) == deadline(A)(C) . cq expire(A)(C) = C if now(A)(C) =/= deadline(A)(C) . } }
Set absolute values:
#!python module SET-ABS { imports { ex(TRANSITION) pr(DECLARED-ALARM) pr(USED-ALARM) pr(DEADLINE) pr(CYCLE) pr(ALARM-BASE) } signature { op setAbs : Alarm Nat Nat -> Transition } axioms { vars C : State vars A : Alarm vars N M : Nat cq A @ declaredAlarm(C) = true if pre(setAbs(A,N,M)(C)) . cq (A @ usedAlarm(C)) = false if pre(setAbs(A,N,M)(C)) . cq (0 <= N and N <= maxallowedvalue(alarmBase(A))) = true if pre(setAbs(A,N,M)(C)) . cq (M =/= 0 implies (mincycle(alarmBase(A)) <= M and M <= maxallowedvalue(alarmBase(A)))) = true if pre(setAbs(A,N,M)(C)) . cq deadline(A)(setAbs(A,N,M)(C)) = N if pre(setAbs(A,N,M)(C)) . cq cycle(A)(setAbs(A,N,M)(C)) = M if pre(setAbs(A,N,M)(C)) . cq usedAlarm(setAbs(A,N,M)(C)) = usedAlarm(C), A if pre(setAbs(A,N,M)(C)) . eq rev(deadline(A),setAbs(A,N,M)) = true . eq rev(cycle(A),setAbs(A,N,M)) = true . eq rev(usedAlarm,setAbs(A,N,M)) = true . } }
Set relative values:
#!python module SET-REL { imports { ex(TRANSITION) pr(DECLARED-ALARM) pr(USED-ALARM) pr(NOW) pr(DEADLINE) pr(CYCLE) pr(ALARM-BASE) } signature { op setRel : Alarm Nat Nat -> Transition } axioms { vars C : State vars A : Alarm vars N M : Nat cq A @ declaredAlarm(C) = true if pre(setRel(A,N,M)(C)) . cq (A @ usedAlarm(C)) = false if pre(setRel(A,N,M)(C)) . cq (0 <= N and N <= maxallowedvalue(alarmBase(A))) = true if pre(setRel(A,N,M)(C)) . cq (M =/= 0 implies (mincycle(alarmBase(A)) <= M and M <= maxallowedvalue(alarmBase(A)))) = true if pre(setRel(A,N,M)(C)) . cq now(A)(setRel(A,N,M)(C)) = 0 if pre(setRel(A,N,M)(C)) . cq deadline(A)(setRel(A,N,M)(C)) = N if pre(setRel(A,N,M)(C)) . cq cycle(A)(setRel(A,N,M)(C)) = M if pre(setRel(A,N,M)(C)) . cq usedAlarm(setRel(A,N,M)(C)) = usedAlarm(C), A if pre(setRel(A,N,M)(C)) . eq rev(now(A),setRel(A,N,M)) = true . eq rev(deadline(A),setRel(A,N,M)) = true . eq rev(cycle(A),setRel(A,N,M)) = true . eq rev(usedAlarm,setRel(A,N,M)) = true . } }
Increase counter:
#!python module TICK { imports { ex(TRANSITION) pr(ALARM) pr(NAT) pr(NOW) } signature { op tick : Alarm Nat -> Transition } axioms { vars C : State vars A : Alarm vars N : Nat eq now(A)(tick(A,N)(C)) = now(A)(C) + N . eq rev(now(A),tick(A,N)) = true . } }
System services
GetAlarmBaseļ¼
#!python module GET-ALARM-BASE { imports { pr(COMPLEMENT) pr(INTERFACE) pr(ALARM-BASE) ex(SYSTEM-SERVICE) pr(DECLARED-ALARM) ex(RESULT-ALARM-BASE) pr(NORMAL) pr(API-ERROR) } signature { op GetAlarmBase : Alarm -> SystemService } axioms { vars C : System vars A : Alarm cq A @ declaredAlarm(state(C)) = true if pre(GetAlarmBase(A)(C)) . eq state(GetAlarmBase(A)(C)) = state(C) . cq alarmBase,result(GetAlarmBase(A)(C))) = alarmBase(A) if pre(GetAlarmBase(A)(C) . cq status(GetAlarmBase(A)(C)) = E-OK if pre(GetAlarmBase(A)(C) . cq status(GetAlarmBase(A)(C)) = E-OS-ID if not(A @ declaredAlarm(state(C))) . } }
GetAlarm:
#!python module GET-ALARM { imports { pr(COMPLEMENT) pr(ALARM-BASE) pr(INTERFACE) ex(SYSTEM-SERVICE) pr(DECLARED-ALARM) pr(USED-ALARM) pr(REMAINDER) pr(DEADLINE) pr(NOW) pr(NORMAL) pr(API-ERROR) } signature { op GetAlarm : Alarm -> SystemService } axioms { vars C : System vars A : Alarm cq A @ declaredAlarm(state(C)) = true if pre(GetAlarm(A)(C)) . cq A @ usedAlarm(state(C)) = true if pre(GetAlarm(A)(C)) . cq remainder,result(GetAlarm(A)(C))) = deadline(A)(state(C)) - now(A)(state(C)) if pre(GetAlarm(A)(C) . eq state(GetAlarm(A)(C)) = state(C) . cq status(GetAlarm(A)(C)) = E-OK if pre(GetAlarm(A)(C) . cq status(GetAlarm(A)(C)) = E-OS-ID if not(A @ declaredAlarm(state(C))) . cq status(GetAlarm(A)(C)) = E-OS-NOFUNC if not(A @ usedAlarm(state(C))) and A @ declaredAlarm(state(C)) . } }
SetRelAlarm:
#!python module SET-REL-ALARM { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(SET-REL) pr(NAT) pr(NORMAL) pr(API-ERROR) } signature { op SetRelAlarm : Alarm Nat Nat -> SystemService } axioms { vars C : System vars A : Alarm vars N M : Nat cq pre(setRel(A,N,M)(state(C))) = true if pre(SetRelAlarm(A,N,M)(C)) . cq state(SetRelAlarm(A,N,M)(C)) = setRel(A,N,M)(state(C)) if pre(SetRelAlarm(A,N,M)(C) . cq status(SetRelAlarm(A,N,M)(C)) = E-OK if pre(SetRelAlarm(A,N,M)(C) . cq status(SetRelAlarm(A,N,M)(C)) = E-OS-ID if not(A @ declaredAlarm(state(C))) . cq status(SetRelAlarm(A,N,M)(C)) = E-OS-STATE if A @ usedAlarm(state(C)) . cq status(SetRelAlarm(A,N,M)(C)) = E-OS-VALUE if not(0 <= N and N <= maxallowedvalue(alarmBase(A))) . cq status(SetRelAlarm(A,N,M)(C)) = E-OS-VALUE if not(M =/= 0 implies (mincycle(alarmBase(A)) <= M and M <= maxallowedvalue(alarmBase(A)))) . } }
SetAbsAlarm:
#!python module SET-ABS-ALARM { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(SET-ABS) pr(NAT) pr(NORMAL) pr(API-ERROR) } signature { op SetAbsAlarm : Alarm Nat Nat -> SystemService } axioms { vars C : System vars A : Alarm vars N M : Nat cq pre(setAbs(A,N,M)(state(C))) = true if pre(SetAbsAlarm(A,N,M)(C)) . cq state(SetAbsAlarm(A,N,M)(C)) = setAbs(A,N,M)(state(C)) if pre(SetAbsAlarm(A,N,M)(C) . cq status(SetAbsAlarm(A,N,M)(C)) = E-OK if pre(SetAbsAlarm(A,N,M)(C) . cq status(SetAbsAlarm(A,N,M)(C)) = E-OS-ID if not(A @ declaredAlarm(state(C))) . cq status(SetAbsAlarm(A,N,M)(C)) = E-OS-STATE if A @ usedAlarm(state(C)) . cq status(SetAbsAlarm(A,N,M)(C)) = E-OS-VALUE if not(0 <= N and N <= maxallowedvalue(alarmBase(A))) . cq status(SetAbsAlarm(A,N,M)(C)) = E-OS-VALUE if not(M =/= 0 implies (mincycle(alarmBase(A)) <= M and M <= maxallowedvalue(alarmBase(A)))) . } }
CancelAlarm:
#!python module CANCEL-ALARM { imports { pr(COMPLEMENT) pr(ALARM-BASE) pr(INTERFACE) ex(SYSTEM-SERVICE) pr(DECLARED-ALARM) pr(CANCEL) pr(NORMAL) pr(API-ERROR) } signature { op CancelAlarm : Alarm -> SystemService } axioms { vars C : System vars A : Alarm cq pre(cancel(A)(state(C)) = true if pre(CancelAlarm(A)(C)) . cq state(CancelAlarm(A)(C)) = cancel(A)(state(C)) if pre(CancelAlarm(A)(C) . cq status(CancelAlarm(A)(C)) = E-OK if pre(CancelAlarm(A)(C) . cq status(CancelAlarm(A)(C)) = E-OS-ID if not(A @ declaredAlarm(state(C))) . cq status(CancelAlarm(A)(C)) = E-OS-NOFUNC if not(A @ usedAlarm(state(C))) and A @ declaredAlarm(state(C)) . } }
Updated