API Reference

C++ Reference

class rocs::System

A system template class with typenames <T,X,U>.

This is a very basic system class, which can be derived as discrete-time, continuous-time, control systems or even systems without controls.

Subclassed by rocs::ContinuousTime, rocs::DTCntlSys< F >, rocs::DTSwSys< F >, rocs::DTSys< F >

Public Functions

inline System(const char *name, const double t, const int xd, const int ud = 1)

A Constructor.

Parameters

  • name – [in] The control problem name

  • t – [in] The sampling time

  • xd – [in] The state dimension

  • ud – [in] The input dimension (default=1)

inline void init_workspace(const ivec &ws)

Initialize the workspace.

Parameters

ws – [in] An interval vector

inline void init_workspace(const double lb[], const double ub[])

Initialize the workspace.

Parameters

  • lb – [in] An array of lower bound

  • ub – [in] An array of upper bound

inline void init_inputset(const double mu[], const double lb[], const double ub[])

Initialize the input set.

Parameters

  • mu – [in] An array of grid width

  • lb – [in] An array of lower bound

  • ub – [in] An array of upper bound

inline void init_inputset(vecRn &U)

Initialize the input set.

Parameters

U – [in] An array of selected input values (double)

Public Members

const char *_name

The system name

double _tau

The sampling time

int _xdim

The state dimension

ivec _workspace

The state space

int _udim

The input dimension

grid _ugrid

A grid of controls

template<typename F>
class DTCntlSys : public rocs::System

A discrete-time system class with real-valued controls.

template<typename F>
class DTSwSys : public rocs::System

A discrete-time switched system class with finite number of modes.

template<typename F>
class DTSys : public rocs::System

A discrete-time system class without controls.

template<typename F>
class CTCntlSys : public rocs::ContinuousTime

A continuous-time real-valued control system class.

template<typename F>
class CTSwSys : public rocs::ContinuousTime

A continuous-time switched system class.

template<typename F>
class CTSys : public rocs::ContinuousTime

A continuous-time system class without controls.

class rocs::params

A parameter class.

It controls the precision of reachable set computation for the flowTaylor class.

Public Functions

inline params()

A default Constructor.

Default: kmax=10, tol=0.01, alpha=0.5, beta=2,eps=0.01.

inline params(const int maxorder, const double tolerance, const double a, const double b)

A Constructor.

Parameters

  • maxorder – [in] The maximum order for Taylor expansion

  • tolerance – [in] The tolerance to determine the highest Taylor order

  • a – [in] alpha=a

  • b – [in] beta=b

Public Members

int kmax

The maximum order

double tol

The tolerance to determine the order k

double alpha

The error distribution factor

double beta

The bloating factor

double eps

The precision control parameter

template<typename F, typename S, typename P>
class rocs::flowTaylor

A Taylor model class for reachable set computation.

Public Functions

inline flowTaylor(const P u, params *pdata, const double T = 0.01, const double delta = 0, const double K = 1.0)

A Constructor for systems with controls.

inline flowTaylor(params *pdata, const double T = 0.01, const double delta = 0, const double K = 1.0)

A Constructor for systems without controls.

inline void construct_helper()

Pre-computation of some coefficients.

  • _parameters->eps: \((al*t)*del/(Ke^t)\)

  • _logdel1: \(\log((1-al)*del/K)\)

  • _logdel2: \(\log(t)\)

If K is known a priori, it should be set in constructor (see ).

inline void reset_taylor_coeffs()

Reset Taylor coefficients.

inline void init_taylor_coeffs(S *x)

Initialize Taylor coefficients.

inline void eval_taylor_coeffs(int order = 5)

Evaluate Taylor coefficients.

inline void print_taylor_coeffs()

Print Taylor coefficients.

inline double eval_taylorterm_bound(const ivec &x, int k = 10)

Evaluate the bound of Taylor terms for intervals.

Parameters

  • x – [in] A given interval

  • k – [in] The order of the Taylor model (=10 by default)

inline void eval_taylor_terms(ivec &y, const ivec &x, int k = 10)

Evaluate the Taylor model approximation of order k for intervals.

Parameters

  • y – [inout] An interval storing the evaluation results

  • x – [in] A given interval

  • k – [in] The order of the Taylor model (=10 by default)

