diff --git a/momba/engine/translator.py b/momba/engine/translator.py index b8493cb5..7d980dfc 100644 --- a/momba/engine/translator.py +++ b/momba/engine/translator.py @@ -520,6 +520,19 @@ def _extract_constraints( }, } ) + elif isinstance(head, expressions.Equality): + # equal is ≤ and ≥, not equal is < and > + ops = [operators.ComparisonOperator.LE, operators.ComparisonOperator.GE] + if head.operator is operators.EqualityOperator.NEQ: + ops = [operators.ComparisonOperator.LT, operators.ComparisonOperator.GT] + + pending.extend( + [ + expressions.Comparison(ops[0], head.left, head.right), + expressions.Comparison(ops[1], head.left, head.right), + ] + ) + else: conjuncts.append(head) return ExtractedConstraints(conjuncts, constraints) diff --git a/tests/resources/eq_constraints.jani b/tests/resources/eq_constraints.jani new file mode 100644 index 00000000..b2b3cd12 --- /dev/null +++ b/tests/resources/eq_constraints.jani @@ -0,0 +1,177 @@ +{ + "jani-version": 1, + "name": "EqualityConstraints", + "type": "ta", + "actions": [], + "variables": [ + { + "name": "x", + "type": "clock", + "initial-value": 0 + }, + { + "name": "y", + "type": "clock", + "initial-value": 0 + } + ], + "properties": [], + "automata": [ + { + "name": "T", + "locations": [ + { + "name": "l0", + "time-progress": { + "exp": { + "op": "≤", + "left": "y", + "right": 2 + } + } + }, + { + "name": "l1", + "time-progress": { + "exp": { + "op": "≤", + "left": "y", + "right": 1 + } + } + }, + { + "name": "l2", + "time-progress": { + "exp": { + "op": "≤", + "left": "y", + "right": 1 + } + } + }, + { + "name": "l3", + "time-progress": { + "exp": { + "op": "≤", + "left": "y", + "right": 1 + } + } + } + ], + "initial-locations": [ + "l0" + ], + "edges": [ + { + "comment": "l0 - x=1 - y:=0 -> l1", + "location": "l0", + "guard": { + "exp": { + "op": "=", + "left": "x", + "right": 1 + } + }, + "destinations": [ + { + "location": "l1", + "assignments": [ + { + "ref": "y", + "value": 0 + } + ] + } + ] + }, + { + "comment": "l0 - y ≤ 2 - y:=0 -> l3", + "location": "l0", + "guard": { + "exp": { + "op": "≤", + "left": "y", + "right": 2 + } + }, + "destinations": [ + { + "location": "l3", + "assignments": [ + { + "ref": "y", + "value": 0 + } + ] + } + ] + }, + { + "comment": "l1 - y := 0 -> l0", + "location": "l1", + "destinations": [ + { + "location": "l0", + "assignments": [ + { + "ref": "y", + "value": 0 + } + ] + } + ] + }, + { + "comment": "l1 -> l2", + "location": "l1", + "destinations": [ + { + "location": "l2" + } + ] + }, + { + "comment": "l2 - y := 0 -> l0", + "location": "l2", + "destinations": [ + { + "location": "l0", + "assignments": [ + { + "ref": "y", + "value": 0 + } + ] + } + ] + }, + { + "comment": "l3 - x := 0 -> l0", + "location": "l3", + "destinations": [ + { + "location": "l0", + "assignments": [ + { + "ref": "x", + "value": 0 + } + ] + } + ] + } + ] + } + ], + "system": { + "elements": [ + { + "automaton": "T" + } + ], + "syncs": [] + } +} \ No newline at end of file diff --git a/tests/test_eq_constraints.py b/tests/test_eq_constraints.py new file mode 100644 index 00000000..0a4a8607 --- /dev/null +++ b/tests/test_eq_constraints.py @@ -0,0 +1,19 @@ +# -*- coding:utf-8 -*- +# +# Copyright (C) 2024, Raffael Senn + +import pathlib + + +from momba import engine, jani +from momba.engine import time + +EQ_CONSTRAINTS_MODEL = ( + pathlib.Path(__file__).parent / "resources" / "eq_constraints.jani" +) + + +def test_eq_constraints_exploration() -> None: + network = jani.load_model(EQ_CONSTRAINTS_MODEL.read_text(encoding="utf-8")) + e = engine.Explorer(network, time.GlobalTime) + print("Done!")