Skip to content

Commit

Permalink
Adding function and interpreted predicates
Browse files Browse the repository at this point in the history
  • Loading branch information
hkff committed Jan 22, 2016
1 parent c8ae593 commit 108a5c7
Showing 4 changed files with 154 additions and 2 deletions.
62 changes: 62 additions & 0 deletions fotl/fotl.py
Original file line number Diff line number Diff line change
@@ -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
7 changes: 7 additions & 0 deletions fotl/fotlmon.py
Original file line number Diff line number Diff line change
@@ -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)

83 changes: 83 additions & 0 deletions fotl/lib.py
Original file line number Diff line number Diff line change
@@ -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 <http://www.gnu.org/licenses/>.
"""
__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)

4 changes: 2 additions & 2 deletions ltl/ltl.py
Original file line number Diff line number Diff line change
@@ -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)

0 comments on commit 108a5c7

Please sign in to comment.