[rtems-central commit] validation: Support N/A in the action transitions

Sebastian Huber sebh at rtems.org
Mon Jul 27 12:22:54 UTC 2020


Module:    rtems-central
Branch:    master
Commit:    244b2771339059836c1dc22c3664f1b4fa772f51
Changeset: http://git.rtems.org/rtems-central/commit/?id=244b2771339059836c1dc22c3664f1b4fa772f51

Author:    Sebastian Huber <sebastian.huber at embedded-brains.de>
Date:      Mon Jul 27 09:23:13 2020 +0200

validation: Support N/A in the action transitions

Sometimes the pre-conditions are not independent and it is necessary to
mark pre-conditions as not applicable in a particular transition.

---

 rtemsspec/tests/spec-validation/action2.yml        |  11 +-
 rtemsspec/tests/test_validation.py                 | 204 +++++++++++++++++++--
 rtemsspec/validation.py                            |  97 +++++++---
 spec/spec/requirement-action-name.yml              |   8 +-
 .../requirement-action-transition-pre-states.yml   |   8 +-
 5 files changed, 278 insertions(+), 50 deletions(-)

diff --git a/rtemsspec/tests/spec-validation/action2.yml b/rtemsspec/tests/spec-validation/action2.yml
index caafed7..a2a2334 100644
--- a/rtemsspec/tests/spec-validation/action2.yml
+++ b/rtemsspec/tests/spec-validation/action2.yml
@@ -138,7 +138,16 @@ transition-map:
     B: Y
   pre-conditions:
     A: all
-    B: all
+    B:
+    - X
+- enabled-by: true
+  post-conditions:
+    A: Y
+    B: X
+  pre-conditions:
+    A: N/A
+    B:
+    - Y
 rationale: null
 references: []
 text: |
diff --git a/rtemsspec/tests/test_validation.py b/rtemsspec/tests/test_validation.py
index 603d943..c9c4a9d 100644
--- a/rtemsspec/tests/test_validation.py
+++ b/rtemsspec/tests/test_validation.py
@@ -167,7 +167,8 @@ def test_validation(tmpdir):
 typedef enum {
   ClassicTaskIdentification_Pre_Name_Invalid,
   ClassicTaskIdentification_Pre_Name_Self,
-  ClassicTaskIdentification_Pre_Name_Valid
+  ClassicTaskIdentification_Pre_Name_Valid,
+  ClassicTaskIdentification_Pre_Name_NA
 } ClassicTaskIdentification_Pre_Name;
 
 typedef enum {
@@ -176,12 +177,14 @@ typedef enum {
   ClassicTaskIdentification_Pre_Node_Invalid,
   ClassicTaskIdentification_Pre_Node_SearchAll,
   ClassicTaskIdentification_Pre_Node_SearchOther,
-  ClassicTaskIdentification_Pre_Node_SearchLocal
+  ClassicTaskIdentification_Pre_Node_SearchLocal,
+  ClassicTaskIdentification_Pre_Node_NA
 } ClassicTaskIdentification_Pre_Node;
 
 typedef enum {
   ClassicTaskIdentification_Pre_Id_NullPtr,
-  ClassicTaskIdentification_Pre_Id_Valid
+  ClassicTaskIdentification_Pre_Id_Valid,
+  ClassicTaskIdentification_Pre_Id_NA
 } ClassicTaskIdentification_Pre_Id;
 
 typedef enum {
@@ -189,7 +192,8 @@ typedef enum {
   ClassicTaskIdentification_Post_Status_InvAddr,
   ClassicTaskIdentification_Post_Status_InvName,
   ClassicTaskIdentification_Post_Status_InvNode,
-  ClassicTaskIdentification_Post_Status_InvId
+  ClassicTaskIdentification_Post_Status_InvId,
+  ClassicTaskIdentification_Post_Status_NA
 } ClassicTaskIdentification_Post_Status;
 
 typedef enum {
@@ -197,7 +201,8 @@ typedef enum {
   ClassicTaskIdentification_Post_Id_NullPtr,
   ClassicTaskIdentification_Post_Id_Self,
   ClassicTaskIdentification_Post_Id_LocalTask,
-  ClassicTaskIdentification_Post_Id_RemoteTask
+  ClassicTaskIdentification_Post_Id_RemoteTask,
+  ClassicTaskIdentification_Post_Id_NA
 } ClassicTaskIdentification_Post_Id;
 
 /**
@@ -289,6 +294,9 @@ static void ClassicTaskIdentification_Pre_Name_Prepare(
       ctx->name = rtems_build_name( 'T', 'A', 'S', 'K' );
       break;
     }
+
+    case ClassicTaskIdentification_Pre_Name_NA:
+      break;
   }
 
   /* Epilogue */
@@ -329,6 +337,9 @@ static void ClassicTaskIdentification_Pre_Node_Prepare(
       ctx->node = RTEMS_SEARCH_LOCAL_NODE;
       break;
     }
+
+    case ClassicTaskIdentification_Pre_Node_NA:
+      break;
   }
 }
 
@@ -348,6 +359,9 @@ static void ClassicTaskIdentification_Pre_Id_Prepare(
       ctx->id = &ctx->id_value;
       break;
     }
+
+    case ClassicTaskIdentification_Pre_Id_NA:
+      break;
   }
 }
 
