feat: add support for equality constraints in TA (#14)

koehlma · Feb 8, 2024 · 2d0177a · 2d0177a
1 parent d0c16d3
commit 2d0177a
Show file tree

Hide file tree

Showing 3 changed files with 209 additions and 0 deletions.
diff --git 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
@@ -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": []
+    }
+}
diff --git a/tests/test_eq_constraints.py b/tests/test_eq_constraints.py
@@ -0,0 +1,19 @@
+# -*- coding:utf-8 -*-
+#
+# Copyright (C) 2024, Raffael Senn <raffael.senn@uni-konstanz.de>
+
+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!")