[rtems-central commit] validation: Add post-condition expressions
Sebastian Huber
sebh at rtems.org
Wed Mar 17 17:37:29 UTC 2021
Module: rtems-central
Branch: master
Commit: 2a4a2574340945c263e5b49f4ae5c9719a54d783
Changeset: http://git.rtems.org/rtems-central/commit/?id=2a4a2574340945c263e5b49f4ae5c9719a54d783
Author: Sebastian Huber <sebastian.huber at embedded-brains.de>
Date: Mon Mar 15 08:55:27 2021 +0100
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(-)
diff --git a/rtemsspec/tests/spec-validation/action2.yml b/rtemsspec/tests/spec-validation/action2.yml
index 626d8a7..4875bad 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 aeb2bbd..3c8614a 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 6945bdc..ae4b2c9 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 0000000..1d56523
--- /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 0000000..c71cca1
--- /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 0000000..6412702
--- /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 0000000..5d9d291
--- /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 0000000..943ec38
--- /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 0000000..f5184ec
--- /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 0b31062..e2f99c7 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 c33df7a..12116c4 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
More information about the vc
mailing list