@@ -381,6 +395,9 @@ static void ClassicTaskIdentification_Post_Status_Check(
       T_rsc(ctx->status, RTEMS_INVALID_ID);
       break;
     }
+
+    case ClassicTaskIdentification_Post_Status_NA:
+      break;
   }
 }
 
@@ -418,6 +435,9 @@ static void ClassicTaskIdentification_Post_Id_Check(
       T_eq_u32(ctx->id_value, ctx->id_remote_task);
       break;
     }
+
+    case ClassicTaskIdentification_Post_Id_NA:
+      break;
   }
 }
 
@@ -614,6 +634,94 @@ static const uint8_t ClassicTaskIdentification_TransitionMap[][ 2 ] = {
   }
 };
 
+static const struct {
+  uint8_t Pre_Name_NA : 1;
+  uint8_t Pre_Node_NA : 1;
+  uint8_t Pre_Id_NA : 1;
+} ClassicTaskIdentification_TransitionInfo[] = {
+  {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+#if defined(RTEMS_MULTIPROCESSING)
+    0, 0, 0
+#else
+    0, 0, 0
+#endif
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }, {
+#if defined(RTEMS_MULTIPROCESSING)
+    0, 0, 0
+#else
+    0, 0, 0
+#endif
+  }, {
+    0, 0, 0
+  }, {
+    0, 0, 0
+  }
+};
+
 /**
  * @fn void T_case_body_ClassicTaskIdentification( void )
  *
@@ -635,19 +743,37 @@ T_TEST_CASE_FIXTURE(
 
   for (
     ctx->pcs[ 0 ] = ClassicTaskIdentification_Pre_Name_Invalid;
-    ctx->pcs[ 0 ] != ClassicTaskIdentification_Pre_Name_Valid + 1;
+    ctx->pcs[ 0 ] < ClassicTaskIdentification_Pre_Name_NA;
     ++ctx->pcs[ 0 ]
   ) {
+    if ( ClassicTaskIdentification_TransitionInfo[ index ].Pre_Name_NA ) {
+      ctx->pcs[ 0 ] = ClassicTaskIdentification_Pre_Name_NA;
+      index += ( ClassicTaskIdentification_Pre_Name_NA - 1 )
+        * ClassicTaskIdentification_Pre_Node_NA
+        * ClassicTaskIdentification_Pre_Id_NA;
+    }
+
     for (
       ctx->pcs[ 1 ] = ClassicTaskIdentification_Pre_Node_Local;
-      ctx->pcs[ 1 ] != ClassicTaskIdentification_Pre_Node_SearchLocal + 1;
+      ctx->pcs[ 1 ] < ClassicTaskIdentification_Pre_Node_NA;
       ++ctx->pcs[ 1 ]
     ) {
+      if ( ClassicTaskIdentification_TransitionInfo[ index ].Pre_Node_NA ) {
+        ctx->pcs[ 1 ] = ClassicTaskIdentification_Pre_Node_NA;
+        index += ( ClassicTaskIdentification_Pre_Node_NA - 1 )
+          * ClassicTaskIdentification_Pre_Id_NA;
+      }
+
       for (
         ctx->pcs[ 2 ] = ClassicTaskIdentification_Pre_Id_NullPtr;
-        ctx->pcs[ 2 ] != ClassicTaskIdentification_Pre_Id_Valid + 1;
+        ctx->pcs[ 2 ] < ClassicTaskIdentification_Pre_Id_NA;
         ++ctx->pcs[ 2 ]
       ) {
+        if ( ClassicTaskIdentification_TransitionInfo[ index ].Pre_Id_NA ) {
+          ctx->pcs[ 2 ] = ClassicTaskIdentification_Pre_Id_NA;
+          index += ( ClassicTaskIdentification_Pre_Id_NA - 1 );
+        }
+
         ClassicTaskIdentification_Pre_Name_Prepare( ctx, ctx->pcs[ 0 ] );
         ClassicTaskIdentification_Pre_Node_Prepare( ctx, ctx->pcs[ 1 ] );
         ClassicTaskIdentification_Pre_Id_Prepare( ctx, ctx->pcs[ 2 ] );
@@ -916,22 +1042,26 @@ extern "C" {
 
 typedef enum {
   Action2_Pre_A_X,
-  Action2_Pre_A_Y
+  Action2_Pre_A_Y,
+  Action2_Pre_A_NA
 } Action2_Pre_A;
 
 typedef enum {
   Action2_Pre_B_X,
-  Action2_Pre_B_Y
+  Action2_Pre_B_Y,
+  Action2_Pre_B_NA
 } Action2_Pre_B;
 
 typedef enum {
   Action2_Post_A_X,
-  Action2_Post_A_Y
+  Action2_Post_A_Y,
+  Action2_Post_A_NA
 } Action2_Post_A;
 
 typedef enum {
   Action2_Post_B_X,
-  Action2_Post_B_Y
+  Action2_Post_B_Y,
+  Action2_Post_B_NA
 } Action2_Post_B;
 
 /* Header code for Action 2 with Action2_Run() */
