Skip to content

Stl_mpc #24

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
nightkidwyxc wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Stl_mpc #24

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a134797
First attempt for stl-mpc
nightkidwyxc Mar 23, 2021
afa765e
Modify the algrithom to get better prediction for next step for stl-mpc
nightkidwyxc Apr 20, 2021
1c20194
Get some commets for stl-mpc
nightkidwyxc Apr 20, 2021
596a0f6
Add event cases
nightkidwyxc May 14, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions stl/stl.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
211 changes: 211 additions & 0 deletions stl/test/model_test.lp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,211 @@
\ Model STL formula: ((G[0.0, 2.0] (x >= 3.0)) && (F[0.0, 6.0] (y >= 5.0)) && (G[0.0, 2.0] (z >= 1.0)))
\ LP format - for model browsing. Use MPS format to capture full model detail.
Minimize
- rho + 0 u_0 + 0 v_0 + 0 w_0 + 0 u_1 + 0 v_1 + 0 w_1 + 0 u_2 + 0 v_2
+ 0 w_2 + 0 u_3 + 0 v_3 + 0 w_3 + 0 u_4 + 0 v_4 + 0 w_4 + 0 u_5 + 0 v_5
+ 0 w_5 + 0 u_6 + 0 v_6 + 0 w_6 + 0 u_14 + 0 v_14 + 0 w_14
Subject To
R0: x_0 = 4
R1: y_0 = 1
R2: z_0 = -1
R3: x_1 = 1
R4: y_1 = 2
R5: z_1 = -1
R6: x_2 = 3
R7: y_2 = 5
R8: z_2 = -1
R9: x_3 = 0
R10: y_3 = 3
R11: z_3 = -4
R12: x_4 = 2
R13: y_4 = 1
R14: z_4 = -1
R15: x_5 = 2
R16: y_5 = -1
R17: z_5 = 2
R18: x_6 = 1
R19: y_6 = 1
R20: z_6 = 1
R21: x_7 = 0
R22: y_7 = -1
R23: z_7 = 2
R24: - x_7 - u_7 + x_8 = 0
R25: - y_7 - v_7 + y_8 = 0
R26: - z_7 - w_7 + z_8 = 0
R27: - x_8 - u_8 + x_9 = 0
R28: - y_8 - v_8 + y_9 = 0
R29: - z_8 - w_8 + z_9 = 0
R30: - x_9 - u_9 + x_10 = 0
R31: - y_9 - v_9 + y_10 = 0
R32: - z_9 - w_9 + z_10 = 0
R33: - x_10 - u_10 + x_11 = 0
R34: - y_10 - v_10 + y_11 = 0
R35: - z_10 - w_10 + z_11 = 0
R36: - x_11 - u_11 + x_12 = 0
R37: - y_11 - v_11 + y_12 = 0
R38: - z_11 - w_11 + z_12 = 0
R39: - x_12 - u_12 + x_13 = 0
R40: - y_12 - v_12 + y_13 = 0
R41: - z_12 - w_12 + z_13 = 0
R42: - x_13 - u_13 + x_14 = 0
R43: - y_13 - v_13 + y_14 = 0
R44: - z_13 - w_13 + z_14 = 0
R45: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 <= 3
R46: - rho + x_0 - 20 predicate_2dx22dd95ed78b4d217_0 >= -17
R47: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 <= 3
R48: - rho + x_1 - 20 predicate_2dx22dd95ed78b4d217_1 >= -17
R49: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 <= 3
R50: - rho + x_2 - 20 predicate_2dx22dd95ed78b4d217_2 >= -17
R51: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_0 <= 0
R52: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_1 <= 0
R53: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_2 <= 0
R54: always_2dx69bcdd71a3ff42e3_0 - predicate_2dx22dd95ed78b4d217_0
- predicate_2dx22dd95ed78b4d217_1 - predicate_2dx22dd95ed78b4d217_2
>= -2
R55: - rho + y_0 - 20 predicate_2bx2516753055d0b842_0 <= 5
R56: - rho + y_0 - 20 predicate_2bx2516753055d0b842_0 >= -15
R57: - rho + y_1 - 20 predicate_2bx2516753055d0b842_1 <= 5
R58: - rho + y_1 - 20 predicate_2bx2516753055d0b842_1 >= -15
R59: - rho + y_2 - 20 predicate_2bx2516753055d0b842_2 <= 5
R60: - rho + y_2 - 20 predicate_2bx2516753055d0b842_2 >= -15
R61: - rho + y_3 - 20 predicate_2bx2516753055d0b842_3 <= 5
R62: - rho + y_3 - 20 predicate_2bx2516753055d0b842_3 >= -15
R63: - rho + y_4 - 20 predicate_2bx2516753055d0b842_4 <= 5
R64: - rho + y_4 - 20 predicate_2bx2516753055d0b842_4 >= -15
R65: - rho + y_5 - 20 predicate_2bx2516753055d0b842_5 <= 5
R66: - rho + y_5 - 20 predicate_2bx2516753055d0b842_5 >= -15
R67: - rho + y_6 - 20 predicate_2bx2516753055d0b842_6 <= 5
R68: - rho + y_6 - 20 predicate_2bx2516753055d0b842_6 >= -15
R69: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_0 >= 0
R70: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_1 >= 0
R71: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_2 >= 0
R72: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_3 >= 0
R73: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_4 >= 0
R74: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_5 >= 0
R75: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_6 >= 0
R76: event_2dx53fa3e0ebe26c54b_0 - predicate_2bx2516753055d0b842_0
- predicate_2bx2516753055d0b842_1 - predicate_2bx2516753055d0b842_2
- predicate_2bx2516753055d0b842_3 - predicate_2bx2516753055d0b842_4
- predicate_2bx2516753055d0b842_5 - predicate_2bx2516753055d0b842_6
<= 0
R77: - rho + z_0 - 20 predicate_2dx33b18e258c171243_0 <= 1
R78: - rho + z_0 - 20 predicate_2dx33b18e258c171243_0 >= -19
R79: - rho + z_1 - 20 predicate_2dx33b18e258c171243_1 <= 1
R80: - rho + z_1 - 20 predicate_2dx33b18e258c171243_1 >= -19
R81: - rho + z_2 - 20 predicate_2dx33b18e258c171243_2 <= 1
R82: - rho + z_2 - 20 predicate_2dx33b18e258c171243_2 >= -19
R83: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_0 <= 0
R84: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_1 <= 0
R85: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_2 <= 0
R86: always_2dx7c33fe6ba9ff9e2b_0 - predicate_2dx33b18e258c171243_0
- predicate_2dx33b18e258c171243_1 - predicate_2dx33b18e258c171243_2
>= -2
R87: and_2dx5295e3d99f627fa8_0 - always_2dx69bcdd71a3ff42e3_0 <= 0
R88: and_2dx5295e3d99f627fa8_0 - event_2dx53fa3e0ebe26c54b_0 <= 0
R89: and_2dx5295e3d99f627fa8_0 - always_2dx7c33fe6ba9ff9e2b_0 <= 0
R90: and_2dx5295e3d99f627fa8_0 - always_2dx69bcdd71a3ff42e3_0
- event_2dx53fa3e0ebe26c54b_0 - always_2dx7c33fe6ba9ff9e2b_0 >= -2
formula_satisfaction: and_2dx5295e3d99f627fa8_0 = 1
Bounds
-infinity <= rho <= 999
-4 <= x_0 <= 5
-4 <= y_0 <= 5
-4 <= z_0 <= 5
-3 <= u_0 <= 2
-2 <= v_0 <= 3
-3 <= w_0 <= 3
-4 <= x_1 <= 5
-4 <= y_1 <= 5
-4 <= z_1 <= 5
-3 <= u_1 <= 2
-2 <= v_1 <= 3
-3 <= w_1 <= 3
-4 <= x_2 <= 5
-4 <= y_2 <= 5
-4 <= z_2 <= 5
-3 <= u_2 <= 2
-2 <= v_2 <= 3
-3 <= w_2 <= 3
-4 <= x_3 <= 5
-4 <= y_3 <= 5
-4 <= z_3 <= 5
-3 <= u_3 <= 2
-2 <= v_3 <= 3
-3 <= w_3 <= 3
-4 <= x_4 <= 5
-4 <= y_4 <= 5
-4 <= z_4 <= 5
-3 <= u_4 <= 2
-2 <= v_4 <= 3
-3 <= w_4 <= 3
-4 <= x_5 <= 5
-4 <= y_5 <= 5
-4 <= z_5 <= 5
-3 <= u_5 <= 2
-2 <= v_5 <= 3
-3 <= w_5 <= 3
-4 <= x_6 <= 5
-4 <= y_6 <= 5
-4 <= z_6 <= 5
-3 <= u_6 <= 2
-2 <= v_6 <= 3
-3 <= w_6 <= 3
-4 <= x_7 <= 5
-4 <= y_7 <= 5
-4 <= z_7 <= 5
-3 <= u_7 <= 2
-2 <= v_7 <= 3
-3 <= w_7 <= 3
-4 <= x_8 <= 5
-4 <= y_8 <= 5
-4 <= z_8 <= 5
-3 <= u_8 <= 2
-2 <= v_8 <= 3
-3 <= w_8 <= 3
-4 <= x_9 <= 5
-4 <= y_9 <= 5
-4 <= z_9 <= 5
-3 <= u_9 <= 2
-2 <= v_9 <= 3
-3 <= w_9 <= 3
-4 <= x_10 <= 5
-4 <= y_10 <= 5
-4 <= z_10 <= 5
-3 <= u_10 <= 2
-2 <= v_10 <= 3
-3 <= w_10 <= 3
-4 <= x_11 <= 5
-4 <= y_11 <= 5
-4 <= z_11 <= 5
-3 <= u_11 <= 2
-2 <= v_11 <= 3
-3 <= w_11 <= 3
-4 <= x_12 <= 5
-4 <= y_12 <= 5
-4 <= z_12 <= 5
-3 <= u_12 <= 2
-2 <= v_12 <= 3
-3 <= w_12 <= 3
-4 <= x_13 <= 5
-4 <= y_13 <= 5
-4 <= z_13 <= 5
-3 <= u_13 <= 2
-2 <= v_13 <= 3
-3 <= w_13 <= 3
-4 <= x_14 <= 5
-4 <= y_14 <= 5
-4 <= z_14 <= 5
-3 <= u_14 <= 2
-2 <= v_14 <= 3
-3 <= w_14 <= 3
Binaries
and_2dx5295e3d99f627fa8_0 always_2dx69bcdd71a3ff42e3_0
predicate_2dx22dd95ed78b4d217_0 predicate_2dx22dd95ed78b4d217_1
predicate_2dx22dd95ed78b4d217_2 event_2dx53fa3e0ebe26c54b_0
predicate_2bx2516753055d0b842_0 predicate_2bx2516753055d0b842_1
predicate_2bx2516753055d0b842_2 predicate_2bx2516753055d0b842_3
predicate_2bx2516753055d0b842_4 predicate_2bx2516753055d0b842_5
predicate_2bx2516753055d0b842_6 always_2dx7c33fe6ba9ff9e2b_0
predicate_2dx33b18e258c171243_0 predicate_2dx33b18e258c171243_1
predicate_2dx33b18e258c171243_2
End
Loading