From 09868157a35c9310858b90092c13471251b2e201 Mon Sep 17 00:00:00 2001 From: Cristian-Ioan Vasile Date: Sat, 16 May 2020 09:28:54 -0400 Subject: [PATCH 1/2] Made time specification parameters integers. --- stl/stl2milp.py | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/stl/stl2milp.py b/stl/stl2milp.py index 920704c..057565f 100644 --- a/stl/stl2milp.py +++ b/stl/stl2milp.py @@ -114,10 +114,9 @@ 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)) @@ -125,11 +124,9 @@ def eventually(self, formula, z, t): 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)) @@ -140,7 +137,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) @@ -173,4 +170,4 @@ def until(self, formula, z, t): + sum(z_children_left[:t+a+k+1])) self.model.addConstr(z >= z_conj) - self.model.addConstr(z <= sum(z_aux)) \ No newline at end of file + self.model.addConstr(z <= sum(z_aux)) From 3f3c1fbbc74c2ec59eacfb69bab94d733c529486 Mon Sep 17 00:00:00 2001 From: Cristian-Ioan Vasile Date: Sat, 16 May 2020 09:34:11 -0400 Subject: [PATCH 2/2] Updated license notices. --- stl/stl.g4 | 3 ++- stl/stl.py | 3 ++- stl/stl2milp.py | 3 ++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/stl/stl.g4 b/stl/stl.g4 index 5ab2f23..8a05c5b 100644 --- a/stl/stl.g4 +++ b/stl/stl.g4 @@ -2,8 +2,9 @@ grammar stl; @header { ''' - Copyright (C) 2015-2018 Cristian Ioan Vasile + 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. ''' } diff --git a/stl/stl.py b/stl/stl.py index 3e02419..68ab383 100644 --- a/stl/stl.py +++ b/stl/stl.py @@ -1,6 +1,7 @@ ''' - Copyright (C) 2015-2018 Cristian Ioan Vasile + 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. ''' diff --git a/stl/stl2milp.py b/stl/stl2milp.py index 057565f..66966fb 100644 --- a/stl/stl2milp.py +++ b/stl/stl2milp.py @@ -1,6 +1,7 @@ ''' - Copyright (C) 2018 Cristian Ioan Vasile + Copyright (C) 2018-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. '''