From 2abf76ae72f65f93385b34f6b289d8f4d85da1b6 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Thu, 2 Mar 2017 20:59:07 +0100 Subject: [PATCH] logics module --- logics/__init__.py | 2 + logics/rsltl.py | 129 +++++++++++++++++++++++++++++++++++++++++ smt/smt_checker_rsc.py | 7 +++ 3 files changed, 138 insertions(+) create mode 100644 logics/__init__.py create mode 100644 logics/rsltl.py diff --git a/logics/__init__.py b/logics/__init__.py new file mode 100644 index 0000000..9579ea8 --- /dev/null +++ b/logics/__init__.py @@ -0,0 +1,2 @@ +from logics.rsltl import Formula_rsLTL +from logics.rsltl import BagDescription diff --git a/logics/rsltl.py b/logics/rsltl.py new file mode 100644 index 0000000..a83ecb0 --- /dev/null +++ b/logics/rsltl.py @@ -0,0 +1,129 @@ +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 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 = ""): + 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.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: + 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) + + @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) + + 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 Formula_rsLTL(object): + + 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): + if self.f_type == rsLTL_form_type.bag: + return repr(self.bag_descr) + 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.sub_operand) + "]( " + repr(self.left_operand) + " )" + if self.f_type == rsLTL_form_type.next: + 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.sub_operand) + "]" + repr(self.right_operand) + " )" + if self.f_type == rsLTL_form_type.release: + 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, sub, arg): + return cls(rsLTL_form_type.next, L_oper = arg, sub_oper = sub) + + @classmethod + def f_G(cls, sub, arg): + return cls(rsLTL_form_type.globally, L_oper = arg, sub_oper = sub) + + @classmethod + 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, 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) + + def __or__(self, other): + return FormulaLTL(rsLTL_form_type.l_or, L_oper = self, R_oper = other) + + def __invert__(self): + return FormulaLTL(rsLTL_form_type.l_not, L_oper = self) + +#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) + + + diff --git a/smt/smt_checker_rsc.py b/smt/smt_checker_rsc.py index c9fae4c..16f83b0 100644 --- a/smt/smt_checker_rsc.py +++ b/smt/smt_checker_rsc.py @@ -9,6 +9,8 @@ from itertools import chain import resource from colour import * +import logics + # def simplify(x): # return x @@ -362,6 +364,11 @@ class SmtCheckerRSC(object): if int(var_rep) > 0: print(" " + self.rs.get_entity_name(var_id) + "=" + var_rep, end="") print(" }") + + def check_rsltl(self, formula, print_witness=True): + """Bounded Model Checking for rsLTL properties""" + + def check_reachability(self, state, print_witness=True, print_time=True, print_mem=True, max_level=100):