@@ -1088,6 +1218,9 @@ static void Action2_Pre_A_Prepare( Action2_Context *ctx, Action2_Pre_A state )
       /* Pre A Y */
       break;
     }
+
+    case Action2_Pre_A_NA:
+      break;
   }
 
   /* Pre A epilogue. */
@@ -1107,6 +1240,9 @@ static void Action2_Pre_B_Prepare( Action2_Context *ctx, Action2_Pre_B state )
       /* Pre B Y */
       break;
     }
+
+    case Action2_Pre_B_NA:
+      break;
   }
 
   /* Pre B epilogue. */
@@ -1126,6 +1262,9 @@ static void Action2_Post_A_Check( Action2_Context *ctx, Action2_Post_A state )
       /* Post A Y */
       break;
     }
+
+    case Action2_Post_A_NA:
+      break;
   }
 
   /* Post A epilogue. */
@@ -1145,6 +1284,9 @@ static void Action2_Post_B_Check( Action2_Context *ctx, Action2_Post_B state )
       /* Post B Y */
       break;
     }
+
+    case Action2_Post_B_NA:
+      break;
   }
 
   /* Post B epilogue. */
@@ -1212,14 +1354,29 @@ static const uint8_t Action2_TransitionMap[][ 2 ] = {
     Action2_Post_A_X,
     Action2_Post_B_Y
   }, {
-    Action2_Post_A_X,
-    Action2_Post_B_Y
+    Action2_Post_A_Y,
+    Action2_Post_B_X
   }, {
     Action2_Post_A_X,
     Action2_Post_B_Y
   }, {
-    Action2_Post_A_X,
-    Action2_Post_B_Y
+    Action2_Post_A_Y,
+    Action2_Post_B_X
+  }
+};
+
+static const struct {
+  uint8_t Pre_A_NA : 1;
+  uint8_t Pre_B_NA : 1;
+} Action2_TransitionInfo[] = {
+  {
+    0, 0
+  }, {
+    1, 0
+  }, {
+    0, 0
+  }, {
+    1, 0
   }
 };
 
