Bag descriptions; oper. overloading for FormLTL and BagDescription

formula_ltl.py

@@ -1,36 +1,94 @@
 from enum import Enum
 
-LTL_form_type = Enum('LTL_form_type', 'proposition negation globally next until release')
+LTL_form_type = Enum('LTL_form_type', 'bag l_and l_or l_not globally next until release')
+BagDesc_oper = Enum('BagDesc_oper', 'entity l_and l_or l_not lt le eq ge gt')
+
+class BagDescription(object):
+    def __init__(self, f_type, L_oper = None, R_oper = None, entity = ""):
+        self.f_type = f_type
+        self.left_operand = L_oper
+        self.right_operand = R_oper
+        self.entity = entity
+        
+    def __repr__(self):
+        if self.f_type == BagDesc_oper.entity:
+            return self.entity
+        if self.f_type == BagDesc_oper.l_and:
+            return "( " + repr(self.left_operand) + " & " + repr(self.right_operand) + " )"
+        if self.f_type == BagDesc_oper.l_or:
+            return "( " + repr(self.left_operand) + " | " + repr(self.right_operand) + " )"
+        if self.f_type == BagDesc_oper.l_not:
+            return "~" + repr(self.left_operand)
+        if self.f_type == BagDesc_oper.entity:
+            return entity
+        if self.f_type == BagDesc_oper.lt:
+            return repr(self.left_operand) + " < " + repr(self.right_operand)
+        if self.f_type == BagDesc_oper.le:
+            return repr(self.left_operand) + " <= " + repr(self.right_operand)
+        if self.f_type == BagDesc_oper.eq:
+            return repr(self.left_operand) + " == " + repr(self.right_operand)
+        if self.f_type == BagDesc_oper.ge:
+            return repr(self.left_operand) + " >= " + repr(self.right_operand)
+        if self.f_type == BagDesc_oper.gt:
+            return repr(self.left_operand) + " > " + repr(self.right_operand)
+
+    @classmethod
+    def f_entity(cls, entity_name):
+        return cls(BagDesc_oper.entity, entity = entity_name)
+        
+    def __lt__(self, other):
+        return BagDescription(BagDesc_oper.lt, L_oper = self, R_oper = other)
+        
+    def __le__(self, other):
+        return BagDescription(BagDesc_oper.le, L_oper = self, R_oper = other)
+        
+    def __eq__(self, other):
+        return BagDescription(BagDesc_oper.eq, L_oper = self, R_oper = other)
+    
+    def __ge__(self, other):
+        return BagDescription(BagDesc_oper.ge, L_oper = self, R_oper = other)
+    
+    def __gt__(self, other):
+        return BagDescription(BagDesc_oper.gt, L_oper = self, R_oper = other)
+        
+    def __and__(self, other):
+        return BagDescription(BagDesc_oper.l_and, L_oper = self, R_oper = other)
+    
+    def __or__(self, other):
+        return BagDescription(BagDesc_oper.l_or, L_oper = self, R_oper = other)
+    
+    def __invert__(self):
+        return BagDescription(BagDesc_oper.l_not, L_oper = self)
 
 class FormulaLTL(object):
     
-    def __init__(self, type, L_oper = None, R_oper = None, proposition = ""):
-        self.type = type
+    def __init__(self, f_type, L_oper = None, R_oper = None, bag = None):
+        self.f_type = f_type
         self.left_operand = L_oper
         self.right_operand = R_oper
-        self.proposition = proposition
+        self.bag_descr = bag
     
     def __repr__(self):
-        if self.type == LTL_form_type.proposition:
-            return self.proposition
-        if self.type == LTL_form_type.negation:
-            return "NOT( " + repr(self.left_operand) + " )"
-        if self.type == LTL_form_type.globally:
+        if self.f_type == LTL_form_type.bag:
+            return repr(self.bag_descr)
+        if self.f_type == LTL_form_type.l_not:
+            return "~( " + repr(self.left_operand) + " )"
+        if self.f_type == LTL_form_type.globally:
             return "G( " + repr(self.left_operand) + " )"
-        if self.type == LTL_form_type.next:
+        if self.f_type == LTL_form_type.next:
             return "X( " + repr(self.left_operand) + " )"
-        if self.type == LTL_form_type.until:
+        if self.f_type == LTL_form_type.l_and:
+            return "( " + repr(self.left_operand) + " & " + repr(self.right_operand) + " )"
+        if self.f_type == LTL_form_type.l_or:
+            return "( " + repr(self.left_operand) + " | " + repr(self.right_operand) + " )"
+        if self.f_type == LTL_form_type.until:
             return "( " + repr(self.left_operand) + " U " + repr(self.right_operand) + " )"
-        if self.type == LTL_form_type.release:
+        if self.f_type == LTL_form_type.release:
             return "( " + repr(self.left_operand) + " R " + repr(self.right_operand) + " )"
 
     @classmethod
-    def f_prop(cls, proposition_name):
-        return cls(LTL_form_type.proposition, proposition = proposition_name)
-
-    @classmethod
-    def f_NOT(cls, arg):
-        return cls(LTL_form_type.negation, L_oper = arg)
+    def f_bag(cls, bag_descr):
+        return cls(LTL_form_type.bag, bag = bag_descr)
 
     @classmethod
     def f_X(cls, arg):
@@ -48,10 +106,16 @@ class FormulaLTL(object):
     def f_R(cls, arg_L, arg_R):
         return cls(LTL_form_type.release, L_oper = arg_L, R_oper = arg_R)
         
+    def __and__(self, other):
+        return FormulaLTL(LTL_form_type.l_and, L_oper = self, R_oper = other)
     
-x = FormulaLTL.f_NOT( FormulaLTL.f_X( FormulaLTL.f_prop("a") ) )
+    def __or__(self, other):
+        return FormulaLTL(LTL_form_type.l_or, L_oper = self, R_oper = other)
     
+    def __invert__(self):
+        return FormulaLTL(LTL_form_type.l_not, L_oper = self)
+
+
+x = ~( FormulaLTL.f_X( FormulaLTL.f_bag( ~((BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) ) ) ) & FormulaLTL.f_X( FormulaLTL.f_bag( ~((BagDescription.f_entity("ent3") == 1) ) ) ) 
 print(x)
 
-        
-