**ROCS** is a robust symbolic control synthesis tool for nonlinear systems. It provides two control synthesis methods from linear temporal logic (LTL) formulas:
- Abstraction-based control synthesis (to be added): state and control space are uniformly discretized.
- Specification-guided control synthesis: state space are partitioned adaptively with respect to given specifications and local dynamics of the systems.
## Installation
### Prerequisite packages and softwares
**ROCS** is currently a package of c++ APIs, which only need to be included and no recompiliation required.
## Installation ##
### Prerequisite packages and softwares ###
- boost c++ libraries (http://www.boost.org): libraries for graph searching, ode solvers;
- armadillo (http://arma.sourceforge.net): a c++ linear algebra library;
- matlab: control simulation and graphics.
### Configuration
- Update the environment variable DYLD_LIBRARY_PATH in terminal:
### Configuration of Matlab ###
- Matlab 2017a and earlier versions are supported.
- Follow the instruction Matlab documentation on **Set run-time library path on Mac and Linux systems**, e.g.,
- On Mac OSX: update the environment variable DYLD_LIBRARY_PATH by placing the following commands in a startup script (~/.profile):
- For Mac users, recommend to use *Homebrew* with simple command in terminal:
```
$brew install armadillo
```
- For Linux users, packages such as *cmake*, *openBLAS*, *LAPACK* and *ARPACK*. Follow the instruction on http://arma.sourceforge.net/download.html.
## Usage
- Clone this repositary. Source code will be downloaded and ready for use.
## Usage ##
- Clone this repositary.
- Make sure the prerequisites are installed.
- Go to the folder *examples*, modify the *Makefile* according to your actual installed paths of prerequisites, e.g.
```
BOOSTROOT = /usr/local/Cellar/boost/1.62.0
MATLABROOT = /Applications/MATLAB_R2016a.app
LINALGROOT = /usr/local/Cellar/armadillo/7.500.2
```
- Type `make` in command window to compile examples. For example, for dcdc example, type `make dcdc` in command window.
- Execute compiled examples by typing the name of the executable, e.g. `./dcdc`.
- Prepare the configuration file for build:
+ The default configuration file *configMake* in the root path is for Mac OSX, the user only need to modify the paths for the external packages, e.g.,
```
BSTDIR := /usr/local/opt/boost
MATDIR := /Applications/MATLAB_R2016a.app
LADIR := /usr/local/opt/armadillo
```
+ for Linux users, rename the file *Make-linux* to *configMake*. If all the prerequisites are installed in the default paths, only modify the matlab path, e.g.,
```
MATDIR = /usr/local/MATLAB/R2016b
```
- To run examples, go to the folder *examples*:
+ To build all the examples: type `$ make examples` in terminal.
+ To build one of the examples: go to the corresponding subfolder and type `$ make` in terminal.
- Execute compiled examples by typing the name of the generated executable, e.g. `./dcdc`. **Data will be generated in each subfolder corresponding to the specific example**.
- Run *simulation.m* in the same example folder using matlab.
## Examples
## Examples ##
Simulations of the examples can be found under the folder *examples*:
-*examples/car*: Robot car reach avoid control: reach a target region while avoiding obstacles.
-*examples/ipdl*: Inverted pendulum reach stay control: reach and stay in the upright position.
-*examples/poly*: Polynomial systems region of attraction computation.
-*examples/temperature*: Room temperature control (4-mode system): reach and stay in desired room and heater temperatures.
-*examples/temp*: Room temperature control (4-mode system): reach and stay in desired room and heater temperatures.
## Create your own examples
## Create your own examples ##
To create your own examples, you have to provide a *main file* specifying all necessary problem settings and an additional file of system dynamics. For the DCDC converter example,
- main file: *DemoDcdc.cpp*
- vectorfield file: *dcdc.hpp*
## Features included
## Features included ##
- Basic invariance and reachability control for discrete-time systems.
- Buchi, coBuchi and reach-stay (a simpler version of coBuchi) control synthesis algorithms.
## Features under developement
## Features under developement ##
- Control synthesis from more complex LTL formulas.