Refine the partition and establish transitions based on reachability analysis.

Reference

[NOTM12]

See Also

prop2partition.pwa_partition, prop2partition.part2convex

Parameters:

• part - PropPreservingPartition object
• ssys - LtiSysDyn or PwaSysDyn object
• N - horizon length
• min_cell_volume - the minimum volume of cells in the resulting partition.
• closed_loop - boolean indicating whether the `closed loop` algorithm should be used. default True.
• conservative - if true, force sequence in reachability analysis to stay inside starting cell. If false, safety is ensured by keeping the sequence inside a convexified version of the original proposition preserving cell.
• max_num_poly - maximum number of polytopes in a region to use in reachability analysis.
• use_all_horizon - in closed loop algorithm: if we should look for reachability also in less than N steps.
• trans_length - the number of polytopes allowed to cross in a transition. a value of 1 checks transitions only between neighbors, a value of 2 checks neighbors of neighbors and so on.
• remove_trans - if True, remove found transitions between non-neighbors.
• abs_tol - maximum volume for an "empty" polytope
• plotit (boolean, default = False) - plot partitioning as it evolves
• save_img (boolean, default = False) - save snapshots of partitioning to PDF files, requires plotit=True
• cont_props (list of Polytope) - continuous propositions to plot

Returns: AbstractPwa

default False.

UNDER DEVELOPMENT; function signature may change without notice. Calling will result in NotImplementedError.

Parallel implementation of discretize_switched.

Uses the multiprocessing package.

Abstract switched dynamics over given partition.

Parameters:

• hybrid_sys (SwitchedSysDyn) - dynamics of switching modes
• disc_params (dict (keyed by mode) of dicts.) - discretization parameters passed to discretize for each mode. See discretize for details.
• plot (bool) - save partition images
• show_ts, only_adjacent - options for AbstractPwa.plot.
• ppp (PropPreservingPartition)

Returns: AbstractSwitched

abstracted dynamics, some attributes are dict keyed by mode

Construct merged transitions.

Parameters:

• abstr (dict of AbstractPwa)
• merged_abstr (AbstractSwitched)

Find which transitions are feasible in given mode.

Used for the candidate transitions of the merged partition.

Returns: scipy.sparse.lil_matrix

LOGTIME in #processors parallel merging.

Assuming sufficient number of processors.

UNDER DEVELOPMENT; function signature may change without notice. Calling will result in NotImplementedError.

Merge multiple abstractions.

Parameters:

• abstractions (dict of AbstractPwa) - keyed by mode

Returns:

(merged_abstraction, ap_labeling) where:

• merged_abstraction: AbstractSwitched
• ap_labeling: dict

Merge an Abstraction with the current partition iterate.

Parameters:

• old_regions (list of Region) - A list of Region that is from either:
  1. The ppp of the first (initial) AbstractPwa to be merged.
  2. A list of already-merged regions
• ab2 (AbstractPwa) - Abstracted piecewise affine dynamics to be merged into the
• cur_mode (tuple) - mode to be merged
• prev_modes (list of tuple) - list of modes that have already been merged together
• old_parents (dict of modes to list of region indices in list old_regions or dict of region indices to regions in original ppp for that mode) - dict of modes that have already been merged to dict of indices of new regions to indices of regions
• old_ap_labeling (dict of tuples to sets) - dict of states of already-merged modes to sets of propositions for each state

Returns:

the following:

• new_list, list of new regions
• parents, same as input param old_parents, except that it includes the mode that was just merged and for list of regions in return value new_list
• ap_labeling, same as input param old_ap_labeling, except that it includes the mode that was just merged.