Changeset 244b277 in rtems-central


Ignore:
Timestamp:
Jul 27, 2020, 7:23:13 AM (2 weeks ago)
Author:
Sebastian Huber <sebastian.huber@…>
Branches:
master
Children:
55e17d2
Parents:
fd31f9d
git-author:
Sebastian Huber <sebastian.huber@…> (07/27/20 07:23:13)
git-committer:
Sebastian Huber <sebastian.huber@…> (07/27/20 12:21:19)
Message:

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.

Files:
5 edited

Legend:

Unmodified
Added
Removed
  • rtemsspec/tests/spec-validation/action2.yml

    rfd31f9d r244b277  
    139139  pre-conditions:
    140140    A: all
    141     B: all
     141    B:
     142    - X
     143- enabled-by: true
     144  post-conditions:
     145    A: Y
     146    B: X
     147  pre-conditions:
     148    A: N/A
     149    B:
     150    - Y
    142151rationale: null
    143152references: []
  • rtemsspec/tests/test_validation.py

    rfd31f9d r244b277  
    168168  ClassicTaskIdentification_Pre_Name_Invalid,
    169169  ClassicTaskIdentification_Pre_Name_Self,
    170   ClassicTaskIdentification_Pre_Name_Valid
     170  ClassicTaskIdentification_Pre_Name_Valid,
     171  ClassicTaskIdentification_Pre_Name_NA
    171172} ClassicTaskIdentification_Pre_Name;
    172173
     
    177178  ClassicTaskIdentification_Pre_Node_SearchAll,
    178179  ClassicTaskIdentification_Pre_Node_SearchOther,
    179   ClassicTaskIdentification_Pre_Node_SearchLocal
     180  ClassicTaskIdentification_Pre_Node_SearchLocal,
     181  ClassicTaskIdentification_Pre_Node_NA
    180182} ClassicTaskIdentification_Pre_Node;
    181183
    182184typedef enum {
    183185  ClassicTaskIdentification_Pre_Id_NullPtr,
    184   ClassicTaskIdentification_Pre_Id_Valid
     186  ClassicTaskIdentification_Pre_Id_Valid,
     187  ClassicTaskIdentification_Pre_Id_NA
    185188} ClassicTaskIdentification_Pre_Id;
    186189
     
    190193  ClassicTaskIdentification_Post_Status_InvName,
    191194  ClassicTaskIdentification_Post_Status_InvNode,
    192   ClassicTaskIdentification_Post_Status_InvId
     195  ClassicTaskIdentification_Post_Status_InvId,
     196  ClassicTaskIdentification_Post_Status_NA
    193197} ClassicTaskIdentification_Post_Status;
    194198
     
    198202  ClassicTaskIdentification_Post_Id_Self,
    199203  ClassicTaskIdentification_Post_Id_LocalTask,
    200   ClassicTaskIdentification_Post_Id_RemoteTask
     204  ClassicTaskIdentification_Post_Id_RemoteTask,
     205  ClassicTaskIdentification_Post_Id_NA
    201206} ClassicTaskIdentification_Post_Id;
    202207
     
    290295      break;
    291296    }
     297
     298    case ClassicTaskIdentification_Pre_Name_NA:
     299      break;
    292300  }
    293301
     
    330338      break;
    331339    }
     340
     341    case ClassicTaskIdentification_Pre_Node_NA:
     342      break;
    332343  }
    333344}
     
    349360      break;
    350361    }
     362
     363    case ClassicTaskIdentification_Pre_Id_NA:
     364      break;
    351365  }
    352366}
     
    382396      break;
    383397    }
     398
     399    case ClassicTaskIdentification_Post_Status_NA:
     400      break;
    384401  }
    385402}
     
    419436      break;
    420437    }
     438
     439    case ClassicTaskIdentification_Post_Id_NA:
     440      break;
    421441  }
    422442}
     
    615635};
    616636
     637static const struct {
     638  uint8_t Pre_Name_NA : 1;
     639  uint8_t Pre_Node_NA : 1;
     640  uint8_t Pre_Id_NA : 1;
     641} ClassicTaskIdentification_TransitionInfo[] = {
     642  {
     643    0, 0, 0
     644  }, {
     645    0, 0, 0
     646  }, {
     647    0, 0, 0
     648  }, {
     649    0, 0, 0
     650  }, {
     651    0, 0, 0
     652  }, {
     653    0, 0, 0
     654  }, {
     655    0, 0, 0
     656  }, {
     657    0, 0, 0
     658  }, {
     659    0, 0, 0
     660  }, {
     661    0, 0, 0
     662  }, {
     663    0, 0, 0
     664  }, {
     665    0, 0, 0
     666  }, {
     667    0, 0, 0
     668  }, {
     669    0, 0, 0
     670  }, {
     671    0, 0, 0
     672  }, {
     673    0, 0, 0
     674  }, {
     675    0, 0, 0
     676  }, {
     677    0, 0, 0
     678  }, {
     679    0, 0, 0
     680  }, {
     681    0, 0, 0
     682  }, {
     683    0, 0, 0
     684  }, {
     685    0, 0, 0
     686  }, {
     687    0, 0, 0
     688  }, {
     689    0, 0, 0
     690  }, {
     691    0, 0, 0
     692  }, {
     693    0, 0, 0
     694  }, {
     695    0, 0, 0
     696  }, {
     697#if defined(RTEMS_MULTIPROCESSING)
     698    0, 0, 0
     699#else
     700    0, 0, 0
     701#endif
     702  }, {
     703    0, 0, 0
     704  }, {
     705    0, 0, 0
     706  }, {
     707    0, 0, 0
     708  }, {
     709    0, 0, 0
     710  }, {
     711    0, 0, 0
     712  }, {
     713#if defined(RTEMS_MULTIPROCESSING)
     714    0, 0, 0
     715#else
     716    0, 0, 0
     717#endif
     718  }, {
     719    0, 0, 0
     720  }, {
     721    0, 0, 0
     722  }
     723};
     724
    617725/**
    618726 * @fn void T_case_body_ClassicTaskIdentification( void )
     
    636744  for (
    637745    ctx->pcs[ 0 ] = ClassicTaskIdentification_Pre_Name_Invalid;
    638     ctx->pcs[ 0 ] != ClassicTaskIdentification_Pre_Name_Valid + 1;
     746    ctx->pcs[ 0 ] < ClassicTaskIdentification_Pre_Name_NA;
    639747    ++ctx->pcs[ 0 ]
    640748  ) {
     749    if ( ClassicTaskIdentification_TransitionInfo[ index ].Pre_Name_NA ) {
     750      ctx->pcs[ 0 ] = ClassicTaskIdentification_Pre_Name_NA;
     751      index += ( ClassicTaskIdentification_Pre_Name_NA - 1 )
     752        * ClassicTaskIdentification_Pre_Node_NA
     753        * ClassicTaskIdentification_Pre_Id_NA;
     754    }
     755
    641756    for (
    642757      ctx->pcs[ 1 ] = ClassicTaskIdentification_Pre_Node_Local;
    643       ctx->pcs[ 1 ] != ClassicTaskIdentification_Pre_Node_SearchLocal + 1;
     758      ctx->pcs[ 1 ] < ClassicTaskIdentification_Pre_Node_NA;
    644759      ++ctx->pcs[ 1 ]
    645760    ) {
     761      if ( ClassicTaskIdentification_TransitionInfo[ index ].Pre_Node_NA ) {
     762        ctx->pcs[ 1 ] = ClassicTaskIdentification_Pre_Node_NA;
     763        index += ( ClassicTaskIdentification_Pre_Node_NA - 1 )
     764          * ClassicTaskIdentification_Pre_Id_NA;
     765      }
     766
    646767      for (
    647768        ctx->pcs[ 2 ] = ClassicTaskIdentification_Pre_Id_NullPtr;
    648         ctx->pcs[ 2 ] != ClassicTaskIdentification_Pre_Id_Valid + 1;
     769        ctx->pcs[ 2 ] < ClassicTaskIdentification_Pre_Id_NA;
    649770        ++ctx->pcs[ 2 ]
    650771      ) {
     772        if ( ClassicTaskIdentification_TransitionInfo[ index ].Pre_Id_NA ) {
     773          ctx->pcs[ 2 ] = ClassicTaskIdentification_Pre_Id_NA;
     774          index += ( ClassicTaskIdentification_Pre_Id_NA - 1 );
     775        }
     776
    651777        ClassicTaskIdentification_Pre_Name_Prepare( ctx, ctx->pcs[ 0 ] );
    652778        ClassicTaskIdentification_Pre_Node_Prepare( ctx, ctx->pcs[ 1 ] );
     
    9171043typedef enum {
    9181044  Action2_Pre_A_X,
    919   Action2_Pre_A_Y
     1045  Action2_Pre_A_Y,
     1046  Action2_Pre_A_NA
    9201047} Action2_Pre_A;
    9211048
    9221049typedef enum {
    9231050  Action2_Pre_B_X,
    924   Action2_Pre_B_Y
     1051  Action2_Pre_B_Y,
     1052  Action2_Pre_B_NA
    9251053} Action2_Pre_B;
    9261054
    9271055typedef enum {
    9281056  Action2_Post_A_X,
    929   Action2_Post_A_Y
     1057  Action2_Post_A_Y,
     1058  Action2_Post_A_NA
    9301059} Action2_Post_A;
    9311060
    9321061typedef enum {
    9331062  Action2_Post_B_X,
    934   Action2_Post_B_Y
     1063  Action2_Post_B_Y,
     1064  Action2_Post_B_NA
    9351065} Action2_Post_B;
    9361066
     
    10891219      break;
    10901220    }
     1221
     1222    case Action2_Pre_A_NA:
     1223      break;
    10911224  }
    10921225
     
    11081241      break;
    11091242    }
     1243
     1244    case Action2_Pre_B_NA:
     1245      break;
    11101246  }
    11111247
     
    11271263      break;
    11281264    }
     1265
     1266    case Action2_Post_A_NA:
     1267      break;
    11291268  }
    11301269
     
    11461285      break;
    11471286    }
     1287
     1288    case Action2_Post_B_NA:
     1289      break;
    11481290  }
    11491291
     
    12131355    Action2_Post_B_Y
    12141356  }, {
     1357    Action2_Post_A_Y,
     1358    Action2_Post_B_X
     1359  }, {
    12151360    Action2_Post_A_X,
    12161361    Action2_Post_B_Y
    12171362  }, {
    1218     Action2_Post_A_X,
    1219     Action2_Post_B_Y
    1220   }, {
    1221     Action2_Post_A_X,
    1222     Action2_Post_B_Y
     1363    Action2_Post_A_Y,
     1364    Action2_Post_B_X
     1365  }
     1366};
     1367
     1368static const struct {
     1369  uint8_t Pre_A_NA : 1;
     1370  uint8_t Pre_B_NA : 1;
     1371} Action2_TransitionInfo[] = {
     1372  {
     1373    0, 0
     1374  }, {
     1375    1, 0
     1376  }, {
     1377    0, 0
     1378  }, {
     1379    1, 0
    12231380  }
    12241381};
     
    12411398  for (
    12421399    ctx->pcs[ 0 ] = Action2_Pre_A_X;
    1243     ctx->pcs[ 0 ] != Action2_Pre_A_Y + 1;
     1400    ctx->pcs[ 0 ] < Action2_Pre_A_NA;
    12441401    ++ctx->pcs[ 0 ]
    12451402  ) {
     1403    if ( Action2_TransitionInfo[ index ].Pre_A_NA ) {
     1404      ctx->pcs[ 0 ] = Action2_Pre_A_NA;
     1405      index += ( Action2_Pre_A_NA - 1 )
     1406        * Action2_Pre_B_NA;
     1407    }
     1408
    12461409    for (
    12471410      ctx->pcs[ 1 ] = Action2_Pre_B_X;
    1248       ctx->pcs[ 1 ] != Action2_Pre_B_Y + 1;
     1411      ctx->pcs[ 1 ] < Action2_Pre_B_NA;
    12491412      ++ctx->pcs[ 1 ]
    12501413    ) {
     1414      if ( Action2_TransitionInfo[ index ].Pre_B_NA ) {
     1415        ctx->pcs[ 1 ] = Action2_Pre_B_NA;
     1416        index += ( Action2_Pre_B_NA - 1 );
     1417      }
     1418
    12511419      Action2_Pre_A_Prepare( ctx, ctx->pcs[ 0 ] );
    12521420      Action2_Pre_B_Prepare( ctx, ctx->pcs[ 1 ] );
  • rtemsspec/validation.py

    rfd31f9d r244b277  
    2626
    2727import itertools
     28import math
    2829import os
    2930from typing import Any, Dict, List, NamedTuple, Optional, Tuple
     
    201202
    202203
    203 class _PostCondition(NamedTuple):
    204     """ A set of post conditions with an enabled by expression. """
     204class _Transition(NamedTuple):
     205    """
     206    A transition to a set of post conditions with an enabled by expression.
     207    """
    205208    enabled_by: str
    206     conditions: Tuple[int, ...]
     209    post_conditions: Tuple[int, ...]
     210    info: str
    207211
    208212
    209213_DirectiveIndexToEnum = Tuple[Tuple[str, ...], ...]
    210 _TransitionMap = List[List[_PostCondition]]
     214_TransitionMap = List[List[_Transition]]
    211215
    212216
     
    225229            f"{prefix}_{condition['name']}_{state['name']}"
    226230            for state in condition["states"]
    227         ]) for index, condition in enumerate(conditions))
     231        ] + [f"{prefix}_{condition['name']}_NA"])
     232        for index, condition in enumerate(conditions))
    228233
    229234
     
    354359                         transition: Dict[str,
    355360                                          Any], transition_map: _TransitionMap,
    356                          post: Tuple[int, ...]) -> None:
     361                         pre_cond_not_applicables: List[str],
     362                         post_cond: Tuple[int, ...]) -> None:
    357363        # pylint: disable=too-many-arguments
    358364        if condition_index < self._pre_condition_count:
     
    362368            states = transition["pre-conditions"][condition["name"]]
    363369            if isinstance(states, str):
    364                 assert states == "all"
     370                assert states in ["all", "N/A"]
    365371                for index in range(state_count):
    366                     self._add_transitions(condition_index + 1,
    367                                           map_index + index, transition,
    368                                           transition_map, post)
     372                    self._add_transitions(
     373                        condition_index + 1, map_index + index, transition,
     374                        transition_map,
     375                        pre_cond_not_applicables + [str(int(states == "N/A"))],
     376                        post_cond)
    369377            else:
    370378                for state in states:
     
    372380                        condition_index + 1, map_index +
    373381                        self._pre_state_to_index[condition_index][state],
    374                         transition, transition_map, post)
     382                        transition, transition_map,
     383                        pre_cond_not_applicables + ["0"], post_cond)
    375384        else:
    376385            enabled_by = enabled_by_to_exp(transition["enabled-by"],
    377386                                           ExpressionMapper())
    378387            assert enabled_by != "1" or not transition_map[map_index]
    379             transition_map[map_index].append(_PostCondition(enabled_by, post))
     388            transition_map[map_index].append(
     389                _Transition(enabled_by, post_cond,
     390                            "    " + ", ".join(pre_cond_not_applicables)))
    380391
    381392    def _get_transition_map(self) -> _TransitionMap:
     
    391402                transition["post-conditions"][self._post_index_to_name[index]]]
    392403                         for index in range(self._post_condition_count))
    393             self._add_transitions(0, 0, transition, transition_map, post)
     404            self._add_transitions(0, 0, transition, transition_map, [], post)
    394405        return transition_map
    395406
     
    406417            " = {", "  {"
    407418        ])
    408         elements = []
     419        map_elements = []
     420        info_elements = []
    409421        for transistions in transition_map:
    410422            assert transistions[0].enabled_by == "1"
    411423            if len(transistions) == 1:
    412                 elements.append(
     424                map_elements.append(
    413425                    self._post_condition_enumerators(
    414                         transistions[0].conditions))
     426                        transistions[0].post_conditions))
     427                info_elements.append(transistions[0].info)
    415428            else:
    416429                ifelse = "#if "
    417                 enumerators = []  # type: List[str]
     430                map_enumerators = []  # type: List[str]
     431                info_enumerators = []  # type: List[str]
    418432                for variant in transistions[1:]:
    419                     enumerators.append(ifelse + variant.enabled_by)
    420                     enumerators.append(
    421                         self._post_condition_enumerators(variant.conditions))
     433                    map_enumerators.append(ifelse + variant.enabled_by)
     434                    info_enumerators.append(ifelse + variant.enabled_by)
     435                    map_enumerators.append(
     436                        self._post_condition_enumerators(
     437                            variant.post_conditions))
     438                    info_enumerators.append(variant.info)
    422439                    ifelse = "#elif "
    423                 enumerators.append("#else")
    424                 enumerators.append(
     440                map_enumerators.append("#else")
     441                info_enumerators.append("#else")
     442                map_enumerators.append(
    425443                    self._post_condition_enumerators(
    426                         transistions[0].conditions))
    427                 enumerators.append("#endif")
    428                 elements.append("\n".join(enumerators))
    429         content.append(["\n  }, {\n".join(elements), "  }", "};"])
     444                        transistions[0].post_conditions))
     445                info_enumerators.append(transistions[0].info)
     446                map_enumerators.append("#endif")
     447                info_enumerators.append("#endif")
     448                map_elements.append("\n".join(map_enumerators))
     449                info_elements.append("\n".join(info_enumerators))
     450        content.append(["\n  }, {\n".join(map_elements), "  }", "};"])
     451        pre_bits = 2**max(math.ceil(math.log2(self._pre_condition_count)), 3)
     452        content.add("static const struct {")
     453        with content.indent():
     454            for condition in self["pre-conditions"]:
     455                content.append(
     456                    f"uint{pre_bits}_t Pre_{condition['name']}_NA : 1;")
     457        content.add([f"}} {self.ident}_TransitionInfo[] = {{", "  {"])
     458        content.append(["\n  }, {\n".join(info_elements), "  }", "};"])
    430459
    431460    def _add_action(self, content: CContent) -> None:
     461        content.add_blank_line()
    432462        for index, enum in enumerate(self._pre_index_to_enum):
    433463            content.append(f"{enum[0]}_Prepare( ctx, ctx->pcs[ {index} ] );")
     
    446476            begin = self._pre_index_to_enum[index][1]
    447477            end = self._pre_index_to_enum[index][-1]
    448             with content.for_loop(f"{var} = {begin}", f"{var} != {end} + 1",
     478            with content.for_loop(f"{var} = {begin}", f"{var} < {end}",
    449479                                  f"++{var}"):
     480                name = self._item['pre-conditions'][index]["name"]
     481                pre_na = f"{self.ident}_TransitionInfo[ index ].Pre_{name}_NA"
     482                with content.condition(pre_na):
     483                    content.append(f"{var} = {end};")
     484                    content.append(f"index += ( {end} - 1 )")
     485                    for index_2 in range(index + 1, self._pre_condition_count):
     486                        with content.indent():
     487                            content.append(
     488                                f"* {self._pre_index_to_enum[index_2][-1]}")
     489                    content.lines[-1] += ";"
    450490                self._add_for_loops(content, index + 1)
    451491        else:
     
    509549                            content.append("break;")
    510550                        content.add("}")
     551                    content.add(f"case {enum[-1]}:")
     552                    with content.indent():
     553                        content.append("break;")
    511554                content.add("}")
    512555                content.add(self.substitute_code(condition["test-epilogue"]))
  • spec/spec/requirement-action-name.yml

    rfd31f9d r244b277  
    1111  str:
    1212    assert:
    13     - re: ^[A-Z][a-zA-Z0-9]+$
     13      and:
     14      - re: ^[A-Z][a-zA-Z0-9]+$
     15      - not:
     16          eq: NA
    1417    description: |
    1518      It shall be the name of a condition or a state of a condition used to
     
    1821      The rationale for this is that the names are used in tables and the
    1922      horizontal space is limited by the page width.  The more conditions you
    20       have in an action requirement, the shorter the names should be.
     23      have in an action requirement, the shorter the names should be.  The name
     24      ``NA`` is reserved and indicates that a condition is not applicable.
    2125spec-name: Action Requirement Name
    2226spec-type: requirement-action-name
  • spec/spec/requirement-action-transition-pre-states.yml

    rfd31f9d r244b277  
    1616  str:
    1717    assert:
    18       eq: all
     18      in:
     19      - all
     20      - N/A
    1921    description: |
    20       The value represents all states of the pre-condition in the transition.
     22      The value ``all`` represents all states of the pre-condition in this
     23      transition.  The value ``N/A`` marks the pre-condition as not applicable
     24      in this transition.
    2125spec-name: Action Requirement Transition Pre-Condition State Set
    2226spec-type: requirement-action-transition-pre-states
Note: See TracChangeset for help on using the changeset viewer.