[rtems-central commit] validation: More compact post-conditions
Sebastian Huber
sebh at rtems.org
Mon Apr 19 14:58:39 UTC 2021
Module: rtems-central
Branch: master
Commit: 640e2df3d2d59dcf534d888db433b143087be054
Changeset: http://git.rtems.org/rtems-central/commit/?id=640e2df3d2d59dcf534d888db433b143087be054
Author: Sebastian Huber <sebastian.huber at embedded-brains.de>
Date: Fri Apr 16 22:16:14 2021 +0200
validation: More compact post-conditions
---
rtemsspec/tests/spec-validation/action3.yml | 212 ++++++++++++++++++++++++++++
rtemsspec/tests/spec-validation/tp.yml | 1 +
rtemsspec/tests/test_validation.py | 2 +
rtemsspec/validation.py | 70 ++++++---
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 0000000..237dffd
--- /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 a8b281d..825ee2e 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 9c6f57e..a08e1c6 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 2d60d99..aa8e385 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:
More information about the vc
mailing list