diff --git a/stl/stl.py b/stl/stl.py index 3901a35..b6b8c5c 100644 --- a/stl/stl.py +++ b/stl/stl.py @@ -352,8 +352,8 @@ 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) && y > 2 && z<=8")) + # 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) parser = stlParser(tokens) diff --git a/stl/test/model_test.lp b/stl/test/model_test.lp new file mode 100644 index 0000000..6e95697 --- /dev/null +++ b/stl/test/model_test.lp @@ -0,0 +1,211 @@ +\ Model STL formula: ((G[0.0, 2.0] (x >= 3.0)) && (F[0.0, 6.0] (y >= 5.0)) && (G[0.0, 2.0] (z >= 1.0))) +\ LP format - for model browsing. Use MPS format to capture full model detail. +Minimize + - rho + 0 u_0 + 0 v_0 + 0 w_0 + 0 u_1 + 0 v_1 + 0 w_1 + 0 u_2 + 0 v_2 + + 0 w_2 + 0 u_3 + 0 v_3 + 0 w_3 + 0 u_4 + 0 v_4 + 0 w_4 + 0 u_5 + 0 v_5 + + 0 w_5 + 0 u_6 + 0 v_6 + 0 w_6 + 0 u_14 + 0 v_14 + 0 w_14 +Subject To + R0: x_0 = 4 + R1: y_0 = 1 + R2: z_0 = -1 + R3: x_1 = 1 + R4: y_1 = 2 + R5: z_1 = -1 + R6: x_2 = 3 + R7: y_2 = 5 + R8: z_2 = -1 + R9: x_3 = 0 + R10: y_3 = 3 + R11: z_3 = -4 + R12: x_4 = 2 + R13: y_4 = 1 + R14: z_4 = -1 + R15: x_5 = 2 + R16: y_5 = -1 + R17: z_5 = 2 + R18: x_6 = 1 + R19: y_6 = 1 + R20: z_6 = 1 + R21: x_7 = 0 + R22: y_7 = -1 + R23: z_7 = 2 + R24: - x_7 - u_7 + x_8 = 0 + R25: - y_7 - v_7 + y_8 = 0 + R26: - z_7 - w_7 + z_8 = 0 + R27: - x_8 - u_8 + x_9 = 0 + R28: - y_8 - v_8 + y_9 = 0 + R29: - z_8 - w_8 + z_9 = 0 + R30: - x_9 - u_9 + x_10 = 0 + R31: - y_9 - v_9 + y_10 = 0 + R32: - z_9 - w_9 + z_10 = 0 + R33: - x_10 - u_10 + x_11 = 0 + R34: - y_10 - v_10 + y_11 = 0 + R35: - z_10 - w_10 + z_11 = 0 + R36: - x_11 - u_11 + x_12 = 0 + R37: - y_11 - v_11 + y_12 = 0 + R38: - z_11 - w_11 + z_12 = 0 + R39: - x_12 - u_12 + x_13 = 0 + R40: - y_12 - v_12 + y_13 = 0 + R41: - z_12 - w_12 + z_13 = 0 + R42: - x_13 - u_13 + x_14 = 0 + R43: - y_13 - v_13 + y_14 = 0 + R44: - z_13 - w_13 + z_14 = 0 + R45: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 <= 3 + R46: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 >= -17 + R47: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 <= 3 + R48: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 >= -17 + R49: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 <= 3 + R50: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 >= -17 + R51: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_0 <= 0 + R52: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_1 <= 0 + R53: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_2 <= 0 + R54: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_0 + - predicate_2dx22dd95ed78b4d217_1 - predicate_2dx22dd95ed78b4d217_2 + >= -2 + R55: - rho + y_0 - 20 predicate_2bx2516753055d0b842_0 <= 5 + R56: - rho + y_0 - 20 predicate_2bx2516753055d0b842_0 >= -15 + R57: - rho + y_1 - 20 predicate_2bx2516753055d0b842_1 <= 5 + R58: - rho + y_1 - 20 predicate_2bx2516753055d0b842_1 >= -15 + R59: - rho + y_2 - 20 predicate_2bx2516753055d0b842_2 <= 5 + R60: - rho + y_2 - 20 predicate_2bx2516753055d0b842_2 >= -15 + R61: - rho + y_3 - 20 predicate_2bx2516753055d0b842_3 <= 5 + R62: - rho + y_3 - 20 predicate_2bx2516753055d0b842_3 >= -15 + R63: - rho + y_4 - 20 predicate_2bx2516753055d0b842_4 <= 5 + R64: - rho + y_4 - 20 predicate_2bx2516753055d0b842_4 >= -15 + R65: - rho + y_5 - 20 predicate_2bx2516753055d0b842_5 <= 5 + R66: - rho + y_5 - 20 predicate_2bx2516753055d0b842_5 >= -15 + R67: - rho + y_6 - 20 predicate_2bx2516753055d0b842_6 <= 5 + R68: - rho + y_6 - 20 predicate_2bx2516753055d0b842_6 >= -15 + R69: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_0 >= 0 + R70: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_1 >= 0 + R71: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_2 >= 0 + R72: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_3 >= 0 + R73: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_4 >= 0 + R74: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_5 >= 0 + R75: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_6 >= 0 + R76: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_0 + - predicate_2bx2516753055d0b842_1 - predicate_2bx2516753055d0b842_2 + - predicate_2bx2516753055d0b842_3 - predicate_2bx2516753055d0b842_4 + - predicate_2bx2516753055d0b842_5 - predicate_2bx2516753055d0b842_6 + <= 0 + R77: - rho + z_0 - 20 predicate_2dx33b18e258c171243_0 <= 1 + R78: - rho + z_0 - 20 predicate_2dx33b18e258c171243_0 >= -19 + R79: - rho + z_1 - 20 predicate_2dx33b18e258c171243_1 <= 1 + R80: - rho + z_1 - 20 predicate_2dx33b18e258c171243_1 >= -19 + R81: - rho + z_2 - 20 predicate_2dx33b18e258c171243_2 <= 1 + R82: - rho + z_2 - 20 predicate_2dx33b18e258c171243_2 >= -19 + R83: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_0 <= 0 + R84: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_1 <= 0 + R85: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_2 <= 0 + R86: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_0 + - predicate_2dx33b18e258c171243_1 - predicate_2dx33b18e258c171243_2 + >= -2 + R87: and_2dx5295e3d99f627fa8_0 - always_2dx69bcdd71a3ff42e3_0 <= 0 + R88: and_2dx5295e3d99f627fa8_0 - event_2dx53fa3e0ebe26c54b_0 <= 0 + R89: and_2dx5295e3d99f627fa8_0 - always_2dx7c33fe6ba9ff9e2b_0 <= 0 + R90: and_2dx5295e3d99f627fa8_0 - always_2dx69bcdd71a3ff42e3_0 + - event_2dx53fa3e0ebe26c54b_0 - always_2dx7c33fe6ba9ff9e2b_0 >= -2 + formula_satisfaction: and_2dx5295e3d99f627fa8_0 = 1 +Bounds + -infinity <= rho <= 999 + -4 <= x_0 <= 5 + -4 <= y_0 <= 5 + -4 <= z_0 <= 5 + -3 <= u_0 <= 2 + -2 <= v_0 <= 3 + -3 <= w_0 <= 3 + -4 <= x_1 <= 5 + -4 <= y_1 <= 5 + -4 <= z_1 <= 5 + -3 <= u_1 <= 2 + -2 <= v_1 <= 3 + -3 <= w_1 <= 3 + -4 <= x_2 <= 5 + -4 <= y_2 <= 5 + -4 <= z_2 <= 5 + -3 <= u_2 <= 2 + -2 <= v_2 <= 3 + -3 <= w_2 <= 3 + -4 <= x_3 <= 5 + -4 <= y_3 <= 5 + -4 <= z_3 <= 5 + -3 <= u_3 <= 2 + -2 <= v_3 <= 3 + -3 <= w_3 <= 3 + -4 <= x_4 <= 5 + -4 <= y_4 <= 5 + -4 <= z_4 <= 5 + -3 <= u_4 <= 2 + -2 <= v_4 <= 3 + -3 <= w_4 <= 3 + -4 <= x_5 <= 5 + -4 <= y_5 <= 5 + -4 <= z_5 <= 5 + -3 <= u_5 <= 2 + -2 <= v_5 <= 3 + -3 <= w_5 <= 3 + -4 <= x_6 <= 5 + -4 <= y_6 <= 5 + -4 <= z_6 <= 5 + -3 <= u_6 <= 2 + -2 <= v_6 <= 3 + -3 <= w_6 <= 3 + -4 <= x_7 <= 5 + -4 <= y_7 <= 5 + -4 <= z_7 <= 5 + -3 <= u_7 <= 2 + -2 <= v_7 <= 3 + -3 <= w_7 <= 3 + -4 <= x_8 <= 5 + -4 <= y_8 <= 5 + -4 <= z_8 <= 5 + -3 <= u_8 <= 2 + -2 <= v_8 <= 3 + -3 <= w_8 <= 3 + -4 <= x_9 <= 5 + -4 <= y_9 <= 5 + -4 <= z_9 <= 5 + -3 <= u_9 <= 2 + -2 <= v_9 <= 3 + -3 <= w_9 <= 3 + -4 <= x_10 <= 5 + -4 <= y_10 <= 5 + -4 <= z_10 <= 5 + -3 <= u_10 <= 2 + -2 <= v_10 <= 3 + -3 <= w_10 <= 3 + -4 <= x_11 <= 5 + -4 <= y_11 <= 5 + -4 <= z_11 <= 5 + -3 <= u_11 <= 2 + -2 <= v_11 <= 3 + -3 <= w_11 <= 3 + -4 <= x_12 <= 5 + -4 <= y_12 <= 5 + -4 <= z_12 <= 5 + -3 <= u_12 <= 2 + -2 <= v_12 <= 3 + -3 <= w_12 <= 3 + -4 <= x_13 <= 5 + -4 <= y_13 <= 5 + -4 <= z_13 <= 5 + -3 <= u_13 <= 2 + -2 <= v_13 <= 3 + -3 <= w_13 <= 3 + -4 <= x_14 <= 5 + -4 <= y_14 <= 5 + -4 <= z_14 <= 5 + -3 <= u_14 <= 2 + -2 <= v_14 <= 3 + -3 <= w_14 <= 3 +Binaries + and_2dx5295e3d99f627fa8_0 always_2dx69bcdd71a3ff42e3_0 + predicate_2dx22dd95ed78b4d217_0 predicate_2dx22dd95ed78b4d217_1 + predicate_2dx22dd95ed78b4d217_2 event_2dx53fa3e0ebe26c54b_0 + predicate_2bx2516753055d0b842_0 predicate_2bx2516753055d0b842_1 + predicate_2bx2516753055d0b842_2 predicate_2bx2516753055d0b842_3 + predicate_2bx2516753055d0b842_4 predicate_2bx2516753055d0b842_5 + predicate_2bx2516753055d0b842_6 always_2dx7c33fe6ba9ff9e2b_0 + predicate_2dx33b18e258c171243_0 predicate_2dx33b18e258c171243_1 + predicate_2dx33b18e258c171243_2 +End diff --git a/stl/test/stl2milp.lp b/stl/test/stl2milp.lp new file mode 100644 index 0000000..0dd312a --- /dev/null +++ b/stl/test/stl2milp.lp @@ -0,0 +1,344 @@ +\ Model STL formula: ((G[0.0, 2.0] (x >= 3.0)) && (F[0.0, 6.0] (y >= 5.0)) && (G[0.0, 2.0] (z >= 1.0))) +\ LP format - for model browsing. Use MPS format to capture full model detail. +Minimize + - rho + 0 u_29 + 0 v_29 + 0 w_29 +Subject To + R0: - x_0 - u_0 + x_1 = 0 + R1: - y_0 - v_0 + y_1 = 0 + R2: - z_0 - w_0 + z_1 = 0 + R3: - x_1 - u_1 + x_2 = 0 + R4: - y_1 - v_1 + y_2 = 0 + R5: - z_1 - w_1 + z_2 = 0 + R6: - x_2 - u_2 + x_3 = 0 + R7: - y_2 - v_2 + y_3 = 0 + R8: - z_2 - w_2 + z_3 = 0 + R9: - x_3 - u_3 + x_4 = 0 + R10: - y_3 - v_3 + y_4 = 0 + R11: - z_3 - w_3 + z_4 = 0 + R12: - x_4 - u_4 + x_5 = 0 + R13: - y_4 - v_4 + y_5 = 0 + R14: - z_4 - w_4 + z_5 = 0 + R15: - x_5 - u_5 + x_6 = 0 + R16: - y_5 - v_5 + y_6 = 0 + R17: - z_5 - w_5 + z_6 = 0 + R18: - x_6 - u_6 + x_7 = 0 + R19: - y_6 - v_6 + y_7 = 0 + R20: - z_6 - w_6 + z_7 = 0 + R21: - x_7 - u_7 + x_8 = 0 + R22: - y_7 - v_7 + y_8 = 0 + R23: - z_7 - w_7 + z_8 = 0 + R24: - x_8 - u_8 + x_9 = 0 + R25: - y_8 - v_8 + y_9 = 0 + R26: - z_8 - w_8 + z_9 = 0 + R27: - x_9 - u_9 + x_10 = 0 + R28: - y_9 - v_9 + y_10 = 0 + R29: - z_9 - w_9 + z_10 = 0 + R30: - x_10 - u_10 + x_11 = 0 + R31: - y_10 - v_10 + y_11 = 0 + R32: - z_10 - w_10 + z_11 = 0 + R33: - x_11 - u_11 + x_12 = 0 + R34: - y_11 - v_11 + y_12 = 0 + R35: - z_11 - w_11 + z_12 = 0 + R36: - x_12 - u_12 + x_13 = 0 + R37: - y_12 - v_12 + y_13 = 0 + R38: - z_12 - w_12 + z_13 = 0 + R39: - x_13 - u_13 + x_14 = 0 + R40: - y_13 - v_13 + y_14 = 0 + R41: - z_13 - w_13 + z_14 = 0 + R42: - x_14 - u_14 + x_15 = 0 + R43: - y_14 - v_14 + y_15 = 0 + R44: - z_14 - w_14 + z_15 = 0 + R45: - x_15 - u_15 + x_16 = 0 + R46: - y_15 - v_15 + y_16 = 0 + R47: - z_15 - w_15 + z_16 = 0 + R48: - x_16 - u_16 + x_17 = 0 + R49: - y_16 - v_16 + y_17 = 0 + R50: - z_16 - w_16 + z_17 = 0 + R51: - x_17 - u_17 + x_18 = 0 + R52: - y_17 - v_17 + y_18 = 0 + R53: - z_17 - w_17 + z_18 = 0 + R54: - x_18 - u_18 + x_19 = 0 + R55: - y_18 - v_18 + y_19 = 0 + R56: - z_18 - w_18 + z_19 = 0 + R57: - x_19 - u_19 + x_20 = 0 + R58: - y_19 - v_19 + y_20 = 0 + R59: - z_19 - w_19 + z_20 = 0 + R60: - x_20 - u_20 + x_21 = 0 + R61: - y_20 - v_20 + y_21 = 0 + R62: - z_20 - w_20 + z_21 = 0 + R63: - x_21 - u_21 + x_22 = 0 + R64: - y_21 - v_21 + y_22 = 0 + R65: - z_21 - w_21 + z_22 = 0 + R66: - x_22 - u_22 + x_23 = 0 + R67: - y_22 - v_22 + y_23 = 0 + R68: - z_22 - w_22 + z_23 = 0 + R69: - x_23 - u_23 + x_24 = 0 + R70: - y_23 - v_23 + y_24 = 0 + R71: - z_23 - w_23 + z_24 = 0 + R72: - x_24 - u_24 + x_25 = 0 + R73: - y_24 - v_24 + y_25 = 0 + R74: - z_24 - w_24 + z_25 = 0 + R75: - x_25 - u_25 + x_26 = 0 + R76: - y_25 - v_25 + y_26 = 0 + R77: - z_25 - w_25 + z_26 = 0 + R78: - x_26 - u_26 + x_27 = 0 + R79: - y_26 - v_26 + y_27 = 0 + R80: - z_26 - w_26 + z_27 = 0 + R81: - x_27 - u_27 + x_28 = 0 + R82: - y_27 - v_27 + y_28 = 0 + R83: - z_27 - w_27 + z_28 = 0 + R84: - x_28 - u_28 + x_29 = 0 + R85: - y_28 - v_28 + y_29 = 0 + R86: - z_28 - w_28 + z_29 = 0 + R87: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 <= 3 + R88: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 >= -17 + R89: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 <= 3 + R90: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 >= -17 + R91: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 <= 3 + R92: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 >= -17 + R93: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_0 <= 0 + R94: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_1 <= 0 + R95: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_2 <= 0 + R96: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_0 + - predicate_2dx22dd95ed78b4d217_1 - predicate_2dx22dd95ed78b4d217_2 + >= -2 + R97: - rho + y_0 - 20 predicate_2bx2516753055d0b842_0 <= 5 + R98: - rho + y_0 - 20 predicate_2bx2516753055d0b842_0 >= -15 + R99: - rho + y_1 - 20 predicate_2bx2516753055d0b842_1 <= 5 + R100: - rho + y_1 - 20 predicate_2bx2516753055d0b842_1 >= -15 + R101: - rho + y_2 - 20 predicate_2bx2516753055d0b842_2 <= 5 + R102: - rho + y_2 - 20 predicate_2bx2516753055d0b842_2 >= -15 + R103: - rho + y_3 - 20 predicate_2bx2516753055d0b842_3 <= 5 + R104: - rho + y_3 - 20 predicate_2bx2516753055d0b842_3 >= -15 + R105: - rho + y_4 - 20 predicate_2bx2516753055d0b842_4 <= 5 + R106: - rho + y_4 - 20 predicate_2bx2516753055d0b842_4 >= -15 + R107: - rho + y_5 - 20 predicate_2bx2516753055d0b842_5 <= 5 + R108: - rho + y_5 - 20 predicate_2bx2516753055d0b842_5 >= -15 + R109: - rho + y_6 - 20 predicate_2bx2516753055d0b842_6 <= 5 + R110: - rho + y_6 - 20 predicate_2bx2516753055d0b842_6 >= -15 + R111: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_0 >= 0 + R112: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_1 >= 0 + R113: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_2 >= 0 + R114: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_3 >= 0 + R115: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_4 >= 0 + R116: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_5 >= 0 + R117: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_6 >= 0 + R118: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_0 + - predicate_2bx2516753055d0b842_1 - predicate_2bx2516753055d0b842_2 + - predicate_2bx2516753055d0b842_3 - predicate_2bx2516753055d0b842_4 + - predicate_2bx2516753055d0b842_5 - predicate_2bx2516753055d0b842_6 + <= 0 + R119: - rho + z_0 - 20 predicate_2dx33b18e258c171243_0 <= 1 + R120: - rho + z_0 - 20 predicate_2dx33b18e258c171243_0 >= -19 + R121: - rho + z_1 - 20 predicate_2dx33b18e258c171243_1 <= 1 + R122: - rho + z_1 - 20 predicate_2dx33b18e258c171243_1 >= -19 + R123: - rho + z_2 - 20 predicate_2dx33b18e258c171243_2 <= 1 + R124: - rho + z_2 - 20 predicate_2dx33b18e258c171243_2 >= -19 + R125: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_0 <= 0 + R126: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_1 <= 0 + R127: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_2 <= 0 + R128: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_0 + - predicate_2dx33b18e258c171243_1 - predicate_2dx33b18e258c171243_2 + >= -2 + R129: and_2dx5295e3d99f627fa8_0 - always_2dx69bcdd71a3ff42e3_0 <= 0 + R130: and_2dx5295e3d99f627fa8_0 - event_2dx53fa3e0ebe26c54b_0 <= 0 + R131: and_2dx5295e3d99f627fa8_0 - always_2dx7c33fe6ba9ff9e2b_0 <= 0 + R132: and_2dx5295e3d99f627fa8_0 - always_2dx69bcdd71a3ff42e3_0 + - event_2dx53fa3e0ebe26c54b_0 - always_2dx7c33fe6ba9ff9e2b_0 >= -2 + formula_satisfaction: and_2dx5295e3d99f627fa8_0 = 1 + R134: x_0 = 3 + R135: y_0 = 4 + R136: z_0 = 2 +Bounds + -infinity <= rho <= 999 + -4 <= x_0 <= 5 + -4 <= y_0 <= 5 + -4 <= z_0 <= 5 + -3 <= u_0 <= 2 + -2 <= v_0 <= 3 + -3 <= w_0 <= 3 + -4 <= x_1 <= 5 + -4 <= y_1 <= 5 + -4 <= z_1 <= 5 + -3 <= u_1 <= 2 + -2 <= v_1 <= 3 + -3 <= w_1 <= 3 + -4 <= x_2 <= 5 + -4 <= y_2 <= 5 + -4 <= z_2 <= 5 + -3 <= u_2 <= 2 + -2 <= v_2 <= 3 + -3 <= w_2 <= 3 + -4 <= x_3 <= 5 + -4 <= y_3 <= 5 + -4 <= z_3 <= 5 + -3 <= u_3 <= 2 + -2 <= v_3 <= 3 + -3 <= w_3 <= 3 + -4 <= x_4 <= 5 + -4 <= y_4 <= 5 + -4 <= z_4 <= 5 + -3 <= u_4 <= 2 + -2 <= v_4 <= 3 + -3 <= w_4 <= 3 + -4 <= x_5 <= 5 + -4 <= y_5 <= 5 + -4 <= z_5 <= 5 + -3 <= u_5 <= 2 + -2 <= v_5 <= 3 + -3 <= w_5 <= 3 + -4 <= x_6 <= 5 + -4 <= y_6 <= 5 + -4 <= z_6 <= 5 + -3 <= u_6 <= 2 + -2 <= v_6 <= 3 + -3 <= w_6 <= 3 + -4 <= x_7 <= 5 + -4 <= y_7 <= 5 + -4 <= z_7 <= 5 + -3 <= u_7 <= 2 + -2 <= v_7 <= 3 + -3 <= w_7 <= 3 + -4 <= x_8 <= 5 + -4 <= y_8 <= 5 + -4 <= z_8 <= 5 + -3 <= u_8 <= 2 + -2 <= v_8 <= 3 + -3 <= w_8 <= 3 + -4 <= x_9 <= 5 + -4 <= y_9 <= 5 + -4 <= z_9 <= 5 + -3 <= u_9 <= 2 + -2 <= v_9 <= 3 + -3 <= w_9 <= 3 + -4 <= x_10 <= 5 + -4 <= y_10 <= 5 + -4 <= z_10 <= 5 + -3 <= u_10 <= 2 + -2 <= v_10 <= 3 + -3 <= w_10 <= 3 + -4 <= x_11 <= 5 + -4 <= y_11 <= 5 + -4 <= z_11 <= 5 + -3 <= u_11 <= 2 + -2 <= v_11 <= 3 + -3 <= w_11 <= 3 + -4 <= x_12 <= 5 + -4 <= y_12 <= 5 + -4 <= z_12 <= 5 + -3 <= u_12 <= 2 + -2 <= v_12 <= 3 + -3 <= w_12 <= 3 + -4 <= x_13 <= 5 + -4 <= y_13 <= 5 + -4 <= z_13 <= 5 + -3 <= u_13 <= 2 + -2 <= v_13 <= 3 + -3 <= w_13 <= 3 + -4 <= x_14 <= 5 + -4 <= y_14 <= 5 + -4 <= z_14 <= 5 + -3 <= u_14 <= 2 + -2 <= v_14 <= 3 + -3 <= w_14 <= 3 + -4 <= x_15 <= 5 + -4 <= y_15 <= 5 + -4 <= z_15 <= 5 + -3 <= u_15 <= 2 + -2 <= v_15 <= 3 + -3 <= w_15 <= 3 + -4 <= x_16 <= 5 + -4 <= y_16 <= 5 + -4 <= z_16 <= 5 + -3 <= u_16 <= 2 + -2 <= v_16 <= 3 + -3 <= w_16 <= 3 + -4 <= x_17 <= 5 + -4 <= y_17 <= 5 + -4 <= z_17 <= 5 + -3 <= u_17 <= 2 + -2 <= v_17 <= 3 + -3 <= w_17 <= 3 + -4 <= x_18 <= 5 + -4 <= y_18 <= 5 + -4 <= z_18 <= 5 + -3 <= u_18 <= 2 + -2 <= v_18 <= 3 + -3 <= w_18 <= 3 + -4 <= x_19 <= 5 + -4 <= y_19 <= 5 + -4 <= z_19 <= 5 + -3 <= u_19 <= 2 + -2 <= v_19 <= 3 + -3 <= w_19 <= 3 + -4 <= x_20 <= 5 + -4 <= y_20 <= 5 + -4 <= z_20 <= 5 + -3 <= u_20 <= 2 + -2 <= v_20 <= 3 + -3 <= w_20 <= 3 + -4 <= x_21 <= 5 + -4 <= y_21 <= 5 + -4 <= z_21 <= 5 + -3 <= u_21 <= 2 + -2 <= v_21 <= 3 + -3 <= w_21 <= 3 + -4 <= x_22 <= 5 + -4 <= y_22 <= 5 + -4 <= z_22 <= 5 + -3 <= u_22 <= 2 + -2 <= v_22 <= 3 + -3 <= w_22 <= 3 + -4 <= x_23 <= 5 + -4 <= y_23 <= 5 + -4 <= z_23 <= 5 + -3 <= u_23 <= 2 + -2 <= v_23 <= 3 + -3 <= w_23 <= 3 + -4 <= x_24 <= 5 + -4 <= y_24 <= 5 + -4 <= z_24 <= 5 + -3 <= u_24 <= 2 + -2 <= v_24 <= 3 + -3 <= w_24 <= 3 + -4 <= x_25 <= 5 + -4 <= y_25 <= 5 + -4 <= z_25 <= 5 + -3 <= u_25 <= 2 + -2 <= v_25 <= 3 + -3 <= w_25 <= 3 + -4 <= x_26 <= 5 + -4 <= y_26 <= 5 + -4 <= z_26 <= 5 + -3 <= u_26 <= 2 + -2 <= v_26 <= 3 + -3 <= w_26 <= 3 + -4 <= x_27 <= 5 + -4 <= y_27 <= 5 + -4 <= z_27 <= 5 + -3 <= u_27 <= 2 + -2 <= v_27 <= 3 + -3 <= w_27 <= 3 + -4 <= x_28 <= 5 + -4 <= y_28 <= 5 + -4 <= z_28 <= 5 + -3 <= u_28 <= 2 + -2 <= v_28 <= 3 + -3 <= w_28 <= 3 + -4 <= x_29 <= 5 + -4 <= y_29 <= 5 + -4 <= z_29 <= 5 + -3 <= u_29 <= 2 + -2 <= v_29 <= 3 + -3 <= w_29 <= 3 +Binaries + and_2dx5295e3d99f627fa8_0 always_2dx69bcdd71a3ff42e3_0 + predicate_2dx22dd95ed78b4d217_0 predicate_2dx22dd95ed78b4d217_1 + predicate_2dx22dd95ed78b4d217_2 event_2dx53fa3e0ebe26c54b_0 + predicate_2bx2516753055d0b842_0 predicate_2bx2516753055d0b842_1 + predicate_2bx2516753055d0b842_2 predicate_2bx2516753055d0b842_3 + predicate_2bx2516753055d0b842_4 predicate_2bx2516753055d0b842_5 + predicate_2bx2516753055d0b842_6 always_2dx7c33fe6ba9ff9e2b_0 + predicate_2dx33b18e258c171243_0 predicate_2dx33b18e258c171243_1 + predicate_2dx33b18e258c171243_2 +End diff --git a/stl/test/stl2milp_test.py b/stl/test/stl2milp_test.py index 83e574b..7ed432d 100644 --- a/stl/test/stl2milp_test.py +++ b/stl/test/stl2milp_test.py @@ -13,6 +13,10 @@ import sys sys.path.append('..') +import gurobipy as grb + +import matplotlib.pyplot as plt + from stl import Operation, RelOperation, STLFormula from stlLexer import stlLexer from stlParser import stlParser @@ -25,8 +29,14 @@ # formula = "(x > 10) && F[0, 2] y > 2 || G[1, 6] z > 8" # formula = "G[2,4] F[1,3](x>=3)" # formula = "(x <= 10) && F[0, 2] y > 2 && G[1, 6] (z < 8) && G[1,6] (z > 3)" -formula = 'G[0,1] x >= 3' +# Define the formula that you want to apply +# formula = 'G[0,10] x >= 3 && G[2,4] F[20,24] (y >= 2) && G[21, 26] (z <= 4) && G[21,26] (z >= 3)' +# formula = 'G[0,6] x >= 3 && G[0,6] (y >= 2) && G[0, 6] (z >= 1)' +formula = 'G[0,2] x >= 3 && F[0,6] (y >= 5) && G[0, 2] (z >= 1)' + + +# Stl2milp Initialization lexer = stlLexer(InputStream(formula)) tokens = CommonTokenStream(lexer) parser = stlParser(tokens) @@ -36,10 +46,76 @@ print('AST:', str(ast)) -stl_milp = stl2milp(ast, ranges={'x': [-4, 5]}, robust=True) +stl_milp = stl2milp(ast, ranges={'x': [-4, 5], 'y': [-4, 5], 'z': [-4, 5]}, robust=True) +stl_milp.M = 20 + +# Define the matrixes that used for linear system +# M = [[1, 2, 3], [4, 5, 6],[7, 8, 9]] +# B = [[7, 8, 9], [4, 5, 6],[1, 2, 3]] +M = [[1, 0, 0], [0, 1, 0],[0, 0, 1]] +B = [[1, 0, 0], [0, 1, 0],[0, 0, 1]] + +# system variables and the time period +period = 30 +x = dict() +y = dict() +z = dict() +u = dict() +v = dict() +w = dict() + +for k in range(period): + name = "x_{}".format(k) + x[k] = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=-4, ub=5, name=name) + name = "y_{}".format(k) + y[k] = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=-4, ub=5, name=name) + name = "z_{}".format(k) + z[k] = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=-4, ub=5, name=name) + name = "u_{}".format(k) + u[k] = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=-3, ub=2, name=name) + name = "v_{}".format(k) + v[k] = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=-2, ub=3, name=name) + name = "w_{}".format(k) + w[k] = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=-3, ub=3, name=name) + +# use system variables in STL spec encoding +stl_milp.variables['x'] = x +stl_milp.variables['y'] = y +stl_milp.variables['z'] = z +stl_milp.variables['u'] = u +stl_milp.variables['v'] = v +stl_milp.variables['w'] = w + + +# system constraints +for k in range(period-1): + stl_milp.model.addConstr(x[k+1] == M[0][0] * x[k] + M[0][1] * y[k] + M[0][2] * z[k] + \ + B[0][0] * u[k] + B[0][1] * v[k] + B[0][2] * w[k]) + stl_milp.model.addConstr(y[k+1] == M[1][0] * x[k] + M[1][1] * y[k] + M[1][2] * z[k] + \ + B[1][0] * u[k] + B[1][1] * v[k] + B[1][2] * w[k]) + stl_milp.model.addConstr(z[k+1] == M[2][0] * x[k] + M[2][1] * y[k] + M[2][2] * z[k] + \ + B[2][0] * u[k] + B[2][1] * v[k] + B[2][2] * w[k]) + +# add the specification (STL) constraints stl_milp.translate(satisfaction=True) + +# x = stl_milp.variables['x'] +# n = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=1, ub=2, name="n") +# stl_milp.model.addConstr(x[1] == x[0] + n) +stl_milp.variables['x'] = x +stl_milp.variables['y'] = y +stl_milp.variables['z'] = z + + + +stl_milp.model.addConstr(x[0] == 3) +stl_milp.model.addConstr(y[0] == 4) +stl_milp.model.addConstr(z[0] == 2) + +# Solve the problem with gurobi stl_milp.model.optimize() +# Print the solutions of the variables print('Vars') for var in stl_milp.model.getVars(): print(var.VarName, ':', var.x) @@ -53,3 +129,31 @@ print(str(obj), ':', obj.getValue()) stl_milp.model.write('stl2milp.lp') + +# Plot the variables with time changes +t = stl_milp.variables['y'].keys() + +x_vals = [var.x for var in stl_milp.variables['x'].values()] +y_vals = [var.x for var in stl_milp.variables['y'].values()] +z_vals = [var.x for var in stl_milp.variables['z'].values()] +u_vals = [var.x for var in stl_milp.variables['u'].values()] +v_vals = [var.x for var in stl_milp.variables['v'].values()] +w_vals = [var.x for var in stl_milp.variables['w'].values()] + +fig, axs = plt.subplots(3, 2) +fig.suptitle('subplots') +axs[0][0].plot(t, x_vals) +axs[0][0].set_title('x vs t') +axs[1][0].plot(t, y_vals) +axs[1][0].set_title('y vs t') +axs[2][0].plot(t, z_vals) +axs[2][0].set_title('z vs t') +axs[0][1].plot(t, u_vals) +axs[0][1].set_title('u vs t') +axs[1][1].plot(t, v_vals) +axs[1][1].set_title('v vs t') +axs[2][1].plot(t, w_vals) +axs[2][1].set_title('w vs t') +fig.tight_layout() +plt.show() + diff --git a/stl/test/stl_mpc.py b/stl/test/stl_mpc.py new file mode 100644 index 0000000..3e84fc3 --- /dev/null +++ b/stl/test/stl_mpc.py @@ -0,0 +1,199 @@ +#!/usr/bin/env python3 + +""" + 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. + + @author: Weizhou Zhou, Cristian-Ioan Vasile +""" +from antlr4 import InputStream, CommonTokenStream + +import sys +sys.path.append('..') + +import gurobipy as grb + +import matplotlib.pyplot as plt + +from stl import Operation, RelOperation, STLFormula +from stlLexer import stlLexer +from stlParser import stlParser +from stlVisitor import stlVisitor + +from stl import STLAbstractSyntaxTreeExtractor + +from stl2milp import stl2milp + +# formula = "(x > 10) && F[0, 2] y > 2 || G[1, 6] z > 8" +# formula = "G[2,4] F[1,3](x>=3)" +# formula = "(x <= 10) && F[0, 2] y > 2 && G[1, 6] (z < 8) && G[1,6] (z > 3)" + +# Define the formula that you want to apply +# formula = 'G[0,10] x >= 3 && G[2,4] F[20,24] (y > 2) && G[21, 26] (z < 8) && G[21,26] (z > 3)' +formula = 'G[0,2] x >= 3 && F[0,6] (y >= 5) && G[0, 2] (z >= 1)' +# formula = 'G[0,10] x >= 3 && G[12,15] x <= 1 && G[17, 24] x>= 4' + +# Define the matrixes that used for linear system +# M = [[1, 2, 3], [4, 5, 6],[7, 8, 9]] +# B = [[7, 8, 9], [4, 5, 6],[1, 2, 3]] +M = [[1, 0, 0], [0, 1, 0],[0, 0, 1]] +B = [[1, 0, 0], [0, 1, 0],[0, 0, 1]] + + +# Stl2milp Initialization +lexer = stlLexer(InputStream(formula)) +tokens = CommonTokenStream(lexer) +parser = stlParser(tokens) +t = parser.stlProperty() +print(t.toStringTree()) +ast = STLAbstractSyntaxTreeExtractor().visit(t) + +print('AST:', str(ast)) + +def stl_milp_solver(x_init, y_init, z_init, current_step, period, event): +# x_init, y_init, z_init = 2, 2, -3 + # Define the general range for x y z + stl_milp = stl2milp(ast, ranges={'x': [-4, 5], 'y': [-4, 5], 'z': [-4, 5]}, robust=True) + stl_milp.M = 20 + + # Define the matrixes that used for linear system + # M = [[1, 2, 3], [4, 5, 6],[7, 8, 9]] + # B = [[7, 8, 9], [4, 5, 6],[1, 2, 3]] + + # system variables and the time period + # period = 26 + x = dict() + y = dict() + z = dict() + u = dict() + v = dict() + w = dict() + + if current_step < period - 1: + backward_steps = current_step + else: + backward_steps = period - 1 + + for k in range(period + backward_steps): + name = "x_{}".format(k) + x[k] = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=-4, ub=5, name=name) + name = "y_{}".format(k) + y[k] = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=-4, ub=5, name=name) + name = "z_{}".format(k) + z[k] = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=-4, ub=5, name=name) + name = "u_{}".format(k) + u[k] = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=-3, ub=2, name=name) + name = "v_{}".format(k) + v[k] = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=-2, ub=3, name=name) + name = "w_{}".format(k) + w[k] = stl_milp.model.addVar(vtype=grb.GRB.CONTINUOUS, lb=-3, ub=3, name=name) + + # use system variables in STL spec encoding + stl_milp.variables['x'] = x + stl_milp.variables['y'] = y + stl_milp.variables['z'] = z + stl_milp.variables['u'] = u + stl_milp.variables['v'] = v + stl_milp.variables['w'] = w + + # define the inital states for each mpc step + for i in range(backward_steps + 1): + stl_milp.model.addConstr(x[i] == x_init[current_step - backward_steps + i]) + stl_milp.model.addConstr(y[i] == y_init[current_step - backward_steps + i]) + stl_milp.model.addConstr(z[i] == z_init[current_step - backward_steps + i]) + + # system constraints + for k in range(backward_steps, period + backward_steps - 1): + stl_milp.model.addConstr(x[k+1] == M[0][0] * x[k] + M[0][1] * y[k] + M[0][2] * z[k] + \ + B[0][0] * u[k] + B[0][1] * v[k] + B[0][2] * w[k]) + stl_milp.model.addConstr(y[k+1] == M[1][0] * x[k] + M[1][1] * y[k] + M[1][2] * z[k] + \ + B[1][0] * u[k] + B[1][1] * v[k] + B[1][2] * w[k]) + stl_milp.model.addConstr(z[k+1] == M[2][0] * x[k] + M[2][1] * y[k] + M[2][2] * z[k] + \ + B[2][0] * u[k] + B[2][1] * v[k] + B[2][2] * w[k]) + + + # add the specification (STL) constraints + stl_milp.translate(satisfaction=True) + + # Add event constraints + + if current_step == event - 1: + + stl_milp.model.addConstr(x[backward_steps + 1] >= 1) + stl_milp.model.addConstr(y[backward_steps + 1] >= 1) + stl_milp.model.addConstr(z[backward_steps + 1] >= 1) + + # Solve the problem with gurobi + stl_milp.model.optimize() + stl_milp.model.write('model_test.lp') + + + x_vals = [var.x for var in stl_milp.variables['x'].values()] + y_vals = [var.x for var in stl_milp.variables['y'].values()] + z_vals = [var.x for var in stl_milp.variables['z'].values()] + + # Plot the variables with time changes + # t = stl_milp.variables['y'].keys() + + # x_vals = [var.x for var in stl_milp.variables['x'].values()] + # y_vals = [var.x for var in stl_milp.variables['y'].values()] + # z_vals = [var.x for var in stl_milp.variables['z'].values()] + # u_vals = [var.x for var in stl_milp.variables['u'].values()] + # v_vals = [var.x for var in stl_milp.variables['v'].values()] + # w_vals = [var.x for var in stl_milp.variables['w'].values()] + + # fig, axs = plt.subplots(3, 2) + # fig.suptitle('subplots') + # axs[0][0].plot(t, x_vals) + # axs[0][0].set_title('x vs t') + # axs[1][0].plot(t, y_vals) + # axs[1][0].set_title('y vs t') + # axs[2][0].plot(t, z_vals) + # axs[2][0].set_title('z vs t') + # axs[0][1].plot(t, u_vals) + # axs[0][1].set_title('u vs t') + # axs[1][1].plot(t, v_vals) + # axs[1][1].set_title('v vs t') + # axs[2][1].plot(t, w_vals) + # axs[2][1].set_title('w vs t') + # fig.tight_layout() + # plt.show() + + # return x_vals[1], y_vals[1], z_vals[1] + x_init[current_step + 1] = x_vals[backward_steps + 1] + y_init[current_step + 1] = y_vals[backward_steps + 1] + z_init[current_step + 1] = z_vals[backward_steps + 1] + # print( x_init[current_step + 1], x_init[current_step + 1], x_init[current_step + 1]) + +#print(stl_milp_solver(2, 2, -3)) + +def main(): + # Based on the formula, you need to define the period and the steps for it. + # Normally, period should bigger than the formula range and steps should be bigger than period + steps = 12 + period = 8 + event = 10 + x_init, y_init, z_init = 3, 4, 2 + x = [0 if i != 0 else x_init for i in range(steps + period)] + y = [0 if i != 0 else y_init for i in range(steps + period)] + z = [0 if i != 0 else z_init for i in range(steps + period)] + t = [i for i in range(steps + period)] + + for i in range(0, steps): + stl_milp_solver(x, y, z, i, period, event) + + fig, axs = plt.subplots(3) + fig.suptitle('subplots') + axs[0].plot(t, x) + axs[0].set_title('x vs t') + axs[1].plot(t, y) + axs[1].set_title('y vs t') + axs[2].plot(t, z) + axs[2].set_title('z vs t') + fig.tight_layout() + plt.show() + +if __name__ =='__main__': + main() \ No newline at end of file