inline void eval_taylor_kthterm(ivec &y, int k)

Evaluate the kth term (remainder) of the Taylor model.

Parameters

  • y – [inout] An interval storing the evaluation results

  • k – [in] The order of the Taylor model (=10 by default)

inline void eval_taylor_apriori(const ivec &x, int k = 10)

Evaluate the apriori enclosure of an interval ODE solution.

Parameters

  • x – [in] A given interval

  • k – [in] The order of the Taylor model (=10 by default)

inline bool compute_reachset_valid(ivec &y, const ivec &x)

Compute a valid reachable set.

Parameters

  • y – [inout] The reachable set in terms of interval

  • x – A given interval

Returns

1 if success and 0 otherwise

inline void compute_reachset_robust(ivec &y)

Compute a reachable set that satisfies robustly complete condition.

Parameters

y – [inout] The reachable set in terms of interval

inline bool reachset_robust(ivec &y, const ivec &x, double eps)

Consider robustness when width([x]) < epsilon.

Parameters

  • y – [inout] The reachable set in terms of interval

  • x – [in] A given interval

  • eps – [in] The given precision

Returns

1 if the reachable set is validated.

Public Members

double _tau

The continuous time horizon

double _delta

The bound of the perturbation

double _K

The maximum operator norm of jacobian (df^[i]/dx)

int _kbar

The valid order (locally updated)

double _wbar

The width of the enclosure (locally updated)

T<S> yterms[F::n]

Taylor terms of the solution (independent variables)

T<S> fterms[F::n]

The dependent variables of yterms

T<S> yrems[F::n]

The remainder (evaluated by apriori enclosure)

T<S> frems[F::n]

The dependent variables of yrems

params *_parameters

The pointer to a parameters class.

double _logdel2

The variables to store intermediate info

ivec _p

Sum of yterms[i]*[0,1]

ivec _u

yrem

ivec _xenc

The enclosure

Public Static Attributes

static const interval I = interval(0, 1)

The interval \([0,1]\).

static const interval II = interval(-1, 1)

The interval \([-1,1]\).

Friends

friend friend double eval_epsilon (flowTaylor &f)

Evaluate the local epsilon using the local a prior enclosure.

A friend function of the class flowTaylor.

Parameters

f – [in] A flowTaylor object

Returns

the local precision.

class rocs::CSolver

The specification-guided engine solver.

The state space of the system is partitioned on-the-fly, which results in a non-uniform partition. Control synthesis w.r.t. an LTL formula relies on its translation to a transition matrix _M. After control synthesis, the controller _ctlr is filled. Computational info is recorded in _fpiter and _timer.

Public Functions

template<typename system>
inline CSolver(system *ptrsys, size_t nProps = 0, BISECT bs = ABSMAX, size_t maxi = UINT_MAX)

A constructor.

Set the maximum number of iterations if you want the iteration to stop earlier.

Parameters

  • ptrsys – [in] The pointer to the system dynamics

  • nProps – [in] The number of propositions (default=0)

  • bs – [in] The bisection type (default=ABSMAX)

  • maxi – [in] The maximum number of iterations (default=UINT_MAX)

void set_M(const std::vector<UintSmall> &outedge)

Set the vector _M.

Construct with relative subdivision.

Parameters

  • ptrsys – the pointer to the system dynamics.

  • maxi – the maximum number of iterations. Construct with absolute subdivision and default maximum number of iterations.

  • ptrsys – the pointer to the system dynamics.

  • maxi – the maximum number of iterations.

  • outedge – [in] The lvalue ref to the input transition matrix

int bisect_axis(ivec &box, const double eps[])

Determine the bisection axis.

Parameters

  • box – [inout] The interval vector to be bisected

  • eps – [in] The given precision of the grid, i.e., the minimum size of a grid

void labeling(const double lb[], const double ub[], UintSmall prop)

Assign a label to a given hyper-rectangle in the state space.

Parameters

  • lb – [in] The lower bound of the interval

  • ub – [in] The upper bound of the interval

  • prop – [in] The proposition of type UintSmall

void labeling(ivec &area, UintSmall prop)

Assign a label to a given hyper-rectangle in the state space.

Parameters

  • area – [in] The interval vector

  • prop – [in] The proposition of type UintSmall

void init_winset()