@@ -1240,14 +1397,25 @@ void Action2_Run( int *a, int b, int *c )
 
   for (
     ctx->pcs[ 0 ] = Action2_Pre_A_X;
-    ctx->pcs[ 0 ] != Action2_Pre_A_Y + 1;
+    ctx->pcs[ 0 ] < Action2_Pre_A_NA;
     ++ctx->pcs[ 0 ]
   ) {
+    if ( Action2_TransitionInfo[ index ].Pre_A_NA ) {
+      ctx->pcs[ 0 ] = Action2_Pre_A_NA;
+      index += ( Action2_Pre_A_NA - 1 )
+        * Action2_Pre_B_NA;
+    }
+
     for (
       ctx->pcs[ 1 ] = Action2_Pre_B_X;
-      ctx->pcs[ 1 ] != Action2_Pre_B_Y + 1;
+      ctx->pcs[ 1 ] < Action2_Pre_B_NA;
       ++ctx->pcs[ 1 ]
     ) {
+      if ( Action2_TransitionInfo[ index ].Pre_B_NA ) {
+        ctx->pcs[ 1 ] = Action2_Pre_B_NA;
+        index += ( Action2_Pre_B_NA - 1 );
+      }
+
       Action2_Pre_A_Prepare( ctx, ctx->pcs[ 0 ] );
       Action2_Pre_B_Prepare( ctx, ctx->pcs[ 1 ] );
       /* Action */
diff --git a/rtemsspec/validation.py b/rtemsspec/validation.py
index fd75824..f914143 100644
--- a/rtemsspec/validation.py
+++ b/rtemsspec/validation.py
@@ -25,6 +25,7 @@
 # POSSIBILITY OF SUCH DAMAGE.
 
 import itertools
+import math
 import os
 from typing import Any, Dict, List, NamedTuple, Optional, Tuple
 
@@ -200,14 +201,17 @@ class _TestSuiteItem(_TestItem):
         content.add("/** @} */")
 
 
-class _PostCondition(NamedTuple):
-    """ A set of post conditions with an enabled by expression. """
+class _Transition(NamedTuple):
+    """
+    A transition to a set of post conditions with an enabled by expression.
+    """
     enabled_by: str
-    conditions: Tuple[int, ...]
+    post_conditions: Tuple[int, ...]
+    info: str
 
 
 _DirectiveIndexToEnum = Tuple[Tuple[str, ...], ...]
-_TransitionMap = List[List[_PostCondition]]
+_TransitionMap = List[List[_Transition]]
 
 
 def _directive_state_to_index(
@@ -224,7 +228,8 @@ def _directive_index_to_enum(prefix: str,
         tuple([f"{prefix}_{condition['name']}"] + [
             f"{prefix}_{condition['name']}_{state['name']}"
             for state in condition["states"]
-        ]) for index, condition in enumerate(conditions))
+        ] + [f"{prefix}_{condition['name']}_NA"])
+        for index, condition in enumerate(conditions))
 
 
 def _directive_add_enum(content: CContent,
@@ -353,7 +358,8 @@ class _TestDirectiveItem(_TestItem):
     def _add_transitions(self, condition_index: int, map_index: int,
                          transition: Dict[str,
                                           Any], transition_map: _TransitionMap,
-                         post: Tuple[int, ...]) -> None:
+                         pre_cond_not_applicables: List[str],
+                         post_cond: Tuple[int, ...]) -> None:
         # pylint: disable=too-many-arguments
         if condition_index < self._pre_condition_count:
             condition = self._pre_index_to_condition[condition_index]
