From 68c824e2f1d6a0df4193f9013f38d7d368fd0883 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Wed, 1 Mar 2017 21:08:41 +0100 Subject: [PATCH] Parameters for rsLTL --- formula_rsltl.py | 39 +++++++++++++++++++++++---------------- 1 file changed, 23 insertions(+), 16 deletions(-) diff --git a/formula_rsltl.py b/formula_rsltl.py index e92e755..1323cfb 100644 --- a/formula_rsltl.py +++ b/formula_rsltl.py @@ -1,7 +1,7 @@ from enum import Enum rsLTL_form_type = Enum('rsLTL_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') +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 = ""): @@ -13,6 +13,8 @@ class BagDescription(object): def __repr__(self): if self.f_type == BagDesc_oper.entity: return self.entity + if self.f_type == BagDesc_oper.true: + return "TRUE" 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: @@ -36,6 +38,10 @@ class BagDescription(object): def f_entity(cls, 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) @@ -62,10 +68,11 @@ class BagDescription(object): class FormulaLTL(object): - def __init__(self, f_type, L_oper = None, R_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 def __repr__(self): @@ -74,37 +81,37 @@ class FormulaLTL(object): if self.f_type == rsLTL_form_type.l_not: return "~( " + repr(self.left_operand) + " )" if self.f_type == rsLTL_form_type.globally: - return "G( " + repr(self.left_operand) + " )" + return "G[" + repr(self.sub_operand) + "]( " + repr(self.left_operand) + " )" if self.f_type == rsLTL_form_type.next: - return "X( " + repr(self.left_operand) + " )" + return "X[" + repr(self.sub_operand) + "]( " + repr(self.left_operand) + " )" if self.f_type == rsLTL_form_type.l_and: return "( " + repr(self.left_operand) + " & " + repr(self.right_operand) + " )" if self.f_type == rsLTL_form_type.l_or: return "( " + repr(self.left_operand) + " | " + repr(self.right_operand) + " )" if self.f_type == rsLTL_form_type.until: - return "( " + repr(self.left_operand) + " U " + 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.release: - return "( " + repr(self.left_operand) + " R " + repr(self.right_operand) + " )" + return "( " + repr(self.left_operand) + " R[" + repr(self.sub_operand) + "]" + repr(self.right_operand) + " )" @classmethod def f_bag(cls, bag_descr): return cls(rsLTL_form_type.bag, bag = bag_descr) @classmethod - def f_X(cls, arg): - return cls(rsLTL_form_type.next, L_oper = arg) + def f_X(cls, sub, arg): + return cls(rsLTL_form_type.next, L_oper = arg, sub_oper = sub) @classmethod - def f_G(cls, arg): - return cls(rsLTL_form_type.globally, L_oper = arg) + def f_G(cls, sub, arg): + return cls(rsLTL_form_type.globally, L_oper = arg, sub_oper = sub) @classmethod - def f_U(cls, arg_L, arg_R): - return cls(rsLTL_form_type.until, L_oper = arg_L, R_oper = arg_R) + def f_U(cls, sub, arg_L, arg_R): + return cls(rsLTL_form_type.until, L_oper = arg_L, R_oper = arg_R, sub_oper = sub) @classmethod - def f_R(cls, arg_L, arg_R): - return cls(rsLTL_form_type.release, L_oper = arg_L, R_oper = arg_R) + def f_R(cls, sub, arg_L, arg_R): + return cls(rsLTL_form_type.release, L_oper = arg_L, R_oper = arg_R, sub_oper = sub) def __and__(self, other): return FormulaLTL(rsLTL_form_type.l_and, L_oper = self, R_oper = other) @@ -115,7 +122,7 @@ class FormulaLTL(object): def __invert__(self): return FormulaLTL(rsLTL_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) ) ) ) +x = ~( FormulaLTL.f_X(BagDescription.f_TRUE(), FormulaLTL.f_bag( ~((BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) ) ) ) & FormulaLTL.f_X(BagDescription.f_TRUE(), FormulaLTL.f_bag( ~((BagDescription.f_entity("ent3") == 1) ) ) ) print(x) +