SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause copyrights: - Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) enabled-by: true functional-type: action links: - role: interface-function uid: ../if/server-fire-when post-conditions: - name: Status states: - name: Ok test-code: | T_rsc_success( ctx->status ); text: | The return status of ${../if/server-fire-when:/name} shall be ${../../status/if/successful:/name}. - name: NotDef test-code: | T_rsc( ctx->status, RTEMS_NOT_DEFINED ); text: | The return status of ${../if/server-fire-when:/name} shall be ${../../status/if/not-defined:/name} - name: InvId test-code: | T_rsc( ctx->status, RTEMS_INVALID_ID ); text: | The return status of ${../if/server-fire-when:/name} shall be ${../../status/if/invalid-id:/name}. - name: InvAddr test-code: | T_rsc( ctx->status, RTEMS_INVALID_ADDRESS ); text: | The return status of ${../if/server-fire-when:/name} shall be ${../../status/if/invalid-address:/name}. - name: InvClock test-code: | T_rsc( ctx->status, RTEMS_INVALID_CLOCK ); text: | The return status of ${../if/server-fire-when:/name} shall be ${../../status/if/invalid-clock:/name}. - name: IncStat test-code: | T_rsc( ctx->status, RTEMS_INCORRECT_STATE ); text: | The return status of ${../if/server-fire-when:/name} shall be ${../../status/if/incorrect-state:/name}. test-epilogue: null test-prologue: null - name: Context states: - name: None test-code: | T_eq_int( class, TIMER_DORMANT ); text: | The timer shall have never been ${../glossary/scheduled:/term}. See also ${../glossary/none:/term}. - name: Interrupt test-code: | T_eq_int( class & TIMER_CLASS_BIT_ON_TASK, 0 ); text: | The timer shall be in ${../glossary/interruptcontext:/term}. - name: Server test-code: | T_eq_int( class & TIMER_CLASS_BIT_ON_TASK, TIMER_CLASS_BIT_ON_TASK ); text: | The timer shall be in ${../glossary/servercontext:/term}. - name: Nop test-code: | T_eq_int( class, ctx->pre_class ); text: | Objects referenced by parameters in the past call to ${../if/server-fire-when:/name} shall not be accessed by the ${../if/server-fire-when:/name} call. See also ${../glossary/nop:/term}. test-epilogue: null test-prologue: | Timer_Classes class; class = GetTimerClass( ctx->timer_id ); - name: Clock states: - name: None test-code: | T_eq_int( class, TIMER_DORMANT ); text: | The timer shall have never been ${../glossary/scheduled:/term}. - name: Ticks test-code: | T_eq_int( class & TIMER_CLASS_BIT_TIME_OF_DAY, 0 ); text: | The timer shall use the ${../glossary/ticksbasedclock:/term}. - name: Realtime test-code: | T_eq_int( class & TIMER_CLASS_BIT_TIME_OF_DAY, TIMER_CLASS_BIT_TIME_OF_DAY ); text: | The timer shall use the ${../glossary/realtimeclock:/term}. - name: Nop test-code: | T_eq_int( class, ctx->pre_class ); text: | Objects referenced by parameters in the past call to ${../if/server-fire-when:/name} shall not be accessed by the ${../if/server-fire-when:/name} call. test-epilogue: null test-prologue: | Timer_Classes class; class = GetTimerClass( ctx->timer_id ); - name: State states: - name: Scheduled test-code: | TriggerTimer( ctx, &ctx->tod_till_fire ); T_eq_int( ctx->invocations, 1 ); text: | The timer shall be in ${../glossary/scheduled:/term} ${../glossary/state:/term}. - name: Nop test-code: | T_eq_int( ctx->post_state, ctx->pre_state ); text: | Objects referenced by parameters in the past call to ${../if/server-fire-when:/name} shall not be accessed by the ${../if/server-fire-when:/name} call. test-epilogue: null test-prologue: null - name: WallTime states: - name: Param test-code: | T_eq_mem( &ctx->tod_till_fire, ctx->wall_time_param, sizeof( ctx->tod_till_fire ) ); text: | The ${../glossary/timerserviceroutine:/term} shall be invoked at the wall time (see ${../glossary/realtimeclock:/term}), which was provided by the ${../if/server-fire-when:/params[1]/name} parameter in the past call to ${../if/server-fire-when:/name}. - name: Nop test-code: | /* * Whether the timer is scheduled has already been tested by the * "Nop" "State" post-condition above. */ T_eq_u32( ctx->post_scheduling_data.interval, ctx->pre_scheduling_data.interval ); text: | If and when the ${../glossary/timerserviceroutine:/term} will be invoked shall not be changed by the past call to ${../if/server-fire-when:/name}. test-epilogue: null test-prologue: null - name: Routine states: - name: Param test-code: | T_eq_int( ctx->invocations, 1 ); text: | The function reference used to invoke the ${../glossary/timerserviceroutine:/term} when the timer will ${../glossary/fire:/term} shall be the one provided by the ${../if/server-fire-when:/params[2]/name} parameter in the past call to ${../if/server-fire-when:/name}. - name: Nop test-code: | T_eq_ptr( ctx->post_scheduling_data.routine, ctx->pre_scheduling_data.routine ); text: | The function reference used for any invocation of the ${../glossary/timerserviceroutine:/term} shall not be changed by the past call to ${../if/server-fire-when:/name}. test-epilogue: null test-prologue: null - name: UserData states: - name: Param test-code: | T_eq_ptr( ctx->routine_user_data, ctx ); text: | The user data argument for invoking the ${../glossary/timerserviceroutine:/term} when the timer will ${../glossary/fire:/term} shall be the one provided by the ${../if/server-fire-when:/params[3]/name} parameter in the past call to ${../if/server-fire-when:/name}. - name: Nop test-code: | T_eq_ptr( ctx->post_scheduling_data.user_data, ctx->pre_scheduling_data.user_data ); text: | The user data argument used for any invocation of the ${../glossary/timerserviceroutine:/term} shall not be changed by the past call to ${../if/server-fire-when:/name}. test-epilogue: null test-prologue: null pre-conditions: - name: Server states: - name: Init test-code: | rtems_status_code status; status = rtems_timer_initiate_server( RTEMS_TIMER_SERVER_DEFAULT_PRIORITY, RTEMS_MINIMUM_STACK_SIZE, RTEMS_DEFAULT_ATTRIBUTES ); T_rsc_success( status ); text: | While the Timer Server task has been successfully initialized by a call to ${../if/initiate-server:/name}. - name: NotInit test-code: | DeleteTimerServer(); text: | While the Timer Server task has not been initialized and does not exist. test-epilogue: null test-prologue: null - name: RtClock states: - name: Set test-code: | ctx->pre_cond_tod = &tod_now; text: | While the ${../glossary/realtimeclock:/term} is set to a valid time-of-day. - name: Unset test-code: | ctx->pre_cond_tod = NULL; text: | While the ${../glossary/realtimeclock:/term} has never been set. test-epilogue: null test-prologue: null - name: Routine states: - name: Valid test-code: | ctx->routine_param = TimerServiceRoutine; text: | While the ${../if/server-fire-when:/params[2]/name} parameter references an object of type ${../if/service-routine-entry:/name}. - name: 'Null' test-code: | ctx->routine_param = NULL; text: | While the ${../if/server-fire-when:/params[2]/name} parameter is ${/c/if/null:/name}.. test-epilogue: null test-prologue: null - name: WallTime states: - name: Valid test-code: | ctx->wall_time_param = &tod_schedule; text: | While the ${../if/server-fire-when:/params[1]/name} parameter is a positive (greater than 0) number. - name: Invalid test-code: | ctx->wall_time_param = &tod_invalid; text: | While the ${../if/server-fire-when:/params[1]/name} parameter is invalid. - name: 'Null' test-code: | ctx->wall_time_param = NULL; text: | While the ${../if/server-fire-when:/params[1]/name} parameter is 0. test-epilogue: null test-prologue: null - name: Id states: - name: Valid test-code: | ctx->id_param = ctx->timer_id; text: | While the ${../if/server-fire-when:/params[0]/name} parameter is valid. - name: Invalid test-code: | ctx->id_param = RTEMS_ID_NONE; text: | While the ${../if/server-fire-when:/params[0]/name} parameter is invalid. test-epilogue: null test-prologue: null - name: Context states: - name: None test-code: | ctx->pre_cond_contex = PRE_NONE; text: | While the ${../glossary/timerserviceroutine:/term} has never been ${../glossary/scheduled:/term} since creation of the timer. See also ${../glossary/none:/term}. - name: Interrupt test-code: | ctx->pre_cond_contex = PRE_INTERRUPT; text: | While the timer is in ${../glossary/interruptcontext:/term}. - name: Server test-code: | ctx->pre_cond_contex = PRE_SERVER; text: | While the timer is in ${../glossary/servercontext:/term}. test-epilogue: null test-prologue: null - name: Clock states: - name: None test-code: | T_eq_int( ctx->pre_cond_contex, PRE_NONE ); text: | While the timer has never been ${../glossary/scheduled:/term} since creation of the timer. - name: Ticks test-code: | rtems_status_code status; if ( ctx->pre_cond_contex == PRE_INTERRUPT ) { status = rtems_timer_fire_after( ctx->timer_id, SCHEDULE_SOON, TimerServiceRoutine, ctx ); } else { status = rtems_timer_server_fire_after( ctx->timer_id, SCHEDULE_SOON, TimerServiceRoutine, ctx ); } T_rsc_success( status ); text: | While the ${../glossary/clock:/term} used to determine when the timer will ${../glossary/fire:/term} is the ${../glossary/ticksbasedclock:/term}. - name: Realtime test-code: | rtems_status_code status; T_rsc_success( rtems_clock_set( &tod_now ) ); if ( ctx->pre_cond_contex == PRE_INTERRUPT ) { status = rtems_timer_fire_when( ctx->timer_id, &tod_schedule, TimerServiceRoutine, ctx ); } else { status = rtems_timer_server_fire_when( ctx->timer_id, &tod_schedule, TimerServiceRoutine, ctx ); } T_rsc_success( status ); text: | While the ${../glossary/clock:/term} used to determine when the timer will ${../glossary/fire:/term} is the ${../glossary/realtimeclock:/term}. test-epilogue: null test-prologue: null - name: State states: - name: Inactive test-code: | TriggerTimer( ctx, NULL ); T_eq_int( ctx->invocations, ( ctx->pre_cond_contex == PRE_NONE ) ? 0 : 1 ); ctx->invocations = 0; ctx->pre_state = TIMER_INACTIVE; text: | While the timer is in ${../glossary/inactive:/term} ${../glossary/state:/term}. - name: Scheduled test-code: | /* The timer was already scheduled in the "Clock" pre-conditions. */ ctx->pre_state = TIMER_SCHEDULED; text: | While the timer is in ${../glossary/scheduled:/term} ${../glossary/state:/term}. - name: Pending test-code: | T_rsc_success( rtems_task_suspend( GetTimerServerTaskId() ) ); TriggerTimer( ctx, NULL ); T_eq_int( ctx->invocations, 0 ); ctx->pre_state = TIMER_PENDING; text: | While the timer is in ${../glossary/pending:/term} ${../glossary/state:/term}. test-epilogue: null test-prologue: null rationale: null references: [] requirement-type: functional skip-reasons: NotExist: | The pre-condition combination of ${../glossary/context:/term}, ${../glossary/clock:/term} and ${../glossary/state:/term} cannot be produced and does therefore not exist. ClockNotSet: | When the ${../glossary/realtimeclock:/term} is not set, the timer cannot be in pre-condition *Clock* *Realtime* because it is not possible to call the directives ${../if/fire-when:/name} or ${../if/server-fire-when:/name} with ${/glossary/statuscode:/term} ${../../status/if/successful:/name}. NoServer: | If the server task is not initialized, the timer cannot be in ${../glossary/servercontext:/term}. test-action: | GetTimerSchedulingData( ctx->timer_id, &ctx->pre_scheduling_data ); ctx->pre_class = GetTimerClass( ctx->timer_id ); if ( ctx->pre_cond_tod == NULL ) { UnsetClock(); } else { T_rsc_success( rtems_clock_set( ctx->pre_cond_tod ) ); } ctx->status = rtems_timer_server_fire_when( ctx->id_param, ctx->wall_time_param, ctx->routine_param, ctx ); ctx->post_state = GetTimerState( ctx->timer_id ); GetTimerSchedulingData( ctx->timer_id, &ctx->post_scheduling_data ); /* Ignoring return status: the timer server task may be suspended or not. */ rtems_task_resume( GetTimerServerTaskId() ); test-brief: null test-cleanup: | T_rsc_success( rtems_timer_delete( ctx->timer_id ) ); DeleteTimerServer(); test-context: - brief: | This member contains a valid id of a timer. description: null member: | rtems_id timer_id - brief: | This member specifies the ${../if/server-fire-when:/params[0]/name} parameter for the action. description: null member: | rtems_id id_param - brief: | This member specifies the ${../if/server-fire-when:/params[1]/name} parameter for the action. description: null member: | const rtems_time_of_day *wall_time_param - brief: | This member specifies the ${../if/server-fire-when:/params[2]/name} parameter for the action. description: null member: | rtems_timer_service_routine_entry routine_param - brief: | This member contains the returned ${/glossary/statuscode:/term} of the action. description: null member: | rtems_status_code status - brief: | This member contains a counter of invocations of the ${../glossary/timerserviceroutine:/term}. description: null member: | int invocations - brief: | Function TriggerTimer() is used to figure out when the ${../glossary/timerserviceroutine:/term} gets executed. This member contains the time-of-day when the ${../glossary/timerserviceroutine:/term} fires (see ${../glossary/fire:/term}). description: null member: | rtems_time_of_day tod_till_fire - brief: | This member contains the user data given to the ${../glossary/timerserviceroutine:/term} when called. description: null member: | void *routine_user_data - brief: | This member specifies which pre-condition ${../glossary/context:/term} (${../glossary/none:/term}, ${../glossary/interruptcontext:/term}, ${../glossary/servercontext:/term}) must be created before the ${../if/server-fire-when:/name} action gets executed. description: null member: | PreConditionContext pre_cond_contex - brief: | This member specifies the pre-condition state of the ${../glossary/realtimeclock:/term}. It should either be set to the value referenced by pre_cond_tod or if ${/c/if/null:/name}, then the ${../glossary/realtimeclock:/term} should be not set. description: null member: | const rtems_time_of_day *pre_cond_tod - brief: | This member stores internal ${../glossary/clock:/term} and ${../glossary/context:/term} settings of the timer before the execution of the test action. description: null member: | Timer_Classes pre_class - brief: | This member stores the ${../glossary/state:/term} of the timer before the execution of the test action. description: null member: | Timer_States pre_state - brief: | This member stores the ${../glossary/state:/term} of the timer after the execution of the test action. description: null member: | Timer_States post_state - brief: | This member stores the scheduling data of the timer before the execution of the test action. description: null member: | Timer_Scheduling_Data pre_scheduling_data - brief: | This member stores the scheduling data of the timer after the execution of the test action. description: null member: | Timer_Scheduling_Data post_scheduling_data test-context-support: | typedef enum { PRE_NONE = 0, PRE_INTERRUPT = 1, PRE_SERVER = 2 } PreConditionContext; typedef enum { SCHEDULE_NONE = 0, SCHEDULE_SOON = 1, SCHEDULE_MAX = 5 } Scheduling_Ticks; test-description: null test-header: null test-includes: - rtems.h test-local-includes: - tx-support.h test-prepare: | rtems_status_code status; status = rtems_timer_create( rtems_build_name( 'T', 'I', 'M', 'E' ), &ctx->timer_id ); T_rsc_success( status ); ctx->invocations = 0; ctx->routine_user_data = NULL; test-setup: null test-stop: null test-support: | static const rtems_time_of_day tod_now = { 2000, 1, 1, 0, 0, 0, 0 }; static const rtems_time_of_day tod_schedule = { 2000, 1, 1, 5, 0, 0, 0 }; static const rtems_time_of_day tod_invalid = { 1985, 1, 1, 0, 0, 0, 0 }; static void TriggerTimer( const RtemsTimerReqServerFireWhen_Context *ctx, rtems_time_of_day *tod_fire ) { rtems_time_of_day tod = tod_now; int invocations_old = ctx->invocations; int i; /* Fire the timer service routine for ticks and realtime clock */ for ( i = 1; i <= SCHEDULE_MAX; ++i ) { ClockTick(); } for ( i = 1; i < 24; ++i ) { tod.hour = i; T_rsc_success( rtems_clock_set( &tod ) ); if ( tod_fire != NULL && ctx->invocations > invocations_old ) { *tod_fire = tod; break; } } } RTEMS_INLINE_ROUTINE void TimerServiceRoutine( rtems_id timer_id, void *user_data ) { RtemsTimerReqServerFireWhen_Context *ctx = user_data; ++( ctx->invocations ); ctx->routine_user_data = user_data; } test-target: testsuites/validation/tc-timer-server-fire-when.c test-teardown: brief: Make sure the ${../glossary/realtimeclock:/term} is not set after this test. code: | UnsetClock(); description: null text: ${.:text-template} transition-map: - enabled-by: true post-conditions: Status: Ok Context: Server Clock: Realtime State: Scheduled WallTime: Param Routine: Param UserData: Param pre-conditions: Server: - Init RtClock: - Set Routine: - Valid WallTime: - Valid Id: - Valid Context: - None Clock: - None State: - Inactive - enabled-by: true post-conditions: Status: Ok Context: Server Clock: Realtime State: Scheduled WallTime: Param Routine: Param UserData: Param pre-conditions: Server: - Init RtClock: - Set Routine: - Valid WallTime: - Valid Id: - Valid Context: - Server Clock: - Ticks - Realtime State: all - enabled-by: true post-conditions: Status: Ok Context: Server Clock: Realtime State: Scheduled WallTime: Param Routine: Param UserData: Param pre-conditions: Server: - Init RtClock: - Set Routine: - Valid WallTime: - Valid Id: - Valid Context: - Interrupt Clock: - Ticks - Realtime State: - Inactive - Scheduled - enabled-by: true post-conditions: NotExist pre-conditions: Server: all RtClock: all Routine: all WallTime: all Id: all Context: - None Clock: - None State: - Scheduled - Pending - enabled-by: true post-conditions: NotExist pre-conditions: Server: all RtClock: all Routine: all WallTime: all Id: all Context: - None Clock: - Ticks - Realtime State: all - enabled-by: true post-conditions: NotExist pre-conditions: Server: all RtClock: all Routine: all WallTime: all Id: all Context: - Interrupt - Server Clock: - None State: all - enabled-by: true post-conditions: NotExist pre-conditions: Server: all RtClock: - Set Routine: all WallTime: all Id: all Context: - Interrupt Clock: - Ticks - Realtime State: - Pending - enabled-by: true post-conditions: NotExist pre-conditions: Server: all RtClock: - Unset Routine: all WallTime: all Id: all Context: - Interrupt Clock: - Ticks State: - Pending - enabled-by: true post-conditions: NoServer pre-conditions: Server: - NotInit RtClock: all Routine: all WallTime: all Id: all Context: - Server Clock: - Ticks - Realtime State: all - enabled-by: true post-conditions: ClockNotSet pre-conditions: Server: - Init RtClock: - Unset Routine: all WallTime: all Id: all Context: - Interrupt - Server Clock: - Realtime State: all - enabled-by: true post-conditions: ClockNotSet pre-conditions: Server: - NotInit RtClock: - Unset Routine: all WallTime: all Id: all Context: - Interrupt Clock: - Realtime State: all - enabled-by: true post-conditions: Status: NotDef Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Unset Routine: all WallTime: all Id: all Context: - None Clock: - None State: - Inactive - enabled-by: true post-conditions: Status: NotDef Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Unset Routine: all WallTime: all Id: all Context: - Server Clock: - Ticks State: all - enabled-by: true post-conditions: Status: NotDef Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Unset Routine: all WallTime: all Id: all Context: - Interrupt Clock: - Ticks State: - Inactive - Scheduled - enabled-by: true post-conditions: Status: InvId Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Set Routine: - Valid WallTime: - Valid Id: - Invalid Context: - None Clock: - None State: - Inactive - enabled-by: true post-conditions: Status: InvId Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Set Routine: - Valid WallTime: - Valid Id: - Invalid Context: - Server Clock: - Ticks - Realtime State: all - enabled-by: true post-conditions: Status: InvId Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Set Routine: - Valid WallTime: - Valid Id: - Invalid Context: - Interrupt Clock: - Ticks - Realtime State: - Inactive - Scheduled - enabled-by: true post-conditions: Status: InvAddr Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Set Routine: - 'Null' WallTime: - Valid - Invalid Id: all Context: - None Clock: - None State: - Inactive - enabled-by: true post-conditions: Status: InvAddr Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Set Routine: - 'Null' WallTime: - Valid - Invalid Id: all Context: - Server Clock: - Ticks - Realtime State: all - enabled-by: true post-conditions: Status: InvAddr Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Set Routine: - 'Null' WallTime: - Valid - Invalid Id: all Context: - Interrupt Clock: - Ticks - Realtime State: - Inactive - Scheduled - enabled-by: true post-conditions: Status: InvClock Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Set Routine: - Valid WallTime: - Invalid Id: all Context: - None Clock: - None State: - Inactive - enabled-by: true post-conditions: Status: InvClock Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Set Routine: - Valid WallTime: - Invalid Id: all Context: - Server Clock: - Ticks - Realtime State: all - enabled-by: true post-conditions: Status: InvClock Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Set Routine: - Valid WallTime: - Invalid Id: all Context: - Interrupt Clock: - Ticks - Realtime State: - Inactive - Scheduled - enabled-by: true post-conditions: Status: InvAddr Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Set Routine: all WallTime: - 'Null' Id: all Context: - None Clock: - None State: - Inactive - enabled-by: true post-conditions: Status: InvAddr Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Set Routine: all WallTime: - 'Null' Id: all Context: - Server Clock: - Ticks - Realtime State: all - enabled-by: true post-conditions: Status: InvAddr Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - Init RtClock: - Set Routine: all WallTime: - 'Null' Id: all Context: - Interrupt Clock: - Ticks - Realtime State: - Inactive - Scheduled - enabled-by: true post-conditions: Status: IncStat Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - NotInit RtClock: all Routine: all WallTime: all Id: all Context: - None Clock: - None State: - Inactive - enabled-by: true post-conditions: Status: IncStat Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - NotInit RtClock: - Set Routine: all WallTime: all Id: all Context: - Interrupt Clock: - Ticks - Realtime State: - Inactive - Scheduled - enabled-by: true post-conditions: Status: IncStat Context: Nop Clock: Nop State: Nop WallTime: Nop Routine: Nop UserData: Nop pre-conditions: Server: - NotInit RtClock: - Unset Routine: all WallTime: all Id: all Context: - Interrupt Clock: - Ticks State: - Inactive - Scheduled type: requirement