====================

# Linearizer Benchmark

.. contents::

This repository contains benchmark reproducing experiments from our paper

"Linearising Discrete Time Hybrid Systems"

submitted to IEEE Transactions on Automatic Control.

To provide faithful reproduction of our experiments and easy execution on any platform we packaged benchmark as a software container.

The only needed prerequisite for its execution is `Docker <https://docker.com>`

*,that can be installed using instructions from*.

`the official website <https://docs.docker.com/engine/installation/>`

After Docker installation you need to perform following steps to execute the benchmark:

Build the image:

::docker build -t mclab/linearizer-benchmark .

As an alternative you can download a prebuilt image from official docker hub:

::

docker pull mclab/linearizer-benchmark

Run the container:

::docker run --rm -it mclab/linearizer-benchmark

Now you are inside the shell of the benchmark container.

From here you can execute different parts of the benchmark described below.

# Evaluation of linearisation algorithm

This part of the benchmark evaluates performance of our linearisation algorithm implemented in `linearizer <https://bitbucket.org/mclab/linearizer>`

_ library.

## Linearisation of :math:`y \cos{x}`

Tool `lin_benchmark_1`

computes linearisation of the function :math:`y \cos(x)`

on the interval :math:`[0,2\pi]\times[-\alpha,\alpha]`

.

::

Usage:

lin_benchmark_1: --alpha=<val> --eps=<val> -m <num> -o <file>

lin_benchmark_1: -h|--help

--alpha=<val> y ranges in [-alpha,alpha]

--eps=<val> error threshold

-m <num> number of sampling points

-o <file> output file

-h, --help print help message

Example invocation that computes linearisation of :math:`y \cos(x)`

on the interval :math:`[0,2\pi]\times[-2,2]`

using :math:`\varepsilon=0.1`

as upper bound for linearisation error

and :math:`m=80`

number of sampling points:

::

lin_benchmark_1 --alpha=2 --eps=0.1 -m 80 -o lin.txt

During the execution tool reports the current progress, number of intervals in the cover, CPU time and peak RAM usage.

::

Progress n CPU (sec) RAM (KB)

0.10% 5 0.0511 36648

0.15% 7 0.0632 36648

...

The output is a text file with very simple format.

First line contains two numbers: the number of intervals in the computer cover and the arity of the input function.

The rest of the file tool fills line by line with the elements of the following matrices:

- matrix representing lower bounds of the cover intervals(element :math:
`(i,j)`

is the lower bound of :math:`i`

-th interval for :math:`j`

-th dimension) - matrix representing upper bounds of the cover intervals (element :math:
`(i,j)`

is the upper bound of :math:`i`

-th interval for :math:`j`

-th dimension) - matrix representing under-approximation
- matrix representing over-approximation

Source code of the tool is available in the directory `linearisation/src`

.

## Term-wise approach

Tool `lin_benchmark_2`

computes linearisation of the function

:math:`\sum_{i=1}^{t} x_{i} x_{i+1}`

.

This can be done

- giving this function as it is to the linearisation algorithm (
*monolithic*approach) - treating each element of the sum separately (
*term-wise*approach)

::

Usage:

lin_benchmark_2: -t <num> -w <val> --eps=<val> -m <num> -o <file> [--term-wise]

lin_benchmark_2: -h|--help

-t <num> number of terms (1..4)

-w <val> x_{i} ranges in [-w,w]

--eps=<val> error threshold

-m <num> number of sampling points

-o <file> output file

--term-wise use term-wise approach

-h, --help print help message

Example invocation that computes linearisation of

:math:`x_1x_2+x_2x_3+x_3x_4`

on the interval :math:`[-2,2]^{4}`

using term-wise approach and

:math:`\varepsilon=1.0`

as upper bound for linearisation error

and :math:`m=10`

number of sampling points:

::

lin_benchmark_2 -t 3 -w 2 --eps=0.1 -m 10 -o lin.txt --term-wise

The execution log format and output format are the same as of `lin_benchmark_1`

.

The only difference is that when term-wise approach is used, :math:`t`

output files are produced, one for each term.

Source code of the tool is available in the directory `linearisation/src`

.

# Control software synthesis

This part of the benchmark demonstrates how our linearisation approach combined with`QKS <http://mclab.di.uniroma1.it/site/index.php/software/38-qks-intro>`

_

tool can be used to automatically generate control software

for a non-linear Discrete Time Hybrid System.

Our workflow consists of following steps:

- Linearisation
- Replication of transition relation
- Controller synthesis
- Simulation of closed loop system

We apply this workflow to the model of inverted pendulum with different frictions.

In the paper we presented 3 experiments with following configurations

(:math:`\varepsilon`

is the upper bound for linearisation error,

:math:`b`

is the number of quantization bits):

- :math:
`\varepsilon=0.5`

