Feature/wstl support

stl/test/wstl_syntax_tests.py

@@ -0,0 +1,38 @@
+'''
+ Copyright (C) 2020 Cristian Ioan Vasile <cvasile@lehigh.edu>
+ Explainable Robotics Lab, Lehigh University
+ See license.txt file for license information.
+'''
+
+from StringIO import StringIO
+
+from antlr4 import InputStream, CommonTokenStream
+
+import sys
+sys.path.append('..')
+
+from wstlLexer import wstlLexer
+from wstlParser import wstlParser
+from wstlVisitor import wstlVisitor
+
+# Parse the WSTL formulae strings
+
+with open('wstl_syntax_tests.txt', 'rt') as fin:
+    text = StringIO()
+    for line in fin:
+        if line.strip():
+            text.write(line)
+        else:
+            input_string = text.getvalue()
+            print(input_string.strip())
+            lexer = wstlLexer(InputStream(input_string))
+            tokens = CommonTokenStream(lexer)
+            parser = wstlParser(tokens)
+            t = parser.wstlProperty()
+            if t.weight is None:
+                print(None)
+            else:
+                print(t.weight.text)
+
+            text.close()
+            text = StringIO()

stl/test/wstl_syntax_tests.txt

@@ -0,0 +1,49 @@
+<>[1, 3] (y <= 2)
+
+[][1, 3] (y <= 2)
+
+(y > 1) U[1, 3] (y <= 2)
+
+(y > 1) R[1, 3] (y <= 2)
+
+(y > 1) & (y <= 2)
+
+(y > 1) & (y <= 2) & (y > 3)
+
+(y > 1) | (y <= 2) | (y > 3)
+
+(y > 1) | (y <= 2)
+
+(y > 1) & (y <= 2) | (y > 3)
+
+& (y <= 2, y > 3, x < 0.2)
+
+| (y <= 2, y > 3, x < 0.2)
+
+<>[1, 3]^weight1 (y <= 2)
+
+[][1, 3]^weight1 (y <= 2)
+
+(y > 1) U[1, 3]^weight1 (y <= 2)
+
+(y > 1) R[1, 3]^weight1 (y <= 2)
+
+(y > 1) &^weight1 (y <= 2)
+
+(y > 1) &^weight1 (y <= 2) &^weight2 (y > 3)
+
+(y > 1) |^weight1 (y <= 2) |^weight2 (y > 3)
+
+(y > 1) |^weight1 (y <= 2)
+
+(y > 1) &^weight1 (y <= 2) |^weight2 (y > 3)
+
+&^weight1 (y <= 2, y > 3, x < 0.2)
+
+|^weight1 (y <= 2, y > 3, x < 0.2)
+
+&^weight (
+ [][1, 2]^w1 (x < 3),
+ <>[3, 5]^w2 (y > 2),
+ (z < 6) |^p3 (e = 2)
+)

stl/test/wstl_test.py

@@ -0,0 +1,78 @@
+from antlr4 import InputStream, CommonTokenStream
+
+import numpy as np
+
+import sys
+sys.path.append('..')
+
+from stl import Operation, RelOperation, STLFormula
+from wstlLexer import wstlLexer
+from wstlParser import wstlParser
+from wstlVisitor import wstlVisitor
+
+from wstl import WSTLAbstractSyntaxTreeExtractor
+
+from wstl2milp import wstl2milp
+
+from gurobipy import *
+
+
+# Create a new model
+m = Model("mip1")
+
+# Parse the WSTL formula string
+# lexer = wstlLexer(InputStream("<>[1, 3]^weight1 (y <= 2)"))
+# lexer = wstlLexer(InputStream("[][1, 3]^weight1 (y <= 2)"))
+# lexer = wstlLexer(InputStream("(y > 1) U[1, 3]^weight1 (y <= 2)"))
+# lexer = wstlLexer(InputStream("(y > 1) &^weight1 (y <= 2)"))
+# lexer = wstlLexer(InputStream("(y > 1) &^weight1 (y <= 2) &^weight2 (y > 3)"))
+# lexer = wstlLexer(InputStream("(y > 1) |^weight1 (y <= 2) |^weight2 (y > 3)"))
+# lexer = wstlLexer(InputStream("(y > 1) |^weight1 (y <= 2)"))
+# lexer = wstlLexer(InputStream("(y > 1) &^weight1 (y <= 2) |^weight2 (y > 3)"))
+# lexer = wstlLexer(InputStream("&&^weight1 (F[2, 5] (y <= 2), y > 3, x < 0.2)"))
+
+lexer = wstlLexer(InputStream("&&^weight1 (F[1, 4]^weight2 (x >= 2), x > 0.1)"))
+tokens = CommonTokenStream(lexer)
+parser = wstlParser(tokens)
+t = parser.wstlProperty()
+
+# Get AST from parse tree
+weights = {'weight1': lambda x: 0.5, 'weight2': lambda x: 0.25}
+ast = WSTLAbstractSyntaxTreeExtractor(weights).visit(t)
+
+# Translate WSTL to MILP and retrieve integer variable for the formula
+wstl_milp = wstl2milp(ast, model=m)
+z_formula, rho_formula = wstl_milp.translate()
+
+# Get/create state variables
+varname = 'x'
+end_time = 4
+x = [wstl_milp.variables[varname].get(time, m.addVar(lb= -GRB.INFINITY,
+                                                     ub= GRB.INFINITY))
+     for time in range(end_time + 1)]
+m.update()
+
+# Add dynamics constraints
+for time in range(end_time): # example of state transition (system dynamics)
+    m.addConstr(x[time+1] == x[time] - 0.1)
+
+for time in range(end_time + 1): # example if state constraints (e.g., safety)
+    m.addConstr(x[time] >= 0)
+
+# Set objective
+m.setObjective(rho_formula, GRB.MAXIMIZE)
+m.update()
+
+m.write('milp.mps')
+
+# Solve problem
+m.optimize()
+
+if (m.status == 2):
+    y = np.array([x[i].X for i in range(end_time+1)], dtype=np.float)
+else:
+    print("cannot solve...")
+    y = None
+
+# Print solution
+print(y)

