cleanup

crap_bucket/bftype.py

@@ -0,0 +1,9 @@
+#from enum import Enum
+
+class opertype:
+    """Boolean Formulae Types"""
+    unspec = 0
+    o_and = 1
+    o_or = 2
+    o_not = 3
+    o_var = 10

crap_bucket/boolform.py

@@ -0,0 +1,69 @@
+#!/usr/bin/env python
+
+import bftype
+
+class BoolForm:
+
+    def __init__(self, a=None):
+        self.initAll()
+        if a != None and isinstance(a, int):
+            self.setupVarNode(a)
+
+    def initAll(self):
+        self.oper = bftype.opertype.unspec
+
+    def setupConjunction(self, lhs, rhs):
+        self.oper = bftype.opertype.o_and
+        self.sfLeft = lhs
+        self.sfRight = rhs
+
+    def setupDisjunction(self, lhs, rhs):
+        self.oper = bftype.opertype.o_or
+        self.sfLeft = lhs
+        self.sfRight = rhs
+
+    def setupNegation(self, form):
+        self.oper = bftype.opertype.o_not
+        self.subForm = form
+
+    def setupVarNode(self, var_id):
+        if not isinstance(var_id, int):
+            print("var_id must be an integer")
+            raise
+        self.oper = bftype.opertype.o_var
+        self.varid = var_id
+
+    def __add__(self, x):
+        r = BoolForm()
+        r.setupDisjunction(self,x)
+        return r
+
+    def __mul__(self, x):
+        r = BoolForm()
+        r.setupConjunction(self,x)
+        return r
+
+    def __neg__(self):
+        r = BoolForm()
+        r.setupNegation(self)
+        return r
+
+    def __str__(self):
+        if self.oper == bftype.opertype.o_or:
+            return "(" + str(self.sfLeft) + " or " + str(self.sfRight) + ")"
+        elif self.oper == bftype.opertype.o_and:
+            return "(" + str(self.sfLeft) + " and " + str(self.sfRight) + ")"
+        elif self.oper == bftype.opertype.o_not:
+            return "-" + str(self.subForm)
+        elif self.oper == bftype.opertype.o_var:
+            return str(self.varid)
+        else:
+            print("This should not happen. Unknown operator?")
+            raise
+
+if __name__ == "__main__":
+
+    y = (BoolForm(1) + -BoolForm(2) * BoolForm(3)) + BoolForm(2)
+    
+    print(y)
+

crap_bucket/example.py

@@ -0,0 +1,39 @@
+from z3 import *
+
+p0 = Bool('p0')
+p1 = Bool('p1')
+p2 = Bool('p2') 
+p3 = Bool('p3')
+p4 = Bool('p4')
+
+p0e = Bool('p0e')
+p1e = Bool('p1e')
+p2e = Bool('p2e')
+p3e = Bool('p3e')
+p4e = Bool('p4e')
+
+p0p = Bool('p0p')
+p1p = Bool('p1p')
+p2p = Bool('p2p')
+p3p = Bool('p3p')
+p4p = Bool('p4p')
+
+Cd_a1 = And( Or(p1,p1e), Or(p4,p4e), Not( Or(p2,p2e) ) )
+Cd_a2 = And( Or(p2,p2e),             Not( Or(p3,p3e) ) )
+Cd_a3 = And( Or(p1,p1e), Or(p3,p3e), Not( Or(p2,p2e) ) )
+Cd_a4 = And( Or(p3,p3e),             Not( Or(p2,p2e) ) )
+
+En1 = Or(Cd_a1,Cd_a2,Cd_a3,Cd_a4)
+En2 = Or(Cd_a1,Cd_a3)
+En3 = Cd_a2
+En4 = Cd_a2
+
+Pr1 = Or( And(En1,p1p) , And( Not(En1), Not(p1p)) )
+Pr2 = Or( And(En2,p2p) , And( Not(En2), Not(p2p)) )
+Pr3 = Or( And(En3,p3p) , And( Not(En3), Not(p3p)) )
+Pr4 = Or( And(En4,p4p) , And( Not(En4), Not(p4p)) )
+
+PrConjunction = And( Pr1, Pr2, Pr3, Pr4 )
+
+print PrConjunction
+

crap_bucket/testca.py

@@ -0,0 +1,16 @@
+#!/usr/bin/env python
+
+from rctsys import *
+import rs_examples
+
+rs = rs_examples.toy_ex3()
+
+ca = ContextAutomaton(rs)
+
+ca.add_state("st1")
+ca.add_init_state("in")
+
+ca.add_transition("st1", {"1","2"}, "in")
+
+ca.show()
+