@@ -361,22 +367,27 @@ class _TestDirectiveItem(_TestItem):
             map_index *= state_count
             states = transition["pre-conditions"][condition["name"]]
             if isinstance(states, str):
-                assert states == "all"
+                assert states in ["all", "N/A"]
                 for index in range(state_count):
-                    self._add_transitions(condition_index + 1,
-                                          map_index + index, transition,
-                                          transition_map, post)
+                    self._add_transitions(
+                        condition_index + 1, map_index + index, transition,
+                        transition_map,
+                        pre_cond_not_applicables + [str(int(states == "N/A"))],
+                        post_cond)
             else:
                 for state in states:
                     self._add_transitions(
                         condition_index + 1, map_index +
                         self._pre_state_to_index[condition_index][state],
-                        transition, transition_map, post)
+                        transition, transition_map,
+                        pre_cond_not_applicables + ["0"], post_cond)
         else:
             enabled_by = enabled_by_to_exp(transition["enabled-by"],
                                            ExpressionMapper())
             assert enabled_by != "1" or not transition_map[map_index]
-            transition_map[map_index].append(_PostCondition(enabled_by, post))
+            transition_map[map_index].append(
+                _Transition(enabled_by, post_cond,
+                            "    " + ", ".join(pre_cond_not_applicables)))
 
     def _get_transition_map(self) -> _TransitionMap:
         transition_count = 1
@@ -390,7 +401,7 @@ class _TestDirectiveItem(_TestItem):
             post = tuple(self._post_state_to_index[index][
                 transition["post-conditions"][self._post_index_to_name[index]]]
                          for index in range(self._post_condition_count))
-            self._add_transitions(0, 0, transition, transition_map, post)
+            self._add_transitions(0, 0, transition, transition_map, [], post)
         return transition_map
 
     def _post_condition_enumerators(self, conditions: Any) -> str:
@@ -405,30 +416,49 @@ class _TestDirectiveItem(_TestItem):
             f"{self.ident}_TransitionMap[][ {self._post_condition_count} ]"
             " = {", "  {"
         ])
-        elements = []
+        map_elements = []
+        info_elements = []
         for transistions in transition_map:
             assert transistions[0].enabled_by == "1"
             if len(transistions) == 1:
-                elements.append(
+                map_elements.append(
                     self._post_condition_enumerators(
-                        transistions[0].conditions))
+                        transistions[0].post_conditions))
+                info_elements.append(transistions[0].info)
             else:
                 ifelse = "#if "
-                enumerators = []  # type: List[str]
+                map_enumerators = []  # type: List[str]
+                info_enumerators = []  # type: List[str]
                 for variant in transistions[1:]:
-                    enumerators.append(ifelse + variant.enabled_by)
-                    enumerators.append(
-                        self._post_condition_enumerators(variant.conditions))
+                    map_enumerators.append(ifelse + variant.enabled_by)
+                    info_enumerators.append(ifelse + variant.enabled_by)
+                    map_enumerators.append(
+                        self._post_condition_enumerators(
+                            variant.post_conditions))
+                    info_enumerators.append(variant.info)
                     ifelse = "#elif "
-                enumerators.append("#else")
-                enumerators.append(
+                map_enumerators.append("#else")
+                info_enumerators.append("#else")
+                map_enumerators.append(
                     self._post_condition_enumerators(
-                        transistions[0].conditions))
-                enumerators.append("#endif")
-                elements.append("\n".join(enumerators))
-        content.append(["\n  }, {\n".join(elements), "  }", "};"])
+                        transistions[0].post_conditions))
+                info_enumerators.append(transistions[0].info)
+                map_enumerators.append("#endif")
+                info_enumerators.append("#endif")
+                map_elements.append("\n".join(map_enumerators))
+                info_elements.append("\n".join(info_enumerators))
+        content.append(["\n  }, {\n".join(map_elements), "  }", "};"])
+        pre_bits = 2**max(math.ceil(math.log2(self._pre_condition_count)), 3)
+        content.add("static const struct {")
+        with content.indent():
+            for condition in self["pre-conditions"]:
+                content.append(
+                    f"uint{pre_bits}_t Pre_{condition['name']}_NA : 1;")
+        content.add([f"}} {self.ident}_TransitionInfo[] = {{", "  {"])
+        content.append(["\n  }, {\n".join(info_elements), "  }", "};"])
 
     def _add_action(self, content: CContent) -> None:
