Package for ARCH submission 15
==============================

This package contains two parts. First, is the Simulink/Stateflow files for Model 3 
and Model 2 that are based on the powertrain control verification benchmark. Second,
is the executable for C2E2 that is used for verifying the invariant properties of 
different driver behaviors of Model 3. The description and the parameters for each 
of the Simulink/Stateflow models is given in their respective directories. 

In the rest of this README file, we will describe the instructions to install the 
requirements and running the version of C2E2 that is used for verifying the powertrain 
control systems. For modifying the other elements of the benchmark, such as changing
the initial set of states, the safety property, and the driver behaviors, please 
refer to the README file in the wd/ directory. In this package, we submit the instructions for
running 32 bit binary file for running C2E2 on Ubuntu (or debian systems) and the relevant files.

How to run C2E2-powertrain benchmark
====================================

This folder containts 3 subfolders namely /capd, /eigen, and /wd. The binary for running
C2E2 is provided in /wd. C2E2 uses glpk, flex, bison, gmp, and capd packages for performing 
simulation based verification. In order to run C2E2, it requires installing these packages 
as administrator. Run the following command for installing all the requirements.

$ sudo ./installRequirements

After installing the required packages, in order to compile the C++ model files that describe
the hybrid automata CAPD needs to be installed using the following command.

$ ./installCAPD

Once CAPD is installed in your local machine and all the requirements are installed, verify the
invariant properties of C2E2 for behavior 1 by running the following commands.

$ cd wd/
$ ./compileAndExecute-behavior1
$ ./C2E2 < Configuration-C2E2-behavior1

For verifying invariant properties for behavior 2, run the following commands.

$ ./compileAndExecute-behavior2
$ ./C2E2 < Configuration-C2E2-behavior2

The C++ files which model the ODEs for the polynomial hybrid automata, model the guards,
and the invariants corresponding to behavior 1 are given as simulator1.cpp, guards1.cpp,
and invariants1.cpp respectively. Similar files for behavior 2 are given as simulator2.cpp,
guards2.cpp, and invariants2.cpp respectively. The configuration files provided as input
to C2E2 provide information about the initial set, unsafe set, and the time horizon for
verification. Details to modify the user behaviors and initial and unsafe sets are given in
the README-modify-parameters.txt file in /wd directory. After the verification, the reachable
set of states are proved in the text file ReachSetPowertrain.dat corresponding to each mode
of the hybrid automata.

Possible Issues
===============

The binary distributed along with this package requires that the packages flex, bison, glpk,
to be installed as sudo and should be in the system include path. In case if the binary has 
a linking issue and this leads to issues in running the executable on a 32 bit ubuntu machine, 
please report the issues to Parasara Sridhar Duggirala (duggira3@illinois.edu) immediately. 
We would be more than happy to resolve them.