validation: Add post-condition expressions

8 files changed, 191 insertions, 1 deletions

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