validation: Add post-condition expressions

11 files changed, 693 insertions, 121 deletions

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