From a1347975ebf106c99f55e6c3017a6d5c6f224241 Mon Sep 17 00:00:00 2001 From: Your Name Date: Tue, 23 Mar 2021 15:49:50 -0400 Subject: [PATCH 1/4] First attempt for stl-mpc --- stl/stl.py | 4 +- stl/test/model_test.lp | 146 ++++++++++++ stl/test/stl2milp.lp | 452 ++++++++++++++++++++++++++++++++++++++ stl/test/stl2milp_test.py | 98 ++++++++- stl/test/stl_mpc.py | 175 +++++++++++++++ 5 files changed, 871 insertions(+), 4 deletions(-) create mode 100644 stl/test/model_test.lp create mode 100644 stl/test/stl2milp.lp create mode 100644 stl/test/stl_mpc.py 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..162fa63 --- /dev/null +++ b/stl/test/model_test.lp @@ -0,0 +1,146 @@ +\ Model STL formula: ((G[0.0, 2.0] (x >= 3.0)) && (F[0.0, 6.0] (y >= 4.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_7 + 0 v_7 + 0 w_7 +Subject To + R0: x_0 = 3 + R1: y_0 = -1 + R2: z_0 = 1 + R3: - x_0 - u_0 + x_1 = 0 + R4: - y_0 - v_0 + y_1 = 0 + R5: - z_0 - w_0 + z_1 = 0 + R6: - x_1 - u_1 + x_2 = 0 + R7: - y_1 - v_1 + y_2 = 0 + R8: - z_1 - w_1 + z_2 = 0 + R9: - x_2 - u_2 + x_3 = 0 + R10: - y_2 - v_2 + y_3 = 0 + R11: - z_2 - w_2 + z_3 = 0 + R12: - x_3 - u_3 + x_4 = 0 + R13: - y_3 - v_3 + y_4 = 0 + R14: - z_3 - w_3 + z_4 = 0 + R15: - x_4 - u_4 + x_5 = 0 + R16: - y_4 - v_4 + y_5 = 0 + R17: - z_4 - w_4 + z_5 = 0 + R18: - x_5 - u_5 + x_6 = 0 + R19: - y_5 - v_5 + y_6 = 0 + R20: - z_5 - w_5 + z_6 = 0 + R21: - x_6 - u_6 + x_7 = 0 + R22: - y_6 - v_6 + y_7 = 0 + R23: - z_6 - w_6 + z_7 = 0 + R24: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 <= 3 + R25: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 >= -17 + R26: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 <= 3 + R27: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 >= -17 + R28: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 <= 3 + R29: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 >= -17 + R30: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_0 <= 0 + R31: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_1 <= 0 + R32: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_2 <= 0 + R33: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_0 + - predicate_2dx22dd95ed78b4d217_1 - predicate_2dx22dd95ed78b4d217_2 + >= -2 + R34: - rho + y_0 - 20 predicate_2bx1735b9f08705a189_0 <= 4 + R35: - rho + y_0 - 20 predicate_2bx1735b9f08705a189_0 >= -16 + R36: - rho + y_1 - 20 predicate_2bx1735b9f08705a189_1 <= 4 + R37: - rho + y_1 - 20 predicate_2bx1735b9f08705a189_1 >= -16 + R38: - rho + y_2 - 20 predicate_2bx1735b9f08705a189_2 <= 4 + R39: - rho + y_2 - 20 predicate_2bx1735b9f08705a189_2 >= -16 + R40: - rho + y_3 - 20 predicate_2bx1735b9f08705a189_3 <= 4 + R41: - rho + y_3 - 20 predicate_2bx1735b9f08705a189_3 >= -16 + R42: - rho + y_4 - 20 predicate_2bx1735b9f08705a189_4 <= 4 + R43: - rho + y_4 - 20 predicate_2bx1735b9f08705a189_4 >= -16 + R44: - rho + y_5 - 20 predicate_2bx1735b9f08705a189_5 <= 4 + R45: - rho + y_5 - 20 predicate_2bx1735b9f08705a189_5 >= -16 + R46: - rho + y_6 - 20 predicate_2bx1735b9f08705a189_6 <= 4 + R47: - rho + y_6 - 20 predicate_2bx1735b9f08705a189_6 >= -16 + R48: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_0 >= 0 + R49: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_1 >= 0 + R50: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_2 >= 0 + R51: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_3 >= 0 + R52: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_4 >= 0 + R53: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_5 >= 0 + R54: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_6 >= 0 + R55: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_0 + - predicate_2bx1735b9f08705a189_1 - predicate_2bx1735b9f08705a189_2 + - predicate_2bx1735b9f08705a189_3 - predicate_2bx1735b9f08705a189_4 + - predicate_2bx1735b9f08705a189_5 - predicate_2bx1735b9f08705a189_6 + <= 0 + R56: - rho + z_0 - 20 predicate_2dx33b18e258c171243_0 <= 1 + R57: - rho + z_0 - 20 predicate_2dx33b18e258c171243_0 >= -19 + R58: - rho + z_1 - 20 predicate_2dx33b18e258c171243_1 <= 1 + R59: - rho + z_1 - 20 predicate_2dx33b18e258c171243_1 >= -19 + R60: - rho + z_2 - 20 predicate_2dx33b18e258c171243_2 <= 1 + R61: - rho + z_2 - 20 predicate_2dx33b18e258c171243_2 >= -19 + R62: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_0 <= 0 + R63: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_1 <= 0 + R64: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_2 <= 0 + R65: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_0 + - predicate_2dx33b18e258c171243_1 - predicate_2dx33b18e258c171243_2 + >= -2 + R66: and_2bx118e22bf358da4df_0 - always_2dx69bcdd71a3ff42e3_0 <= 0 + R67: and_2bx118e22bf358da4df_0 - event_2bx21312f0771487ac4_0 <= 0 + R68: and_2bx118e22bf358da4df_0 - always_2dx7c33fe6ba9ff9e2b_0 <= 0 + R69: and_2bx118e22bf358da4df_0 - always_2dx69bcdd71a3ff42e3_0 + - event_2bx21312f0771487ac4_0 - always_2dx7c33fe6ba9ff9e2b_0 >= -2 + formula_satisfaction: and_2bx118e22bf358da4df_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 +Binaries + and_2bx118e22bf358da4df_0 always_2dx69bcdd71a3ff42e3_0 + predicate_2dx22dd95ed78b4d217_0 predicate_2dx22dd95ed78b4d217_1 + predicate_2dx22dd95ed78b4d217_2 event_2bx21312f0771487ac4_0 + predicate_2bx1735b9f08705a189_0 predicate_2bx1735b9f08705a189_1 + predicate_2bx1735b9f08705a189_2 predicate_2bx1735b9f08705a189_3 + predicate_2bx1735b9f08705a189_4 predicate_2bx1735b9f08705a189_5 + predicate_2bx1735b9f08705a189_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..92dc25f --- /dev/null +++ b/stl/test/stl2milp.lp @@ -0,0 +1,452 @@ +\ Model STL formula: ((G[0.0, 10.0] (x >= 3.0)) && (G[2.0, 4.0] (F[20.0, 24.0] (y >= 2.0))) && (G[21.0, 26.0] (z <= 4.0)) && (G[21.0, 26.0] (z >= 3.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: - rho + x_3 - 20 predicate_2dx22dd95ed78b4d217_3 <= 3 + R94: - rho + x_3 - 20 predicate_2dx22dd95ed78b4d217_3 >= -17 + R95: - rho + x_4 - 20 predicate_2dx22dd95ed78b4d217_4 <= 3 + R96: - rho + x_4 - 20 predicate_2dx22dd95ed78b4d217_4 >= -17 + R97: - rho + x_5 - 20 predicate_2dx22dd95ed78b4d217_5 <= 3 + R98: - rho + x_5 - 20 predicate_2dx22dd95ed78b4d217_5 >= -17 + R99: - rho + x_6 - 20 predicate_2dx22dd95ed78b4d217_6 <= 3 + R100: - rho + x_6 - 20 predicate_2dx22dd95ed78b4d217_6 >= -17 + R101: - rho + x_7 - 20 predicate_2dx22dd95ed78b4d217_7 <= 3 + R102: - rho + x_7 - 20 predicate_2dx22dd95ed78b4d217_7 >= -17 + R103: - rho + x_8 - 20 predicate_2dx22dd95ed78b4d217_8 <= 3 + R104: - rho + x_8 - 20 predicate_2dx22dd95ed78b4d217_8 >= -17 + R105: - rho + x_9 - 20 predicate_2dx22dd95ed78b4d217_9 <= 3 + R106: - rho + x_9 - 20 predicate_2dx22dd95ed78b4d217_9 >= -17 + R107: - rho + x_10 - 20 predicate_2dx22dd95ed78b4d217_10 <= 3 + R108: - rho + x_10 - 20 predicate_2dx22dd95ed78b4d217_10 >= -17 + R109: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_0 <= 0 + R110: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_1 <= 0 + R111: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_2 <= 0 + R112: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_3 <= 0 + R113: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_4 <= 0 + R114: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_5 <= 0 + R115: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_6 <= 0 + R116: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_7 <= 0 + R117: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_8 <= 0 + R118: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_9 <= 0 + R119: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_10 + <= 0 + R120: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_0 + - predicate_2dx22dd95ed78b4d217_1 - predicate_2dx22dd95ed78b4d217_2 + - predicate_2dx22dd95ed78b4d217_3 - predicate_2dx22dd95ed78b4d217_4 + - predicate_2dx22dd95ed78b4d217_5 - predicate_2dx22dd95ed78b4d217_6 + - predicate_2dx22dd95ed78b4d217_7 - predicate_2dx22dd95ed78b4d217_8 + - predicate_2dx22dd95ed78b4d217_9 - predicate_2dx22dd95ed78b4d217_10 + >= -10 + R121: - rho + y_22 - 20 predicate_2dx48c103ba2c928dd_22 <= 2 + R122: - rho + y_22 - 20 predicate_2dx48c103ba2c928dd_22 >= -18 + R123: - rho + y_23 - 20 predicate_2dx48c103ba2c928dd_23 <= 2 + R124: - rho + y_23 - 20 predicate_2dx48c103ba2c928dd_23 >= -18 + R125: - rho + y_24 - 20 predicate_2dx48c103ba2c928dd_24 <= 2 + R126: - rho + y_24 - 20 predicate_2dx48c103ba2c928dd_24 >= -18 + R127: - rho + y_25 - 20 predicate_2dx48c103ba2c928dd_25 <= 2 + R128: - rho + y_25 - 20 predicate_2dx48c103ba2c928dd_25 >= -18 + R129: - rho + y_26 - 20 predicate_2dx48c103ba2c928dd_26 <= 2 + R130: - rho + y_26 - 20 predicate_2dx48c103ba2c928dd_26 >= -18 + R131: event_2bx7784b52277146866_2 - predicate_2dx48c103ba2c928dd_22 >= 0 + R132: event_2bx7784b52277146866_2 - predicate_2dx48c103ba2c928dd_23 >= 0 + R133: event_2bx7784b52277146866_2 - predicate_2dx48c103ba2c928dd_24 >= 0 + R134: event_2bx7784b52277146866_2 - predicate_2dx48c103ba2c928dd_25 >= 0 + R135: event_2bx7784b52277146866_2 - predicate_2dx48c103ba2c928dd_26 >= 0 + R136: event_2bx7784b52277146866_2 - predicate_2dx48c103ba2c928dd_22 + - predicate_2dx48c103ba2c928dd_23 - predicate_2dx48c103ba2c928dd_24 + - predicate_2dx48c103ba2c928dd_25 - predicate_2dx48c103ba2c928dd_26 + <= 0 + R137: - rho + y_27 - 20 predicate_2dx48c103ba2c928dd_27 <= 2 + R138: - rho + y_27 - 20 predicate_2dx48c103ba2c928dd_27 >= -18 + R139: - predicate_2dx48c103ba2c928dd_23 + event_2bx7784b52277146866_3 + >= 0 + R140: - predicate_2dx48c103ba2c928dd_24 + event_2bx7784b52277146866_3 + >= 0 + R141: - predicate_2dx48c103ba2c928dd_25 + event_2bx7784b52277146866_3 + >= 0 + R142: - predicate_2dx48c103ba2c928dd_26 + event_2bx7784b52277146866_3 + >= 0 + R143: event_2bx7784b52277146866_3 - predicate_2dx48c103ba2c928dd_27 >= 0 + R144: - predicate_2dx48c103ba2c928dd_23 - predicate_2dx48c103ba2c928dd_24 + - predicate_2dx48c103ba2c928dd_25 - predicate_2dx48c103ba2c928dd_26 + + event_2bx7784b52277146866_3 - predicate_2dx48c103ba2c928dd_27 <= 0 + R145: - rho + y_28 - 20 predicate_2dx48c103ba2c928dd_28 <= 2 + R146: - rho + y_28 - 20 predicate_2dx48c103ba2c928dd_28 >= -18 + R147: - predicate_2dx48c103ba2c928dd_24 + event_2bx7784b52277146866_4 + >= 0 + R148: - predicate_2dx48c103ba2c928dd_25 + event_2bx7784b52277146866_4 + >= 0 + R149: - predicate_2dx48c103ba2c928dd_26 + event_2bx7784b52277146866_4 + >= 0 + R150: - predicate_2dx48c103ba2c928dd_27 + event_2bx7784b52277146866_4 + >= 0 + R151: event_2bx7784b52277146866_4 - predicate_2dx48c103ba2c928dd_28 >= 0 + R152: - predicate_2dx48c103ba2c928dd_24 - predicate_2dx48c103ba2c928dd_25 + - predicate_2dx48c103ba2c928dd_26 - predicate_2dx48c103ba2c928dd_27 + + event_2bx7784b52277146866_4 - predicate_2dx48c103ba2c928dd_28 <= 0 + R153: always_2bx29c2cf03abdaadd0_0 - event_2bx7784b52277146866_2 <= 0 + R154: always_2bx29c2cf03abdaadd0_0 - event_2bx7784b52277146866_3 <= 0 + R155: always_2bx29c2cf03abdaadd0_0 - event_2bx7784b52277146866_4 <= 0 + R156: always_2bx29c2cf03abdaadd0_0 - event_2bx7784b52277146866_2 + - event_2bx7784b52277146866_3 - event_2bx7784b52277146866_4 >= -2 + R157: rho + z_21 + 20 predicate_2bx150bb59745841544_21 >= 4 + R158: rho + z_21 + 20 predicate_2bx150bb59745841544_21 <= 24 + R159: rho + z_22 + 20 predicate_2bx150bb59745841544_22 >= 4 + R160: rho + z_22 + 20 predicate_2bx150bb59745841544_22 <= 24 + R161: rho + z_23 + 20 predicate_2bx150bb59745841544_23 >= 4 + R162: rho + z_23 + 20 predicate_2bx150bb59745841544_23 <= 24 + R163: rho + z_24 + 20 predicate_2bx150bb59745841544_24 >= 4 + R164: rho + z_24 + 20 predicate_2bx150bb59745841544_24 <= 24 + R165: rho + z_25 + 20 predicate_2bx150bb59745841544_25 >= 4 + R166: rho + z_25 + 20 predicate_2bx150bb59745841544_25 <= 24 + R167: rho + z_26 + 20 predicate_2bx150bb59745841544_26 >= 4 + R168: rho + z_26 + 20 predicate_2bx150bb59745841544_26 <= 24 + R169: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_21 + <= 0 + R170: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_22 + <= 0 + R171: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_23 + <= 0 + R172: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_24 + <= 0 + R173: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_25 + <= 0 + R174: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_26 + <= 0 + R175: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_21 + - predicate_2bx150bb59745841544_22 - predicate_2bx150bb59745841544_23 + - predicate_2bx150bb59745841544_24 - predicate_2bx150bb59745841544_25 + - predicate_2bx150bb59745841544_26 >= -5 + R176: - rho + z_21 - 20 predicate_2dx17f01b49409b1295_21 <= 3 + R177: - rho + z_21 - 20 predicate_2dx17f01b49409b1295_21 >= -17 + R178: - rho + z_22 - 20 predicate_2dx17f01b49409b1295_22 <= 3 + R179: - rho + z_22 - 20 predicate_2dx17f01b49409b1295_22 >= -17 + R180: - rho + z_23 - 20 predicate_2dx17f01b49409b1295_23 <= 3 + R181: - rho + z_23 - 20 predicate_2dx17f01b49409b1295_23 >= -17 + R182: - rho + z_24 - 20 predicate_2dx17f01b49409b1295_24 <= 3 + R183: - rho + z_24 - 20 predicate_2dx17f01b49409b1295_24 >= -17 + R184: - rho + z_25 - 20 predicate_2dx17f01b49409b1295_25 <= 3 + R185: - rho + z_25 - 20 predicate_2dx17f01b49409b1295_25 >= -17 + R186: - rho + z_26 - 20 predicate_2dx17f01b49409b1295_26 <= 3 + R187: - rho + z_26 - 20 predicate_2dx17f01b49409b1295_26 >= -17 + R188: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_21 + <= 0 + R189: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_22 + <= 0 + R190: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_23 + <= 0 + R191: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_24 + <= 0 + R192: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_25 + <= 0 + R193: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_26 + <= 0 + R194: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_21 + - predicate_2dx17f01b49409b1295_22 - predicate_2dx17f01b49409b1295_23 + - predicate_2dx17f01b49409b1295_24 - predicate_2dx17f01b49409b1295_25 + - predicate_2dx17f01b49409b1295_26 >= -5 + R195: and_2bx43a2c068eac23333_0 - always_2dx778710aa24bf45ad_0 <= 0 + R196: and_2bx43a2c068eac23333_0 - always_2bx29c2cf03abdaadd0_0 <= 0 + R197: and_2bx43a2c068eac23333_0 - always_2dx7e9697b6ff524b6d_0 <= 0 + R198: and_2bx43a2c068eac23333_0 - always_2dx798ea4c82d31ac76_0 <= 0 + R199: and_2bx43a2c068eac23333_0 - always_2dx778710aa24bf45ad_0 + - always_2bx29c2cf03abdaadd0_0 - always_2dx7e9697b6ff524b6d_0 + - always_2dx798ea4c82d31ac76_0 >= -3 + formula_satisfaction: and_2bx43a2c068eac23333_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 + -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_2bx43a2c068eac23333_0 always_2dx778710aa24bf45ad_0 + predicate_2dx22dd95ed78b4d217_0 predicate_2dx22dd95ed78b4d217_1 + predicate_2dx22dd95ed78b4d217_2 predicate_2dx22dd95ed78b4d217_3 + predicate_2dx22dd95ed78b4d217_4 predicate_2dx22dd95ed78b4d217_5 + predicate_2dx22dd95ed78b4d217_6 predicate_2dx22dd95ed78b4d217_7 + predicate_2dx22dd95ed78b4d217_8 predicate_2dx22dd95ed78b4d217_9 + predicate_2dx22dd95ed78b4d217_10 always_2bx29c2cf03abdaadd0_0 + event_2bx7784b52277146866_2 predicate_2dx48c103ba2c928dd_22 + predicate_2dx48c103ba2c928dd_23 predicate_2dx48c103ba2c928dd_24 + predicate_2dx48c103ba2c928dd_25 predicate_2dx48c103ba2c928dd_26 + event_2bx7784b52277146866_3 predicate_2dx48c103ba2c928dd_27 + event_2bx7784b52277146866_4 predicate_2dx48c103ba2c928dd_28 + always_2dx7e9697b6ff524b6d_0 predicate_2bx150bb59745841544_21 + predicate_2bx150bb59745841544_22 predicate_2bx150bb59745841544_23 + predicate_2bx150bb59745841544_24 predicate_2bx150bb59745841544_25 + predicate_2bx150bb59745841544_26 always_2dx798ea4c82d31ac76_0 + predicate_2dx17f01b49409b1295_21 predicate_2dx17f01b49409b1295_22 + predicate_2dx17f01b49409b1295_23 predicate_2dx17f01b49409b1295_24 + predicate_2dx17f01b49409b1295_25 predicate_2dx17f01b49409b1295_26 +End diff --git a/stl/test/stl2milp_test.py b/stl/test/stl2milp_test.py index 83e574b..c84924d 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,13 @@ # 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)' + + +# Stl2milp Initialization lexer = stlLexer(InputStream(formula)) tokens = CommonTokenStream(lexer) parser = stlParser(tokens) @@ -36,10 +45,67 @@ 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) + +# 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 +119,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..73c7e32 --- /dev/null +++ b/stl/test/stl_mpc.py @@ -0,0 +1,175 @@ +#!/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 >= 4) && G[0, 2] (z >= 1)' + +# 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): +# 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 = 8 + 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 + + # define the inital states for each mpc step + stl_milp.model.addConstr(x[0] == x_init) + stl_milp.model.addConstr(y[0] == y_init) + stl_milp.model.addConstr(z[0] == z_init) + + # 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) + + # 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] + +#print(stl_milp_solver(2, 2, -3)) + +def main(): + steps = 30 + x_init, y_init, z_init = 3, 4, 1 + x = [0 if i != 0 else x_init for i in range(steps)] + y = [0 if i != 0 else y_init for i in range(steps)] + z = [0 if i != 0 else z_init for i in range(steps)] + t = [i for i in range(steps)] + + for i in range(1, steps): + x[i], y[i], z[i] = stl_milp_solver(x[i - 1], y[i - 1], z[i - 1]) + + 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 From afa765e8442dcf2671e940e9952f2a944c199172 Mon Sep 17 00:00:00 2001 From: Your Name Date: Tue, 20 Apr 2021 01:54:20 -0400 Subject: [PATCH 2/4] Modify the algrithom to get better prediction for next step for stl-mpc --- stl/test/model_test.lp | 207 +++++++++++++++++++++++++++-------------- stl/test/stl_mpc.py | 41 +++++--- 2 files changed, 162 insertions(+), 86 deletions(-) diff --git a/stl/test/model_test.lp b/stl/test/model_test.lp index 162fa63..484a520 100644 --- a/stl/test/model_test.lp +++ b/stl/test/model_test.lp @@ -1,86 +1,109 @@ \ Model STL formula: ((G[0.0, 2.0] (x >= 3.0)) && (F[0.0, 6.0] (y >= 4.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_7 + 0 v_7 + 0 w_7 + - 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 = 3 - R1: y_0 = -1 - R2: z_0 = 1 - R3: - x_0 - u_0 + x_1 = 0 - R4: - y_0 - v_0 + y_1 = 0 - R5: - z_0 - w_0 + z_1 = 0 - R6: - x_1 - u_1 + x_2 = 0 - R7: - y_1 - v_1 + y_2 = 0 - R8: - z_1 - w_1 + z_2 = 0 - R9: - x_2 - u_2 + x_3 = 0 - R10: - y_2 - v_2 + y_3 = 0 - R11: - z_2 - w_2 + z_3 = 0 - R12: - x_3 - u_3 + x_4 = 0 - R13: - y_3 - v_3 + y_4 = 0 - R14: - z_3 - w_3 + z_4 = 0 - R15: - x_4 - u_4 + x_5 = 0 - R16: - y_4 - v_4 + y_5 = 0 - R17: - z_4 - w_4 + z_5 = 0 - R18: - x_5 - u_5 + x_6 = 0 - R19: - y_5 - v_5 + y_6 = 0 - R20: - z_5 - w_5 + z_6 = 0 - R21: - x_6 - u_6 + x_7 = 0 - R22: - y_6 - v_6 + y_7 = 0 - R23: - z_6 - w_6 + z_7 = 0 - R24: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 <= 3 - R25: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 >= -17 - R26: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 <= 3 - R27: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 >= -17 - R28: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 <= 3 - R29: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 >= -17 - R30: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_0 <= 0 - R31: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_1 <= 0 - R32: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_2 <= 0 - R33: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_0 + R0: x_0 = 0 + R1: y_0 = 2 + R2: z_0 = -1 + R3: x_1 = 2 + R4: y_1 = 2 + R5: z_1 = -1 + R6: x_2 = 4 + R7: y_2 = 2 + R8: z_2 = -1 + R9: x_3 = 1 + R10: y_3 = 2 + R11: z_3 = -1 + R12: x_4 = 3 + R13: y_4 = 2 + R14: z_4 = -1 + R15: x_5 = 0 + R16: y_5 = 2 + R17: z_5 = -1 + R18: x_6 = 2 + R19: y_6 = 2 + R20: z_6 = -1 + R21: x_7 = 4 + R22: y_7 = 2 + R23: z_7 = -1 + 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 - R34: - rho + y_0 - 20 predicate_2bx1735b9f08705a189_0 <= 4 - R35: - rho + y_0 - 20 predicate_2bx1735b9f08705a189_0 >= -16 - R36: - rho + y_1 - 20 predicate_2bx1735b9f08705a189_1 <= 4 - R37: - rho + y_1 - 20 predicate_2bx1735b9f08705a189_1 >= -16 - R38: - rho + y_2 - 20 predicate_2bx1735b9f08705a189_2 <= 4 - R39: - rho + y_2 - 20 predicate_2bx1735b9f08705a189_2 >= -16 - R40: - rho + y_3 - 20 predicate_2bx1735b9f08705a189_3 <= 4 - R41: - rho + y_3 - 20 predicate_2bx1735b9f08705a189_3 >= -16 - R42: - rho + y_4 - 20 predicate_2bx1735b9f08705a189_4 <= 4 - R43: - rho + y_4 - 20 predicate_2bx1735b9f08705a189_4 >= -16 - R44: - rho + y_5 - 20 predicate_2bx1735b9f08705a189_5 <= 4 - R45: - rho + y_5 - 20 predicate_2bx1735b9f08705a189_5 >= -16 - R46: - rho + y_6 - 20 predicate_2bx1735b9f08705a189_6 <= 4 - R47: - rho + y_6 - 20 predicate_2bx1735b9f08705a189_6 >= -16 - R48: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_0 >= 0 - R49: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_1 >= 0 - R50: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_2 >= 0 - R51: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_3 >= 0 - R52: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_4 >= 0 - R53: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_5 >= 0 - R54: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_6 >= 0 - R55: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_0 + R55: - rho + y_0 - 20 predicate_2bx1735b9f08705a189_0 <= 4 + R56: - rho + y_0 - 20 predicate_2bx1735b9f08705a189_0 >= -16 + R57: - rho + y_1 - 20 predicate_2bx1735b9f08705a189_1 <= 4 + R58: - rho + y_1 - 20 predicate_2bx1735b9f08705a189_1 >= -16 + R59: - rho + y_2 - 20 predicate_2bx1735b9f08705a189_2 <= 4 + R60: - rho + y_2 - 20 predicate_2bx1735b9f08705a189_2 >= -16 + R61: - rho + y_3 - 20 predicate_2bx1735b9f08705a189_3 <= 4 + R62: - rho + y_3 - 20 predicate_2bx1735b9f08705a189_3 >= -16 + R63: - rho + y_4 - 20 predicate_2bx1735b9f08705a189_4 <= 4 + R64: - rho + y_4 - 20 predicate_2bx1735b9f08705a189_4 >= -16 + R65: - rho + y_5 - 20 predicate_2bx1735b9f08705a189_5 <= 4 + R66: - rho + y_5 - 20 predicate_2bx1735b9f08705a189_5 >= -16 + R67: - rho + y_6 - 20 predicate_2bx1735b9f08705a189_6 <= 4 + R68: - rho + y_6 - 20 predicate_2bx1735b9f08705a189_6 >= -16 + R69: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_0 >= 0 + R70: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_1 >= 0 + R71: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_2 >= 0 + R72: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_3 >= 0 + R73: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_4 >= 0 + R74: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_5 >= 0 + R75: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_6 >= 0 + R76: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_0 - predicate_2bx1735b9f08705a189_1 - predicate_2bx1735b9f08705a189_2 - predicate_2bx1735b9f08705a189_3 - predicate_2bx1735b9f08705a189_4 - predicate_2bx1735b9f08705a189_5 - predicate_2bx1735b9f08705a189_6 <= 0 - R56: - rho + z_0 - 20 predicate_2dx33b18e258c171243_0 <= 1 - R57: - rho + z_0 - 20 predicate_2dx33b18e258c171243_0 >= -19 - R58: - rho + z_1 - 20 predicate_2dx33b18e258c171243_1 <= 1 - R59: - rho + z_1 - 20 predicate_2dx33b18e258c171243_1 >= -19 - R60: - rho + z_2 - 20 predicate_2dx33b18e258c171243_2 <= 1 - R61: - rho + z_2 - 20 predicate_2dx33b18e258c171243_2 >= -19 - R62: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_0 <= 0 - R63: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_1 <= 0 - R64: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_2 <= 0 - R65: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_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 - R66: and_2bx118e22bf358da4df_0 - always_2dx69bcdd71a3ff42e3_0 <= 0 - R67: and_2bx118e22bf358da4df_0 - event_2bx21312f0771487ac4_0 <= 0 - R68: and_2bx118e22bf358da4df_0 - always_2dx7c33fe6ba9ff9e2b_0 <= 0 - R69: and_2bx118e22bf358da4df_0 - always_2dx69bcdd71a3ff42e3_0 + R87: and_2bx118e22bf358da4df_0 - always_2dx69bcdd71a3ff42e3_0 <= 0 + R88: and_2bx118e22bf358da4df_0 - event_2bx21312f0771487ac4_0 <= 0 + R89: and_2bx118e22bf358da4df_0 - always_2dx7c33fe6ba9ff9e2b_0 <= 0 + R90: and_2bx118e22bf358da4df_0 - always_2dx69bcdd71a3ff42e3_0 - event_2bx21312f0771487ac4_0 - always_2dx7c33fe6ba9ff9e2b_0 >= -2 formula_satisfaction: and_2bx118e22bf358da4df_0 = 1 Bounds @@ -133,6 +156,48 @@ Bounds -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_2bx118e22bf358da4df_0 always_2dx69bcdd71a3ff42e3_0 predicate_2dx22dd95ed78b4d217_0 predicate_2dx22dd95ed78b4d217_1 diff --git a/stl/test/stl_mpc.py b/stl/test/stl_mpc.py index 73c7e32..ae68549 100644 --- a/stl/test/stl_mpc.py +++ b/stl/test/stl_mpc.py @@ -51,7 +51,7 @@ print('AST:', str(ast)) -def stl_milp_solver(x_init, y_init, z_init): +def stl_milp_solver(x_init, y_init, z_init, current_step): # 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) @@ -70,7 +70,12 @@ def stl_milp_solver(x_init, y_init, z_init): v = dict() w = dict() - for k in range(period): + 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) @@ -93,12 +98,13 @@ def stl_milp_solver(x_init, y_init, z_init): stl_milp.variables['w'] = w # define the inital states for each mpc step - stl_milp.model.addConstr(x[0] == x_init) - stl_milp.model.addConstr(y[0] == y_init) - stl_milp.model.addConstr(z[0] == z_init) + 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(period-1): + 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] + \ @@ -145,20 +151,25 @@ def stl_milp_solver(x_init, y_init, z_init): # fig.tight_layout() # plt.show() - return x_vals[1], y_vals[1], z_vals[1] + # 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(): steps = 30 - x_init, y_init, z_init = 3, 4, 1 - x = [0 if i != 0 else x_init for i in range(steps)] - y = [0 if i != 0 else y_init for i in range(steps)] - z = [0 if i != 0 else z_init for i in range(steps)] - t = [i for i in range(steps)] - - for i in range(1, steps): - x[i], y[i], z[i] = stl_milp_solver(x[i - 1], y[i - 1], z[i - 1]) + period = 8 + 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) fig, axs = plt.subplots(3) fig.suptitle('subplots') From 1c2019499af1425f5ba88431d1d7182df4c7220e Mon Sep 17 00:00:00 2001 From: Your Name Date: Tue, 20 Apr 2021 16:13:07 -0400 Subject: [PATCH 3/4] Get some commets for stl-mpc --- stl/test/model_test.lp | 571 +++++++++++++++++++++++++++++++++-------- stl/test/stl_mpc.py | 13 +- 2 files changed, 474 insertions(+), 110 deletions(-) diff --git a/stl/test/model_test.lp b/stl/test/model_test.lp index 484a520..8699908 100644 --- a/stl/test/model_test.lp +++ b/stl/test/model_test.lp @@ -1,111 +1,263 @@ -\ Model STL formula: ((G[0.0, 2.0] (x >= 3.0)) && (F[0.0, 6.0] (y >= 4.0)) && (G[0.0, 2.0] (z >= 1.0))) +\ Model STL formula: ((G[0.0, 10.0] (x >= 3.0)) && (G[12.0, 15.0] (x <= 1.0)) && (G[17.0, 24.0] (x >= 4.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 + + 0 w_5 + 0 u_6 + 0 v_6 + 0 w_6 + 0 u_7 + 0 v_7 + 0 w_7 + 0 u_8 + 0 v_8 + + 0 w_8 + 0 u_9 + 0 v_9 + 0 w_9 + 0 u_10 + 0 v_10 + 0 w_10 + 0 u_11 + + 0 v_11 + 0 w_11 + 0 u_12 + 0 v_12 + 0 w_12 + 0 u_13 + 0 v_13 + 0 w_13 + + 0 u_14 + 0 v_14 + 0 w_14 + 0 u_15 + 0 v_15 + 0 w_15 + 0 u_16 + 0 v_16 + + 0 w_16 + 0 u_17 + 0 v_17 + 0 w_17 + 0 u_18 + 0 v_18 + 0 w_18 + 0 u_19 + + 0 v_19 + 0 w_19 + 0 u_20 + 0 v_20 + 0 w_20 + 0 u_21 + 0 v_21 + 0 w_21 + + 0 u_22 + 0 v_22 + 0 w_22 + 0 u_23 + 0 v_23 + 0 w_23 + 0 u_48 + 0 v_48 + + 0 w_48 Subject To - R0: x_0 = 0 - R1: y_0 = 2 - R2: z_0 = -1 - R3: x_1 = 2 - R4: y_1 = 2 - R5: z_1 = -1 - R6: x_2 = 4 - R7: y_2 = 2 - R8: z_2 = -1 - R9: x_3 = 1 - R10: y_3 = 2 - R11: z_3 = -1 + R0: x_0 = 3 + R1: y_0 = 5 + R2: z_0 = 5 + R3: x_1 = 3 + R4: y_1 = 3 + R5: z_1 = 2 + R6: x_2 = 3 + R7: y_2 = 5 + R8: z_2 = 2 + R9: x_3 = 3 + R10: y_3 = 3 + R11: z_3 = 5 R12: x_4 = 3 R13: y_4 = 2 - R14: z_4 = -1 - R15: x_5 = 0 + R14: z_4 = 2 + R15: x_5 = 3 R16: y_5 = 2 R17: z_5 = -1 - R18: x_6 = 2 - R19: y_6 = 2 - R20: z_6 = -1 - R21: x_7 = 4 - R22: y_7 = 2 - R23: z_7 = -1 - 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 + R18: x_6 = 0 + R19: y_6 = 0 + R20: z_6 = 2 + R21: x_7 = -3 + R22: y_7 = -2 + R23: z_7 = 5 + R24: x_8 = -1 + R25: y_8 = 1 + R26: z_8 = 2 + R27: x_9 = 1 + R28: y_9 = 4 + R29: z_9 = 5 + R30: x_10 = 0 + R31: y_10 = 2 + R32: z_10 = 2 + R33: x_11 = 2 + R34: y_11 = 5 + R35: z_11 = 5 + R36: x_12 = 4 + R37: y_12 = 3 + R38: z_12 = 2 + R39: x_13 = 4 + R40: y_13 = 1 + R41: z_13 = 2 + R42: x_14 = 4 + R43: y_14 = -1 + R44: z_14 = -1 + R45: x_15 = 4 + R46: y_15 = 2 + R47: z_15 = 2 + R48: x_16 = 4 + R49: y_16 = 5 + R50: z_16 = -1 + R51: x_17 = 4 + R52: y_17 = 3 + R53: z_17 = 2 + R54: x_18 = 4 + R55: y_18 = 4 + R56: z_18 = 5 + R57: x_19 = 5 + R58: y_19 = 2 + R59: z_19 = 2 + R60: x_20 = 2 + R61: y_20 = 0 + R62: z_20 = 2 + R63: x_21 = 2 + R64: y_21 = 3 + R65: z_21 = 2 + R66: x_22 = 2 + R67: y_22 = 1 + R68: z_22 = 2 + R69: x_23 = 2 + R70: y_23 = -1 + R71: z_23 = 2 + R72: x_24 = 2 + R73: y_24 = 2 + R74: z_24 = 2 + R75: - x_24 - u_24 + x_25 = 0 + R76: - y_24 - v_24 + y_25 = 0 + R77: - z_24 - w_24 + z_25 = 0 + R78: - x_25 - u_25 + x_26 = 0 + R79: - y_25 - v_25 + y_26 = 0 + R80: - z_25 - w_25 + z_26 = 0 + R81: - x_26 - u_26 + x_27 = 0 + R82: - y_26 - v_26 + y_27 = 0 + R83: - z_26 - w_26 + z_27 = 0 + R84: - x_27 - u_27 + x_28 = 0 + R85: - y_27 - v_27 + y_28 = 0 + R86: - z_27 - w_27 + z_28 = 0 + R87: - x_28 - u_28 + x_29 = 0 + R88: - y_28 - v_28 + y_29 = 0 + R89: - z_28 - w_28 + z_29 = 0 + R90: - x_29 - u_29 + x_30 = 0 + R91: - y_29 - v_29 + y_30 = 0 + R92: - z_29 - w_29 + z_30 = 0 + R93: - x_30 - u_30 + x_31 = 0 + R94: - y_30 - v_30 + y_31 = 0 + R95: - z_30 - w_30 + z_31 = 0 + R96: - x_31 - u_31 + x_32 = 0 + R97: - y_31 - v_31 + y_32 = 0 + R98: - z_31 - w_31 + z_32 = 0 + R99: - x_32 - u_32 + x_33 = 0 + R100: - y_32 - v_32 + y_33 = 0 + R101: - z_32 - w_32 + z_33 = 0 + R102: - x_33 - u_33 + x_34 = 0 + R103: - y_33 - v_33 + y_34 = 0 + R104: - z_33 - w_33 + z_34 = 0 + R105: - x_34 - u_34 + x_35 = 0 + R106: - y_34 - v_34 + y_35 = 0 + R107: - z_34 - w_34 + z_35 = 0 + R108: - x_35 - u_35 + x_36 = 0 + R109: - y_35 - v_35 + y_36 = 0 + R110: - z_35 - w_35 + z_36 = 0 + R111: - x_36 - u_36 + x_37 = 0 + R112: - y_36 - v_36 + y_37 = 0 + R113: - z_36 - w_36 + z_37 = 0 + R114: - x_37 - u_37 + x_38 = 0 + R115: - y_37 - v_37 + y_38 = 0 + R116: - z_37 - w_37 + z_38 = 0 + R117: - x_38 - u_38 + x_39 = 0 + R118: - y_38 - v_38 + y_39 = 0 + R119: - z_38 - w_38 + z_39 = 0 + R120: - x_39 - u_39 + x_40 = 0 + R121: - y_39 - v_39 + y_40 = 0 + R122: - z_39 - w_39 + z_40 = 0 + R123: - x_40 - u_40 + x_41 = 0 + R124: - y_40 - v_40 + y_41 = 0 + R125: - z_40 - w_40 + z_41 = 0 + R126: - x_41 - u_41 + x_42 = 0 + R127: - y_41 - v_41 + y_42 = 0 + R128: - z_41 - w_41 + z_42 = 0 + R129: - x_42 - u_42 + x_43 = 0 + R130: - y_42 - v_42 + y_43 = 0 + R131: - z_42 - w_42 + z_43 = 0 + R132: - x_43 - u_43 + x_44 = 0 + R133: - y_43 - v_43 + y_44 = 0 + R134: - z_43 - w_43 + z_44 = 0 + R135: - x_44 - u_44 + x_45 = 0 + R136: - y_44 - v_44 + y_45 = 0 + R137: - z_44 - w_44 + z_45 = 0 + R138: - x_45 - u_45 + x_46 = 0 + R139: - y_45 - v_45 + y_46 = 0 + R140: - z_45 - w_45 + z_46 = 0 + R141: - x_46 - u_46 + x_47 = 0 + R142: - y_46 - v_46 + y_47 = 0 + R143: - z_46 - w_46 + z_47 = 0 + R144: - x_47 - u_47 + x_48 = 0 + R145: - y_47 - v_47 + y_48 = 0 + R146: - z_47 - w_47 + z_48 = 0 + R147: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 <= 3 + R148: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 >= -17 + R149: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 <= 3 + R150: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 >= -17 + R151: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 <= 3 + R152: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 >= -17 + R153: - rho + x_3 - 20 predicate_2dx22dd95ed78b4d217_3 <= 3 + R154: - rho + x_3 - 20 predicate_2dx22dd95ed78b4d217_3 >= -17 + R155: - rho + x_4 - 20 predicate_2dx22dd95ed78b4d217_4 <= 3 + R156: - rho + x_4 - 20 predicate_2dx22dd95ed78b4d217_4 >= -17 + R157: - rho + x_5 - 20 predicate_2dx22dd95ed78b4d217_5 <= 3 + R158: - rho + x_5 - 20 predicate_2dx22dd95ed78b4d217_5 >= -17 + R159: - rho + x_6 - 20 predicate_2dx22dd95ed78b4d217_6 <= 3 + R160: - rho + x_6 - 20 predicate_2dx22dd95ed78b4d217_6 >= -17 + R161: - rho + x_7 - 20 predicate_2dx22dd95ed78b4d217_7 <= 3 + R162: - rho + x_7 - 20 predicate_2dx22dd95ed78b4d217_7 >= -17 + R163: - rho + x_8 - 20 predicate_2dx22dd95ed78b4d217_8 <= 3 + R164: - rho + x_8 - 20 predicate_2dx22dd95ed78b4d217_8 >= -17 + R165: - rho + x_9 - 20 predicate_2dx22dd95ed78b4d217_9 <= 3 + R166: - rho + x_9 - 20 predicate_2dx22dd95ed78b4d217_9 >= -17 + R167: - rho + x_10 - 20 predicate_2dx22dd95ed78b4d217_10 <= 3 + R168: - rho + x_10 - 20 predicate_2dx22dd95ed78b4d217_10 >= -17 + R169: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_0 <= 0 + R170: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_1 <= 0 + R171: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_2 <= 0 + R172: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_3 <= 0 + R173: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_4 <= 0 + R174: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_5 <= 0 + R175: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_6 <= 0 + R176: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_7 <= 0 + R177: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_8 <= 0 + R178: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_9 <= 0 + R179: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_10 + <= 0 + R180: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_0 - predicate_2dx22dd95ed78b4d217_1 - predicate_2dx22dd95ed78b4d217_2 - >= -2 - R55: - rho + y_0 - 20 predicate_2bx1735b9f08705a189_0 <= 4 - R56: - rho + y_0 - 20 predicate_2bx1735b9f08705a189_0 >= -16 - R57: - rho + y_1 - 20 predicate_2bx1735b9f08705a189_1 <= 4 - R58: - rho + y_1 - 20 predicate_2bx1735b9f08705a189_1 >= -16 - R59: - rho + y_2 - 20 predicate_2bx1735b9f08705a189_2 <= 4 - R60: - rho + y_2 - 20 predicate_2bx1735b9f08705a189_2 >= -16 - R61: - rho + y_3 - 20 predicate_2bx1735b9f08705a189_3 <= 4 - R62: - rho + y_3 - 20 predicate_2bx1735b9f08705a189_3 >= -16 - R63: - rho + y_4 - 20 predicate_2bx1735b9f08705a189_4 <= 4 - R64: - rho + y_4 - 20 predicate_2bx1735b9f08705a189_4 >= -16 - R65: - rho + y_5 - 20 predicate_2bx1735b9f08705a189_5 <= 4 - R66: - rho + y_5 - 20 predicate_2bx1735b9f08705a189_5 >= -16 - R67: - rho + y_6 - 20 predicate_2bx1735b9f08705a189_6 <= 4 - R68: - rho + y_6 - 20 predicate_2bx1735b9f08705a189_6 >= -16 - R69: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_0 >= 0 - R70: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_1 >= 0 - R71: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_2 >= 0 - R72: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_3 >= 0 - R73: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_4 >= 0 - R74: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_5 >= 0 - R75: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_6 >= 0 - R76: event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_0 - - predicate_2bx1735b9f08705a189_1 - predicate_2bx1735b9f08705a189_2 - - predicate_2bx1735b9f08705a189_3 - predicate_2bx1735b9f08705a189_4 - - predicate_2bx1735b9f08705a189_5 - predicate_2bx1735b9f08705a189_6 + - predicate_2dx22dd95ed78b4d217_3 - predicate_2dx22dd95ed78b4d217_4 + - predicate_2dx22dd95ed78b4d217_5 - predicate_2dx22dd95ed78b4d217_6 + - predicate_2dx22dd95ed78b4d217_7 - predicate_2dx22dd95ed78b4d217_8 + - predicate_2dx22dd95ed78b4d217_9 - predicate_2dx22dd95ed78b4d217_10 + >= -10 + R181: rho + x_12 + 20 predicate_2dx797b9146c700e2d3_12 >= 1 + R182: rho + x_12 + 20 predicate_2dx797b9146c700e2d3_12 <= 21 + R183: rho + x_13 + 20 predicate_2dx797b9146c700e2d3_13 >= 1 + R184: rho + x_13 + 20 predicate_2dx797b9146c700e2d3_13 <= 21 + R185: rho + x_14 + 20 predicate_2dx797b9146c700e2d3_14 >= 1 + R186: rho + x_14 + 20 predicate_2dx797b9146c700e2d3_14 <= 21 + R187: rho + x_15 + 20 predicate_2dx797b9146c700e2d3_15 >= 1 + R188: rho + x_15 + 20 predicate_2dx797b9146c700e2d3_15 <= 21 + R189: always_2dx96788d971626418_0 - predicate_2dx797b9146c700e2d3_12 <= 0 + R190: always_2dx96788d971626418_0 - predicate_2dx797b9146c700e2d3_13 <= 0 + R191: always_2dx96788d971626418_0 - predicate_2dx797b9146c700e2d3_14 <= 0 + R192: always_2dx96788d971626418_0 - predicate_2dx797b9146c700e2d3_15 <= 0 + R193: always_2dx96788d971626418_0 - predicate_2dx797b9146c700e2d3_12 + - predicate_2dx797b9146c700e2d3_13 - predicate_2dx797b9146c700e2d3_14 + - predicate_2dx797b9146c700e2d3_15 >= -3 + R194: - rho + x_17 - 20 predicate_2dx30be4d89f565bb0c_17 <= 4 + R195: - rho + x_17 - 20 predicate_2dx30be4d89f565bb0c_17 >= -16 + R196: - rho + x_18 - 20 predicate_2dx30be4d89f565bb0c_18 <= 4 + R197: - rho + x_18 - 20 predicate_2dx30be4d89f565bb0c_18 >= -16 + R198: - rho + x_19 - 20 predicate_2dx30be4d89f565bb0c_19 <= 4 + R199: - rho + x_19 - 20 predicate_2dx30be4d89f565bb0c_19 >= -16 + R200: - rho + x_20 - 20 predicate_2dx30be4d89f565bb0c_20 <= 4 + R201: - rho + x_20 - 20 predicate_2dx30be4d89f565bb0c_20 >= -16 + R202: - rho + x_21 - 20 predicate_2dx30be4d89f565bb0c_21 <= 4 + R203: - rho + x_21 - 20 predicate_2dx30be4d89f565bb0c_21 >= -16 + R204: - rho + x_22 - 20 predicate_2dx30be4d89f565bb0c_22 <= 4 + R205: - rho + x_22 - 20 predicate_2dx30be4d89f565bb0c_22 >= -16 + R206: - rho + x_23 - 20 predicate_2dx30be4d89f565bb0c_23 <= 4 + R207: - rho + x_23 - 20 predicate_2dx30be4d89f565bb0c_23 >= -16 + R208: - rho + x_24 - 20 predicate_2dx30be4d89f565bb0c_24 <= 4 + R209: - rho + x_24 - 20 predicate_2dx30be4d89f565bb0c_24 >= -16 + R210: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_17 + <= 0 + R211: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_18 + <= 0 + R212: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_19 + <= 0 + R213: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_20 + <= 0 + R214: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_21 + <= 0 + R215: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_22 + <= 0 + R216: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_23 + <= 0 + R217: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_24 <= 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_2bx118e22bf358da4df_0 - always_2dx69bcdd71a3ff42e3_0 <= 0 - R88: and_2bx118e22bf358da4df_0 - event_2bx21312f0771487ac4_0 <= 0 - R89: and_2bx118e22bf358da4df_0 - always_2dx7c33fe6ba9ff9e2b_0 <= 0 - R90: and_2bx118e22bf358da4df_0 - always_2dx69bcdd71a3ff42e3_0 - - event_2bx21312f0771487ac4_0 - always_2dx7c33fe6ba9ff9e2b_0 >= -2 - formula_satisfaction: and_2bx118e22bf358da4df_0 = 1 + R218: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_17 + - predicate_2dx30be4d89f565bb0c_18 - predicate_2dx30be4d89f565bb0c_19 + - predicate_2dx30be4d89f565bb0c_20 - predicate_2dx30be4d89f565bb0c_21 + - predicate_2dx30be4d89f565bb0c_22 - predicate_2dx30be4d89f565bb0c_23 + - predicate_2dx30be4d89f565bb0c_24 >= -7 + R219: and_2bx774dabba49604f84_0 - always_2dx778710aa24bf45ad_0 <= 0 + R220: and_2bx774dabba49604f84_0 - always_2dx96788d971626418_0 <= 0 + R221: and_2bx774dabba49604f84_0 - always_2dx33306d9e7f58b6b0_0 <= 0 + R222: and_2bx774dabba49604f84_0 - always_2dx778710aa24bf45ad_0 + - always_2dx96788d971626418_0 - always_2dx33306d9e7f58b6b0_0 >= -2 + formula_satisfaction: and_2bx774dabba49604f84_0 = 1 Bounds -infinity <= rho <= 999 -4 <= x_0 <= 5 @@ -198,14 +350,223 @@ Bounds -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 + -4 <= x_30 <= 5 + -4 <= y_30 <= 5 + -4 <= z_30 <= 5 + -3 <= u_30 <= 2 + -2 <= v_30 <= 3 + -3 <= w_30 <= 3 + -4 <= x_31 <= 5 + -4 <= y_31 <= 5 + -4 <= z_31 <= 5 + -3 <= u_31 <= 2 + -2 <= v_31 <= 3 + -3 <= w_31 <= 3 + -4 <= x_32 <= 5 + -4 <= y_32 <= 5 + -4 <= z_32 <= 5 + -3 <= u_32 <= 2 + -2 <= v_32 <= 3 + -3 <= w_32 <= 3 + -4 <= x_33 <= 5 + -4 <= y_33 <= 5 + -4 <= z_33 <= 5 + -3 <= u_33 <= 2 + -2 <= v_33 <= 3 + -3 <= w_33 <= 3 + -4 <= x_34 <= 5 + -4 <= y_34 <= 5 + -4 <= z_34 <= 5 + -3 <= u_34 <= 2 + -2 <= v_34 <= 3 + -3 <= w_34 <= 3 + -4 <= x_35 <= 5 + -4 <= y_35 <= 5 + -4 <= z_35 <= 5 + -3 <= u_35 <= 2 + -2 <= v_35 <= 3 + -3 <= w_35 <= 3 + -4 <= x_36 <= 5 + -4 <= y_36 <= 5 + -4 <= z_36 <= 5 + -3 <= u_36 <= 2 + -2 <= v_36 <= 3 + -3 <= w_36 <= 3 + -4 <= x_37 <= 5 + -4 <= y_37 <= 5 + -4 <= z_37 <= 5 + -3 <= u_37 <= 2 + -2 <= v_37 <= 3 + -3 <= w_37 <= 3 + -4 <= x_38 <= 5 + -4 <= y_38 <= 5 + -4 <= z_38 <= 5 + -3 <= u_38 <= 2 + -2 <= v_38 <= 3 + -3 <= w_38 <= 3 + -4 <= x_39 <= 5 + -4 <= y_39 <= 5 + -4 <= z_39 <= 5 + -3 <= u_39 <= 2 + -2 <= v_39 <= 3 + -3 <= w_39 <= 3 + -4 <= x_40 <= 5 + -4 <= y_40 <= 5 + -4 <= z_40 <= 5 + -3 <= u_40 <= 2 + -2 <= v_40 <= 3 + -3 <= w_40 <= 3 + -4 <= x_41 <= 5 + -4 <= y_41 <= 5 + -4 <= z_41 <= 5 + -3 <= u_41 <= 2 + -2 <= v_41 <= 3 + -3 <= w_41 <= 3 + -4 <= x_42 <= 5 + -4 <= y_42 <= 5 + -4 <= z_42 <= 5 + -3 <= u_42 <= 2 + -2 <= v_42 <= 3 + -3 <= w_42 <= 3 + -4 <= x_43 <= 5 + -4 <= y_43 <= 5 + -4 <= z_43 <= 5 + -3 <= u_43 <= 2 + -2 <= v_43 <= 3 + -3 <= w_43 <= 3 + -4 <= x_44 <= 5 + -4 <= y_44 <= 5 + -4 <= z_44 <= 5 + -3 <= u_44 <= 2 + -2 <= v_44 <= 3 + -3 <= w_44 <= 3 + -4 <= x_45 <= 5 + -4 <= y_45 <= 5 + -4 <= z_45 <= 5 + -3 <= u_45 <= 2 + -2 <= v_45 <= 3 + -3 <= w_45 <= 3 + -4 <= x_46 <= 5 + -4 <= y_46 <= 5 + -4 <= z_46 <= 5 + -3 <= u_46 <= 2 + -2 <= v_46 <= 3 + -3 <= w_46 <= 3 + -4 <= x_47 <= 5 + -4 <= y_47 <= 5 + -4 <= z_47 <= 5 + -3 <= u_47 <= 2 + -2 <= v_47 <= 3 + -3 <= w_47 <= 3 + -4 <= x_48 <= 5 + -4 <= y_48 <= 5 + -4 <= z_48 <= 5 + -3 <= u_48 <= 2 + -2 <= v_48 <= 3 + -3 <= w_48 <= 3 Binaries - and_2bx118e22bf358da4df_0 always_2dx69bcdd71a3ff42e3_0 + and_2bx774dabba49604f84_0 always_2dx778710aa24bf45ad_0 predicate_2dx22dd95ed78b4d217_0 predicate_2dx22dd95ed78b4d217_1 - predicate_2dx22dd95ed78b4d217_2 event_2bx21312f0771487ac4_0 - predicate_2bx1735b9f08705a189_0 predicate_2bx1735b9f08705a189_1 - predicate_2bx1735b9f08705a189_2 predicate_2bx1735b9f08705a189_3 - predicate_2bx1735b9f08705a189_4 predicate_2bx1735b9f08705a189_5 - predicate_2bx1735b9f08705a189_6 always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_0 predicate_2dx33b18e258c171243_1 - predicate_2dx33b18e258c171243_2 + predicate_2dx22dd95ed78b4d217_2 predicate_2dx22dd95ed78b4d217_3 + predicate_2dx22dd95ed78b4d217_4 predicate_2dx22dd95ed78b4d217_5 + predicate_2dx22dd95ed78b4d217_6 predicate_2dx22dd95ed78b4d217_7 + predicate_2dx22dd95ed78b4d217_8 predicate_2dx22dd95ed78b4d217_9 + predicate_2dx22dd95ed78b4d217_10 always_2dx96788d971626418_0 + predicate_2dx797b9146c700e2d3_12 predicate_2dx797b9146c700e2d3_13 + predicate_2dx797b9146c700e2d3_14 predicate_2dx797b9146c700e2d3_15 + always_2dx33306d9e7f58b6b0_0 predicate_2dx30be4d89f565bb0c_17 + predicate_2dx30be4d89f565bb0c_18 predicate_2dx30be4d89f565bb0c_19 + predicate_2dx30be4d89f565bb0c_20 predicate_2dx30be4d89f565bb0c_21 + predicate_2dx30be4d89f565bb0c_22 predicate_2dx30be4d89f565bb0c_23 + predicate_2dx30be4d89f565bb0c_24 End diff --git a/stl/test/stl_mpc.py b/stl/test/stl_mpc.py index ae68549..6515427 100644 --- a/stl/test/stl_mpc.py +++ b/stl/test/stl_mpc.py @@ -32,7 +32,8 @@ # 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 >= 4) && G[0, 2] (z >= 1)' +# formula = 'G[0,2] x >= 3 && F[0,6] (y >= 4) && 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]] @@ -51,7 +52,7 @@ print('AST:', str(ast)) -def stl_milp_solver(x_init, y_init, z_init, current_step): +def stl_milp_solver(x_init, y_init, z_init, current_step, period): # 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) @@ -62,7 +63,7 @@ def stl_milp_solver(x_init, y_init, z_init, current_step): # B = [[7, 8, 9], [4, 5, 6],[1, 2, 3]] # system variables and the time period - period = 8 + # period = 26 x = dict() y = dict() z = dict() @@ -160,8 +161,10 @@ def stl_milp_solver(x_init, y_init, z_init, current_step): #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 = 30 - period = 8 + period = 25 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)] @@ -169,7 +172,7 @@ def main(): t = [i for i in range(steps + period)] for i in range(0, steps): - stl_milp_solver(x, y, z, i) + stl_milp_solver(x, y, z, i, period ) fig, axs = plt.subplots(3) fig.suptitle('subplots') From 596a0f62c739c71684d1e76eaadae00d20f46c52 Mon Sep 17 00:00:00 2001 From: Your Name Date: Thu, 13 May 2021 23:39:54 -0400 Subject: [PATCH 4/4] Add event cases --- stl/test/model_test.lp | 573 +++++++------------------------------- stl/test/stl2milp.lp | 228 ++++----------- stl/test/stl2milp_test.py | 12 +- stl/test/stl_mpc.py | 22 +- 4 files changed, 193 insertions(+), 642 deletions(-) diff --git a/stl/test/model_test.lp b/stl/test/model_test.lp index 8699908..6e95697 100644 --- a/stl/test/model_test.lp +++ b/stl/test/model_test.lp @@ -1,263 +1,111 @@ -\ Model STL formula: ((G[0.0, 10.0] (x >= 3.0)) && (G[12.0, 15.0] (x <= 1.0)) && (G[17.0, 24.0] (x >= 4.0))) +\ 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_7 + 0 v_7 + 0 w_7 + 0 u_8 + 0 v_8 - + 0 w_8 + 0 u_9 + 0 v_9 + 0 w_9 + 0 u_10 + 0 v_10 + 0 w_10 + 0 u_11 - + 0 v_11 + 0 w_11 + 0 u_12 + 0 v_12 + 0 w_12 + 0 u_13 + 0 v_13 + 0 w_13 - + 0 u_14 + 0 v_14 + 0 w_14 + 0 u_15 + 0 v_15 + 0 w_15 + 0 u_16 + 0 v_16 - + 0 w_16 + 0 u_17 + 0 v_17 + 0 w_17 + 0 u_18 + 0 v_18 + 0 w_18 + 0 u_19 - + 0 v_19 + 0 w_19 + 0 u_20 + 0 v_20 + 0 w_20 + 0 u_21 + 0 v_21 + 0 w_21 - + 0 u_22 + 0 v_22 + 0 w_22 + 0 u_23 + 0 v_23 + 0 w_23 + 0 u_48 + 0 v_48 - + 0 w_48 + + 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 = 3 - R1: y_0 = 5 - R2: z_0 = 5 - R3: x_1 = 3 - R4: y_1 = 3 - R5: z_1 = 2 + 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 = 2 - R9: x_3 = 3 + R8: z_2 = -1 + R9: x_3 = 0 R10: y_3 = 3 - R11: z_3 = 5 - R12: x_4 = 3 - R13: y_4 = 2 - R14: z_4 = 2 - R15: x_5 = 3 - R16: y_5 = 2 - R17: z_5 = -1 - R18: x_6 = 0 - R19: y_6 = 0 - R20: z_6 = 2 - R21: x_7 = -3 - R22: y_7 = -2 - R23: z_7 = 5 - R24: x_8 = -1 - R25: y_8 = 1 - R26: z_8 = 2 - R27: x_9 = 1 - R28: y_9 = 4 - R29: z_9 = 5 - R30: x_10 = 0 - R31: y_10 = 2 - R32: z_10 = 2 - R33: x_11 = 2 - R34: y_11 = 5 - R35: z_11 = 5 - R36: x_12 = 4 - R37: y_12 = 3 - R38: z_12 = 2 - R39: x_13 = 4 - R40: y_13 = 1 - R41: z_13 = 2 - R42: x_14 = 4 - R43: y_14 = -1 - R44: z_14 = -1 - R45: x_15 = 4 - R46: y_15 = 2 - R47: z_15 = 2 - R48: x_16 = 4 - R49: y_16 = 5 - R50: z_16 = -1 - R51: x_17 = 4 - R52: y_17 = 3 - R53: z_17 = 2 - R54: x_18 = 4 - R55: y_18 = 4 - R56: z_18 = 5 - R57: x_19 = 5 - R58: y_19 = 2 - R59: z_19 = 2 - R60: x_20 = 2 - R61: y_20 = 0 - R62: z_20 = 2 - R63: x_21 = 2 - R64: y_21 = 3 - R65: z_21 = 2 - R66: x_22 = 2 - R67: y_22 = 1 - R68: z_22 = 2 - R69: x_23 = 2 - R70: y_23 = -1 - R71: z_23 = 2 - R72: x_24 = 2 - R73: y_24 = 2 - R74: z_24 = 2 - R75: - x_24 - u_24 + x_25 = 0 - R76: - y_24 - v_24 + y_25 = 0 - R77: - z_24 - w_24 + z_25 = 0 - R78: - x_25 - u_25 + x_26 = 0 - R79: - y_25 - v_25 + y_26 = 0 - R80: - z_25 - w_25 + z_26 = 0 - R81: - x_26 - u_26 + x_27 = 0 - R82: - y_26 - v_26 + y_27 = 0 - R83: - z_26 - w_26 + z_27 = 0 - R84: - x_27 - u_27 + x_28 = 0 - R85: - y_27 - v_27 + y_28 = 0 - R86: - z_27 - w_27 + z_28 = 0 - R87: - x_28 - u_28 + x_29 = 0 - R88: - y_28 - v_28 + y_29 = 0 - R89: - z_28 - w_28 + z_29 = 0 - R90: - x_29 - u_29 + x_30 = 0 - R91: - y_29 - v_29 + y_30 = 0 - R92: - z_29 - w_29 + z_30 = 0 - R93: - x_30 - u_30 + x_31 = 0 - R94: - y_30 - v_30 + y_31 = 0 - R95: - z_30 - w_30 + z_31 = 0 - R96: - x_31 - u_31 + x_32 = 0 - R97: - y_31 - v_31 + y_32 = 0 - R98: - z_31 - w_31 + z_32 = 0 - R99: - x_32 - u_32 + x_33 = 0 - R100: - y_32 - v_32 + y_33 = 0 - R101: - z_32 - w_32 + z_33 = 0 - R102: - x_33 - u_33 + x_34 = 0 - R103: - y_33 - v_33 + y_34 = 0 - R104: - z_33 - w_33 + z_34 = 0 - R105: - x_34 - u_34 + x_35 = 0 - R106: - y_34 - v_34 + y_35 = 0 - R107: - z_34 - w_34 + z_35 = 0 - R108: - x_35 - u_35 + x_36 = 0 - R109: - y_35 - v_35 + y_36 = 0 - R110: - z_35 - w_35 + z_36 = 0 - R111: - x_36 - u_36 + x_37 = 0 - R112: - y_36 - v_36 + y_37 = 0 - R113: - z_36 - w_36 + z_37 = 0 - R114: - x_37 - u_37 + x_38 = 0 - R115: - y_37 - v_37 + y_38 = 0 - R116: - z_37 - w_37 + z_38 = 0 - R117: - x_38 - u_38 + x_39 = 0 - R118: - y_38 - v_38 + y_39 = 0 - R119: - z_38 - w_38 + z_39 = 0 - R120: - x_39 - u_39 + x_40 = 0 - R121: - y_39 - v_39 + y_40 = 0 - R122: - z_39 - w_39 + z_40 = 0 - R123: - x_40 - u_40 + x_41 = 0 - R124: - y_40 - v_40 + y_41 = 0 - R125: - z_40 - w_40 + z_41 = 0 - R126: - x_41 - u_41 + x_42 = 0 - R127: - y_41 - v_41 + y_42 = 0 - R128: - z_41 - w_41 + z_42 = 0 - R129: - x_42 - u_42 + x_43 = 0 - R130: - y_42 - v_42 + y_43 = 0 - R131: - z_42 - w_42 + z_43 = 0 - R132: - x_43 - u_43 + x_44 = 0 - R133: - y_43 - v_43 + y_44 = 0 - R134: - z_43 - w_43 + z_44 = 0 - R135: - x_44 - u_44 + x_45 = 0 - R136: - y_44 - v_44 + y_45 = 0 - R137: - z_44 - w_44 + z_45 = 0 - R138: - x_45 - u_45 + x_46 = 0 - R139: - y_45 - v_45 + y_46 = 0 - R140: - z_45 - w_45 + z_46 = 0 - R141: - x_46 - u_46 + x_47 = 0 - R142: - y_46 - v_46 + y_47 = 0 - R143: - z_46 - w_46 + z_47 = 0 - R144: - x_47 - u_47 + x_48 = 0 - R145: - y_47 - v_47 + y_48 = 0 - R146: - z_47 - w_47 + z_48 = 0 - R147: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 <= 3 - R148: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 >= -17 - R149: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 <= 3 - R150: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 >= -17 - R151: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 <= 3 - R152: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 >= -17 - R153: - rho + x_3 - 20 predicate_2dx22dd95ed78b4d217_3 <= 3 - R154: - rho + x_3 - 20 predicate_2dx22dd95ed78b4d217_3 >= -17 - R155: - rho + x_4 - 20 predicate_2dx22dd95ed78b4d217_4 <= 3 - R156: - rho + x_4 - 20 predicate_2dx22dd95ed78b4d217_4 >= -17 - R157: - rho + x_5 - 20 predicate_2dx22dd95ed78b4d217_5 <= 3 - R158: - rho + x_5 - 20 predicate_2dx22dd95ed78b4d217_5 >= -17 - R159: - rho + x_6 - 20 predicate_2dx22dd95ed78b4d217_6 <= 3 - R160: - rho + x_6 - 20 predicate_2dx22dd95ed78b4d217_6 >= -17 - R161: - rho + x_7 - 20 predicate_2dx22dd95ed78b4d217_7 <= 3 - R162: - rho + x_7 - 20 predicate_2dx22dd95ed78b4d217_7 >= -17 - R163: - rho + x_8 - 20 predicate_2dx22dd95ed78b4d217_8 <= 3 - R164: - rho + x_8 - 20 predicate_2dx22dd95ed78b4d217_8 >= -17 - R165: - rho + x_9 - 20 predicate_2dx22dd95ed78b4d217_9 <= 3 - R166: - rho + x_9 - 20 predicate_2dx22dd95ed78b4d217_9 >= -17 - R167: - rho + x_10 - 20 predicate_2dx22dd95ed78b4d217_10 <= 3 - R168: - rho + x_10 - 20 predicate_2dx22dd95ed78b4d217_10 >= -17 - R169: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_0 <= 0 - R170: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_1 <= 0 - R171: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_2 <= 0 - R172: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_3 <= 0 - R173: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_4 <= 0 - R174: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_5 <= 0 - R175: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_6 <= 0 - R176: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_7 <= 0 - R177: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_8 <= 0 - R178: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_9 <= 0 - R179: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_10 - <= 0 - R180: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_0 + 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 - - predicate_2dx22dd95ed78b4d217_3 - predicate_2dx22dd95ed78b4d217_4 - - predicate_2dx22dd95ed78b4d217_5 - predicate_2dx22dd95ed78b4d217_6 - - predicate_2dx22dd95ed78b4d217_7 - predicate_2dx22dd95ed78b4d217_8 - - predicate_2dx22dd95ed78b4d217_9 - predicate_2dx22dd95ed78b4d217_10 - >= -10 - R181: rho + x_12 + 20 predicate_2dx797b9146c700e2d3_12 >= 1 - R182: rho + x_12 + 20 predicate_2dx797b9146c700e2d3_12 <= 21 - R183: rho + x_13 + 20 predicate_2dx797b9146c700e2d3_13 >= 1 - R184: rho + x_13 + 20 predicate_2dx797b9146c700e2d3_13 <= 21 - R185: rho + x_14 + 20 predicate_2dx797b9146c700e2d3_14 >= 1 - R186: rho + x_14 + 20 predicate_2dx797b9146c700e2d3_14 <= 21 - R187: rho + x_15 + 20 predicate_2dx797b9146c700e2d3_15 >= 1 - R188: rho + x_15 + 20 predicate_2dx797b9146c700e2d3_15 <= 21 - R189: always_2dx96788d971626418_0 - predicate_2dx797b9146c700e2d3_12 <= 0 - R190: always_2dx96788d971626418_0 - predicate_2dx797b9146c700e2d3_13 <= 0 - R191: always_2dx96788d971626418_0 - predicate_2dx797b9146c700e2d3_14 <= 0 - R192: always_2dx96788d971626418_0 - predicate_2dx797b9146c700e2d3_15 <= 0 - R193: always_2dx96788d971626418_0 - predicate_2dx797b9146c700e2d3_12 - - predicate_2dx797b9146c700e2d3_13 - predicate_2dx797b9146c700e2d3_14 - - predicate_2dx797b9146c700e2d3_15 >= -3 - R194: - rho + x_17 - 20 predicate_2dx30be4d89f565bb0c_17 <= 4 - R195: - rho + x_17 - 20 predicate_2dx30be4d89f565bb0c_17 >= -16 - R196: - rho + x_18 - 20 predicate_2dx30be4d89f565bb0c_18 <= 4 - R197: - rho + x_18 - 20 predicate_2dx30be4d89f565bb0c_18 >= -16 - R198: - rho + x_19 - 20 predicate_2dx30be4d89f565bb0c_19 <= 4 - R199: - rho + x_19 - 20 predicate_2dx30be4d89f565bb0c_19 >= -16 - R200: - rho + x_20 - 20 predicate_2dx30be4d89f565bb0c_20 <= 4 - R201: - rho + x_20 - 20 predicate_2dx30be4d89f565bb0c_20 >= -16 - R202: - rho + x_21 - 20 predicate_2dx30be4d89f565bb0c_21 <= 4 - R203: - rho + x_21 - 20 predicate_2dx30be4d89f565bb0c_21 >= -16 - R204: - rho + x_22 - 20 predicate_2dx30be4d89f565bb0c_22 <= 4 - R205: - rho + x_22 - 20 predicate_2dx30be4d89f565bb0c_22 >= -16 - R206: - rho + x_23 - 20 predicate_2dx30be4d89f565bb0c_23 <= 4 - R207: - rho + x_23 - 20 predicate_2dx30be4d89f565bb0c_23 >= -16 - R208: - rho + x_24 - 20 predicate_2dx30be4d89f565bb0c_24 <= 4 - R209: - rho + x_24 - 20 predicate_2dx30be4d89f565bb0c_24 >= -16 - R210: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_17 - <= 0 - R211: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_18 - <= 0 - R212: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_19 - <= 0 - R213: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_20 - <= 0 - R214: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_21 - <= 0 - R215: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_22 - <= 0 - R216: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_23 - <= 0 - R217: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_24 + >= -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 - R218: always_2dx33306d9e7f58b6b0_0 - predicate_2dx30be4d89f565bb0c_17 - - predicate_2dx30be4d89f565bb0c_18 - predicate_2dx30be4d89f565bb0c_19 - - predicate_2dx30be4d89f565bb0c_20 - predicate_2dx30be4d89f565bb0c_21 - - predicate_2dx30be4d89f565bb0c_22 - predicate_2dx30be4d89f565bb0c_23 - - predicate_2dx30be4d89f565bb0c_24 >= -7 - R219: and_2bx774dabba49604f84_0 - always_2dx778710aa24bf45ad_0 <= 0 - R220: and_2bx774dabba49604f84_0 - always_2dx96788d971626418_0 <= 0 - R221: and_2bx774dabba49604f84_0 - always_2dx33306d9e7f58b6b0_0 <= 0 - R222: and_2bx774dabba49604f84_0 - always_2dx778710aa24bf45ad_0 - - always_2dx96788d971626418_0 - always_2dx33306d9e7f58b6b0_0 >= -2 - formula_satisfaction: and_2bx774dabba49604f84_0 = 1 + 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 @@ -350,223 +198,14 @@ Bounds -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 - -4 <= x_30 <= 5 - -4 <= y_30 <= 5 - -4 <= z_30 <= 5 - -3 <= u_30 <= 2 - -2 <= v_30 <= 3 - -3 <= w_30 <= 3 - -4 <= x_31 <= 5 - -4 <= y_31 <= 5 - -4 <= z_31 <= 5 - -3 <= u_31 <= 2 - -2 <= v_31 <= 3 - -3 <= w_31 <= 3 - -4 <= x_32 <= 5 - -4 <= y_32 <= 5 - -4 <= z_32 <= 5 - -3 <= u_32 <= 2 - -2 <= v_32 <= 3 - -3 <= w_32 <= 3 - -4 <= x_33 <= 5 - -4 <= y_33 <= 5 - -4 <= z_33 <= 5 - -3 <= u_33 <= 2 - -2 <= v_33 <= 3 - -3 <= w_33 <= 3 - -4 <= x_34 <= 5 - -4 <= y_34 <= 5 - -4 <= z_34 <= 5 - -3 <= u_34 <= 2 - -2 <= v_34 <= 3 - -3 <= w_34 <= 3 - -4 <= x_35 <= 5 - -4 <= y_35 <= 5 - -4 <= z_35 <= 5 - -3 <= u_35 <= 2 - -2 <= v_35 <= 3 - -3 <= w_35 <= 3 - -4 <= x_36 <= 5 - -4 <= y_36 <= 5 - -4 <= z_36 <= 5 - -3 <= u_36 <= 2 - -2 <= v_36 <= 3 - -3 <= w_36 <= 3 - -4 <= x_37 <= 5 - -4 <= y_37 <= 5 - -4 <= z_37 <= 5 - -3 <= u_37 <= 2 - -2 <= v_37 <= 3 - -3 <= w_37 <= 3 - -4 <= x_38 <= 5 - -4 <= y_38 <= 5 - -4 <= z_38 <= 5 - -3 <= u_38 <= 2 - -2 <= v_38 <= 3 - -3 <= w_38 <= 3 - -4 <= x_39 <= 5 - -4 <= y_39 <= 5 - -4 <= z_39 <= 5 - -3 <= u_39 <= 2 - -2 <= v_39 <= 3 - -3 <= w_39 <= 3 - -4 <= x_40 <= 5 - -4 <= y_40 <= 5 - -4 <= z_40 <= 5 - -3 <= u_40 <= 2 - -2 <= v_40 <= 3 - -3 <= w_40 <= 3 - -4 <= x_41 <= 5 - -4 <= y_41 <= 5 - -4 <= z_41 <= 5 - -3 <= u_41 <= 2 - -2 <= v_41 <= 3 - -3 <= w_41 <= 3 - -4 <= x_42 <= 5 - -4 <= y_42 <= 5 - -4 <= z_42 <= 5 - -3 <= u_42 <= 2 - -2 <= v_42 <= 3 - -3 <= w_42 <= 3 - -4 <= x_43 <= 5 - -4 <= y_43 <= 5 - -4 <= z_43 <= 5 - -3 <= u_43 <= 2 - -2 <= v_43 <= 3 - -3 <= w_43 <= 3 - -4 <= x_44 <= 5 - -4 <= y_44 <= 5 - -4 <= z_44 <= 5 - -3 <= u_44 <= 2 - -2 <= v_44 <= 3 - -3 <= w_44 <= 3 - -4 <= x_45 <= 5 - -4 <= y_45 <= 5 - -4 <= z_45 <= 5 - -3 <= u_45 <= 2 - -2 <= v_45 <= 3 - -3 <= w_45 <= 3 - -4 <= x_46 <= 5 - -4 <= y_46 <= 5 - -4 <= z_46 <= 5 - -3 <= u_46 <= 2 - -2 <= v_46 <= 3 - -3 <= w_46 <= 3 - -4 <= x_47 <= 5 - -4 <= y_47 <= 5 - -4 <= z_47 <= 5 - -3 <= u_47 <= 2 - -2 <= v_47 <= 3 - -3 <= w_47 <= 3 - -4 <= x_48 <= 5 - -4 <= y_48 <= 5 - -4 <= z_48 <= 5 - -3 <= u_48 <= 2 - -2 <= v_48 <= 3 - -3 <= w_48 <= 3 Binaries - and_2bx774dabba49604f84_0 always_2dx778710aa24bf45ad_0 + and_2dx5295e3d99f627fa8_0 always_2dx69bcdd71a3ff42e3_0 predicate_2dx22dd95ed78b4d217_0 predicate_2dx22dd95ed78b4d217_1 - predicate_2dx22dd95ed78b4d217_2 predicate_2dx22dd95ed78b4d217_3 - predicate_2dx22dd95ed78b4d217_4 predicate_2dx22dd95ed78b4d217_5 - predicate_2dx22dd95ed78b4d217_6 predicate_2dx22dd95ed78b4d217_7 - predicate_2dx22dd95ed78b4d217_8 predicate_2dx22dd95ed78b4d217_9 - predicate_2dx22dd95ed78b4d217_10 always_2dx96788d971626418_0 - predicate_2dx797b9146c700e2d3_12 predicate_2dx797b9146c700e2d3_13 - predicate_2dx797b9146c700e2d3_14 predicate_2dx797b9146c700e2d3_15 - always_2dx33306d9e7f58b6b0_0 predicate_2dx30be4d89f565bb0c_17 - predicate_2dx30be4d89f565bb0c_18 predicate_2dx30be4d89f565bb0c_19 - predicate_2dx30be4d89f565bb0c_20 predicate_2dx30be4d89f565bb0c_21 - predicate_2dx30be4d89f565bb0c_22 predicate_2dx30be4d89f565bb0c_23 - predicate_2dx30be4d89f565bb0c_24 + 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 index 92dc25f..0dd312a 100644 --- a/stl/test/stl2milp.lp +++ b/stl/test/stl2milp.lp @@ -1,4 +1,4 @@ -\ Model STL formula: ((G[0.0, 10.0] (x >= 3.0)) && (G[2.0, 4.0] (F[20.0, 24.0] (y >= 2.0))) && (G[21.0, 26.0] (z <= 4.0)) && (G[21.0, 26.0] (z >= 3.0))) +\ 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 @@ -96,157 +96,59 @@ Subject To 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: - rho + x_3 - 20 predicate_2dx22dd95ed78b4d217_3 <= 3 - R94: - rho + x_3 - 20 predicate_2dx22dd95ed78b4d217_3 >= -17 - R95: - rho + x_4 - 20 predicate_2dx22dd95ed78b4d217_4 <= 3 - R96: - rho + x_4 - 20 predicate_2dx22dd95ed78b4d217_4 >= -17 - R97: - rho + x_5 - 20 predicate_2dx22dd95ed78b4d217_5 <= 3 - R98: - rho + x_5 - 20 predicate_2dx22dd95ed78b4d217_5 >= -17 - R99: - rho + x_6 - 20 predicate_2dx22dd95ed78b4d217_6 <= 3 - R100: - rho + x_6 - 20 predicate_2dx22dd95ed78b4d217_6 >= -17 - R101: - rho + x_7 - 20 predicate_2dx22dd95ed78b4d217_7 <= 3 - R102: - rho + x_7 - 20 predicate_2dx22dd95ed78b4d217_7 >= -17 - R103: - rho + x_8 - 20 predicate_2dx22dd95ed78b4d217_8 <= 3 - R104: - rho + x_8 - 20 predicate_2dx22dd95ed78b4d217_8 >= -17 - R105: - rho + x_9 - 20 predicate_2dx22dd95ed78b4d217_9 <= 3 - R106: - rho + x_9 - 20 predicate_2dx22dd95ed78b4d217_9 >= -17 - R107: - rho + x_10 - 20 predicate_2dx22dd95ed78b4d217_10 <= 3 - R108: - rho + x_10 - 20 predicate_2dx22dd95ed78b4d217_10 >= -17 - R109: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_0 <= 0 - R110: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_1 <= 0 - R111: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_2 <= 0 - R112: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_3 <= 0 - R113: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_4 <= 0 - R114: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_5 <= 0 - R115: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_6 <= 0 - R116: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_7 <= 0 - R117: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_8 <= 0 - R118: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_9 <= 0 - R119: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_10 - <= 0 - R120: always_2dx778710aa24bf45ad_0 - predicate_2dx22dd95ed78b4d217_0 + 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 - - predicate_2dx22dd95ed78b4d217_3 - predicate_2dx22dd95ed78b4d217_4 - - predicate_2dx22dd95ed78b4d217_5 - predicate_2dx22dd95ed78b4d217_6 - - predicate_2dx22dd95ed78b4d217_7 - predicate_2dx22dd95ed78b4d217_8 - - predicate_2dx22dd95ed78b4d217_9 - predicate_2dx22dd95ed78b4d217_10 - >= -10 - R121: - rho + y_22 - 20 predicate_2dx48c103ba2c928dd_22 <= 2 - R122: - rho + y_22 - 20 predicate_2dx48c103ba2c928dd_22 >= -18 - R123: - rho + y_23 - 20 predicate_2dx48c103ba2c928dd_23 <= 2 - R124: - rho + y_23 - 20 predicate_2dx48c103ba2c928dd_23 >= -18 - R125: - rho + y_24 - 20 predicate_2dx48c103ba2c928dd_24 <= 2 - R126: - rho + y_24 - 20 predicate_2dx48c103ba2c928dd_24 >= -18 - R127: - rho + y_25 - 20 predicate_2dx48c103ba2c928dd_25 <= 2 - R128: - rho + y_25 - 20 predicate_2dx48c103ba2c928dd_25 >= -18 - R129: - rho + y_26 - 20 predicate_2dx48c103ba2c928dd_26 <= 2 - R130: - rho + y_26 - 20 predicate_2dx48c103ba2c928dd_26 >= -18 - R131: event_2bx7784b52277146866_2 - predicate_2dx48c103ba2c928dd_22 >= 0 - R132: event_2bx7784b52277146866_2 - predicate_2dx48c103ba2c928dd_23 >= 0 - R133: event_2bx7784b52277146866_2 - predicate_2dx48c103ba2c928dd_24 >= 0 - R134: event_2bx7784b52277146866_2 - predicate_2dx48c103ba2c928dd_25 >= 0 - R135: event_2bx7784b52277146866_2 - predicate_2dx48c103ba2c928dd_26 >= 0 - R136: event_2bx7784b52277146866_2 - predicate_2dx48c103ba2c928dd_22 - - predicate_2dx48c103ba2c928dd_23 - predicate_2dx48c103ba2c928dd_24 - - predicate_2dx48c103ba2c928dd_25 - predicate_2dx48c103ba2c928dd_26 - <= 0 - R137: - rho + y_27 - 20 predicate_2dx48c103ba2c928dd_27 <= 2 - R138: - rho + y_27 - 20 predicate_2dx48c103ba2c928dd_27 >= -18 - R139: - predicate_2dx48c103ba2c928dd_23 + event_2bx7784b52277146866_3 - >= 0 - R140: - predicate_2dx48c103ba2c928dd_24 + event_2bx7784b52277146866_3 - >= 0 - R141: - predicate_2dx48c103ba2c928dd_25 + event_2bx7784b52277146866_3 - >= 0 - R142: - predicate_2dx48c103ba2c928dd_26 + event_2bx7784b52277146866_3 - >= 0 - R143: event_2bx7784b52277146866_3 - predicate_2dx48c103ba2c928dd_27 >= 0 - R144: - predicate_2dx48c103ba2c928dd_23 - predicate_2dx48c103ba2c928dd_24 - - predicate_2dx48c103ba2c928dd_25 - predicate_2dx48c103ba2c928dd_26 - + event_2bx7784b52277146866_3 - predicate_2dx48c103ba2c928dd_27 <= 0 - R145: - rho + y_28 - 20 predicate_2dx48c103ba2c928dd_28 <= 2 - R146: - rho + y_28 - 20 predicate_2dx48c103ba2c928dd_28 >= -18 - R147: - predicate_2dx48c103ba2c928dd_24 + event_2bx7784b52277146866_4 - >= 0 - R148: - predicate_2dx48c103ba2c928dd_25 + event_2bx7784b52277146866_4 - >= 0 - R149: - predicate_2dx48c103ba2c928dd_26 + event_2bx7784b52277146866_4 - >= 0 - R150: - predicate_2dx48c103ba2c928dd_27 + event_2bx7784b52277146866_4 - >= 0 - R151: event_2bx7784b52277146866_4 - predicate_2dx48c103ba2c928dd_28 >= 0 - R152: - predicate_2dx48c103ba2c928dd_24 - predicate_2dx48c103ba2c928dd_25 - - predicate_2dx48c103ba2c928dd_26 - predicate_2dx48c103ba2c928dd_27 - + event_2bx7784b52277146866_4 - predicate_2dx48c103ba2c928dd_28 <= 0 - R153: always_2bx29c2cf03abdaadd0_0 - event_2bx7784b52277146866_2 <= 0 - R154: always_2bx29c2cf03abdaadd0_0 - event_2bx7784b52277146866_3 <= 0 - R155: always_2bx29c2cf03abdaadd0_0 - event_2bx7784b52277146866_4 <= 0 - R156: always_2bx29c2cf03abdaadd0_0 - event_2bx7784b52277146866_2 - - event_2bx7784b52277146866_3 - event_2bx7784b52277146866_4 >= -2 - R157: rho + z_21 + 20 predicate_2bx150bb59745841544_21 >= 4 - R158: rho + z_21 + 20 predicate_2bx150bb59745841544_21 <= 24 - R159: rho + z_22 + 20 predicate_2bx150bb59745841544_22 >= 4 - R160: rho + z_22 + 20 predicate_2bx150bb59745841544_22 <= 24 - R161: rho + z_23 + 20 predicate_2bx150bb59745841544_23 >= 4 - R162: rho + z_23 + 20 predicate_2bx150bb59745841544_23 <= 24 - R163: rho + z_24 + 20 predicate_2bx150bb59745841544_24 >= 4 - R164: rho + z_24 + 20 predicate_2bx150bb59745841544_24 <= 24 - R165: rho + z_25 + 20 predicate_2bx150bb59745841544_25 >= 4 - R166: rho + z_25 + 20 predicate_2bx150bb59745841544_25 <= 24 - R167: rho + z_26 + 20 predicate_2bx150bb59745841544_26 >= 4 - R168: rho + z_26 + 20 predicate_2bx150bb59745841544_26 <= 24 - R169: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_21 - <= 0 - R170: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_22 - <= 0 - R171: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_23 - <= 0 - R172: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_24 - <= 0 - R173: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_25 - <= 0 - R174: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_26 - <= 0 - R175: always_2dx7e9697b6ff524b6d_0 - predicate_2bx150bb59745841544_21 - - predicate_2bx150bb59745841544_22 - predicate_2bx150bb59745841544_23 - - predicate_2bx150bb59745841544_24 - predicate_2bx150bb59745841544_25 - - predicate_2bx150bb59745841544_26 >= -5 - R176: - rho + z_21 - 20 predicate_2dx17f01b49409b1295_21 <= 3 - R177: - rho + z_21 - 20 predicate_2dx17f01b49409b1295_21 >= -17 - R178: - rho + z_22 - 20 predicate_2dx17f01b49409b1295_22 <= 3 - R179: - rho + z_22 - 20 predicate_2dx17f01b49409b1295_22 >= -17 - R180: - rho + z_23 - 20 predicate_2dx17f01b49409b1295_23 <= 3 - R181: - rho + z_23 - 20 predicate_2dx17f01b49409b1295_23 >= -17 - R182: - rho + z_24 - 20 predicate_2dx17f01b49409b1295_24 <= 3 - R183: - rho + z_24 - 20 predicate_2dx17f01b49409b1295_24 >= -17 - R184: - rho + z_25 - 20 predicate_2dx17f01b49409b1295_25 <= 3 - R185: - rho + z_25 - 20 predicate_2dx17f01b49409b1295_25 >= -17 - R186: - rho + z_26 - 20 predicate_2dx17f01b49409b1295_26 <= 3 - R187: - rho + z_26 - 20 predicate_2dx17f01b49409b1295_26 >= -17 - R188: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_21 - <= 0 - R189: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_22 - <= 0 - R190: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_23 - <= 0 - R191: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_24 - <= 0 - R192: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_25 - <= 0 - R193: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_26 + >= -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 - R194: always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_21 - - predicate_2dx17f01b49409b1295_22 - predicate_2dx17f01b49409b1295_23 - - predicate_2dx17f01b49409b1295_24 - predicate_2dx17f01b49409b1295_25 - - predicate_2dx17f01b49409b1295_26 >= -5 - R195: and_2bx43a2c068eac23333_0 - always_2dx778710aa24bf45ad_0 <= 0 - R196: and_2bx43a2c068eac23333_0 - always_2bx29c2cf03abdaadd0_0 <= 0 - R197: and_2bx43a2c068eac23333_0 - always_2dx7e9697b6ff524b6d_0 <= 0 - R198: and_2bx43a2c068eac23333_0 - always_2dx798ea4c82d31ac76_0 <= 0 - R199: and_2bx43a2c068eac23333_0 - always_2dx778710aa24bf45ad_0 - - always_2bx29c2cf03abdaadd0_0 - always_2dx7e9697b6ff524b6d_0 - - always_2dx798ea4c82d31ac76_0 >= -3 - formula_satisfaction: and_2bx43a2c068eac23333_0 = 1 + 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 @@ -430,23 +332,13 @@ Bounds -2 <= v_29 <= 3 -3 <= w_29 <= 3 Binaries - and_2bx43a2c068eac23333_0 always_2dx778710aa24bf45ad_0 + and_2dx5295e3d99f627fa8_0 always_2dx69bcdd71a3ff42e3_0 predicate_2dx22dd95ed78b4d217_0 predicate_2dx22dd95ed78b4d217_1 - predicate_2dx22dd95ed78b4d217_2 predicate_2dx22dd95ed78b4d217_3 - predicate_2dx22dd95ed78b4d217_4 predicate_2dx22dd95ed78b4d217_5 - predicate_2dx22dd95ed78b4d217_6 predicate_2dx22dd95ed78b4d217_7 - predicate_2dx22dd95ed78b4d217_8 predicate_2dx22dd95ed78b4d217_9 - predicate_2dx22dd95ed78b4d217_10 always_2bx29c2cf03abdaadd0_0 - event_2bx7784b52277146866_2 predicate_2dx48c103ba2c928dd_22 - predicate_2dx48c103ba2c928dd_23 predicate_2dx48c103ba2c928dd_24 - predicate_2dx48c103ba2c928dd_25 predicate_2dx48c103ba2c928dd_26 - event_2bx7784b52277146866_3 predicate_2dx48c103ba2c928dd_27 - event_2bx7784b52277146866_4 predicate_2dx48c103ba2c928dd_28 - always_2dx7e9697b6ff524b6d_0 predicate_2bx150bb59745841544_21 - predicate_2bx150bb59745841544_22 predicate_2bx150bb59745841544_23 - predicate_2bx150bb59745841544_24 predicate_2bx150bb59745841544_25 - predicate_2bx150bb59745841544_26 always_2dx798ea4c82d31ac76_0 - predicate_2dx17f01b49409b1295_21 predicate_2dx17f01b49409b1295_22 - predicate_2dx17f01b49409b1295_23 predicate_2dx17f01b49409b1295_24 - predicate_2dx17f01b49409b1295_25 predicate_2dx17f01b49409b1295_26 + 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 c84924d..7ed432d 100644 --- a/stl/test/stl2milp_test.py +++ b/stl/test/stl2milp_test.py @@ -31,8 +31,9 @@ # 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 <= 4) && G[21,26] (z >= 3)' +# 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 @@ -101,6 +102,15 @@ # 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() diff --git a/stl/test/stl_mpc.py b/stl/test/stl_mpc.py index 6515427..3e84fc3 100644 --- a/stl/test/stl_mpc.py +++ b/stl/test/stl_mpc.py @@ -32,8 +32,8 @@ # 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 >= 4) && G[0, 2] (z >= 1)' -formula = 'G[0,10] x >= 3 && G[12,15] x <= 1 && G[17, 24] x>= 4' +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]] @@ -52,7 +52,7 @@ print('AST:', str(ast)) -def stl_milp_solver(x_init, y_init, z_init, current_step, period): +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) @@ -112,10 +112,19 @@ def stl_milp_solver(x_init, y_init, z_init, current_step, period): 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') @@ -163,8 +172,9 @@ def stl_milp_solver(x_init, y_init, z_init, current_step, period): 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 = 30 - period = 25 + 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)] @@ -172,7 +182,7 @@ def main(): t = [i for i in range(steps + period)] for i in range(0, steps): - stl_milp_solver(x, y, z, i, period ) + stl_milp_solver(x, y, z, i, period, event) fig, axs = plt.subplots(3) fig.suptitle('subplots')