diff --git a/logics/bags.py b/logics/bags.py index 30ef358..b69d694 100644 --- a/logics/bags.py +++ b/logics/bags.py @@ -1,15 +1,18 @@ from enum import Enum -BagDesc_oper = Enum('BagDesc_oper', 'entity true l_and l_or l_not lt le eq ge gt') +BagDesc_oper = Enum( + 'BagDesc_oper', 'entity true 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 = ""): + + 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 - + self.sanity_check() - + def __repr__(self): if self.f_type == BagDesc_oper.entity: return self.entity @@ -31,45 +34,48 @@ class BagDescription(object): 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) - + def sanity_check(self): """Sanity checks""" for operand in (self.left_operand, self.right_operand): if operand: - if not (isinstance(operand, BagDescription) or isinstance(operand, int)): - raise RuntimeError("Unexpected operand type for a bag: " + str(operand)) - + if not( + isinstance(operand, BagDescription) + or isinstance(operand, int)): + raise RuntimeError( + "Unexpected operand type for a bag: " + str(operand)) + @classmethod def f_entity(cls, entity_name): - return cls(BagDesc_oper.entity, entity = entity_name) - + return cls(BagDesc_oper.entity, entity=entity_name) + @classmethod def f_TRUE(cls): return cls(BagDesc_oper.true) - + def __lt__(self, other): - return BagDescription(BagDesc_oper.lt, L_oper = self, R_oper = 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) - + 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) - + 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) - + 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) - + 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) - + 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) - + return BagDescription(BagDesc_oper.l_or, L_oper=self, R_oper=other) + def __invert__(self): - return BagDescription(BagDesc_oper.l_not, L_oper = self) - + return BagDescription(BagDesc_oper.l_not, L_oper=self) + # EOF diff --git a/logics/rsltl.py b/logics/rsltl.py index e8bd959..83d61d1 100644 --- a/logics/rsltl.py +++ b/logics/rsltl.py @@ -3,22 +3,30 @@ from enum import Enum from logics.bags import * -rsLTL_form_type = Enum('rsLTL_form_type', 'bag l_and l_or l_not l_implies t_globally t_finally t_next t_until t_release') +rsLTL_form_type = Enum( + 'rsLTL_form_type', + 'bag l_and l_or l_not l_implies t_globally t_finally t_next t_until t_release') + class Formula_rsLTL(object): - - def __init__(self, f_type, L_oper = None, R_oper = None, sub_oper = None, bag = None): + + def __init__( + self, f_type, L_oper=None, R_oper=None, sub_oper=None, bag=None): self.f_type = f_type self.left_operand = L_oper self.right_operand = R_oper self.sub_operand = sub_oper self.bag_descr = bag - + + if callable(sub_oper): + raise RuntimeError( + "sub_oper should not be a function. Missing () for {0}?".format(sub_oper)) + if isinstance(self.left_operand, BagDescription): self.left_operand = Formula_rsLTL.f_bag(self.left_operand) if isinstance(self.right_operand, BagDescription): self.right_operand = Formula_rsLTL.f_bag(self.right_operand) - + def __repr__(self): if self.f_type == rsLTL_form_type.bag: return repr(self.bag_descr) @@ -37,9 +45,15 @@ class Formula_rsLTL(object): if self.f_type == rsLTL_form_type.l_implies: return "( " + repr(self.left_operand) + " => " + repr(self.right_operand) + " )" if self.f_type == rsLTL_form_type.t_until: - return "( " + repr(self.left_operand) + " U[" + repr(self.sub_operand) + "] " + repr(self.right_operand) + " )" + return "( " + repr( + self.left_operand) + " U[" + repr( + self.sub_operand) + "] " + repr( + self.right_operand) + " )" if self.f_type == rsLTL_form_type.t_release: - return "( " + repr(self.left_operand) + " R[" + repr(self.sub_operand) + "] " + repr(self.right_operand) + " )" + return "( " + repr( + self.left_operand) + " R[" + repr( + self.sub_operand) + "] " + repr( + self.right_operand) + " )" @property def is_bag(self): @@ -47,48 +61,51 @@ class Formula_rsLTL(object): @classmethod def f_bag(cls, bag_descr): - return cls(rsLTL_form_type.bag, bag = bag_descr) + return cls(rsLTL_form_type.bag, bag=bag_descr) @classmethod def f_And(cls, arg_L, arg_R): - return cls(rsLTL_form_type.l_and, L_oper = arg_L, R_oper = arg_R) - + return cls(rsLTL_form_type.l_and, L_oper=arg_L, R_oper=arg_R) + @classmethod def f_Or(cls, arg_L, arg_R): - return cls(rsLTL_form_type.l_or, L_oper = arg_L, R_oper = arg_R) - + return cls(rsLTL_form_type.l_or, L_oper=arg_L, R_oper=arg_R) + @classmethod def f_Implies(cls, arg_L, arg_R): - return cls(rsLTL_form_type.l_implies, L_oper = arg_L, R_oper = arg_R) - + return cls(rsLTL_form_type.l_implies, L_oper=arg_L, R_oper=arg_R) + @classmethod def f_X(cls, sub, arg): - return cls(rsLTL_form_type.t_next, L_oper = arg, sub_oper = sub) + return cls(rsLTL_form_type.t_next, L_oper=arg, sub_oper=sub) @classmethod def f_G(cls, sub, arg): - return cls(rsLTL_form_type.t_globally, L_oper = arg, sub_oper = sub) - + return cls(rsLTL_form_type.t_globally, L_oper=arg, sub_oper=sub) + @classmethod def f_U(cls, sub, arg_L, arg_R): - return cls(rsLTL_form_type.t_until, L_oper = arg_L, R_oper = arg_R, sub_oper = sub) + return cls( + rsLTL_form_type.t_until, L_oper=arg_L, R_oper=arg_R, sub_oper=sub) @classmethod def f_F(cls, sub, arg_L): - return cls(rsLTL_form_type.t_finally, L_oper = arg_L, sub_oper = sub) + return cls(rsLTL_form_type.t_finally, L_oper=arg_L, sub_oper=sub) @classmethod def f_R(cls, sub, arg_L, arg_R): - return cls(rsLTL_form_type.t_release, L_oper = arg_L, R_oper = arg_R, sub_oper = sub) - + return cls( + rsLTL_form_type.t_release, L_oper=arg_L, R_oper=arg_R, + sub_oper=sub) + def __and__(self, other): - return Formula_rsLTL(rsLTL_form_type.l_and, L_oper = self, R_oper = other) - + return Formula_rsLTL(rsLTL_form_type.l_and, L_oper=self, R_oper=other) + def __or__(self, other): - return Formula_rsLTL(rsLTL_form_type.l_or, L_oper = self, R_oper = other) - + return Formula_rsLTL(rsLTL_form_type.l_or, L_oper=self, R_oper=other) + def __invert__(self): - return Formula_rsLTL(rsLTL_form_type.l_not, L_oper = self) + return Formula_rsLTL(rsLTL_form_type.l_not, L_oper=self) -# EOF \ No newline at end of file +# EOF