and :math:`b=8`

- :math:
`\varepsilon=0.5`

and :math:`b=9`

- :math:
`\varepsilon=1.1`

and :math:`b=9`

Other parameters in all experiments were chosen as follows:

- simulation step :math:
`\tau=0.01`

- controller sampling time :math:
`T=0.1`

- friction coefficient above pivot point :math:
`\mu_1=0.01`

- friction coefficient below pivot point :math:
`\mu_2=0`

- torquing force intensity :math:
`F=0.5`

For each experiment there is a directory inside`control_software_synthesis/hybrid`

that contains input and output for each workflow step.

Below you can find detailed description of each step.

## Linearisation

We use our tool `lin4qks`

to computer DTLHS overapproxmating initial DTHS model.

More information about it can be found`here <https://bitbucket.org/mclab/lin4qks>`

_.

Example invocation:

::

lin4qks -i input/model.m -f input/functions.c -o output/model.m

Here lin4qks takes as input file `input/model.m`

, reads definitions of the functions from `input/functions.c`

and writes the output DTLHS to `output/model.m`

.

## Replication of transition relation

After obtaining DTLHS model at the previous step we continue replicating its transition relation :math:`k`

times in such way that

:math:`T=k\tau`

where :math:`T`

is desired controller sampling time and :math:`\tau`

is simulation step.

Tool `replicate4qks`

takes as input the file with the model and how many times to replicate its transition relation.

It outputs model with replicated transition relation together with file containing computed bounds for new variables introduced.

Example invocation:

::

replicate4qks -i input/model.m -o output/model.m -b output/computed_bounds.txt -n 10

## Controller synthesis

Finally `QKS`

is used to automatically synthesize control software.

Example invocation:

::

qks -d input -dk output -no_compute_bounds -on_the_fly

`QKS`

will generate control software (files `ctrl.h`

and `ctrl.c`

) in the `output`

directory.

## Simulation of closed loop system

For the experiment #2 (:math:`\varepsilon=0.5`

and :math:`b=9`

) in which `QKS`

succeeded to find controller we performed also simulation of plugging generated control software into `OpenModelica <https://openmodelica.org>`

_-based simulator.

Simulator can be found in directory `control_software_synthesis/hybrid/simulator`

:

`plant.mo`

is the model of the inverted pendulum.`controller.mo`

is modelica wrapper for our C control software.`closed_loop.mo`

is the model that couples together plant and controller.

Files `ctrl.h`

and `ctrl.c`

generated by `QKS`

must be put into `Resources/Include`

.

Simulation can be started by running `omc run.mos`

# Control software synthesis for switched systems

This part of the benchmarks is aimed at comparison of our approach with the state-of-the-art tool `PESSOA <https://sites.google.com/a/cyphylab.ee.ucla.edu/pessoa/>`

_.

By setting :math:`\mu_1=\mu_2=0.01`

in our model of the inverted pendulum we get a switched system without mode jumps.

We run 1 experiment with `PESSOA`

and 2 experiments with `QKS`

. In all expeirments we used the same sampling time :math:`T=0.1`

.

## PESSOA

Experiment configuration:

- state quantization :math:
`0.0138`

(that corresponds to 9 bits for the angle and 10 bits for the velocity) - input range :math:
`[-0.5,0.5]`

and input quantization :math:`0.5`

Note that this experiment cannot be reproduced inside Docker container, since we cannot redistribute MATLAB environment. To run this experiment navigate inside MATLAB to the directory with the input files and execute `InvPend`

command.

Input and output files can be found in `control_software_synthesis/switched/pessoa`

.

List of the input files:

`InvPend.m`

`pss_dynamics.m`

`dynamic.m`

List of the output files:

`InvPend.bdd`

is the OBDD for the abstraction`InvPendTargetSet.bdd`

is the OBDD for the target set`InvPendController.bdd`

is the OBDD for the controller

Also in the same directory you can find Simulink model `closed_loop.mdl`

that allows simulation of the closed loop system obtained with the generated controller, using S-Function block provided together with PESSOA.

## QKS

We run 2 experiments with `QKS`

with :math:`\tau=0.01`

and with :math:`\tau=0.1`

. In both experiments we used linerisation computed with :math:`\varepsilon=0.1`

as error threshold resulting in 8 intervals. We used 9 bits for state quantization and torquing force intensity :math:`F=0.5`

.

Input and output files for the each step of the control software synthesis flow can be found in `control_software_synthesis/switched/qks`

.

For these experiments we also provide Simulink model for simulation: `closed_loop.mdl`

. Before using it, first copy the needed `ctrl.c`

and `ctrl.h`

files (`QKS`

controller) in the same folder as `closed_loop.mdl`

and then compile `QKS`

controller and S-Function into MATLAB MEX executable file:

::

mex ctrl_sfunction.c ctrl.c