MAI: use TLA+ syntax in examples

tulip-control · Jan 12, 2021 · c5f62fa · c5f62fa
1 parent 00d5559
commit c5f62fa
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 8 deletions.
diff --git a/examples/cudd_statistics.py b/examples/cudd_statistics.py
@@ -8,8 +8,8 @@
 def main():
     b = cudd.BDD()
     b.declare('x', 'y', 'z')
-    u = b.add_expr('x & y & z')
-    u = b.add_expr('x | y | ~ z')
+    u = b.add_expr('x /\ y /\ z')
+    u = b.add_expr('x \/ y \/ ~ z')
     stats = b.statistics()
     pprint.pprint(format_dict(stats))
 

diff --git a/examples/reachability.py b/examples/reachability.py
@@ -20,19 +20,20 @@ def transition_system(bdd):
     dvars = ["x0", "x0'", "x1", "x1'"]
     for var in dvars:
         bdd.add_var(var)
-    s = (
-        "((!x0 & !x1) -> ( (!x0' & !x1') | (x0' & !x1') )) & "
-        "((x0 & !x1) -> ! (x0' & x1')) & "
-        "((!x0 & x1) -> ( (!x0' & x1') | (x0' & !x1') )) & "
-        "! (x0 & x1)")
+    s = '''
+           ((~ x0 /\ ~ x1) => ( (~ x0' /\ ~ x1') \/ (x0' /\ ~ x1') ))
+        /\ ((x0 /\ ~ x1) => ~ (x0' /\ x1'))
+        /\ ((~ x0 /\ x1) => ( (~ x0' /\ x1') \/ (x0' /\ ~ x1') ))
+        /\ ~ (x0 /\ x1)
+        '''
     transitions = bdd.add_expr(s)
     return transitions
 
 
 def least_fixpoint(transitions, bdd):
     """Return ancestor nodes."""
     # target is the set {2}
-    target = bdd.add_expr('!x0 & x1')
+    target = bdd.add_expr('~ x0 /\ x1')
     # start from empty set
     q = bdd.false
     qold = None