stl/wstl.g4

@@ -0,0 +1,58 @@
+grammar wstl;
+
+@header {
+'''
+ Copyright (C) 2020 Cristian Ioan Vasile <cvasile@lehigh.edu>
+ Explainable Robotics Lab, Lehigh University
+ See license.txt file for license information.
+'''
+}
+
+
+wstlProperty:
+         '(' child=wstlProperty ')' #parprop
+    |    booleanExpr #booleanPred
+    |    op=NOT child=wstlProperty #formula
+    |    op=EVENT '[' low=RATIONAL ',' high=RATIONAL ']' ('^' weight=VARIABLE)?
+         child=wstlProperty #formula
+    |    op=ALWAYS '[' low=RATIONAL ',' high=RATIONAL ']' ('^' weight=VARIABLE)?
+         child=wstlProperty #formula
+    |    left=wstlProperty op=IMPLIES right=wstlProperty #formula
+    |    left=wstlProperty op=AND ('^' weight=VARIABLE)?
+         right=wstlProperty #formula
+    |    op=AND ('^' weight=VARIABLE)?
+         '(' wstlProperty (',' wstlProperty)+ ')' #longFormula
+    |    left=wstlProperty op=OR ('^' weight=VARIABLE)?
+         right=wstlProperty #formula
+    |    op=OR ('^' weight=VARIABLE)?
+         '(' wstlProperty (',' wstlProperty)+ ')' #longFormula
+    |    left=wstlProperty op=UNTIL '[' low=RATIONAL ',' high=RATIONAL ']'
+         ('^' weight=VARIABLE)? right=wstlProperty #formula
+    |    left=wstlProperty op=RELEASE '[' low=RATIONAL ',' high=RATIONAL ']'
+         ('^' weight=VARIABLE)? right=wstlProperty #formula
+    ;
+expr:
+        ( '-(' | '(' ) expr ')'
+    |   <assoc=right>   expr '^' expr
+    |   VARIABLE '(' expr ')'
+    |   expr ( '*' | '/' ) expr
+    |   expr ( '+' | '-' ) expr
+    |   RATIONAL
+    |   VARIABLE
+    ;
+booleanExpr:
+         left=expr op=( '<' | '<=' | '=' | '>=' | '>' ) right=expr
+    |    op=BOOLEAN
+    ;
+AND : '&' | '&&' | '/\\' ;
+OR : '|' | '||' | '\\/' ;
+IMPLIES : '=>' ;
+NOT : '!' | '~' ;
+EVENT : 'F' | '<>' ;
+ALWAYS : 'G' | '[]' ;
+UNTIL : 'U' ;
+RELEASE : 'R' ;
+BOOLEAN : 'true' | 'True' | 'false' | 'False' ;
+VARIABLE : ( [a-z] | [A-Z] )( [a-z] | [A-Z] | [0-9] | '_' )* ;
+RATIONAL : ('-')? [0-9]* ('.')? [0-9]+ ( 'E' | 'E-' )? [0-9]* ;
+WS : ( ' ' | '\t' | '\r' | '\n' )+ -> skip ;