From 2a4a2574340945c263e5b49f4ae5c9719a54d783 Mon Sep 17 00:00:00 2001 From: Sebastian Huber Date: Mon, 15 Mar 2021 08:55:27 +0100 Subject: validation: Add post-condition expressions --- rtemsspec/tests/spec-validation/action2.yml | 156 ++++++++++--- rtemsspec/tests/test_validation.py | 256 +++++++++++++++------ rtemsspec/validation.py | 210 ++++++++++++++++- spec/spec/requirement-action-exp-bool-list.yml | 16 ++ spec/spec/requirement-action-exp-bool.yml | 51 ++++ spec/spec/requirement-action-exp-conditions.yml | 26 +++ spec/spec/requirement-action-exp-state-name.yml | 21 ++ spec/spec/requirement-action-exp-states.yml | 25 ++ spec/spec/requirement-action-exp.yml | 46 ++++ .../requirement-action-transition-post-state.yml | 5 + spec/spec/requirement-action-transition-pre.yml | 2 +- 11 files changed, 693 insertions(+), 121 deletions(-) create mode 100644 spec/spec/requirement-action-exp-bool-list.yml create mode 100644 spec/spec/requirement-action-exp-bool.yml create mode 100644 spec/spec/requirement-action-exp-conditions.yml create mode 100644 spec/spec/requirement-action-exp-state-name.yml create mode 100644 spec/spec/requirement-action-exp-states.yml create mode 100644 spec/spec/requirement-action-exp.yml diff --git a/rtemsspec/tests/spec-validation/action2.yml b/rtemsspec/tests/spec-validation/action2.yml index 626d8a70..4875bad8 100644 --- a/rtemsspec/tests/spec-validation/action2.yml +++ b/rtemsspec/tests/spec-validation/action2.yml @@ -7,32 +7,47 @@ links: [] post-conditions: - name: A states: - - name: X + - name: A0 test-code: | - /* Post A X */ + /* Post A 0 */ text: | - Post A X. - - name: Y + Post A 0. + - name: A1 test-code: | - /* Post A Y */ + /* Post A 1 */ text: | - Post A Y. + Post A 1. + - name: A2 + test-code: | + /* Post A 2 */ + text: | + Post A 2. + - name: A3 + test-code: | + /* Post A 3 */ + text: | + Post A 3. test-epilogue: | /* Post A epilogue. */ test-prologue: | /* Post A prologue. */ - name: B states: - - name: X + - name: B0 + test-code: | + /* Post B 0 */ + text: | + Post B 0. + - name: B1 test-code: | - /* Post B X */ + /* Post B 1 */ text: | - Post B X. - - name: Y + Post B 1. + - name: B2 test-code: | - /* Post B Y */ + /* Post B 2 */ text: | - Post B Y. + Post B 2. test-epilogue: | /* Post B epilogue. */ test-prologue: | @@ -40,41 +55,62 @@ post-conditions: pre-conditions: - name: A states: - - name: X + - name: A0 test-code: | - /* Pre A X */ + /* Pre A 0 */ text: | - Pre A X. - - name: Y + Pre A 0. + - name: A1 test-code: | - /* Pre A Y */ + /* Pre A 1 */ text: | - Pre A Y. + Pre A 1. test-epilogue: | /* Pre A epilogue. */ test-prologue: | /* Pre A prologue. */ - name: B states: - - name: X + - name: B0 test-code: | - /* Pre B X */ + /* Pre B 0 */ text: | - Pre B X. - - name: Y + Pre B 0. + - name: B1 test-code: | - /* Pre B Y */ + /* Pre B 1 */ text: | - Pre B Y. - - name: Z + Pre B 1. + - name: B2 test-code: | - /* Pre B Z */ + /* Pre B 1 */ text: | - Pre B Z. + Pre B 1. test-epilogue: | /* Pre B epilogue. */ test-prologue: | /* Pre B prologue. */ +- name: C + states: + - name: C0 + test-code: | + /* Pre C 0 */ + text: | + Pre C 0. + - name: C1 + test-code: | + /* Pre B 1 */ + text: | + Pre C 1. + - name: C2 + test-code: | + /* Pre C 2 */ + text: | + Pre C 2. + test-epilogue: | + /* Pre C epilogue. */ + test-prologue: | + /* Pre C prologue. */ rationale: null references: [] requirement-type: functional @@ -153,30 +189,76 @@ text: | transition-map: - enabled-by: true post-conditions: - A: X - B: Y + A: + - if: + not: + pre-conditions: + B: B0 + then: A0 + - if: + and: + - pre-conditions: + A: A0 + - pre-conditions: + B: B0 + then: A1 + - if: + or: + - pre-conditions: + C: C0 + - pre-conditions: + A: A1 + C: C1 + then: A2 + - else: A3 + B: + - if: + pre-conditions: + A: A0 + then-specified-by: B + - specified-by: B pre-conditions: A: all B: - - X + - B0 + C: all - enabled-by: true post-conditions: - A: Y - B: N/A + A: A1 + B: + - if: + post-conditions: + A: A2 + then: B0 + - if: + post-conditions: + A: + - A0 + - A1 + then: N/A pre-conditions: A: N/A B: - - Y + - B1 + C: all - enabled-by: true post-conditions: SkipReason pre-conditions: A: - - Y + - A1 B: - - Z + - B2 + C: all - enabled-by: true post-conditions: - A: X - B: X + A: + - if: + - pre-conditions: + A: + - A0 + - A1 + then: A2 + - else: A0 + B: B0 pre-conditions: default type: requirement diff --git a/rtemsspec/tests/test_validation.py b/rtemsspec/tests/test_validation.py index aeb2bbd8..3c8614ae 100644 --- a/rtemsspec/tests/test_validation.py +++ b/rtemsspec/tests/test_validation.py @@ -1670,27 +1670,37 @@ extern "C" { */ typedef enum { - Action2_Pre_A_X, - Action2_Pre_A_Y, + Action2_Pre_A_A0, + Action2_Pre_A_A1, Action2_Pre_A_NA } Action2_Pre_A; typedef enum { - Action2_Pre_B_X, - Action2_Pre_B_Y, - Action2_Pre_B_Z, + Action2_Pre_B_B0, + Action2_Pre_B_B1, + Action2_Pre_B_B2, Action2_Pre_B_NA } Action2_Pre_B; typedef enum { - Action2_Post_A_X, - Action2_Post_A_Y, + Action2_Pre_C_C0, + Action2_Pre_C_C1, + Action2_Pre_C_C2, + Action2_Pre_C_NA +} Action2_Pre_C; + +typedef enum { + Action2_Post_A_A0, + Action2_Post_A_A1, + Action2_Post_A_A2, + Action2_Post_A_A3, Action2_Post_A_NA } Action2_Post_A; typedef enum { - Action2_Post_B_X, - Action2_Post_B_Y, + Action2_Post_B_B0, + Action2_Post_B_B1, + Action2_Post_B_B2, Action2_Post_B_NA } Action2_Post_B; @@ -1823,7 +1833,7 @@ typedef struct { /** * @brief This member defines the pre-condition states for the next action. */ - size_t pcs[ 2 ]; + size_t pcs[ 3 ]; /** * @brief This member indicates if the test action loop is currently @@ -1836,21 +1846,29 @@ static Action2_Context Action2_Instance; static const char * const Action2_PreDesc_A[] = { - "X", - "Y", + "A0", + "A1", "NA" }; static const char * const Action2_PreDesc_B[] = { - "X", - "Y", - "Z", + "B0", + "B1", + "B2", + "NA" +}; + +static const char * const Action2_PreDesc_C[] = { + "C0", + "C1", + "C2", "NA" }; static const char * const * const Action2_PreDesc[] = { Action2_PreDesc_A, Action2_PreDesc_B, + Action2_PreDesc_C, NULL }; @@ -1861,19 +1879,19 @@ static void Action2_Pre_A_Prepare( Action2_Context *ctx, Action2_Pre_A state ) /* Pre A prologue. */ switch ( state ) { - case Action2_Pre_A_X: { + case Action2_Pre_A_A0: { /* - * Pre A X. + * Pre A 0. */ - /* Pre A X */ + /* Pre A 0 */ break; } - case Action2_Pre_A_Y: { + case Action2_Pre_A_A1: { /* - * Pre A Y. + * Pre A 1. */ - /* Pre A Y */ + /* Pre A 1 */ break; } @@ -1889,27 +1907,27 @@ static void Action2_Pre_B_Prepare( Action2_Context *ctx, Action2_Pre_B state ) /* Pre B prologue. */ switch ( state ) { - case Action2_Pre_B_X: { + case Action2_Pre_B_B0: { /* - * Pre B X. + * Pre B 0. */ - /* Pre B X */ + /* Pre B 0 */ break; } - case Action2_Pre_B_Y: { + case Action2_Pre_B_B1: { /* - * Pre B Y. + * Pre B 1. */ - /* Pre B Y */ + /* Pre B 1 */ break; } - case Action2_Pre_B_Z: { + case Action2_Pre_B_B2: { /* - * Pre B Z. + * Pre B 1. */ - /* Pre B Z */ + /* Pre B 1 */ break; } @@ -1920,24 +1938,76 @@ static void Action2_Pre_B_Prepare( Action2_Context *ctx, Action2_Pre_B state ) /* Pre B epilogue. */ } +static void Action2_Pre_C_Prepare( Action2_Context *ctx, Action2_Pre_C state ) +{ + /* Pre C prologue. */ + + switch ( state ) { + case Action2_Pre_C_C0: { + /* + * Pre C 0. + */ + /* Pre C 0 */ + break; + } + + case Action2_Pre_C_C1: { + /* + * Pre C 1. + */ + /* Pre B 1 */ + break; + } + + case Action2_Pre_C_C2: { + /* + * Pre C 2. + */ + /* Pre C 2 */ + break; + } + + case Action2_Pre_C_NA: + break; + } + + /* Pre C epilogue. */ +} + static void Action2_Post_A_Check( Action2_Context *ctx, Action2_Post_A state ) { /* Post A prologue. */ switch ( state ) { - case Action2_Post_A_X: { + case Action2_Post_A_A0: { /* - * Post A X. + * Post A 0. */ - /* Post A X */ + /* Post A 0 */ break; } - case Action2_Post_A_Y: { + case Action2_Post_A_A1: { /* - * Post A Y. + * Post A 1. */ - /* Post A Y */ + /* Post A 1 */ + break; + } + + case Action2_Post_A_A2: { + /* + * Post A 2. + */ + /* Post A 2 */ + break; + } + + case Action2_Post_A_A3: { + /* + * Post A 3. + */ + /* Post A 3 */ break; } @@ -1953,19 +2023,27 @@ static void Action2_Post_B_Check( Action2_Context *ctx, Action2_Post_B state ) /* Post B prologue. */ switch ( state ) { - case Action2_Post_B_X: { + case Action2_Post_B_B0: { /* - * Post B X. + * Post B 0. */ - /* Post B X */ + /* Post B 0 */ break; } - case Action2_Post_B_Y: { + case Action2_Post_B_B1: { /* - * Post B Y. + * Post B 1. */ - /* Post B Y */ + /* Post B 1 */ + break; + } + + case Action2_Post_B_B2: { + /* + * Post B 2. + */ + /* Post B 2 */ break; } @@ -2030,24 +2108,37 @@ static void Action2_Cleanup( Action2_Context *ctx ) } typedef struct { - uint8_t Skip : 1; - uint8_t Pre_A_NA : 1; - uint8_t Pre_B_NA : 1; - uint8_t Post_A : 2; - uint8_t Post_B : 2; + uint16_t Skip : 1; + uint16_t Pre_A_NA : 1; + uint16_t Pre_B_NA : 1; + uint16_t Pre_C_NA : 1; + uint16_t Post_A : 3; + uint16_t Post_B : 2; } Action2_Entry; -#define E( x0, x1, x2, x3, x4) { x0, x1, x2, Action2_Post_A_##x3, \\ - Action2_Post_B_##x4 } +#define E( x0, x1, x2, x3, x4, x5) { x0, x1, x2, x3, Action2_Post_A_##x4, \\ + Action2_Post_B_##x5 } static const Action2_Entry Action2_Map[] = { - E( 0, 0, 0, X, Y ), - E( 0, 1, 0, Y, NA ), - E( 0, 0, 0, X, X ), - E( 0, 0, 0, X, Y ), - E( 0, 1, 0, Y, NA ), - E( 1, 0, 0, NA, NA ) + E( 0, 0, 0, 0, A1, B0 ), + E( 0, 0, 0, 0, A1, B0 ), + E( 0, 0, 0, 0, A1, B0 ), + E( 0, 1, 0, 0, A1, NA ), + E( 0, 1, 0, 0, A1, NA ), + E( 0, 1, 0, 0, A1, NA ), + E( 0, 0, 0, 0, A2, B0 ), + E( 0, 0, 0, 0, A2, B0 ), + E( 0, 0, 0, 0, A2, B0 ), + E( 0, 0, 0, 0, A2, B0 ), + E( 0, 0, 0, 0, A2, B0 ), + E( 0, 0, 0, 0, A3, B0 ), + E( 0, 1, 0, 0, A1, NA ), + E( 0, 1, 0, 0, A1, NA ), + E( 0, 1, 0, 0, A1, NA ), + E( 1, 0, 0, 0, NA, NA ), + E( 1, 0, 0, 0, NA, NA ), + E( 1, 0, 0, 0, NA, NA ) }; #undef E @@ -2089,42 +2180,56 @@ void Action2_Run( int *a, int b, int *c ) index = 0; for ( - ctx->pcs[ 0 ] = Action2_Pre_A_X; + ctx->pcs[ 0 ] = Action2_Pre_A_A0; ctx->pcs[ 0 ] < Action2_Pre_A_NA; ++ctx->pcs[ 0 ] ) { if ( Action2_Map[ index ].Pre_A_NA ) { ctx->pcs[ 0 ] = Action2_Pre_A_NA; index += ( Action2_Pre_A_NA - 1 ) - * Action2_Pre_B_NA; + * Action2_Pre_B_NA + * Action2_Pre_C_NA; } for ( - ctx->pcs[ 1 ] = Action2_Pre_B_X; + ctx->pcs[ 1 ] = Action2_Pre_B_B0; ctx->pcs[ 1 ] < Action2_Pre_B_NA; ++ctx->pcs[ 1 ] ) { - Action2_Entry entry; - if ( Action2_Map[ index ].Pre_B_NA ) { ctx->pcs[ 1 ] = Action2_Pre_B_NA; - index += ( Action2_Pre_B_NA - 1 ); + index += ( Action2_Pre_B_NA - 1 ) + * Action2_Pre_C_NA; } - if ( Action2_Map[ index ].Skip ) { + for ( + ctx->pcs[ 2 ] = Action2_Pre_C_C0; + ctx->pcs[ 2 ] < Action2_Pre_C_NA; + ++ctx->pcs[ 2 ] + ) { + Action2_Entry entry; + + if ( Action2_Map[ index ].Pre_C_NA ) { + ctx->pcs[ 2 ] = Action2_Pre_C_NA; + index += ( Action2_Pre_C_NA - 1 ); + } + + if ( Action2_Map[ index ].Skip ) { + ++index; + continue; + } + + Action2_Prepare( ctx ); + Action2_Pre_A_Prepare( ctx, ctx->pcs[ 0 ] ); + Action2_Pre_B_Prepare( ctx, ctx->pcs[ 1 ] ); + Action2_Pre_C_Prepare( ctx, ctx->pcs[ 2 ] ); + Action2_Action( ctx ); + entry = Action2_Map[ index ]; + Action2_Post_A_Check( ctx, entry.Post_A ); + Action2_Post_B_Check( ctx, entry.Post_B ); + Action2_Cleanup( ctx ); ++index; - continue; } - - Action2_Prepare( ctx ); - Action2_Pre_A_Prepare( ctx, ctx->pcs[ 0 ] ); - Action2_Pre_B_Prepare( ctx, ctx->pcs[ 1 ] ); - Action2_Action( ctx ); - entry = Action2_Map[ index ]; - Action2_Post_A_Check( ctx, entry.Post_A ); - Action2_Post_B_Check( ctx, entry.Post_B ); - Action2_Cleanup( ctx ); - ++index; } } @@ -2284,3 +2389,8 @@ def test_validation_invalid_actions(): "for pre-condition set {A=A2}") with pytest.raises(ValueError, match=match): generate(validation_config, item_cache) + action_data["transition-map"][-1]["post-conditions"]["X"] = [] + match = ("cannot determine state for post-condition 'X' of transition map " + "descriptor 1 of spec:/a for pre-condition set {A=A1}") + with pytest.raises(ValueError, match=match): + generate(validation_config, item_cache) diff --git a/rtemsspec/validation.py b/rtemsspec/validation.py index 6945bdc9..ae4b2c9d 100644 --- a/rtemsspec/validation.py +++ b/rtemsspec/validation.py @@ -1,7 +1,7 @@ # SPDX-License-Identifier: BSD-2-Clause """ This module provides functions for the generation of validation tests. """ -# Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) +# Copyright (C) 2020, 2021 embedded brains GmbH (http://www.embedded-brains.de) # # Redistribution and use in source and binary forms, with or without # modification, are permitted provided that the following conditions @@ -486,6 +486,111 @@ def _to_st_name(conditions: List[Any]) -> _IdxToX: for condition in conditions) +class _PostCondContext(NamedTuple): + transition_map: "TransitionMap" + map_idx: int + pre_co_states: Tuple[int, ...] + post_co_states: Tuple[Any, ...] + post_co_idx: int + ops: Any + + +def _post_cond_bool_and(ctx: _PostCondContext, exp: Any) -> bool: + for element in exp: + if not _post_cond_bool_exp(ctx, element): + return False + return True + + +def _post_cond_bool_not(ctx: _PostCondContext, exp: Any) -> bool: + return not _post_cond_bool_exp(ctx, exp) + + +def _post_cond_bool_or(ctx: _PostCondContext, exp: Any) -> bool: + for element in exp: + if _post_cond_bool_exp(ctx, element): + return True + return False + + +def _post_cond_bool_post_cond(ctx: _PostCondContext, exp: Any) -> bool: + for post_co_name, status in exp.items(): + if isinstance(status, str): + status = [status] + post_co_idx = ctx.transition_map.post_co_name_to_co_idx(post_co_name) + st_idx = [ + ctx.transition_map.post_co_idx_st_name_to_st_idx( + post_co_idx, st_name) for st_name in status + ] + if ctx.post_co_states[post_co_idx] not in st_idx: + return False + return True + + +def _post_cond_bool_pre_cond(ctx: _PostCondContext, exp: Any) -> bool: + for pre_co_name, status in exp.items(): + if isinstance(status, str): + status = [status] + pre_co_idx = ctx.transition_map.pre_co_name_to_co_idx(pre_co_name) + st_idx = [ + ctx.transition_map.pre_co_idx_st_name_to_st_idx( + pre_co_idx, st_name) for st_name in status + ] + if ctx.pre_co_states[pre_co_idx] not in st_idx: + return False + return True + + +_POST_COND_BOOL_OPS = { + "and": _post_cond_bool_and, + "not": _post_cond_bool_not, + "or": _post_cond_bool_or, + "post-conditions": _post_cond_bool_post_cond, + "pre-conditions": _post_cond_bool_pre_cond, +} + + +def _post_cond_bool_exp(ctx: _PostCondContext, exp: Any) -> Optional[int]: + if isinstance(exp, list): + return _post_cond_bool_or(ctx, exp) + key = next(iter(exp)) + return _POST_COND_BOOL_OPS[key](ctx, exp[key]) + + +def _post_cond_do_specified_by(ctx: _PostCondContext, pre_co_name: str) -> int: + pre_co_idx = ctx.transition_map.pre_co_name_to_co_idx(pre_co_name) + st_name = ctx.transition_map.pre_co_idx_st_idx_to_st_name( + pre_co_idx, ctx.pre_co_states[pre_co_idx]) + return ctx.transition_map.post_co_idx_st_name_to_st_idx( + ctx.post_co_idx, st_name) + + +def _post_cond_if(ctx: _PostCondContext) -> Optional[int]: + if _post_cond_bool_exp(ctx, ctx.ops["if"]): + if "then-specified-by" in ctx.ops: + return _post_cond_do_specified_by(ctx, + ctx.ops["then-specified-by"]) + return ctx.transition_map.post_co_idx_st_name_to_st_idx( + ctx.post_co_idx, ctx.ops["then"]) + return None + + +def _post_cond_specified_by(ctx: _PostCondContext) -> Optional[int]: + return _post_cond_do_specified_by(ctx, ctx.ops["specified-by"]) + + +def _post_cond_else(ctx: _PostCondContext) -> Optional[int]: + return ctx.transition_map.post_co_idx_st_name_to_st_idx( + ctx.post_co_idx, ctx.ops["else"]) + + +_POST_COND_OP = { + "else": _post_cond_else, + "if": _post_cond_if, + "specified-by": _post_cond_specified_by, +} + + class TransitionMap: """ Representation of an action requirement transition map. """ @@ -494,6 +599,8 @@ class TransitionMap: self._item = item self._pre_co_count = len(item["pre-conditions"]) self._post_co_count = len(item["post-conditions"]) + self._pre_co_idx_st_idx_to_st_name = _to_st_name( + item["pre-conditions"]) self._post_co_idx_st_idx_to_st_name = _to_st_name( item["post-conditions"]) self._pre_co_idx_st_name_to_st_idx = _to_st_idx(item["pre-conditions"]) @@ -502,6 +609,12 @@ class TransitionMap: self._pre_co_idx_to_cond = dict( (co_idx, condition) for co_idx, condition in enumerate(item["pre-conditions"])) + self._pre_co_name_to_co_idx = dict( + (condition["name"], co_idx) + for co_idx, condition in enumerate(item["pre-conditions"])) + self._post_co_name_to_co_idx = dict( + (condition["name"], co_idx) + for co_idx, condition in enumerate(item["post-conditions"])) self._post_co_idx_to_co_name = dict( (co_idx, condition["name"]) for co_idx, condition in enumerate(item["post-conditions"])) @@ -532,9 +645,78 @@ class TransitionMap: map_idx //= count return ", ".join(reversed(conditions)) + def map_idx_to_pre_co_states(self, map_idx: int) -> Tuple[int, ...]: + """ + Maps the transition map index and the associated pre-condition state + indices. + """ + co_states = [] + for condition in reversed(self._item["pre-conditions"]): + count = len(condition["states"]) + co_states.append(int(map_idx % count)) + map_idx //= count + return tuple(reversed(co_states)) + + def pre_co_name_to_co_idx(self, co_name: str) -> int: + """ + Maps the pre-condition name to the associated pre-condition index. + """ + return self._pre_co_name_to_co_idx[co_name] + + def post_co_name_to_co_idx(self, co_name: str) -> int: + """ + Maps the post-condition name to the associated post-condition index. + """ + return self._post_co_name_to_co_idx[co_name] + + def pre_co_idx_st_idx_to_st_name(self, co_idx: int, st_idx: int) -> str: + """ + Maps the pre-condition name and state index to the associated state + name. + """ + return self._pre_co_idx_st_idx_to_st_name[co_idx][st_idx] + + def pre_co_idx_st_name_to_st_idx(self, co_idx: int, st_name: str) -> int: + """ + Maps the pre-condition index and state name to the associated state + index. + """ + return self._pre_co_idx_st_name_to_st_idx[co_idx][st_name] + + def post_co_idx_st_name_to_st_idx(self, co_idx: int, st_name: str) -> int: + """ + Maps the post-condition index and state name to the associated state + index. + """ + return self._post_co_idx_st_name_to_st_idx[co_idx][st_name] + + def _map_post_cond(self, desc_idx: int, map_idx: int, co_idx: int, + post_cond: Tuple[Any, ...]) -> Tuple[Any, ...]: + if isinstance(post_cond[co_idx], int): + return post_cond + pre_co_states = self.map_idx_to_pre_co_states(map_idx) + for ops in post_cond[co_idx]: + idx = _POST_COND_OP[next(iter(ops))](_PostCondContext( + self, map_idx, pre_co_states, post_cond, co_idx, ops)) + if idx is not None: + return post_cond[0:co_idx] + (idx, ) + post_cond[co_idx + 1:] + raise ValueError( + "cannot determine state for post-condition " + f"'{self._post_co_idx_to_co_name[co_idx]}' of transition map " + f"descriptor {desc_idx} of {self._item.spec} for pre-condition " + f"set {{{self._map_index_to_pre_conditions(map_idx)}}}") + + def _make_post_cond(self, desc_idx: int, map_idx: int, + skip_post_cond: Tuple[Any, ...]) -> Tuple[int, ...]: + post_cond = skip_post_cond[1:] + for co_idx in range(len(post_cond)): + post_cond = self._map_post_cond(desc_idx, map_idx, co_idx, + post_cond) + return post_cond + def _add_transitions(self, transition_map: _TransitionMap, desc: Dict[str, Any], desc_idx: int, - skip_post_cond: Tuple[int, ...], co_idx: int, + skip_post_cond: Tuple[Any, ...], co_idx: int, map_idx: int, pre_cond_na: Tuple[int, ...]) -> None: # pylint: disable=too-many-arguments # pylint: disable=too-many-locals @@ -576,16 +758,26 @@ class TransitionMap: "defined by transition map descriptor " f"{transition_map[map_idx][0].desc_idx}") transition_map[map_idx].append( - Transition(desc_idx, enabled_by, skip_post_cond[0], - pre_cond_na, skip_post_cond[1:])) + Transition( + desc_idx, enabled_by, skip_post_cond[0], pre_cond_na, + self._make_post_cond(desc_idx, map_idx, skip_post_cond))) def _add_default(self, transition_map: _TransitionMap, desc_idx: int, skip_post_cond: Tuple[int, ...]) -> None: - for transition in transition_map: + for map_idx, transition in enumerate(transition_map): if not transition: transition.append( - Transition(desc_idx, "1", skip_post_cond[0], - (0, ) * self._pre_co_count, skip_post_cond[1:])) + Transition( + desc_idx, "1", skip_post_cond[0], + (0, ) * self._pre_co_count, + self._make_post_cond(desc_idx, map_idx, + skip_post_cond))) + + def _get_post_cond(self, desc: Dict[str, Any], co_idx: int) -> Any: + info = desc["post-conditions"][self._post_co_idx_to_co_name[co_idx]] + if isinstance(info, str): + return self._post_co_idx_st_name_to_st_idx[co_idx][info] + return info def _build_map(self) -> _TransitionMap: transition_count = 1 @@ -601,9 +793,7 @@ class TransitionMap: if isinstance(desc["post-conditions"], dict): try: skip_post_cond = (0, ) + tuple( - self._post_co_idx_st_name_to_st_idx[co_idx][ - desc["post-conditions"][ - self._post_co_idx_to_co_name[co_idx]]] + self._get_post_cond(desc, co_idx) for co_idx in range(self._post_co_count)) except KeyError as err: msg = (f"transition map descriptor {desc_idx} of " diff --git a/spec/spec/requirement-action-exp-bool-list.yml b/spec/spec/requirement-action-exp-bool-list.yml new file mode 100644 index 00000000..1d565233 --- /dev/null +++ b/spec/spec/requirement-action-exp-bool-list.yml @@ -0,0 +1,16 @@ +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 +links: +- role: spec-member + uid: root +spec-description: null +spec-example: null +spec-info: + list: + description: null + spec-type: requirement-action-exp-bool +spec-name: Action Requirement Boolean Expression List +spec-type: requirement-action-exp-bool-list +type: spec diff --git a/spec/spec/requirement-action-exp-bool.yml b/spec/spec/requirement-action-exp-bool.yml new file mode 100644 index 00000000..c71cca1a --- /dev/null +++ b/spec/spec/requirement-action-exp-bool.yml @@ -0,0 +1,51 @@ +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 +links: +- role: spec-member + uid: root +spec-description: | + A value of this type is a boolean expression. +spec-example: null +spec-info: + dict: + attributes: + and: + description: | + The *and* operator evaluates to the *logical and* of the evaluation + results of the expressions in the list. + spec-type: requirement-action-exp-bool-list + not: + description: | + The *not* operator evaluates to the *logical not* of the evaluation + results of the expression. + spec-type: requirement-action-exp-bool + or: + description: | + The *or* operator evaluates to the *logical or* of the evaluation + results of the expressions in the list. + spec-type: requirement-action-exp-bool-list + post-conditions: + description: | + The *post-conditions* operator evaluates to true, if the + post-condition states of the associated transition are contained in + the specified post-condition set, otherwise to false. + spec-type: requirement-action-exp-conditions + pre-conditions: + description: | + The *pre-conditions* operator evaluates to true, if the pre-condition + states of the associated transition are contained in the specified + pre-condition set, otherwise to false. + spec-type: requirement-action-exp-conditions + description: | + Each attribute defines an operator. + mandatory-attributes: exactly-one + list: + description: | + This list of expressions evaluates to the *logical or* of the evaluation + results of the expressions in the list. + spec-type: requirement-action-exp-bool +spec-name: Action Requirement Boolean Expression +spec-type: requirement-action-exp-bool +type: spec diff --git a/spec/spec/requirement-action-exp-conditions.yml b/spec/spec/requirement-action-exp-conditions.yml new file mode 100644 index 00000000..64127028 --- /dev/null +++ b/spec/spec/requirement-action-exp-conditions.yml @@ -0,0 +1,26 @@ +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 +links: +- role: spec-member + uid: root +spec-description: null +spec-example: null +spec-info: + dict: + attributes: {} + description: | + This set of attributes defines for the specified conditions a set of + states. + generic-attributes: + description: | + There shall be at most one generic attribute key for each condition. + The key name shall be the condition name. The value of each generic + attribute shall be a set of states of the condition. + key-spec-type: requirement-action-name + value-spec-type: requirement-action-exp-states + mandatory-attributes: all +spec-name: Action Requirement Expression Condition Set +spec-type: requirement-action-exp-conditions +type: spec diff --git a/spec/spec/requirement-action-exp-state-name.yml b/spec/spec/requirement-action-exp-state-name.yml new file mode 100644 index 00000000..5d9d291d --- /dev/null +++ b/spec/spec/requirement-action-exp-state-name.yml @@ -0,0 +1,21 @@ +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 +links: +- role: spec-member + uid: root +spec-description: null +spec-example: null +spec-info: + str: + assert: + or: + - re: ^[A-Z][a-zA-Z0-9]+$ + - eq: N/A + description: | + It shall be the name of a state of the condition or ``N/A`` if the + condition is not applicable. +spec-name: Action Requirement Expression State Name +spec-type: requirement-action-exp-state-name +type: spec diff --git a/spec/spec/requirement-action-exp-states.yml b/spec/spec/requirement-action-exp-states.yml new file mode 100644 index 00000000..943ec381 --- /dev/null +++ b/spec/spec/requirement-action-exp-states.yml @@ -0,0 +1,25 @@ +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 +links: +- role: spec-member + uid: root +spec-description: null +spec-example: null +spec-info: + list: + description: | + The list defines a set of states of the condition. + spec-type: requirement-action-exp-state-name + str: + assert: + or: + - re: ^[A-Z][a-zA-Z0-9]+$ + - eq: N/A + description: | + It shall be the name of a state of the condition or ``N/A`` if the + condition is not applicable. +spec-name: Action Requirement Expression State Set +spec-type: requirement-action-exp-states +type: spec diff --git a/spec/spec/requirement-action-exp.yml b/spec/spec/requirement-action-exp.yml new file mode 100644 index 00000000..f5184ecb --- /dev/null +++ b/spec/spec/requirement-action-exp.yml @@ -0,0 +1,46 @@ +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 +links: +- role: spec-member + uid: root +spec-description: null +spec-example: null +spec-info: + dict: + attributes: + else: + description: | + It shall be the name of the state of the post-condition. + spec-type: requirement-action-exp-state-name + if: + description: | + If the boolean expression evaluates to true, then the state is + defined according to the ``then`` attribute value. + spec-type: requirement-action-exp-bool + then: + description: | + It shall be the name of the state of the post-condition. + spec-type: requirement-action-exp-state-name + then-specified-by: + description: | + It shall be the name of a pre-condition. The name of the state of + the pre-condition in the associated transition defines the name of + the state of the post-condition. + spec-type: requirement-action-name + specified-by: + description: | + It shall be the name of a pre-condition. The name of the state of + the pre-condition in the associated transition defines the name of + the state of the post-condition. + spec-type: requirement-action-name + description: | + This set of attributes defines an expression which may define the state + of a post-condition. The ``else`` and ``specified-by`` shall be used + individually. The ``if`` and ``then`` or ``then-specified-by`` + expressions shall be used together. + mandatory-attributes: at-least-one +spec-name: Action Requirement Expression +spec-type: requirement-action-exp +type: spec diff --git a/spec/spec/requirement-action-transition-post-state.yml b/spec/spec/requirement-action-transition-post-state.yml index 0b310629..e2f99c74 100644 --- a/spec/spec/requirement-action-transition-post-state.yml +++ b/spec/spec/requirement-action-transition-post-state.yml @@ -8,6 +8,11 @@ links: spec-description: null spec-example: null spec-info: + list: + description: | + The list contains expressions to define the state of the corresponding + post-condition. + spec-type: requirement-action-exp str: assert: or: diff --git a/spec/spec/requirement-action-transition-pre.yml b/spec/spec/requirement-action-transition-pre.yml index c33df7ab..12116c46 100644 --- a/spec/spec/requirement-action-transition-pre.yml +++ b/spec/spec/requirement-action-transition-pre.yml @@ -12,7 +12,7 @@ spec-info: attributes: {} description: | This set of attributes defines for each pre-condition the set of states - before the action for a transition in an actin requirement. + before the action for a transition in an action requirement. generic-attributes: description: | There shall be exactly one generic attribute key for each -- cgit v1.2.3