Skip to content

Commit

Permalink
add docstrings for stl_toolkit code
Browse files Browse the repository at this point in the history
  • Loading branch information
prathgan committed Jul 26, 2019
1 parent 8e0219f commit 57049f5
Show file tree
Hide file tree
Showing 8 changed files with 49 additions and 19 deletions.
11 changes: 11 additions & 0 deletions coastl/stl_toolkit/stl_constraints.py
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
from .utilities.simple_utilities import remove_gurobi_log, parentheses_match

def create_constraints(node, m=None, maximize_vars=None, minimize_vars=None, remove_log=False, console_log=True, M=10**4, E=10**(-4)):
"""Returns gurobi MILP optimization model to solve for all values binary and continuous variables in STL tree 'node'"""
if m is None:
m = Model("solver")
m.Params.LogToConsole = int(console_log)
Expand Down Expand Up @@ -31,6 +32,7 @@ def create_constraints(node, m=None, maximize_vars=None, minimize_vars=None, rem
return m

def topmost_constr(node, m):
"""Adds constraint for root logic binary variable must equal 1"""
if node.parent is None:
bin_name = get_bin_name(node)
exec(bin_name+"= m.addVar(vtype=GRB.BINARY, name='"+bin_name+"_root')")
Expand All @@ -40,6 +42,7 @@ def topmost_constr(node, m):
return m

def not_constr(node, m):
"""Adds constraint for not ('~') logic"""
self_bin_name = get_bin_name(node)
child1_bin_name = get_bin_name(node.child1)
times = list(range(handle_no_range(node).range_start, handle_no_range(node).range_end+1))
Expand All @@ -65,6 +68,7 @@ def not_constr(node, m):
return m

def and_constr(node, m):
"""Adds constraints for and ('&&') logic"""
self_bin_name = get_bin_name(node)
child1_bin_name = get_bin_name(node.child1)
child2_bin_name = get_bin_name(node.child2)
Expand Down Expand Up @@ -95,6 +99,7 @@ def and_constr(node, m):
return m

def or_constr(node, m):
"""Adds constraints for or ('||') logic"""
self_bin_name = get_bin_name(node)
child1_bin_name = get_bin_name(node.child1)
child2_bin_name = get_bin_name(node.child2)
Expand Down Expand Up @@ -125,6 +130,7 @@ def or_constr(node, m):
return m

def g_constr(node, m):
"""Adds constraints for globally ('G[start,end]') temporal modifier"""
bin_name = get_bin_name(node)
create_new_vars = False
if (not node.gurobi_vars) or create_new_vars:
Expand All @@ -151,6 +157,7 @@ def g_constr(node, m):
return m

def f_constr(node, m):
"""Adds constraints for eventually ('F[start,end]') temporal modifier"""
bin_name = get_bin_name(node)
create_new_vars = False
if (not node.gurobi_vars) or create_new_vars:
Expand All @@ -177,6 +184,7 @@ def f_constr(node, m):
return m

def leq_constr(node, m, M, E, maximize_vars, minimize_vars):
"""Adds constraints for Atomic Predicate nodes with less than or equal to ('<=') logical operator"""
self_bin_name = get_bin_name(node)
times = list(range(handle_no_range(node).range_start, handle_no_range(node).range_end+1))
isolated_exp_orig = isolate_0(node)
Expand Down Expand Up @@ -209,4 +217,7 @@ def leq_constr(node, m, M, E, maximize_vars, minimize_vars):
return m

def geq_constr(node, m):
"""Adds constraints for Atomic Predicate nodes with greater than or equal to ('>=') logical operator
NOTE: not implemented because convention is to write k<=x instead of x>=k
"""
return m
6 changes: 6 additions & 0 deletions coastl/stl_toolkit/stl_constraints_helpers.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
import re

def get_bin_name(inp):
"""Returns corrected name of binary variable for an stl_node, removes disruptive chars"""
alphaDict = {'0':'zero','1':'one','2':'two','3':'three','4':'four','5':'five','6':'six','7':'seven','8':'eight','9':'nine'}
name = ""
if isinstance(inp, str):
Expand Down Expand Up @@ -30,26 +31,30 @@ def get_bin_name(inp):
return name

def replace_operators(str):
"""Returns string with mathematical operators put back"""
str = str.replace('_p_','+')
str = str.replace('_m_','-')
str = str.replace('_t_','*')
str = str.replace('_d_','/')
return str

def remove_operators(str):
"""Returns string with mathematical operators removed"""
str = str.replace('+','')
str = str.replace('-','')
str = str.replace('*','')
str = str.replace('/','')
return str

def handle_no_range(node):
"""Returns stl_node with range set to [0,0] if not previously set"""
if node.range_start==None or node.range_end==None:
node.range_start = 0
node.range_end = 0
return node

def isolate_0(node):
"""Returns string s where 0<s is found from some expression n<k"""
exp = node.string_rep
parts = re.split("<=", exp)
if exp[-1].isalpha():
Expand All @@ -59,5 +64,6 @@ def isolate_0(node):


class SwitchDict(dict):
"""Dictionary subclass with dict.get(x), where x is not in dict, returning None"""
def __getitem__(self, key):
return dict.get(self, key)
31 changes: 15 additions & 16 deletions coastl/stl_toolkit/stl_node.py
Original file line number Diff line number Diff line change
@@ -1,21 +1,20 @@
class Node(object):

"""
Constructs node to be used in tree representing expression of signal temporal logical.
Parameters
----------
parent: pointer to the object of parent of this node
child1: pointer to the object of child1; points to anterior requirement of 'until' logic
child2: pointer to the object of child2; points to posterior condition of 'until' logic
type: part of logic which this node represents; logic (0) or predicate (1)
logic: logic operator which which this node represents, null if predicate node
vars: variables which this node pertains to
range_start: start of range for complex operator nodes, min range
range_end: end of range for complex operator nodes, max range
string_rep: string representation of node
"""
def __init__(self, parent, child1, child2, type, logic, vars, range_start, range_end, string_rep):
"""
Constructs node to be used in tree representing expression of signal temporal logical.
Parameters
----------
parent: pointer to the object of parent of this node
child1: pointer to the object of child1; points to anterior requirement of 'until' logic
child2: pointer to the object of child2; points to posterior condition of 'until' logic
type: part of logic which this node represents; logic (0) or predicate (1)
logic: logic operator which which this node represents, null if predicate node
vars: variables which this node pertains to
range_start: start of range for complex operator nodes, min range
range_end: end of range for complex operator nodes, max range
string_rep: string representation of node
"""
self.__parent = parent
self.__child1 = child1
if child1 is not None:
Expand Down
5 changes: 5 additions & 0 deletions coastl/stl_toolkit/stl_parsing.py
Original file line number Diff line number Diff line change
Expand Up @@ -25,18 +25,23 @@ def parse_logic(logic, range_start, range_end):
return AP_node(AP_info, logic, range_start, range_end)

def not_node(logic, start, end, range_start, range_end):
"""Returns STL tree with all children of '~', with '~' root'"""
return Node(None, parse_logic(logic[start+1:end], range_start, range_end), None, 0, "~", "", range_start, range_end, "~")

def g_node(logic, start, end, range_start, range_end):
"""Returns STL tree with all children of 'G[start,end]', with 'G' root"""
firstnum, secondnum, closep = square_parens(logic, 1)
return Node(None, parse_logic(logic[closep+1:], firstnum, secondnum), None, 0, "G", "", firstnum, secondnum, logic[0:closep+1])

def f_node(logic, start, end, range_start, range_end):
"""Returns STL tree with all children of 'f[start,end]', with 'F' root"""
firstnum, secondnum, closep = square_parens(logic, 1)
return Node(None, parse_logic(logic[closep+1:], firstnum, secondnum), None, 0, "F", "", firstnum, secondnum, logic[0:closep+1])

def con_node(andor_info, range_start, range_end):
"""Returns STL tree with all children of connecting operator ('&&' or '||')"""
return Node(None, parse_logic(andor_info[0], range_start, range_end), parse_logic(andor_info[2], range_start, range_end), 0, andor_info[1], "", range_start, range_end, andor_info[1])

def AP_node(AP_info,logic, range_start, range_end):
"""Returns STL tree Node with atomic predicate logic"""
return Node(None, None, None, 1, AP_info[1], remove_operators(AP_info[0]), range_start, range_end, logic)
5 changes: 5 additions & 0 deletions coastl/stl_toolkit/stl_parsing_helpers.py
Original file line number Diff line number Diff line change
Expand Up @@ -61,19 +61,22 @@ def connector(string):
return -1

def predicate(logic, start, end):
"""Returns information about predicate logic from string form if is predicate"""
is_p, equals_ind = is_predicate(logic, start, end)
if is_p:
return predicate_info(logic, start, equals_ind)
else:
return -1

def is_predicate(logic, start, end):
"""Returns T/F depending on if logic string is predicate and index of predicate operator (<=)"""
equals_ind = logic.index("=")
if equals_ind>end or equals_ind<start:
return True, equals_ind
return False, -1

def predicate_info(logic, start, equals_ind):
"""Returns information about predicate logic from string form"""
var = logic[0:equals_ind]
operator = "="
if var[-1]=="<" or var[-1]==">":
Expand All @@ -82,6 +85,7 @@ def predicate_info(logic, start, equals_ind):
return var, operator

def remove_operators(str):
"""Returns logic string with operators removed"""
str = str.replace('+','')
str = str.replace('-','')
str = str.replace('*','')
Expand All @@ -91,5 +95,6 @@ def remove_operators(str):
return str

class SwitchDict(dict):
"""Dictionary subclass with dict.get(x), where x is not in dict, returning None"""
def __getitem__(self, key):
return dict.get(self, key)
7 changes: 4 additions & 3 deletions coastl/stl_toolkit/stl_processing.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,15 +5,14 @@
from .utilities.simple_utilities import remove_gurobi_log, parentheses_match

def parse_stl(logic, remove_log=False):
"""
"""
"""Parses string of STL logic into an STL tree"""
if not parentheses_match(logic):
raise ValueError("Opening and closing brackets do not match, check '(' and ')'")
stl_tree = parse_logic(logic, None, None)
return stl_tree

def synthesize_stl(stl_node, ret_type=0, remove_log=False, console_log=True, maximize_vars=None, minimize_vars=None):
"""creates constraints and synthesizes solutions for variables in STL tree, returns optimized model"""
m = create_constraints(stl_node, maximize_vars=maximize_vars, minimize_vars=minimize_vars, console_log=console_log)
m.optimize()
if remove_log:
Expand All @@ -24,9 +23,11 @@ def synthesize_stl(stl_node, ret_type=0, remove_log=False, console_log=True, max
return m

def create_model_stl(stl_node, remove_log=False, console_log=True, maximize_vars=None, minimize_vars=None):
"""Creates constrained MILP gurobi model for STL tree"""
return create_constraints(stl_node, maximize_vars=maximize_vars, minimize_vars=minimize_vars, console_log=console_log)

def synthesize_stl(m, ret_type=0):
"""Synthesizes solutions for variables in model m by optimizing model"""
m.optimize()
if ret_type==1:
return m.getVars()
Expand Down
1 change: 1 addition & 0 deletions coastl/stl_toolkit/utilities/object_utilities.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,5 +7,6 @@ def display_tree(root):
print(root)

def display_model(m):
"""Display all varibles in gurobi model m with their values"""
for v in m.getVars():
print('%s %g' % (v.varName, v.x))
2 changes: 2 additions & 0 deletions coastl/stl_toolkit/utilities/simple_utilities.py
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ def remove_dups_stringlist(str):
return ','.join(arr)

def list_to_str(l, commas=True):
"""Converts list to string representation"""
if commas:
return ','.join(l)
else:
Expand All @@ -40,4 +41,5 @@ def parentheses_match(string):
return matched and len(verification_stack) == 0

def remove_gurobi_log():
"""Removes gurobi log after COASTL synthesis function has been run"""
os.remove("gurobi.log")

0 comments on commit 57049f5

Please sign in to comment.