From b6a81b9637452266e64f64e79362132f84839eaf Mon Sep 17 00:00:00 2001 From: Cristian-Ioan Vasile Date: Tue, 7 Jan 2020 19:52:51 -0500 Subject: [PATCH 01/10] Updated grammar to process predicate expressions. --- stl/stl.g4 | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/stl/stl.g4 b/stl/stl.g4 index 5ab2f23..e29d25f 100644 --- a/stl/stl.g4 +++ b/stl/stl.g4 @@ -21,13 +21,14 @@ stlProperty: | left=stlProperty op=UNTIL '[' low=RATIONAL ',' high=RATIONAL ']' right=stlProperty #formula ; expr: - ( '-(' | '(' ) expr ')' - | expr '^' expr - | VARIABLE '(' expr ')' - | expr ( '*' | '/' ) expr - | expr ( '+' | '-' ) expr - | RATIONAL - | VARIABLE + '(' child=expr ')' # parExpr + | '-(' child=expr ')' # negExpr + | base=expr op='^' exp=expr # powExpr + | func=VARIABLE '(' (expr ( ',' expr)* ) ')' #funcExpr + | left=expr op=( '*' | '/' ) right=expr #prodExpr + | left=expr op=( '+' | '-' ) right=expr #sumExpr + | value=RATIONAL #constExpr + | variable=VARIABLE #varExpr ; booleanExpr: left=expr op=( '<' | '<=' | '=' | '>=' | '>' ) right=expr From 38217910670f58e7009b110e34210596a3d1095a Mon Sep 17 00:00:00 2001 From: Cristian-Ioan Vasile Date: Tue, 7 Jan 2020 19:53:35 -0500 Subject: [PATCH 02/10] Added class for expressions. --- stl/stl.py | 113 +++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 110 insertions(+), 3 deletions(-) diff --git a/stl/stl.py b/stl/stl.py index 3e02419..e2be900 100644 --- a/stl/stl.py +++ b/stl/stl.py @@ -1,6 +1,7 @@ ''' - Copyright (C) 2015-2018 Cristian Ioan Vasile + Copyright (C) 2015-2020 Cristian Ioan Vasile Hybrid and Networked Systems (HyNeSs) Group, BU Robotics Lab, Boston University + Explainable Robotics Lab, Lehigh University See license.txt file for license information. ''' @@ -53,6 +54,112 @@ def getString(cls, rop): '''Gets custom string representation for each operation.''' return cls.opnames[rop] +class Expression(object): + '''Abstract Syntax Tree representations of expressions involved in STL + predicates + ''' + NOP, NEG, ADD, PROD, DIV, POW, FUNC, VAR, CONST = range(9) + opnames = [None, '-', '+', '/', '^'] + opcodes = {'-': NEG, '+': ADD, '*' : PROD, '/': DIV, '^': POW} + + @classmethod + def getCode(cls, text): + ''' Gets the code corresponding to the string representation.''' + return cls.opcodes.get(text, cls.NOP) + + @classmethod + def getString(cls, op): + '''Gets custom string representation for each operation.''' + return cls.opnames[op] + + def __init__(self, operation, **kwargs): + '''Constructor''' + self.op = operation + + if self.op == Expression.NEG: + self.child = kwargs['child'] + elif self.op in (Expression.ADD, Expression.PROD): + self.children = kwargs['children'] + elif self.op == Expression.DIV: + self.divident = kwargs['divident'] + self.divisor = kwargs['divisor'] + elif self.op == Expression.POW: + self.base = kwargs['base'] + self.exponent = kwargs['exponent'] + elif self.op == Expression.FUNC: + self.function = kwargs['function'] + self.arguments = kwargs['arguments'] + elif self.op == Expression.VAR: + self.variable = kwargs['variable'] + elif self.op == Expression.CONST: + self.value = kwargs['value'] + + def variables(self): + '''Returns the set of variables involved in the expression.''' + if self.op == Expression.NEG: + return self.child.variables() + elif self.op in (Expression.ADD, Expression.PROD): + return set.union(*[child.variables() for child in self.children]) + elif self.op == Expression.DIV: + return self.divident.variables() & self.divisor.variables() + elif self.op == Expression.POW: + return self.base.variables() & self.exponent.variables() + elif self.op == Expression.FUNC: + return set.union(*[arg.variables() for arg in self.arguments]) + elif self.op == Expression.VAR: + return set([self.variable]) + elif self.op == Expression.CONST: + return set() + + def eval(self, variables): + '''Evaluates the expression using the variables' values.''' + if self.op == Expression.NEG: + return - self.child.eval(variables) + elif self.op == Expression.ADD: + return np.sum([child.eval(variables) for child in self.children]) + elif self.op == Expression.PROD: + return np.prod([child.eval(variables) for child in self.children]) + elif self.op == Expression.DIV: + return self.divident.eval(variables) // self.divisor.eval(variables) + elif self.op == Expression.POW: + return np.pow(self.base.eval(variables), + self.exponent.eval(variables)) + elif self.op == Expression.FUNC: + return self.function(*[arg.eval(variables) + for arg in self.arguments]) + elif self.op == Expression.VAR: + return variables[self.variable] + elif self.op == Expression.CONST: + return self.value + + def __str__(self): + if self.__string is not None: + return self.__string + + if self.op == Expression.NEG: + s = '-({child})'.format(child=self.child) + elif self.op in (Expression.ADD, Expression.PROD): + opname = Expression.getString(self.op) + children = [str(child) for child in self.children] + s = '(' + ' {op} '.format(op=opname).join(children) + ')' + elif self.op == Expression.DIV: + s = '{divident} / {divisor}'.format(divident=self.divident, + divisor=self.divisor) + elif self.op == Expression.POW: + s = '{base} ^ {exponent}'.format(base=self.base, + exponent=self.exponent) + elif self.op == Expression.FUNC: + arguments = [str(arg) for arg in self.arguments] + s = '{func_name}({arguments})'.format( + funcname=self.function.__name__, + arguments=arguments) + elif self.op == Expression.VAR: + s = self.variable + elif self.op == Expression.CONST: + s = str(self.value) + self.__string = s + return self.__string + class STLFormula(object): '''Abstract Syntax Tree representation of an STL formula''' @@ -306,7 +413,7 @@ def visitBooleanExpr(self, ctx): variable=ctx.left.getText(), threshold=float(ctx.right.getText())) def visitParprop(self, ctx): - return self.visit(ctx.child); + return self.visit(ctx.child) class Trace(object): @@ -342,7 +449,7 @@ def __str__(self): print(t.toStringTree()) ast = STLAbstractSyntaxTreeExtractor().visit(t) - print('AST:', ast) + print('AST:', str(ast)) varnames = ['x', 'y', 'z'] data = [[8, 8, 11, 11, 11], [2, 3, 1, 2, 2], [3, 9, 8, 9, 9]] From a877d0c5c20bf1229b897730784c48c6a443e890 Mon Sep 17 00:00:00 2001 From: Cristian-Ioan Vasile Date: Tue, 7 Jan 2020 20:35:37 -0500 Subject: [PATCH 03/10] Simplified expression class and processing. Added expression parsing. --- stl/stl.g4 | 8 +++--- stl/stl.py | 74 +++++++++++++++++++++++++++++++++--------------------- 2 files changed, 49 insertions(+), 33 deletions(-) diff --git a/stl/stl.g4 b/stl/stl.g4 index e29d25f..b59e448 100644 --- a/stl/stl.g4 +++ b/stl/stl.g4 @@ -22,11 +22,11 @@ stlProperty: ; expr: '(' child=expr ')' # parExpr - | '-(' child=expr ')' # negExpr - | base=expr op='^' exp=expr # powExpr + | '-' child=expr # negExpr + | base=expr op='^' exp=expr #algExpr | func=VARIABLE '(' (expr ( ',' expr)* ) ')' #funcExpr - | left=expr op=( '*' | '/' ) right=expr #prodExpr - | left=expr op=( '+' | '-' ) right=expr #sumExpr + | left=expr op=( '*' | '/' ) right=expr #algExpr + | left=expr op=( '+' | '-' ) right=expr #algExpr | value=RATIONAL #constExpr | variable=VARIABLE #varExpr ; diff --git a/stl/stl.py b/stl/stl.py index e2be900..16b0474 100644 --- a/stl/stl.py +++ b/stl/stl.py @@ -58,9 +58,9 @@ class Expression(object): '''Abstract Syntax Tree representations of expressions involved in STL predicates ''' - NOP, NEG, ADD, PROD, DIV, POW, FUNC, VAR, CONST = range(9) - opnames = [None, '-', '+', '/', '^'] - opcodes = {'-': NEG, '+': ADD, '*' : PROD, '/': DIV, '^': POW} + NOP, NEG, ADD, SUB, PROD, DIV, POW, FUNC, VAR, CONST = range(10) + opnames = [None, '-', '+', '-', '*', '/', '^'] + opcodes = {'-': NEG, '+': ADD, '-': SUB, '*': PROD, '/': DIV, '^': POW} @classmethod def getCode(cls, text): @@ -78,14 +78,10 @@ def __init__(self, operation, **kwargs): if self.op == Expression.NEG: self.child = kwargs['child'] - elif self.op in (Expression.ADD, Expression.PROD): - self.children = kwargs['children'] - elif self.op == Expression.DIV: - self.divident = kwargs['divident'] - self.divisor = kwargs['divisor'] - elif self.op == Expression.POW: - self.base = kwargs['base'] - self.exponent = kwargs['exponent'] + elif self.op in (Expression.ADD, Expression.SUB, Expression.PROD, + Expression.DIV, Expression.POW): + self.left = kwargs['left'] + self.right = kwargs['right'] elif self.op == Expression.FUNC: self.function = kwargs['function'] self.arguments = kwargs['arguments'] @@ -94,16 +90,15 @@ def __init__(self, operation, **kwargs): elif self.op == Expression.CONST: self.value = kwargs['value'] + self.__string = None + def variables(self): '''Returns the set of variables involved in the expression.''' if self.op == Expression.NEG: return self.child.variables() - elif self.op in (Expression.ADD, Expression.PROD): - return set.union(*[child.variables() for child in self.children]) - elif self.op == Expression.DIV: - return self.divident.variables() & self.divisor.variables() - elif self.op == Expression.POW: - return self.base.variables() & self.exponent.variables() + elif self.op in (Expression.ADD, Expression.SUB, Expression.PROD, + Expression.DIV, Expression.POW): + return self.left.variables() & self.right.variables() elif self.op == Expression.FUNC: return set.union(*[arg.variables() for arg in self.arguments]) elif self.op == Expression.VAR: @@ -116,9 +111,11 @@ def eval(self, variables): if self.op == Expression.NEG: return - self.child.eval(variables) elif self.op == Expression.ADD: - return np.sum([child.eval(variables) for child in self.children]) + return self.left.eval(variables) + self.right.eval(variables) + elif self.op == Expression.SUB: + return self.left.eval(variables) - self.right.eval(variables) elif self.op == Expression.PROD: - return np.prod([child.eval(variables) for child in self.children]) + return self.left.eval(variables) * self.right.eval(variables) elif self.op == Expression.DIV: return self.divident.eval(variables) // self.divisor.eval(variables) elif self.op == Expression.POW: @@ -138,16 +135,11 @@ def __str__(self): if self.op == Expression.NEG: s = '-({child})'.format(child=self.child) - elif self.op in (Expression.ADD, Expression.PROD): + elif self.op in (Expression.ADD, Expression.SUB, Expression.PROD, + Expression.DIV, Expression.POW): opname = Expression.getString(self.op) - children = [str(child) for child in self.children] - s = '(' + ' {op} '.format(op=opname).join(children) + ')' - elif self.op == Expression.DIV: - s = '{divident} / {divisor}'.format(divident=self.divident, - divisor=self.divisor) - elif self.op == Expression.POW: - s = '{base} ^ {exponent}'.format(base=self.base, - exponent=self.exponent) + s = '({left} {op} {right})'.format(op=opname, left=self.left, + right=self.right) elif self.op == Expression.FUNC: arguments = [str(arg) for arg in self.arguments] s = '{func_name}({arguments})'.format( @@ -408,10 +400,34 @@ def visitBooleanPred(self, ctx): return self.visit(ctx.booleanExpr()) def visitBooleanExpr(self, ctx): + print self.visit(ctx.left) + print self.visit(ctx.right) return STLFormula(Operation.PRED, relation=RelOperation.getCode(ctx.op.text), variable=ctx.left.getText(), threshold=float(ctx.right.getText())) + def visitVarExpr(self, ctx): + return Expression(Expression.VAR, variable=ctx.variable.text) + + def visitConstExpr(self, ctx): + return Expression(Expression.CONST, value=float(ctx.value.text)) + + def visitNegExpr(self, ctx): + return Expression(Expression.NEG, child=self.visit(ctx.child)) + + def visitAlgExpr(self, ctx): + left = self.visit(ctx.left) + right = self.visit(ctx.right) + return Expression(Expression.getCode(ctx.op.text), + left=left, + right=right) + + def visitFuncExpr(self, ctx): + raise NotImplementedError() + + def visitParExpr(self, ctx): + return self.visit(ctx.child); + def visitParprop(self, ctx): return self.visit(ctx.child) @@ -440,7 +456,7 @@ def __str__(self): raise NotImplementedError if __name__ == '__main__': - lexer = stlLexer(InputStream("!(x < 10) && F[0, 2] y > 2 || G[1, 3] z<=8")) + lexer = stlLexer(InputStream("!(x < 10) && F[0, 2] y > 2 || G[1, 3] z<=8 && (-x + 2*y - z< 2) && G[0, 3] (x*x - 4*x + 4 + y*y - 6*y + 9 >= 2)")) # lexer = stlLexer(InputStream("!(x < 10) && y > 2 && z<=8")) tokens = CommonTokenStream(lexer) From 8bb20e60ee7e97b8e5715526b797db55dda5873f Mon Sep 17 00:00:00 2001 From: Cristian-Ioan Vasile Date: Tue, 7 Jan 2020 21:38:39 -0500 Subject: [PATCH 04/10] Updated STL formula class to handle general predicates. --- stl/stl.py | 90 ++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 64 insertions(+), 26 deletions(-) diff --git a/stl/stl.py b/stl/stl.py index 16b0474..3346177 100644 --- a/stl/stl.py +++ b/stl/stl.py @@ -91,20 +91,26 @@ def __init__(self, operation, **kwargs): self.value = kwargs['value'] self.__string = None + self.__variables = None def variables(self): '''Returns the set of variables involved in the expression.''' + if self.__variables is not None: + return self.__variables + if self.op == Expression.NEG: - return self.child.variables() + vars = self.child.variables() elif self.op in (Expression.ADD, Expression.SUB, Expression.PROD, Expression.DIV, Expression.POW): - return self.left.variables() & self.right.variables() + vars = self.left.variables() | self.right.variables() elif self.op == Expression.FUNC: - return set.union(*[arg.variables() for arg in self.arguments]) + vars = set.union(*[arg.variables() for arg in self.arguments]) elif self.op == Expression.VAR: - return set([self.variable]) + vars = set([self.variable]) elif self.op == Expression.CONST: - return set() + vars = set() + self.__variables = vars + return self.__variables def eval(self, variables): '''Evaluates the expression using the variables' values.''' @@ -164,7 +170,7 @@ def __init__(self, operation, **kwargs): self.value = kwargs['value'] elif self.op == Operation.PRED: self.relation = kwargs['relation'] - self.variable = kwargs['variable'] + self.expression = kwargs['expression'] self.threshold = kwargs['threshold'] elif self.op in (Operation.AND, Operation.OR): self.children = kwargs['children'] @@ -194,7 +200,12 @@ def robustness(self, s, t, maximumRobustness=1): else: return -maximumRobustness elif self.op == Operation.PRED: - value = s.value(self.variable, t) + if self.expression.op == Expression.VAR: + value = s.value(self.expression.variable, t) + else: + variables = {variable: s.value(variable, t) + for variable in self.expression.variables()} + value = self.expression.eval(variables) if self.relation in (RelOperation.GE, RelOperation.GT): return value - self.threshold elif self.relation in (RelOperation.LE, RelOperation.LT): @@ -251,28 +262,52 @@ def negate(self): self.op = Operation.negop[self.op] return self + def isSimpleLinear(self): + '''Checks if the predicates of the STL formula are linear monomials, + i.e., just a variable with coefficient 1.''' + if self.op == Operation.PRED: + return self.expression.op == Expression.VAR + elif self.op in (Operation.AND, Operation.OR): + return all([ch.isSimpleLinear() for ch in self.children]) + elif self.op in (Operation.IMPLIES, Operation.UNTIL): + return self.left.isSimpleLinear() and self.right.isSimpleLinear() + elif self.op in (Operation.NOT, Operation.ALWAYS, Operation.EVENT): + return self.child.isSimpleLinear() + def pnf(self): '''Computes the Positive Normal Form of the STL formula, potentially adding new variables. Note: The tree structure is modified in-place. + Note: Only works for STL formulae with simple linear predicates. ''' if self.op == Operation.PRED: + assert self.expression.op == Expression.VAR + neg_var = Expression(Expression.VAR, + variable='{variable}_neg'.format( + variable=self.expression.variable)) + if self.relation in (RelOperation.LE, RelOperation.LT): - self.variable = '{variable}_neg'.format(variable=self.variable) + self.expression.variable = neg_var elif self.relation == RelOperation.EQ: - children = [STLFormula(Operation.PRED, relation=RelOperation.GE, - variable=self.variable, threshold=self.threshold), - STLFormula(Operation.PRED, relation=RelOperation.GE, - variable='{variable}_neg'.format(self.variable), - threshold=-self.threshold)] + children = [STLFormula(Operation.PRED, + relation=RelOperation.GE, + expression=self.expression, + threshold=self.threshold), + STLFormula(Operation.PRED, + relation=RelOperation.GE, + expression=neg_var, + threshold=-self.threshold)] return STLFormula(Operation.AND, children=children) elif self.relation == RelOperation.NQ: - children = [STLFormula(Operation.PRED, relation=RelOperation.GT, - variable=self.variable, threshold=self.threshold), - STLFormula(Operation.PRED, relation=RelOperation.GT, - variable='{variable}_neg'.format(self.variable), - threshold=-self.threshold)] + children = [STLFormula(Operation.PRED, + relation=RelOperation.GT, + expression=self.expression, + threshold=self.threshold), + STLFormula(Operation.PRED, + relation=RelOperation.GT, + expression=neg_var, + threshold=-self.threshold)] return STLFormula(Operation.OR, children=children) elif self.op in (Operation.AND, Operation.OR): self.children = [child.pnf() for child in self.children] @@ -306,7 +341,7 @@ def bound(self): def variables(self): '''Computes the set of variables involved in the STL formula.''' if self.op == Operation.PRED: - return {self.variable} + return self.expression.variables() elif self.op in (Operation.AND, Operation.OR): return set.union(*[child.variables() for child in self.children]) elif self.op in (Operation.IMPLIES, Operation.UNTIL): @@ -339,7 +374,7 @@ def __str__(self): opname = Operation.getString(self.op) if self.op == Operation.PRED: - s = '({v} {rel} {th})'.format(v=self.variable, th=self.threshold, + s = '({e} {rel} {th})'.format(e=self.expression, th=self.threshold, rel=RelOperation.getString(self.relation)) elif self.op == Operation.IMPLIES: s = '{left} {op} {right}'.format(left=self.left, op=opname, @@ -400,11 +435,12 @@ def visitBooleanPred(self, ctx): return self.visit(ctx.booleanExpr()) def visitBooleanExpr(self, ctx): - print self.visit(ctx.left) - print self.visit(ctx.right) + threshold = self.visit(ctx.right) + assert threshold.op == Expression.CONST return STLFormula(Operation.PRED, - relation=RelOperation.getCode(ctx.op.text), - variable=ctx.left.getText(), threshold=float(ctx.right.getText())) + relation=RelOperation.getCode(ctx.op.text), + expression=self.visit(ctx.left), + threshold=threshold.value) def visitVarExpr(self, ctx): return Expression(Expression.VAR, variable=ctx.variable.text) @@ -457,6 +493,7 @@ def __str__(self): if __name__ == '__main__': lexer = stlLexer(InputStream("!(x < 10) && F[0, 2] y > 2 || G[1, 3] z<=8 && (-x + 2*y - z< 2) && G[0, 3] (x*x - 4*x + 4 + y*y - 6*y + 9 >= 2)")) + # lexer = stlLexer(InputStream("!(x < 10) && F[0, 2] y > 2 || G[1, 3] z<=8")) # lexer = stlLexer(InputStream("!(x < 10) && y > 2 && z<=8")) tokens = CommonTokenStream(lexer) @@ -474,5 +511,6 @@ def __str__(self): print('r:', ast.robustness(s, 0)) - pnf = ast.pnf() - print(pnf) + if ast.isSimpleLinear(): + pnf = ast.pnf() + print(pnf) From fd85d540499d0c1e912e9ec8410b125c7db6a988 Mon Sep 17 00:00:00 2001 From: Cristian-Ioan Vasile Date: Tue, 7 Jan 2020 21:40:29 -0500 Subject: [PATCH 05/10] Corrected bug in negate method. --- stl/stl.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/stl/stl.py b/stl/stl.py index 3346177..09eb0a2 100644 --- a/stl/stl.py +++ b/stl/stl.py @@ -249,8 +249,7 @@ def negate(self): if self.op == Operation.PRED: self.relation = RelOperation.negop[self.relation] elif self.op in (Operation.AND, Operation.OR): - self.left = self.left.negate() - self.right = self.right.negate() + [child.negate() for child in self.children] elif self.op == Operation.IMPLIES: self.right = self.right.negate() elif self.op == Operation.NOT: From c6668aad81985652b0d4f96d2b299894e56611c2 Mon Sep 17 00:00:00 2001 From: Cristian-Ioan Vasile Date: Tue, 7 Jan 2020 21:45:45 -0500 Subject: [PATCH 06/10] Updated MILP translation. --- stl/stl2milp.py | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/stl/stl2milp.py b/stl/stl2milp.py index 920704c..95680ce 100644 --- a/stl/stl2milp.py +++ b/stl/stl2milp.py @@ -1,12 +1,13 @@ ''' - Copyright (C) 2018 Cristian Ioan Vasile + Copyright (C) 2018-2020 Cristian Ioan Vasile Hybrid and Networked Systems (HyNeSs) Group, BU Robotics Lab, Boston University + Explainable Robotics Lab, Lehigh University See license.txt file for license information. ''' import gurobipy as grb -from stl import Operation, RelOperation, STLFormula +from stl import Operation, RelOperation, Expression, STLFormula class stl2milp(object): @@ -84,7 +85,8 @@ def add_state(self, state, t): def predicate(self, pred, z, t): '''Adds a predicate to the model.''' assert pred.op == Operation.PRED - v = self.add_state(pred.variable, t) + assert pred.expression.op == Expression.VAR + v = self.add_state(pred.expression.variable, t) if pred.relation in (RelOperation.GE, RelOperation.GT): self.model.addConstr(v - self.M * z <= pred.threshold + self.rho) self.model.addConstr(v + self.M * (1 - z) >= pred.threshold + self.rho) @@ -173,4 +175,4 @@ def until(self, formula, z, t): + sum(z_children_left[:t+a+k+1])) self.model.addConstr(z >= z_conj) - self.model.addConstr(z <= sum(z_aux)) \ No newline at end of file + self.model.addConstr(z <= sum(z_aux)) From 2d22dc8f935f4ba939a4448cdf86953de0ed0af2 Mon Sep 17 00:00:00 2001 From: Cristian-Ioan Vasile Date: Tue, 7 Jan 2020 21:49:06 -0500 Subject: [PATCH 07/10] TRIV: Updated license information. --- stl/stl.g4 | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/stl/stl.g4 b/stl/stl.g4 index b59e448..7fdbf73 100644 --- a/stl/stl.g4 +++ b/stl/stl.g4 @@ -2,8 +2,9 @@ grammar stl; @header { ''' - Copyright (C) 2015-2018 Cristian Ioan Vasile + Copyright (C) 2015-2020 Cristian Ioan Vasile Hybrid and Networked Systems (HyNeSs) Group, BU Robotics Lab, Boston University + Explainable Robotics Lab, Lehigh University See license.txt file for license information. ''' } From 3b5f4dd76c3cc51fd3dd63e05fadeba7e989470d Mon Sep 17 00:00:00 2001 From: Cristian-Ioan Vasile Date: Tue, 7 Jan 2020 21:58:33 -0500 Subject: [PATCH 08/10] Added translation of STL with quadratic predicates to MIQP. --- stl/stl2miqp.py | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 stl/stl2miqp.py diff --git a/stl/stl2miqp.py b/stl/stl2miqp.py new file mode 100644 index 0000000..9ac04ca --- /dev/null +++ b/stl/stl2miqp.py @@ -0,0 +1,30 @@ +''' + Copyright (C) 2018-2020 Cristian Ioan Vasile + Hybrid and Networked Systems (HyNeSs) Group, BU Robotics Lab, Boston University + Explainable Robotics Lab, Lehigh University + See license.txt file for license information. +''' + +import gurobipy as grb + +from stl import Operation, RelOperation +from stl2milp import stl2milp + + +class stl2miqp(stl2milp): + '''Translate an STL formula to an MIQP.''' + + def predicate(self, pred, z, t): + '''Adds a predicate to the model.''' + assert pred.op == Operation.PRED + variables = pred.expression.variables() + variables = {var: self.add_state(var, t) for var in variables} + expr = pred.expression.eval(variables) + if pred.relation in (RelOperation.GE, RelOperation.GT): + self.model.addConstr(expr - self.M * z <= pred.threshold + self.rho) + self.model.addConstr(expr + self.M * (1 - z) >= pred.threshold + self.rho) + elif pred.relation in (RelOperation.LE, RelOperation.LT): + self.model.addConstr(expr + self.M * z >= pred.threshold - self.rho) + self.model.addConstr(expr - self.M * (1 - z) <= pred.threshold - self.rho) + else: + raise NotImplementedError From 95212dd4e8a22723459051fada3b7f8856d1c3e8 Mon Sep 17 00:00:00 2001 From: Cristian-Ioan Vasile Date: Thu, 9 Jan 2020 16:50:10 -0500 Subject: [PATCH 09/10] Made small bug fixes, and finished code for the until operator. --- stl/stl2milp.py | 33 ++++++++++++++++++--------------- stl/stl2miqp.py | 3 +++ 2 files changed, 21 insertions(+), 15 deletions(-) diff --git a/stl/stl2milp.py b/stl/stl2milp.py index 95680ce..9177611 100644 --- a/stl/stl2milp.py +++ b/stl/stl2milp.py @@ -35,6 +35,7 @@ def __init__(self, formula, ranges=None, vtypes=None, model=None, if robust: self.rho = self.model.addVar(vtype=grb.GRB.CONTINUOUS, name='rho', lb=-grb.GRB.INFINITY,ub=grb.GRB.INFINITY, obj=-1) + self.model.addConstr(self.rho >= 0, 'rho_non_negative') else: self.rho = 0 @@ -47,6 +48,12 @@ def __init__(self, formula, ranges=None, vtypes=None, model=None, Operation.UNTIL : self.until } + def translate(self, formula, t=0): + '''Translates the STL formula to MILP model.''' + z_formula = self.to_milp(formula, t) + self.model.addConstr(z_formula == 1, 'formula_satisfaction') + return z_formula + def to_milp(self, formula, t=0): '''Generates the MILP from the STL formula.''' z, added = self.add_formula_variable(formula, t) @@ -78,7 +85,6 @@ def add_state(self, state, t): name='{}_{}'.format(state, t) v = self.model.addVar(vtype=vtype, lb=low, ub=high, name=name) self.variables[state][t] = v - print 'Added state:', state, 'time:', t self.model.update() return self.variables[state][t] @@ -90,10 +96,12 @@ def predicate(self, pred, z, t): if pred.relation in (RelOperation.GE, RelOperation.GT): self.model.addConstr(v - self.M * z <= pred.threshold + self.rho) self.model.addConstr(v + self.M * (1 - z) >= pred.threshold + self.rho) + # TODO: are the next two lines necessary? + self.model.addConstr(v - self.M * z <= pred.threshold) + self.model.addConstr(v + self.M * (1 - z) >= pred.threshold) elif pred.relation in (RelOperation.LE, RelOperation.LT): self.model.addConstr(v + self.M * z >= pred.threshold - self.rho) self.model.addConstr(v - self.M * (1 - z) <= pred.threshold - self.rho) -# raise NotImplementedError else: raise NotImplementedError @@ -116,10 +124,9 @@ def disjunction(self, formula, z, t): def eventually(self, formula, z, t): '''Adds an eventually to the model.''' assert formula.op == Operation.EVENT - a, b = formula.low, formula.high + a, b = int(formula.low), int(formula.high) child = formula.child - print "a=%d,b=%d"%(a,b) - z_children = [self.to_milp(child, t + tau) for tau in range(int(a), int(b+1))] + z_children = [self.to_milp(child, t + tau) for tau in range(a, b+1)] for z_child in z_children: self.model.addConstr(z >= z_child) self.model.addConstr(z <= sum(z_children)) @@ -127,11 +134,9 @@ def eventually(self, formula, z, t): def globally(self, formula, z, t): '''Adds a globally to the model.''' assert formula.op == Operation.ALWAYS - a, b = formula.low, formula.high -# print "a=%d,b=%d,t=%d"%(a,b,t) + a, b = int(formula.low), int(formula.high) child = formula.child - z_children = [self.to_milp(child, t + tau) for tau in range(int(a), int(b+1))] -# print len(z_children) + z_children = [self.to_milp(child, t + tau) for tau in range(a, b+1)] for z_child in z_children: self.model.addConstr(z <= z_child) self.model.addConstr(z >= 1 - len(z_children) + sum(z_children)) @@ -140,9 +145,7 @@ def until(self, formula, z, t): '''Adds an until to the model.''' assert formula.op == Operation.UNTIL - raise NotImplementedError #TODO: under construction - - a, b = formula.low, formula.high + a, b = int(formula.low), int(formula.high) z_children_left = [self.to_milp(formula.left, tau) for tau in range(t, t+b+1)] z_children_right = [self.to_milp(formula.right, tau) @@ -163,16 +166,16 @@ def until(self, formula, z, t): if phi_alw is not None: children.append(phi_alw) phi = STLFormula(Operation.AND, children=children) - z_aux.append(self.add_formula_variable(phi, t)) + z_aux.append(self.add_formula_variable(phi, t)[0]) for k, z_right in enumerate(z_children_right): z_conj = z_aux[k] self.model.addConstr(z_conj <= z_right) for z_left in z_children_left[:t+a+k+1]: self.model.addConstr(z_conj <= z_left) - m = 1 + (t + a + k) + m = 1 + (t + a + k + 1) self.model.addConstr(z_conj >= 1-m + z_right + sum(z_children_left[:t+a+k+1])) - self.model.addConstr(z >= z_conj) + self.model.addConstr(z <= z_conj) self.model.addConstr(z <= sum(z_aux)) diff --git a/stl/stl2miqp.py b/stl/stl2miqp.py index 9ac04ca..c9a691c 100644 --- a/stl/stl2miqp.py +++ b/stl/stl2miqp.py @@ -23,6 +23,9 @@ def predicate(self, pred, z, t): if pred.relation in (RelOperation.GE, RelOperation.GT): self.model.addConstr(expr - self.M * z <= pred.threshold + self.rho) self.model.addConstr(expr + self.M * (1 - z) >= pred.threshold + self.rho) + # TODO: are the next two lines necessary? + self.model.addConstr(v - self.M * z <= pred.threshold) + self.model.addConstr(v + self.M * (1 - z) >= pred.threshold) elif pred.relation in (RelOperation.LE, RelOperation.LT): self.model.addConstr(expr + self.M * z >= pred.threshold - self.rho) self.model.addConstr(expr - self.M * (1 - z) <= pred.threshold - self.rho) From 8720ceb5f572ae8ad912a449e612369ad56186b2 Mon Sep 17 00:00:00 2001 From: erfanaasi Date: Fri, 10 Jan 2020 11:18:44 -0500 Subject: [PATCH 10/10] Fixed bug with var name. --- stl/stl2miqp.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/stl/stl2miqp.py b/stl/stl2miqp.py index c9a691c..91d8d62 100644 --- a/stl/stl2miqp.py +++ b/stl/stl2miqp.py @@ -24,8 +24,8 @@ def predicate(self, pred, z, t): self.model.addConstr(expr - self.M * z <= pred.threshold + self.rho) self.model.addConstr(expr + self.M * (1 - z) >= pred.threshold + self.rho) # TODO: are the next two lines necessary? - self.model.addConstr(v - self.M * z <= pred.threshold) - self.model.addConstr(v + self.M * (1 - z) >= pred.threshold) + self.model.addConstr(expr - self.M * z <= pred.threshold) + self.model.addConstr(expr + self.M * (1 - z) >= pred.threshold) elif pred.relation in (RelOperation.LE, RelOperation.LT): self.model.addConstr(expr + self.M * z >= pred.threshold - self.rho) self.model.addConstr(expr - self.M * (1 - z) <= pred.threshold - self.rho)