Initialize the winning set.

Assume that the _ctlr is already partitioned by the labeling function.

bool targetset_in_sdoms(std::vector<SPtree*> &sdoms)

Check if the related S-domains contain targeted areas.

Parameters

sdoms – [in] A vector of the pointers to the S-domains of all DBA nodes.

void init(SPEC ap, const double lb[], const double ub[])

Initialize _ctlr by an interval constriant.

Assign a goal or an avoid area (an interval) to _ctlr by using tags. Tagging rules are:

  • goal _tag <- 1;

  • free _tag <- 0;

  • free&goal _tag <- 2;

  • avoid _tag <- -1;

  • free&avoid _tag <- -2;

  • f, g & a _tag <- 2;

Parameters

  • ap – [in] A label “GOAL”, “AVOID” or “FREE”

  • lb – [in] lower bound of the interval

  • ub – [in] upper bound of the interval

void init(SPEC ap, ivec &area)

See

init(SPEC ap, const double lb[], const double ub[])

Parameters

area – [in] The given interval

void paver_init(SPnode *node, ivec &box, short itag)

A subroutin of init().

Mark leaf node by itag if interval matches, otherwise, keep parent’s tag.

Parameters

  • node – [in] The node to be splitted w.r.t. box

  • box – [in] A given constraint (an interval)

  • itag – [in] Tag for the constraint 1(goal), -1(avoid)

void init_refine(SPnode *node, ivec &box, short itag)

A subroutin of init().

Refine initialized node.

See

paver_init().

void init(SPEC ap, fcst f, const double eps[])

Initialize _ctlr by a function constraint \(f(x)\leq 0\).

Parameters

  • ap – [in] A label “GOAL”, “AVOID” or “FREE”

  • f – [in] \(f(x)\leq 0\)

  • eps – [in] Paver precision

void sivia(SPtree &sp, SPnode *ptrnode, ivec &cst, fcst f, bool inner, short itag, const double eps[])

The algorithm Set Interval Via Interval Analysis (sivia).

It is performed by using recursive function calls (same as using stacks).

Parameters

  • sp – [in] The root of subpaving

  • ptrnode – [in] The SPnode to be refined

  • cst – [in] The constraint region (an interval)

  • eps – [in] The paver precision

  • inner – [in] The indicator of inner approximation (True)

  • itag – [in] The tag for insiders

void init_goal_area()

Initialize _goal by collecting leaves with tag 1.

Must be used after init() functions.

void init_avoid_area()

Initialize _obs by collecting leaves with tag -1.

Must be used after init() functions.

void compute_winsize()

Compute the normalized length of current winning set: this->_winsize = pow(vol, 1/xdim)

short paver_test(SPtree&, ivec&)

Test if a box is included in the paving.

Parameters

  • sp – the SPtree with tags (-2, -1, 0), 1, 2.

  • box – an interval vector.

Returns

0(outside), 1(inside), 2(undetermined).

template<typename system>
void pre_cntl(system *ptrsys, std::stack<SPnode*>&, std::stack<SPnode*>&, std::stack<SPnode*>&, std::stack<SPnode*>&, const double evaleps[])

Compute the one-step backward reachable set within the scope of the same CSolver.

The set of states that can reach the target set in one step under some u. Exist u for all d.

Parameters

  • l – [inout] Pointers of nodes to be tested (empty on return)

  • l0 – [inout] Outside nodes (updated on return)

  • l1 – [inout] Inside nodes (as above)

  • l2 – [inout] Undetermined nodes (as above)

  • fcn – [in] Function pointer to a vector field

  • eps – [in] Minimum paver size

template<typename system>
void union_of_pres(system *ptrsys, std::vector<SPtree*> &sdoms, std::stack<SPnode*> &l, std::stack<SPnode*> &l0, std::stack<SPnode*> &l1, std::stack<SPnode*> &l2, const double evaleps[])

Compute the union of one-step backward reachable set across different CSolver objects:

\(W_i = \bigcup_j a_{ij}\cap Pre(W_j)\)

The result (union of predecessors) is represented by the updated tags in _ctlr.

See

pre_cntl()

Parameters

sdoms – [in] A vector of the pointers to S-domains of all DBA nodes

void init_leafque(std::stack<SPnode*> &l0, std::stack<SPnode*> &l1, std::stack<SPnode*> &l2)

