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

some sanity checks for a common mistake

Browse Source
This commit is contained in:
Artur Meski
2017-09-03 14:53:39 +01:00
parent 203182c520
commit 4b9aa59aff
2 changed files with 77 additions and 54 deletions
Download Patch File Download Diff File Expand all files Collapse all files

32
logics/bags.py
View File

@@ -1,8 +1,11 @@
from enum import Enum 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): 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.f_type = f_type
self.left_operand = L_oper self.left_operand = L_oper
self.right_operand = R_oper self.right_operand = R_oper
@@ -37,39 +40,42 @@ class BagDescription(object):
for operand in (self.left_operand, self.right_operand): for operand in (self.left_operand, self.right_operand):
if operand: if operand:
if not (isinstance(operand, BagDescription) or isinstance(operand, int)): if not(
raise RuntimeError("Unexpected operand type for a bag: " + str(operand)) isinstance(operand, BagDescription)
or isinstance(operand, int)):
raise RuntimeError(
"Unexpected operand type for a bag: " + str(operand))
@classmethod @classmethod
def f_entity(cls, entity_name): def f_entity(cls, entity_name):
return cls(BagDesc_oper.entity, entity = entity_name) return cls(BagDesc_oper.entity, entity=entity_name)
@classmethod @classmethod
def f_TRUE(cls): def f_TRUE(cls):
return cls(BagDesc_oper.true) return cls(BagDesc_oper.true)
def __lt__(self, other): 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): 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): 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): 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): 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): 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): 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): def __invert__(self):
return BagDescription(BagDesc_oper.l_not, L_oper = self) return BagDescription(BagDesc_oper.l_not, L_oper=self)
# EOF # EOF

49
logics/rsltl.py
View File

@@ -3,17 +3,25 @@ from enum import Enum
from logics.bags import * 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): 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.f_type = f_type
self.left_operand = L_oper self.left_operand = L_oper
self.right_operand = R_oper self.right_operand = R_oper
self.sub_operand = sub_oper self.sub_operand = sub_oper
self.bag_descr = bag 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): if isinstance(self.left_operand, BagDescription):
self.left_operand = Formula_rsLTL.f_bag(self.left_operand) self.left_operand = Formula_rsLTL.f_bag(self.left_operand)
if isinstance(self.right_operand, BagDescription): if isinstance(self.right_operand, BagDescription):
@@ -37,9 +45,15 @@ class Formula_rsLTL(object):
if self.f_type == rsLTL_form_type.l_implies: if self.f_type == rsLTL_form_type.l_implies:
return "( " + repr(self.left_operand) + " => " + repr(self.right_operand) + " )" return "( " + repr(self.left_operand) + " => " + repr(self.right_operand) + " )"
if self.f_type == rsLTL_form_type.t_until: 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: 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 @property
def is_bag(self): def is_bag(self):
@@ -47,48 +61,51 @@ class Formula_rsLTL(object):
@classmethod @classmethod
def f_bag(cls, bag_descr): 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 @classmethod
def f_And(cls, arg_L, arg_R): 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 @classmethod
def f_Or(cls, arg_L, arg_R): 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 @classmethod
def f_Implies(cls, arg_L, arg_R): 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 @classmethod
def f_X(cls, sub, arg): 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 @classmethod
def f_G(cls, sub, arg): 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 @classmethod
def f_U(cls, sub, arg_L, arg_R): 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 @classmethod
def f_F(cls, sub, arg_L): 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 @classmethod
def f_R(cls, sub, arg_L, arg_R): 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): 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): 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): 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 # EOF