route_planning.py

Documentation for the functions in route_planning.py.

add_proposition_constraints_pulp(mpulp, stl_milp, ts, ast, capabilities, agent_classes, bound, vtype='Integer', num_agents=1000)

Adds the proposition constraints. First, the proposition-state variables are defined such that capabilities are not double booked. Second, contraints are added such that proposition are satisfied as best as possible. The variables in the MILP encoding of the STL formula are used for the encoding as the minimizers of over proposition-state variables.

This function uses the PuLP modeling language rather than Gurobi directly.

• The PuLP model variable.

• The MILP encoding of the STL formula obtained from the CaTL specification.

• The transition system specifying the environment.

• The AST of the CaTL specification formula.

• Dictionary of capability encoding that maps capabilities to binary words

represented as integers. - The agent classes given as a dictionary from frozen sets of capabilities to bitmaps (integers). - Time bound. - Variable type (default: integer).’F[0, 10] T(2, orange, {(UV, 1), (Mo, 1)})’

add_system_constraints_pulp(mpulp, ts, agent_classes, capability_distribution, bound)

Computes the constraints that capture the system dynamics.

• The PuLP model object.

• The transition system specifying the environment.

• The agent classes given as a dictionary from frozen sets of capabilities

to bitmaps (integers). - The initial distribution of capabilities at each state. - Time bound.

Note

The initial time constraints

z_{state}_g_0 = eta_{state}_g

is equivalent to

sum_{e=(u, v) in T} z_e_g_W(e) = eta_{state}_g

because of the definition of the team state at TS states, where eta_{state}_g is the number of agents of class g at state {state} at time 0.

computeRobustnessUpperBound(ts, agents, formula)

Computes a loose upper bound on the robustness value.

The robustness value measures whether there are enough agents to satisfy the temporal logic specification in the given transition system. A positive robustness value indicates there are more than enough required agents to satisfy the formula. A negative robustness value indicates that there are not enough required agents to satisfy the formula.

This function computes an upper bound on the robustness value for a given transition system (TS), set of agents, and CaTL formula. This upper bound can be used as a “sanity check” to test if the formula is infeasible for the given TS and set of agents. If the upper bound is negative, then the problem is infeasible. If the upper bound is positive, then it is possible that the problem is feasible.

If the upper bound is negative, there is no point in solving the associated MILP. The problem is infeasible.

Note: This function does not take into account the travel time between regions in the TS.

Parameters

• ts – The transition system

• agents (list) – List of agents in the system. Each agent has the form (initial_state, {capability1, capability2,...}).

• formula – Either a string or a catl.CATLFormula object containing the formula. If a string, it is converted into a catl.CATLFormula object by calling formula = CATLFormula.from_formula(formula).

Returns

Upper bound on the robustness value.

Return type

(float)

compute_agent_classes(agents, capabilities)

Computes the set of agent types w.r.t. capabilities.

Parameters

• agents (list) – List of agents, where agents are tuples (q, cap), q is the initial state of the agent, and cap is the set of capabilities. Agents’ identifiers are their indices in the list.

• capabilities (dict) – Dictionary of capability class encoding that maps capability classes to binary words represented as integers.

Returns

Dictionary of agent capability classes that maps frozen (immutable) sets of capabilities to the binary words encoding the corresponding capability classes.

Return type

(dict)

compute_capability_bitmap(agents)

Computes a bitmap encoding of agents’ capabilities. Each capability is associated with a bit in a binary word of length equal to the number of capabilities.

Parameters

agents (list) –

List containing agent information. The iith entry is a tuple (q, cap) corresponding to the iith agent, where q is the initial state of the agent and cap is the set of all capabilities that agent has.

An example of a valid agents list:

agents = [('q1', {'VIS'}), ('q3', {'LID'}), ('q7', {'LID','IR'})]

Returns

Dictionary mapping capabilities to integers representing the binary words for the capabilities.

Return type

(dict)

compute_initial_capability_distribution(ts, agents, capabilities)

Computes the initial number of agents of each class at each state. Input —– - The transition system specifying the environment. - List of agents, where agents are tuples (q, cap), q is the initial state of the agent, and cap is the set of capabilities. Agents’ identifiers are their indices in the list. - Dictionary of capability encoding that maps capabilities to binary words represented as integers. Output —— Dictionary from states to distribution of agents from each class. The distribution is a list of length equal to the number of capabilities, and each element is the number of agents of having those capabilities (a class).