Initialize queues of leaves for computation.

Parameters

  • l0 – [inout] A stack of leaves with tag=0.

  • l1 – [inout] A stack of leaves with tag=1.

  • l2 – [inout] A stack of leaves with tag=2.

template<typename system>
void inv_compute(system *ptrsys, std::stack<SPnode*> &l0, std::stack<SPnode*> &l1, std::stack<SPnode*> &l2, int d, const double eps[])

Core subroutine for invariance control computation.

See

init_leafqueue() and invariance_control()

Parameters

d – The depth of iteration (0 inner most, 2 outer most)

template<typename system>
void reach_compute(system *ptrsys, std::stack<SPnode*> &l0, std::stack<SPnode*> &l1, std::stack<SPnode*> &l2, int d, const double eps[], bool vareps = false, const double emin[] = nullptr)

Core subroutine for reachability control computation.

See

init_leafque() and reachability_control() and inv_compute()

template<typename system>
bool invariance_control(system *ptrsys, const double eps[])

Compute the maximal controlled invariant set: \(\nu X.(\text{Pre}(X)\cap X)\).

Parameters

eps – [in] The paver precision

Returns

0(empty set), 1(non-empty).

template<typename system>
bool reachability_control(system *ptrsys, const double eps[], bool vareps = false, const double emin[] = nullptr)

Compute the backward reachable set: iterating \(\mu X.(\text{Pre}(X)\cup X)\).

Parameters

  • eps – [in] The absolute or relative paver precision

  • epsmin – [in] The minimum absolute paver size (default=nullptr)

  • vareps – [in] An indicator of whether using variate precision (true-yes, false-no(default))

Returns

0(empty set), 1(non-empty).

template<typename system>
bool reachstay_control(system *ptrsys, const double ei[], const double er[], bool vareps = false, const double ermin[] = nullptr)

Compute the backward reachable set to the maximal controlled invariant set.

A subset of co-Buchi set.

Parameters

  • ei – [in] The relative precision for invariance

  • er – [in] The absolute or relative precision for reachability

  • ermin – [in] The minimum absolute paver size (default=nullptr)

  • vareps – [in] An indicator of whether using variate precision (true-yes, false-no(default)).

Returns

0(empty set), 1(non-empty).

template<typename system>
bool cobuchi(system *ptrsys, const double ei[], const double er[], bool vareps = false, const double ermin[] = nullptr)

Compute the standard coBuchi winning set: \(\nu Y.\nu X.[\text{Pre}(Y)\cup(B\cap \text{Pre}(X))]\).

Relative and adaptive precisions.

See

reachstay_control().

template<typename system>
bool buchi(system *ptrsys, const double eps[], bool vareps = false, const double ermin[] = nullptr)

Compute the standard Buchi winning set: \(\nu Y.\mu X.[(B\cap\text{Pre}(Y))\cup\text{Pre}(X)]\).

See

reachstay_control()

void print_controller_info() const

Print controller info to screen.

void print_controller() const

Print a conrol table to screen.

void log_iterations(const char *filename, int iter)

Write (tag=1) leaf nodes of _ctlr to a log file.

Parameters

  • filename – [in] The log file name

  • iter – [in] The number of iteration

Public Members

SPtree _ctlr

A controller

int _xdim

The state dimension

size_t _nu

The number of control values

std::vector<UintSmall> _M

All the transitions from the current DBA state (q0) to others. If q0>q1 under a proposition with the label i, then _M[i] gives the index of the DBA state q1.

std::vector<ivec> _goal

The goal areas (an array of intervals)

std::vector<ivec> _obs

The avoiding areas (an array of intervals)

BISECT _bstype

The bisection type

size_t _maxiter

The maximum number of iterations

double _winsize

The volume of the winning set

size_t _fpiter[3]

The number of iterations: max alter depth 3

double _timer

The time of solving

template<typename system, typename F>
void rocs::dba_control(std::vector<CSolver*> &w, system *ptrsys, std::vector<SPtree*> &sdoms, UintSmall nNodes, boost::dynamic_bitset<> &isacc, F init_w, UintSmall oid[], const double e[])

Control synthesis for DBA objectives.

The resulting winning set and each sub-controllers are recored in the corresponding CSolver objects.

