validation: More compact post-conditions

4 files changed, 264 insertions, 21 deletions

diff --git a/rtemsspec/tests/spec-validation/action3.yml b/rtemsspec/tests/spec-validation/action3.yml
new file mode 100644
index 00000000..237dffd7
--- /dev/null
+++ b/rtemsspec/tests/spec-validation/action3.yml
@@ -0,0 +1,212 @@
+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
+functional-type: action
+links: []
+post-conditions:
+- name: Position
+  states:
+  - name: InitialFirst
+    test-code: |
+      /* Code */
+    text: |
+      A priority queue associated with the scheduler which contains exactly the
+      enqueueing thread shall be created as the first priority queue of the
+      thread queue.
+  - name: InitialLast
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  - name: First
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  - name: Second
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  - name: FirstFirst
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  - name: SecondFirst
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  - name: FirstLast
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  - name: SecondLast
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  test-epilogue: null
+  test-prologue: null
+pre-conditions:
+- name: EligibleScheduler
+  states:
+  - name: Home
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  - name: Helping
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  test-epilogue: null
+  test-prologue: null
+- name: QueueEligible
+  states:
+  - name: None
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  - name: EQ
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  - name: GT
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  test-epilogue: null
+  test-prologue: null
+- name: QueueIneligible
+  states:
+  - name: None
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  - name: Only
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  - name: Before
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  - name: After
+    test-code: |
+      /* Code */
+    text: |
+      Text.
+  test-epilogue: null
+  test-prologue: null
+rationale: null
+references: []
+requirement-type: functional
+skip-reasons:
+  Invalid: |
+    Text.
+test-action: |
+  /* Code */
+test-brief: null
+test-cleanup: null
+test-context: []
+test-context-support: null
+test-description: null
+test-header: null
+test-includes: []
+test-local-includes: []
+test-prepare: null
+test-setup: null
+test-stop: null
+test-support: null
+test-target: action3.c
+test-teardown: null
+text: |
+  Text.
+transition-map:
+- enabled-by: true
+  post-conditions:
+    Position: InitialFirst
+  pre-conditions:
+    EligibleScheduler: all
+    QueueEligible:
+    - None
+    QueueIneligible:
+    - None
+- enabled-by: true
+  post-conditions:
+    Position: InitialLast
+  pre-conditions:
+    EligibleScheduler: all
+    QueueEligible:
+    - None
+    QueueIneligible:
+    - Only
+- enabled-by: true
+  post-conditions:
+    Position: First
+  pre-conditions:
+    EligibleScheduler: all
+    QueueEligible:
+    - GT
+    QueueIneligible:
+    - None
+- enabled-by: true
+  post-conditions:
+    Position: Second
+  pre-conditions:
+    EligibleScheduler: all
+    QueueEligible:
+    - EQ
+    QueueIneligible:
+    - None
+- enabled-by: true
+  post-conditions:
+    Position: FirstLast
+  pre-conditions:
+    EligibleScheduler: all
+    QueueEligible:
+    - GT
+    QueueIneligible:
+    - Before
+- enabled-by: true
+  post-conditions:
+    Position: SecondLast
+  pre-conditions:
+    EligibleScheduler: all
+    QueueEligible:
+    - EQ
+    QueueIneligible:
+    - Before
+- enabled-by: true
+  post-conditions:
+    Position: FirstFirst
+  pre-conditions:
+    EligibleScheduler: all
+    QueueEligible:
+    - GT
+    QueueIneligible:
+    - After
+- enabled-by: true
+  post-conditions:
+    Position: SecondFirst
+  pre-conditions:
+    EligibleScheduler: all
+    QueueEligible:
+    - EQ
+    QueueIneligible:
+    - After
+- enabled-by: true
+  post-conditions: Invalid
+  pre-conditions: default
+type: requirement
diff --git a/rtemsspec/tests/spec-validation/tp.yml b/rtemsspec/tests/spec-validation/tp.yml
index a8b281d8..825ee2e6 100644
--- a/rtemsspec/tests/spec-validation/tp.yml
+++ b/rtemsspec/tests/spec-validation/tp.yml
@@ -6,5 +6,6 @@ source:
 - tc34.c
 - ts.c
 - action2.c
