artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Parameters for rsLTL

Browse Source
This commit is contained in:
Artur Meski
2017-03-01 21:08:41 +01:00
parent bae7611606
commit 68c824e2f1
1 changed files with 23 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files

39
formula_rsltl.py
View File

@@ -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)