Parameters

  • w – [inout] A vector of S-domains (CSolvers) (assumption: already initialized)

  • ptrsys – [in] The pointer to the system

  • sdoms – [in] The pointers to the S-domains of all DBA states

  • nNodes – [in] The number of DBA states

  • isacc – [in] A vector of binaries (size nNodes) that marks accepting states

  • init_w – [in] A function that initializes labeling function

  • oid – [in] An index mapping between DBA state indices and the indices under consideration in the full list of S-domains.

  • e – [in] A partition precision

class rocs::BSolver

The abstraction-based engine solver.

It is a wrapper class of the core data structures and algorithms defined in C files buchi.h and buchi.c

Public Functions

inline BSolver()

The default constructor.

No other constructors are allowed.

inline ~BSolver()

A destructor to release memory.

inline void construct_dba(int nAP, int nNodes, int q0, std::vector<rocs::UintSmall> &acc, std::vector<std::vector<rocs::UintSmall>> arrayM)

Construct the DBA struct in _sol.

Assign values to

  • n: # of DBA states.

  • k: # of atomic propositions.

  • ini: the initial DBA state.

  • acc: an array (k elements) of BOOL denoting accepting or not.

  • q_prime: the lookup table of size (2^k x n), recording transition relation.

  • q_prime_size: the total # of elements in q_prime (2^k x n).

Parameters

  • nAP – [in] # of atomic propositions

  • nNodes – [in] # of DBA states

  • q0 – [in] The initial state (UintSmall type)

  • acc – [in] The accepting states (a vector of UintSmall variables)

  • arrayM – [in] arrayM The transition matrix (a 2d array of UintSmall variables)

template<typename S>
void load_abstraction(abstraction<S> &abst)

Construct a graph with in-going edges in _sol.

  • nts_pre.n: # of graph states.

  • nts_pre.m: # of edges.

  • nts_pre.graph: an array of reverse graph nodes

  • nts_pre.outdeg: an out degree table of the graph nts_pre

  • nts_pre.in_edge: an array of in-going edges

  • action: # of actions.

Parameters

abst – [in] An abstraction object

template<typename S>
void generate_product(abstraction<S> &abst)

Take product of the forward graph and the DBA.

  • Construct a backward graph for NTS, and do safety processing.

  • Convert the backward graph to a forward graph.

  • Take product of the forward graph and the DBA.

Parameters

abst – [in] An abstraction object

inline void solve_buchigame_on_product()

Solve the buchi game on the product.

inline void write_controller_to_txt(char *filename)

Write controller to a file.

Parameters

filename – [in] The name of the output file

Public Members

HEAD _sol

A HEAD of solver info

class rocs::DSolver

A naive abstraction-based engine solver.

Public Functions

inline DSolver(fts *ts)

A constructor.

Initialize the sizes of member arrays.

Parameters

fts – [in] The pointer to a finite transition system

void reachability(std::vector<size_t> &target)

Solve a reachability game (minimax goal) using djikstra’s algorithm.

The complexity is of O(c*_ntrans). There are edges might be checked more than once, because the maximal cost is taken for all \(k\in (i,j,k)\), where i(start state) and j(input) are given.

Parameters

target – [in] Indices of target area

Returns

an optimal controller in _optctlr member, and a least restrictive controller in _leastctlr.

void invariance(std::vector<size_t> &target)

Solve an invariance game.

Parameters

target – [in] Indices of target area

Returns

a least restrictive controller in _leastctlr.

Public Members

fts *_ts

The pointer to a transitionsystem class

size_t _nw

The number of winning states

boost::dynamic_bitset _win

[N] States in the winning set are marked 1

std::vector<size_t> _optctlr

[N] The optimal input for a state

std::vector<double> _value

[N] The value of the optimal input

boost::dynamic_bitset _leastctlr

[N*M] All feasible inputs for each state

class rocs::DBAparser

A class that parses a DBA given in a file.

The info extracted by parsing:

  • # of DBA states (nNodes)

  • # of atomic propositions (nAP)

  • # of propositions

  • the initial state (q0)

  • the accepting states (acc)

Public Functions

bool open(const std::string filename)

Open a file.

Parameters

filename – [in] The name of the file

Returns

whether or not the file is opened.

void close()

