From 108a5c75dc80e30b6f9828a1db7720b53459d6d1 Mon Sep 17 00:00:00 2001 From: hkff Date: Fri, 22 Jan 2016 18:01:51 +0100 Subject: [PATCH] Adding function and interpreted predicates --- fotl/fotl.py | 62 ++++++++++++++++++++++++++++++++++++ fotl/fotlmon.py | 7 +++++ fotl/lib.py | 83 +++++++++++++++++++++++++++++++++++++++++++++++++ ltl/ltl.py | 4 +-- 4 files changed, 154 insertions(+), 2 deletions(-) create mode 100644 fotl/lib.py diff --git a/fotl/fotl.py b/fotl/fotl.py index 7641e3a..f6dbdad 100644 --- a/fotl/fotl.py +++ b/fotl/fotl.py @@ -117,3 +117,65 @@ def __init__(self, value=None, var=None): def __str__(self): return "%s<-%s" % (self.value, self.var) + + +############################# +# Functions / Interpreted OP +############################# +class IPredicate(Exp): + """ + Interpreted Predicate + """ + def __init__(self, *args): + self.args = args[0] + + def __str__(self): + return "%s(%s)" % (self.__class__.__name__, ",".join([str(x) for x in self.args])) + + def toCODE(self): + return "%s(%s)" % (self.__class__.__name__, ",".join([str(x) for x in self.args])) + + def eval(self, valuation=None): + """ + This method should be always called by subclasses + :param valuation + :return: Arguments evaluation + """ + args2 = [] + for a in self.args: + if isinstance(a, Function) or isinstance(a, IPredicate): + args2.append(Constant(a.eval(valuation=valuation))) + + elif isinstance(a, Variable): + found = False + for v in valuation: + if str(v.var) == a.name: + args2.append(Constant(str(v.value))) + found = True + break + if not found: + raise Exception("IPredicate instantiation failed : missing vars") + else: + args2.append(Constant(a)) + + return args2 + +IP = IPredicate + + +class Function(IPredicate): + """ + Function + """ + def __init__(self, *args): + super().__init__(args[0]) + + def eval(self, valuation=None): + """ + This method should be override to return some value + :param valuation + :return: + """ + return super().eval(valuation=valuation) + +FX = Function diff --git a/fotl/fotlmon.py b/fotl/fotlmon.py index 4abd00d..b4fbf39 100644 --- a/fotl/fotlmon.py +++ b/fotl/fotlmon.py @@ -18,6 +18,7 @@ __author__ = 'walid' from ltl.ltlmon import * from fotl.fotl import * +from fotl.lib import * step = 0 @@ -58,6 +59,12 @@ def prg(self, formula, event, valuation=None): res = ForallConj(e).eval() # return res + elif isinstance(formula, IPredicate): + res = B3(formula.eval(valuation=valuation)) + + elif isinstance(formula, Function): + res = formula.eval(valuation=valuation) + else: res = super().prg(formula, event, valuation) diff --git a/fotl/lib.py b/fotl/lib.py new file mode 100644 index 0000000..829b672 --- /dev/null +++ b/fotl/lib.py @@ -0,0 +1,83 @@ +""" +lib LTL monitor +Copyright (C) 2015 Walid Benghabrit + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +""" +__author__ = 'walid' + +from fotl.fotl import * +import re + + +class Eq(IP): + """ + Equality operator + """ + def __init__(self, *args): + super().__init__(args) + + def eval(self, valuation=None): + args2 = super().eval(valuation=valuation) + return str(args2[0]) == str(args2[1]) + + +class Gt(IP): + """ + Greater than + """ + def __init__(self, *args): + super().__init__(args) + + def eval(self, valuation=None): + args2 = super().eval(valuation=valuation) + return int(args2[0].name) > int(args2[1].name) + + +class Lt(IP): + """ + Greater than + """ + def __init__(self, *args): + super().__init__(args) + + def eval(self, valuation=None): + args2 = super().eval(valuation=valuation) + return int(args2[0].name) < int(args2[1].name) + + +class Regex(IP): + """ + Regular expression + """ + def __init__(self, *args): + super().__init__(args) + + def eval(self, valuation=None): + args2 = super().eval(valuation=valuation) + p = re.compile(args2[1].name) + return False if p.match(args2[0].name) is None else True + + +#################### +# Math functions +#################### +class Add(FX): + def __init__(self, *args): + super().__init__(args) + + def eval(self, valuation=None): + args2 = super().eval(valuation=valuation) + return int(args2[0].name) + int(args2[1].name) + diff --git a/ltl/ltl.py b/ltl/ltl.py index 2c20e1b..d345395 100644 --- a/ltl/ltl.py +++ b/ltl/ltl.py @@ -204,7 +204,7 @@ class Constant(Parameter): Constant """ def equal(self, o): - return (o is not None) and isinstance(o, Constant) and (o.name == self.name) + return (o is not None) and isinstance(o, Constant) and (str(o.name) == str(self.name)) def toLTLFO(self): return "'%s'" % self.name @@ -282,7 +282,7 @@ def instantiate(self, valuation): break if not found: raise Exception("Predicate instantiation failed : missing vars") - p.args.append(Variable(str(x.name))) + # p.args.append(Variable(str(x.name))) elif isinstance(x, Constant): p.args.append(x)