create_system_variables_pulp(mpulp, ts, agent_classes, bound, vtype='Integer', num_agents=1000, regularize=False, alpha=0.5)

Creates the state and transition variables associated with the given transition system using the PuLP framework.

The state variables are z_{state}_{cap}_k, where {state} is a node in the TS graph, {cap} is a capability class encoded as an integer, and k is the time step.

The transition variables are z_{state1}_{state2}_{cap}_k, where {state1} and {state2} define the transition, {cap} is a capability class encoded as an integer, and k is the time step.

• The PuLP model object.

• The transition system specifying the environment.

• The agent classes given as a dictionary from frozen sets of capabilities

to bitmaps (integers). - Time bound. - Variable type (default: integer).

Note

Data structure holding the variables is a list of list of variables, e.g.,

d[‘vars’][k][g] is the z_{q/e}_bitmap(g)_k

where d is the dictionary of attributes for a node q or an edge e in the TS, g is an agent class (frozen set of capabilities), bitmap(g) is the binary encoding of g as an integer, and k is the time step. Also, d[‘vars’] is a list of length `bound+1’, d[‘vars’][k] is a dictionary from frozen sets to gurobi variables.

extract_propositions(ts, ast)

Returns the set of propositions in the formula, and checks that it is included in the transitions system.

• The transition system specifying the environment.

• The AST of the CaTL specification formula.

Set of propositions in the specification formula.

generate_MILP_problems(ts, agents, formula, bound=None, file_name=None, robust=False, regularize=False, alpha=0.5, upperBound=False, replan_grave=None, verbose=True, compress_files=True)

Similar to route_planning(), but simply generates the MILP .lp / .mps problem files without actually solving them.

Parameters

• inputs –

• ts –

• agents –

• formula (str) –

• bound –

• file_name (str) –

• replan_req (bool) –

• robust (bool) –

• regularize (bool) –

• alpha (float) –

• upperBound (bool) –

• load_previous –

• solver_name (str) –

• compute_IIS (bool) –

• verbose –

• compress_files (bool) –

• solver_time_limit (float) – Time limit on the MILP solution process. The MILP will stop after this amount of time. If no time limit is specified, the MILP will run to completion.

Returns

Tuple containing the following elements:

• mpulp: PuLP LpProblem object containing the (solved) MILP corresponding to the planning problem

• replan_data: Object containing the following fields:

  • TODO: [INSERT HERE]

Return type

(tuple)

• The transition system specifying the environment.

• List of agents, where agents are tuples (q, cap), q is the initial state

of the agent, and cap is the set of capabilities. Agents’ identifiers are their indices in the list. - The CaTL specification formula. - The time bound used in the encoding (default: computed from CaTL formula).

TODO: TBD

get_ub(formula, ts, capDict)

Uses recursive relationships to compute the excess capacity of the formula with respect to the team

route_planning(inputs, ts, agents, formula, bound=None, file_name=None, replan_req=False, robust=False, regularize=False, alpha=0.5, upperBound=False, load_previous=False, solver=None, compute_IIS=True, verbose=True, compress_files=True, solver_time_limit=None, solver_threads=None)

Performs route planning for agents agents moving in a transition system ts such that the CaTL specification formula is satisfied.

Parameters

• inputs –

• ts –

• agents –

• formula (str) –

• bound –

• file_name (str) –

• replan_req (bool) –

• robust (bool) –

• regularize (bool) –

• alpha (float) –

• upperBound (bool) –

• load_previous –

• solver_name (str) –

• compute_IIS (bool) –

• verbose –

• compress_files (bool) –

• solver_time_limit (float) – Time limit on the MILP solution process. The MILP will stop after this amount of time. If no time limit is specified, the MILP will run to completion.

Returns

Tuple containing the following elements:

• mpulp: PuLP LpProblem object containing the (solved) MILP corresponding to the planning problem

• replan_data: Object containing the following fields:

  • TODO: [INSERT HERE]

Return type

(tuple)

• The transition system specifying the environment.

• List of agents, where agents are tuples (q, cap), q is the initial state

of the agent, and cap is the set of capabilities. Agents’ identifiers are their indices in the list. - The CaTL specification formula. - The time bound used in the encoding (default: computed from CaTL formula).

TODO: TBD

suppress_output(func)

Prevents a function from printing output to terminal.

Redirects the output to /dev/null. Used to suppress the output of the optimization solvers.