Close the file that has been opened.

void back_to_the_first_line()

Go back to the first line of the file.

UintSmall read_number_of_nodes()

Read the number of states in the given DBA file.

Returns

the nNodes (an UintSmall variable).

UintSmall read_number_of_atomic_propsitions()

Read the number of atomic propositions in the given DBA file.

Returns

the nAP (an UintSmall variable).

UintSmall read_initial_state()

Read the number of propositions in the given DBA file.

Returns

the # of propositions (an UintSmall variable). Read the initial state in the given DBA file.

Returns

the q0 (an UintSmall variable).

void read_accepting_nodes(std::vector<UintSmall> &acc)

Read the accepting states in the given DBA file.

Parameters

acc – [inout] the lvalue reference to a vector of small integers.

void read_spec_name()

Read and display the LTL specification.

void read_propositions()

Read and display the propositions.

void read_transition_matrix(std::vector<std::vector<UintSmall>> &arrayM)

Read the transition matrix.

Parameters

arrayM – [inout] the lvalue reference to the transition matrix (a 2d array of UintSmall variables)

bool rocs::read_spec(std::string specfile, UintSmall &nNodes, UintSmall &nAP, UintSmall &q0, std::vector<std::vector<UintSmall>> &arrayM, std::vector<rocs::UintSmall> &acc)

The non-member function of DBAparser that returns the DBA info.

Parameters

  • specfile – [in] The name of the specification file

  • nNodes – [inout] The # of states (an UintSmall variable)

  • nAP – [inout] The # of atomic propositions (an UintSmall variable)

  • q0 – [inout] The initial state (UintSmall type)

  • arrayM – [inout] The transition matrix (a 2d array of UintSmall variables)

  • acc – [inout] The accepting states (a vector of UintSmall variables)

class rocs::h5FileHandler

An hdf5 file input/output class.

Read and write controller data into hdf5 data format.

Public Functions

inline h5FileHandler(std::string f, unsigned int flag)

A constructor.

Parameters

  • f – [in] The file name

  • flag – [in] H5F_ACC_RDONLY(read), H5F_ACC_TRUNC(write)

inline void create_group(const std::string groupname)

Create an hdf5 group.

Parameters

The – [in] group name

template<typename T>
int write_number(const T x, const std::string varname)

Write a number into an hdf5 file.

The supported types: double, int, long long, unsigned int, etc.

Parameters

  • x – [in] The number

  • varname – [in] The variable name to be written

template<typename T>
inline int write_array(const std::vector<T> &arr, const std::string varname)

Write an std::vector into an hdf5 file.

The supported types: double, int, long long, unsigned int, etc.

Parameters

  • arr – [in] The vector

  • varname – [in] The variable name to be written

template<typename T>
int write_array(const T *arr, const size_t len, const std::string varname)

Write an array into an hdf5 file.

The supported types: double, int, long long, unsigned int, etc.

Parameters

  • arr – [in] The array

  • varname – [in] The variable name to be written

template<typename T>
int write_2d_array(const std::vector<std::vector<T>> &arr, const std::string varname)

Write a 2d std::vector into an hdf5 file.

The supported types: double, int, long long, unsigned int, etc.

Parameters

  • arr – [in] The vector

  • varname – [in] The variable name to be written

template<typename T>
int write_2d_array(const std::vector<T> &arr, const size_t *len, const std::string varname)

Write a 2d array into an hdf5 file.

The supported types: double, int, long long, unsigned int, etc.

Parameters

  • arr – [in] The array

  • varname – [in] The variable name to be written

template<typename T>
int write_2d_array(const T *arr, const size_t *len, const std::string varname)

Write a 2d array into an hdf5 file.

The supported types: double, int, long long, unsigned int, etc.

Parameters

  • arr – [in] The array

  • varname – [in] The variable name to be written

int write_ivec_array(const std::vector<ivec> &arr, const std::string varname)

Write a std::vector of interval vectors into an hdf5 file.

Parameters

  • arr – [in] The vector of interval vectors

  • varname – [in] The variable name to be written

int write_state_space(const ivec &ws, const std::string varname)

Write system state space into an hdf5 file.

Parameters

  • ws – [in] System state space

  • varname – [in] The variable name to be written

int write_input_values(const grid &ugrid, const std::string varname)