+- action3.c
 - other.c
 type: build
diff --git a/rtemsspec/tests/test_validation.py b/rtemsspec/tests/test_validation.py
index 9c6f57ef..a08e1c6f 100644
--- a/rtemsspec/tests/test_validation.py
+++ b/rtemsspec/tests/test_validation.py
@@ -56,6 +56,8 @@ def test_validation(tmpdir):
     transition_map = TransitionMap(item_cache["/action2"])
     assert transition_map.skip_idx_to_name(1) == "SkipReason"
     assert len(list(transition_map.get_post_conditions(["BOOM"]))) == 6
+    transition_map = TransitionMap(item_cache["/action3"])
+    assert len(list(transition_map.get_post_conditions(["RTEMS_SMP"]))) == 9
 
     generate(validation_config, item_cache)
 
diff --git a/rtemsspec/validation.py b/rtemsspec/validation.py
index 2d60d99b..aa8e385b 100644
--- a/rtemsspec/validation.py
+++ b/rtemsspec/validation.py
@@ -626,6 +626,54 @@ PostCond = Tuple[int, ...]
 PreCondsOfPostCond = List[Tuple[List[int], ...]]
 
 
+def _compact(pre_conds: PreCondsOfPostCond) -> PreCondsOfPostCond:
+    while True:
+        last = pre_conds[0]
+        combined_pre_conds = [last]
+        combined_count = 0
+        for row in pre_conds[1:]:
+            if row == last:
+                continue
+            diff = [
+                index for index, states in enumerate(last)
+                if states != row[index]
+            ]
+            if len(diff) == 1:
+                index = diff[0]
+                combined_count += 1
+                last[index].extend(row[index])
+            else:
+                combined_pre_conds.append(row)
+                last = row
+        pre_conds = combined_pre_conds
+        if combined_count == 0:
+            break
+    return pre_conds
+
+
+def _compact_more(pre_conds: PreCondsOfPostCond) -> PreCondsOfPostCond:
+    while True:
+        combined_count = 0
+        next_pre_conds = []
+        while pre_conds:
+            first = pre_conds.pop(0)
+            next_pre_conds.append(first)
+            for row in pre_conds:
+                diff = [
+                    index for index, states in enumerate(first)
+                    if states != row[index]
+                ]
+                if len(diff) == 1:
+                    index = diff[0]
+                    combined_count += 1
+                    first[index].extend(row[index])
+                    pre_conds.remove(row)
+        pre_conds = next_pre_conds
+        if combined_count == 0:
+            break
+    return pre_conds
+
+
 class TransitionMap:
     """ Representation of an action requirement transition map. """
 
@@ -709,27 +757,7 @@ class TransitionMap:
                     map_idx, variant.pre_cond_na)))
         for post_cond, pre_conds in sorted(entries.items(),
                                            key=lambda x: (x[0][0], len(x[1]))):
-            while True:
-                last = pre_conds[0]
-                combined_pre_conds = [last]
-                combined_count = 0
-                for row in pre_conds[1:]:
-                    if row == last:
-                        continue
-                    diff = [
-                        index for index, states in enumerate(last)
-                        if states != row[index]
-                    ]
-                    if len(diff) == 1:
-                        index = diff[0]
-                        combined_count += 1
-                        last[index].extend(row[index])
-                    else:
-                        combined_pre_conds.append(row)
-                        last = row
-                pre_conds = combined_pre_conds
-                if combined_count == 0:
-                    break
+            pre_conds = _compact_more(_compact(pre_conds))
             yield post_cond, pre_conds
 
     def _post_process(self) -> None: