MASCOT-SDS

Controller synthesis for stochastic dynamical system using finite abstraction

System requirements

• Operating system: Linux, Mac OS. We haven't tested the tool on Windows.

• The CUDD library, which can be freely downloaded from https://github.com/ivmai/cudd. See the installation section below for more information on the configuration required during the installation of the library.

• A working distribution of MATLAB for visualization, and a compatible version of GCC compiler for Linux or a compatible version of Xcode for Mac OS for MEX-file compilation. A list of compatible GCC/Xcode versions for different versions of MATLAB can be found here (see the "supported compilers" column): https://www.mathworks.com/support/requirements/previous-releases.html?s_cid=pi_scl_1_R2012a_win64.

Installation

The installation procedure is the same as Mascot and SCOTS, and is given in the following (based on the SCOTS manual):

1. Unzip the provided .zip package of the tool, or clone the repository mascot-sds from the following url: https://gitlab.mpi-sws.org/kmallik/mascot-sds.git. (See here a step-by-step guide for cloning a repository: https://confluence.atlassian.com/bitbucket/clone-a-repository-223217891.html.)

2. Install a working C++ developer environment:

   • Mac OS: Install the latest version of Xcode.app including the command line tools. We used the compiler clang 12.0.0.

   • Linux: Most Linux OS distributions already include all the necessary tools already. We used the compiler GCC 9.3.0.

   • Windows: has not been tested on a Windows machine.

Additionally, for running some of the included examples, you will need the boost c++ libraries. This can be installed by executing the following commands from the command line: for Mac OS use

brew install boost

and for Linux use

sudo apt-get install libboost-all-dev    

3. Install the CUDD library with

   • the C++ object oriented wrapper,

   • the dddmp library, and

   • the shared library

   option enabled. To do that, first download CUDD from the specified link, unzip at any convenient location, open the terminal, navigate to the path of the extracted CUDD folder, and execute the following commands one by one:

   $ ./configure --enable-shared --enable-obj --enable-dddmp --prefix=/opt/local/
   $ make
   $ make check
   $ make install

   The above configuration was used for cudd-3.0.0. The prefix flag specifies the location where the CUDD library will be placed. The location of the CUDD library will be specified using the variable called CUDDPATH in this document and in the Makefiles at several locations. So if the exact same setting is used for the prefix flag as given above, then use CUDDPATH = /opt/local/ all the time.

   Some notes while setting up the CUDD library:

   • We have provided a dummy program in the folder ./test_cudd/ called test.cc to check the CUDD installation. First edit the Makefile to adjust the variable CUDDPATH (if required). Then compile and run the test program by executing the following commands one by one:

     $ make clean
     $ make
     $ ./test

     If no error is generated while executing make and ./test, then the CUDD library was installed correctly.

   • It has been reported that on some linux machines, the header files util.h and config.h were missing in /opt/local, and the fix is to manually copy the files to /opt/local/include by running from the CUDD unzipped location the following:

      $ sudo cp ./util/util.h /opt/local/include/
      $ sudo cp ./config.h /opt/local/include/

   • You need to manually add the CUDD shared library path to the search path of the dynamic linker. Set the environment variable LD_LIBRARY_PATH to point to opt/local/lib (i.e. CUDDPATH/lib). In bash, the command to do this is:

     $ export LD_LIBRARY_PATH="/opt/local/lib"

     and this command can be added into the ~/.bashrc file so that the path is automatically loaded each time.

   • In some Linux Machine, it was reported that setting the variable LD_LIBRARY_PATH was not sufficient for running the mex-binaries from MATLAB. Instead the following worked: Assuming you have root privilege (for Linux), edit the file /etc/ld.so.conf and add /usr/local/lib on its own line at the bottom. Do not remove anything from this file. Run ldconfig to tell the system to update the cache:

     $ sudo ldconfig

4. Install Owl by following the instructions from here: https://gitlab.lrz.de/i7/owl

5. Install cpphoafparser (download and copy paste in the search path): https://automata.tools/hoa/cpphoafparser/

6. Install OpenMP(for parallel implementation): didn't work: https://clang-omp.github.io, this one worked for mac in the end: https://mac.r-project.org/openmp/

7. For Sylvan: Additional things needed for Mac: argp c++ library (can be installed using brew install argp-standalone, sphinx-rtd-theme while building the doc (can be installed using pip3 install sphinx-rtd-theme). Worked smoothly for Linux. Adjustments that were necessary in /usr/local/include/lace.h: change the value of "define LACE_TASKSIZE" to "(20)*P_SZ"

8. Install a recent version of MATLAB. To compile the mex files:

   (a) open MATLAB and setup the mex compiler by

   >> mex -setup C++

   (b) Open a terminal and go to ./mfiles/mexfiles/ (within the directory, see below). Edit the Makefile and adjust the variables (if required)

   MATLABROOT and CUDDPATH

   and run

   $ make

   (The variable MATLABROOT contains the MATLAB root directory, which can be queried by typing matlabroot in the command window of MATLAB. The variable CUDDPATH contains the path to the CUDD installation, and use CUDDPATH=/opt/local/ if the same configuration was used while installing CUDD as mentioned in #3 above.)

Directory Structure

In the repository, you will see the following directory structure:

• ./bdd/ Contains the C++ source code which use Binary Decision Diagrams as the underlying data structure.

• ./contrib/ Contains license files of SCOTS and Mascot.

• ./doc/ C++ Class documentation directory.

• ./examples/adhs21/ Examples shown in the ADHS '21 paper; instructions for running the examples are included in the file ./examples/rabin_examples/bistable_switch/README.md.

• ./examples/rabin_examples/bistable_switch An example based on an oscillator with Rabin specifications; instructions for running the examples are included in the file ./examples/rabin_examples/bistable_switch/README.md.

• ./examples/rabin_examples/experimental Some additional examples with Rabin specifications.

• ./examples/hscc20/ Examples shown in the HSCC '20 paper with the repeatability evaluation instructions.

• ./examples/others/ Other examples.

• ./manual/ SCOTS manual.

• ./mfiles/ Contains some mfiles needed for running the simulations.

• ./mfiles/mexfiles/ mex-file to read the C++ output from file.

• ./test_cudd/ a dummy test program to check the CUDD installation.

• ./utils/ Some C++ header files used by the source code in ./bdd/.

How to Use

See ./examples/hscc20/RE_manual_hscc20.pdf for instructions to synthesize controller and plot trajectories for the examples which were presented in the HSCC '20 paper.