Write control input into an hdf5 file.

Control input is a set of uniformly sampled points from a compact control set \(U\).

Parameters

  • ugrid – [in] A set of control inputs

  • varname – [in] The variable name to be written

template<typename S>
inline void write_problem_setting(const S &sys)

Write control system settings.

The related data includes:

  • the sampling time ts

  • the state space X

  • the control set U

Parameters

sys – [in] A system object

int write_discrete_controller(HEAD *sol)

Write the BSolver controller into an hdf5 file.

Parameters

sol – [in] the head of the controller

int write_discrete_controller(const DSolver &dsol)

Write the DSolver controller into an hdf5 file.

Parameters

dsol – [in] A DSolver object

int write_transitions(const fts &trans)

Write a finite transition system into an hdf5 file.

Parameters

fts – [in] A finite transition system

int write_winning_graph(const Patcher &patcher)

Write the winning graph of a controller generated by the BSolver into an hdf5 file.

Parameters

patcher – [in] A Patcher object

int write_sptree_leaves(const SPtree &ctlr, SPnode *ptrn)

Write a CSolver tree leaves from a given node into an hdf5 file.

Parameters

  • ctlr – [in] A SPtree object

  • ptrn – [in] The given tree node

inline int write_sptree_controller(const CSolver &sol)

Write a CSolver controller into an hdf5 file.

Parameters

sol – [in] A CSolver object

template<typename T>
int read_number(T *ptrd, const std::string varname)

Read a number from an hdf5 file.

The supported types: double, int, long long, unsigned int, etc.

Parameters

  • ptrd – [inout] The number to be read

  • varname – [in] The variable name in the file to be read

template<typename T>
int read_array(std::vector<T> &arr, const std::string varname)

Read an std::vector from an hdf5 file.

The supported types: double, int, long long, unsigned int, etc.

Parameters

  • arr – [inout] The vector to be read

  • varname – [in] The variable name in the file to be read

template<typename T>
int read_2d_array(std::vector<T> &arr, size_t *len, const std::string varname)

Read a 2d array from an hdf5 file.

The supported types: double, int, long long, unsigned int, etc.

Parameters

  • arr – [inout] The vector to be read

  • len – [inout] The length of each dimension

  • varname – [in] The variable name in the file to be read

int read_transitions(fts &trans)

Read a finite transition system from an hdf5 file.

Parameters

fts – [inout] A finite transition system to be read

int read_winning_graph(Patcher &patcher)

Read the winning graph of a controller generated by the BSolver from an hdf5 file.

Parameters

patcher – [inout] A Patcher object to be read

int read_discrete_controller(boost::dynamic_bitset<> &win, boost::dynamic_bitset<> &lsctlr, size_t *cdims, std::vector<size_t> &optctlr, std::vector<double> &value)

Read the DSolver controller from an hdf5 file.

Parameters

  • win – [inout] The winning set (marked by 1)

  • lsctlr – [inout] The least restrict controller (marked by 1)

  • cdim – [inout] The length of each dimension

  • optctlr – [inout] The optimal controller

  • value – [inout] The optimal value

int read_discrete_controller(std::vector<long long> &w_x0, std::vector<long long> &encode3, std::vector<NODE_POST> &nts_ctrlr, std::vector<CTRL> &ctrl, std::vector<int> &q_prime)

Read the BSolver controller from an hdf5 file.

Parameters

  • w_x0 – [inout] The winning set

  • encode3 – [inout] A state index mapping

  • nts_ctrlr – [inout] The indexing table for finding the right entry in ctrl

  • ctrl – [inout] The controller pair (q,u), where q is the DBA state and u is the control input

  • q_prime – [inout] The lookup table for q’

int read_sptree_controller(std::vector<double> &pavings, size_t *pdims, std::vector<int> &tag, boost::dynamic_bitset<> &cntl, size_t *cdims)

Read the CSolver controller from an hdf5 file.

