Merge pull request #10 from git-afsantos/dev-v1.2

HPL v1.2.0

CHANGELOG.md

@@ -4,6 +4,13 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)
 and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html).
 
+## v1.2.0 - 2023-09-08
+### Added
+- `canonical_form(property: HplProperty)` function to `hpl.rewrite` module.
+
+### Changed
+- `HplAstObject.but()` returns the same object if no attributes would change.
+
 ## v1.1.2 - 2023-09-04
 ### Fixed
 - Sanity error when creating some types of predicates that was too strict.

src/hpl/ast/base.py

@@ -59,6 +59,11 @@ def iterate(self) -> Iterator['HplAstObject']:
     def but(self, **kwargs) -> 'HplAstObject':
         metadata = kwargs.get('metadata')
         if metadata is None:
+            for key, value in kwargs.items():
+                if getattr(self, key) is not value:
+                    break
+            else:
+                return self  # nothing changes
             metadata = dict(self.metadata)
         new = evolve(self, **kwargs)
         assert new.metadata is not self.metadata

src/hpl/rewrite.py

@@ -5,7 +5,7 @@
 # Imports
 ###############################################################################
 
-from typing import Tuple, TypeVar, Union
+from typing import List, Tuple, TypeVar, Union
 
 from hpl.ast.expressions import (
     And,
@@ -24,6 +24,7 @@
     is_var_reference,
 )
 from hpl.ast.predicates import HplPredicate, HplVacuousTruth, predicate_from_expression
+from hpl.ast.properties import HplProperty, HplScope
 from hpl.errors import invalid_type
 
 ###############################################################################
@@ -72,6 +73,13 @@ def refactor_reference(predicate_or_expression: P, alias: str) -> Tuple[P, P]:
         return _refactor_ref_expr(predicate_or_expression, alias)
 
 
+def canonical_form(property: HplProperty) -> List[HplProperty]:
+    if property.pattern.is_safety:
+        return _canonical_form_safety(property)
+    assert property.pattern.is_liveness
+    return _canonical_form_liveness(property)
+
+
 ###############################################################################
 # Formula Rewriting - Helper Functions
 ###############################################################################
@@ -203,6 +211,39 @@ def _split_negation(neg: HplUnaryOperator, alias: str) -> Tuple[HplExpression, H
     raise TypeError(f'unknown expression type: {expr!r}')
 
 
+def _canonical_form_safety(property: HplProperty) -> List[HplProperty]:
+    scopes = _canonical_form_scopes(property.scope)
+    pattern = property.pattern
+    patterns = [pattern.but(behaviour=event) for event in pattern.behaviour.simple_events()]
+    if len(scopes) == 1 and len(patterns) == 1:
+        # nothing changed
+        return [property]
+    return [property.but(scope=scope, pattern=pattern) for scope in scopes for pattern in patterns]
+
+
+def _canonical_form_liveness(property: HplProperty) -> List[HplProperty]:
+    scopes = _canonical_form_scopes(property.scope)
+    if property.pattern.is_existence:
+        patterns = [property.pattern]  # no splits
+    else:
+        assert property.pattern.is_response, f'pattern: {property.pattern}'
+        trigger = property.pattern.trigger
+        assert trigger is not None
+        patterns = [property.pattern.but(trigger=event) for event in trigger.simple_events()]
+    if len(scopes) == 1 and len(patterns) == 1:
+        # nothing changed
+        return [property]
+    return [property.but(scope=scope, pattern=pattern) for scope in scopes for pattern in patterns]
+
+
+def _canonical_form_scopes(scope: HplScope) -> List[HplScope]:
+    if scope.is_after:  # after or after-until
+        assert scope.activator is not None
+        return [scope.but(activator=event) for event in scope.activator.simple_events()]
+    assert scope.is_global or scope.is_until
+    return [scope]
+
+
 ###############################################################################
 # Convenience Logic Tests
 ###############################################################################

tests/test_canonical_rewrite.py

@@ -0,0 +1,87 @@
+# SPDX-License-Identifier: MIT
+# Copyright © 2023 André Santos
+
+###############################################################################
+# Imports
+###############################################################################
+
+from hpl.ast.properties import HplProperty
+from hpl.parser import property_parser
+from hpl.rewrite import canonical_form
+
+###############################################################################
+# Predicate Examples
+###############################################################################
+
+
+###############################################################################
+# Test Code
+###############################################################################
+
+parser = property_parser()
+
+
+def test_canonical_global_absence_no_splits():
+    property = parser.parse('globally: no a')
+    outputs = canonical_form(property)
+
+    assert len(outputs) == 1
+    assert outputs[0] is property
+
+
+def test_canonical_global_absence_splits():
+    property = parser.parse('globally: no (a or b)')
+    outputs = canonical_form(property)
+
+    assert len(outputs) == 2
+
+    assert outputs[0].pattern.behaviour.is_simple_event
+    assert outputs[1].pattern.behaviour.is_simple_event
+
+    assert outputs[0].pattern.behaviour is property.pattern.behaviour.event1
+    assert outputs[1].pattern.behaviour is property.pattern.behaviour.event2
+
+
+def test_canonical_global_existence_no_splits():
+    property = parser.parse('globally: some (a or b)')
+    outputs = canonical_form(property)
+
+    assert len(outputs) == 1
+    assert outputs[0] is property
+
+
+def test_canonical_after_existence_splits():
+    property = parser.parse('after (a or b): some (c or d)')
+    outputs = canonical_form(property)
+
+    assert len(outputs) == 2
+
+    assert outputs[0].scope.activator.is_simple_event
+    assert outputs[1].scope.activator.is_simple_event
+
+    assert outputs[0].scope.activator is property.scope.activator.event1
+    assert outputs[1].scope.activator is property.scope.activator.event2
+
+    assert outputs[0].pattern is property.pattern
+    assert outputs[1].pattern is property.pattern
+
+
+def test_canonical_global_response_no_splits():
+    property = parser.parse('globally: a causes (b or c)')
+    outputs = canonical_form(property)
+
+    assert len(outputs) == 1
+    assert outputs[0] is property
+
+
+def test_canonical_global_response_splits():
+    property = parser.parse('globally: (a or b) causes (c or d)')
+    outputs = canonical_form(property)
+
+    assert len(outputs) == 2
+
+    assert outputs[0].pattern.trigger.is_simple_event
+    assert outputs[1].pattern.trigger.is_simple_event
+
+    assert outputs[0].pattern.trigger is property.pattern.trigger.event1
+    assert outputs[1].pattern.trigger is property.pattern.trigger.event2