+        content.add_blank_line()
         for index, enum in enumerate(self._pre_index_to_enum):
             content.append(f"{enum[0]}_Prepare( ctx, ctx->pcs[ {index} ] );")
         content.append(self.substitute_code(self["test-action"]))
@@ -445,8 +475,18 @@ class _TestDirectiveItem(_TestItem):
             var = f"ctx->pcs[ {index} ]"
             begin = self._pre_index_to_enum[index][1]
             end = self._pre_index_to_enum[index][-1]
-            with content.for_loop(f"{var} = {begin}", f"{var} != {end} + 1",
+            with content.for_loop(f"{var} = {begin}", f"{var} < {end}",
                                   f"++{var}"):
+                name = self._item['pre-conditions'][index]["name"]
+                pre_na = f"{self.ident}_TransitionInfo[ index ].Pre_{name}_NA"
+                with content.condition(pre_na):
+                    content.append(f"{var} = {end};")
+                    content.append(f"index += ( {end} - 1 )")
+                    for index_2 in range(index + 1, self._pre_condition_count):
+                        with content.indent():
+                            content.append(
+                                f"* {self._pre_index_to_enum[index_2][-1]}")
+                    content.lines[-1] += ";"
                 self._add_for_loops(content, index + 1)
         else:
             self._add_action(content)
@@ -508,6 +548,9 @@ class _TestDirectiveItem(_TestItem):
                                 self.substitute_code(state["test-code"]))
                             content.append("break;")
                         content.add("}")
+                    content.add(f"case {enum[-1]}:")
+                    with content.indent():
+                        content.append("break;")
                 content.add("}")
                 content.add(self.substitute_code(condition["test-epilogue"]))
 
diff --git a/spec/spec/requirement-action-name.yml b/spec/spec/requirement-action-name.yml
index 62ce8b3..76451ef 100644
--- a/spec/spec/requirement-action-name.yml
+++ b/spec/spec/requirement-action-name.yml
@@ -10,14 +10,18 @@ spec-example: null
 spec-info:
   str:
     assert:
-    - re: ^[A-Z][a-zA-Z0-9]+$
+      and:
+      - re: ^[A-Z][a-zA-Z0-9]+$
+      - not:
+          eq: NA
     description: |
       It shall be the name of a condition or a state of a condition used to
       define pre-conditions and post-conditions of an action requirement.  It
       shall be formatted in CamelCase.  It should be brief and abbreviated.
       The rationale for this is that the names are used in tables and the
       horizontal space is limited by the page width.  The more conditions you
-      have in an action requirement, the shorter the names should be.
+      have in an action requirement, the shorter the names should be.  The name
+      ``NA`` is reserved and indicates that a condition is not applicable.
 spec-name: Action Requirement Name
 spec-type: requirement-action-name
 type: spec
diff --git a/spec/spec/requirement-action-transition-pre-states.yml b/spec/spec/requirement-action-transition-pre-states.yml
index 4c55c87..0d417b1 100644
--- a/spec/spec/requirement-action-transition-pre-states.yml
+++ b/spec/spec/requirement-action-transition-pre-states.yml
@@ -15,9 +15,13 @@ spec-info:
     spec-type: requirement-action-name
   str:
     assert:
-      eq: all
+      in:
+      - all
+      - N/A
     description: |
-      The value represents all states of the pre-condition in the transition.
+      The value ``all`` represents all states of the pre-condition in this
+      transition.  The value ``N/A`` marks the pre-condition as not applicable
+      in this transition.
 spec-name: Action Requirement Transition Pre-Condition State Set
 spec-type: requirement-action-transition-pre-states
 type: spec



More information about the vc mailing list