Parameters

  • pavings – [inout] A 2d array of intervals

  • pdims – [inout] The length of each dimension of pavings

  • tag – [inout] The indicator of winning set (1 if the interval belongs to the winning set)

  • cntl – [inout] The control table (row: # of pavings, column: # of control inputs, 1 if the corresponding control to the cell is permissible)

  • cdim – [inout] The length of each dimension of cntl

class rocs::matWriter

A mat file writer class.

Public Functions

inline bool open()

Open a mat file.

inline bool close()

Close a mat file.

void write_real_number(const double x, const char *varname)

Write a real number to a mat file.

Parameters

  • x – The real number

  • varname – The variable name to be saved as

template<typename T>
void write_real_array(const std::vector<T> x, const char *varname)

Write an array of real numbers to a mat file.

Parameters

  • x – The array of real numbers

  • varname – The variable name to be saved as

void write_state_space(const ivec &ws, const char *varname)

Write the state space to a mat file.

Parameters

  • ws – The system state space (a ivec)

  • varname – The variable name to be saved as

void write_input_values(const grid &ugrid, const char *varname)

Write the input values to a mat file.

Parameters

  • ugrid – The set of input values (a grid)

  • varname – The variable name to be saved as

void write_ivec_array(const std::vector<ivec> &arr, const char *varname)

Write an array of interval vectors to a mat file.

Parameters

  • arr – An array of ivec

  • varname – The variable name to be saved as

void write_sptree_leaves(const SPtree &ctlr, SPnode *ptrn)

Write leaves under a node to a .mat file (Depth-first).

Parameters

  • ctlr – The controller in the form of SPtree

  • ptrn – The pointer to the given node

void write_boundary(grid &g, const std::vector<bool> &win, const char *varname)

Extract the boundary of a given grid.

Parameters

  • g – The grid data

  • win – The list indicating inside/outside of the target region

  • varname – The variable name to be saved as

void write_winset_boundary(const double eta[], const CSolver &sol, const char *varname)

Extract the boundary of the winning set.

Discretize the state space and collect the ones lie on the boundary.

Parameters

  • eta – The grid size of the state space

  • sol – The solver which contains the spec info

  • varname – The variable name to be saved as

template<typename S>
inline void write_problem_setting(const S &sys, const CSolver &sol)

Write the problem setting into a mat file.

Parameters

  • sys – The defined control system (use template type S)

  • sol – The solver that contains the spec info

inline void write_sptree_controller(const CSolver &sol)

Write the controller into a mat file.

The controller is saved in 3 variables:

  • pavings: the interval boxes,

  • ctlr: a list of binary values indicating the admissible control inputs, and

  • tags: the tags (0,1,or 2) of the boxes.

Parameters

sol – The solver which contains the controller info

void write_controller_serialized(const CSolver &sol)

Write the controller into a mat file as arrays (keep tree structure).

  • ctree: index-searching array (2^H-1 x [split axis(1), intervals(2dim)]).

  • cindex: comparison array (# of nodes x intervals(2dim)).

  • cvalue: control array (# of leaves x [index(1), # of control values]).

Parameters

sol – The solver which contains the controller info

void write_transitions(const fts &trans, const char *vtranspost, const char *vpost, const char *vptrpost, const char *vtranspre, const char *vpre, const char *vptrpre)

Save all transitions to a .mat file.

The file is rewritten each time.

Parameters

trans – The transitions to be saved: trans_post, post, postptr, trans_pre, pre, preptr

void write_uniform_grids(const grid &g, const char *varname)

Save uniform grids to a .mat file.

Parameters

  • g – The uniform grid

  • varname – The variable name to be saved as

void write_discrete_controller(const DSolver &dsol, const char *vleastctlr, const char *voptctlr)

Write the DSolver controller into a mat file.

The controller is saved in 2 variables:

  • optctlr: the optimal controller (a vector of control indices).

  • leastctlr: a list of binary values indicating the admissible control inputs.

Parameters

  • sol – The solver which contains the controller info

  • vleastctlr – The least restrictive controller

  • voptctlr – The optimal controller

template<typename S>
void rocs::write_csolvers_to_h5(const S &sys, std::string specfile, std::vector<rocs::CSolver*> &w)

Write control problem setup and synthesized controller into a .h5 file.

Parameters

specfile – the specification file name.

template<typename S>
void rocs::write_results_to_mat(const S &sys, std::string specfile, std::vector<rocs::CSolver*> &w)

Write control problem setup and a CSolver controller into a .mat file.

Parameters

  • sys – [in] The given system

  • specfile – [in] The specification file name

  • w – [in] The CSolver controller

Python API