Skip to content

Fix/integer time units #5

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

Merged
wasserfeder merged 3 commits into from
Jul 12, 2020
Merged

Fix/integer time units #5

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0986815
Made time specification parameters integers.
wasserfeder May 16, 2020
3f3c1fb
Updated license notices.
wasserfeder May 16, 2020
8253567
Merge branch 'master' into fix/integer_time_units
wasserfeder Jul 9, 2020
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
3 changes: 2 additions & 1 deletion stl/stl.g4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,9 @@ grammar stl;

@header {
'''
Copyright (C) 2015-2018 Cristian Ioan Vasile <cvasile@mit.edu>
Copyright (C) 2015-2020 Cristian Ioan Vasile <cvasile@lehigh.edu>
Hybrid and Networked Systems (HyNeSs) Group, BU Robotics Lab, Boston University
Explainable Robotics Lab, Lehigh University
See license.txt file for license information.
'''
}
Expand Down
3 changes: 2 additions & 1 deletion stl/stl.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
'''
Copyright (C) 2015-2018 Cristian Ioan Vasile <cvasile@bu.edu>
Copyright (C) 2015-2020 Cristian Ioan Vasile <cvasile@lehigh.edu>
Hybrid and Networked Systems (HyNeSs) Group, BU Robotics Lab, Boston University
Explainable Robotics Lab, Lehigh University
See license.txt file for license information.
'''

Expand Down
16 changes: 7 additions & 9 deletions stl/stl2milp.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
'''
Copyright (C) 2018 Cristian Ioan Vasile <cvasile@mit.edu>
Copyright (C) 2018-2020 Cristian Ioan Vasile <cvasile@lehigh.edu>
Hybrid and Networked Systems (HyNeSs) Group, BU Robotics Lab, Boston University
Explainable Robotics Lab, Lehigh University
See license.txt file for license information.
'''

Expand Down Expand Up @@ -122,22 +123,19 @@ def disjunction(self, formula, z, t):
def eventually(self, formula, z, t):
'''Adds an eventually to the model.'''
assert formula.op == Operation.EVENT
a, b = formula.low, formula.high
a, b = int(formula.low), int(formula.high)
child = formula.child
print "a=%d,b=%d"%(a,b)
z_children = [self.to_milp(child, t + tau) for tau in range(int(a), int(b+1))]
z_children = [self.to_milp(child, t + tau) for tau in range(a, b+1)]
for z_child in z_children:
self.model.addConstr(z >= z_child)
self.model.addConstr(z <= sum(z_children))

def globally(self, formula, z, t):
'''Adds a globally to the model.'''
assert formula.op == Operation.ALWAYS
a, b = formula.low, formula.high
# print "a=%d,b=%d,t=%d"%(a,b,t)
a, b = int(formula.low), int(formula.high)
child = formula.child
z_children = [self.to_milp(child, t + tau) for tau in range(int(a), int(b+1))]
# print len(z_children)
z_children = [self.to_milp(child, t + tau) for tau in range(a, b+1)]
for z_child in z_children:
self.model.addConstr(z <= z_child)
self.model.addConstr(z >= 1 - len(z_children) + sum(z_children))
Expand All @@ -148,7 +146,7 @@ def until(self, formula, z, t):

raise NotImplementedError #TODO: under construction

a, b = formula.low, formula.high
a, b = int(formula.low), int(formula.high)
z_children_left = [self.to_milp(formula.left, tau)
for tau in range(t, t+b+1)]
z_children_right = [self.to_milp(formula.right, tau)
Expand Down