[rtems-central commit] spec: Add spec for rtems_timer_server_fire_when()
Sebastian Huber
sebh at rtems.org
Mon May 17 06:10:56 UTC 2021
Module: rtems-central
Branch: master
Commit: fa868b296ccd63a76da3d30c2e988a15f1d16bb5
Changeset: http://git.rtems.org/rtems-central/commit/?id=fa868b296ccd63a76da3d30c2e988a15f1d16bb5
Author: Frank Kühndel <frank.kuehndel at embedded-brains.de>
Date: Fri May 14 11:03:59 2021 +0200
spec: Add spec for rtems_timer_server_fire_when()
Adding a specification item to rtems-central for the directive
rtems_timer_server_fire_when() of the timer manager. This item
uses the timer specific glossary terms, too.
---
spec/rtems/timer/req/server-fire-when.yml | 1267 +++++++++++++++++++++++++++++
1 file changed, 1267 insertions(+)
diff --git a/spec/rtems/timer/req/server-fire-when.yml b/spec/rtems/timer/req/server-fire-when.yml
new file mode 100644
index 0000000..00cbf64
--- /dev/null
+++ b/spec/rtems/timer/req/server-fire-when.yml
@@ -0,0 +1,1267 @@
+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
More information about the vc
mailing list