Modifying parameters for verifying powertrain benchmarks using C2E2
===================================================================

The following are the verification parameters that can be modified with the given package.

Initial Set
===========

The initial set of states are provided as a convex polyhedron given as Ax <= b. This set of initial states can be
modified by changing the init-matrix and init-b fields provided in lines 11 and 12 in the Configuration files for 
C2E2. The fields given in Configuration-C2E2-behavior1 corresponding to these fields is given as 

init-matrix=[10000.0,0,0,0,-10000.0,0,0,0,0,1000.0,0,0,0,-1000.0,0,0,0,0,10000.0,0,0,0,-10000.0,0,0,0,0,1000.0,0,0,0,-1000.0]
init-b=[6453.0,-6253.0,14750.0,-14650.0,5573.0,-5573.0,17.0,-17.0]

corresponds to the initial set described as

10000*p <= 6353; -10000*p <= -6353; i.e. p = 0.6353
1000*\lambda <= 14750; -1000*\lambda <= -14650; i.e. \lambda belongs to [14.65,14.75]
10000*p_e <= 5573; -10000*p_e <=-5573; i.e. p_e = 0.5573
1000*i <= 17; -1000*i <= -17; i.e. i = 0.017

One can change these values to increase or decrease the size of the initial set.


Unsafe Set
==========

Similar to Initial Set, the unsafe set is also provided as a convex polyhedron given as Ax <= b. The set of unsafe states
can be modified by changing the unsafe-matrix and unsafe-b fields provided in lines 14 and 15 in the configuration file for
C2E2. The fields given in Configuration-C2E2-behavior1 corresponding to these fields is given as 

unsafe-matrix=[0.0,-1.0,0,0]
unsafe-b=[-15.0]

which represents the unsafe set as

-1*\lambda <= -15.0; i.e. \lambda >= 15.0 is the unsafe region.


Driver Behaviors
================

Changing the driver behavior requires modifying the invariant.cpp and the guard.cpp files and determine the switches
from one mode to another. The conditions for switching currently are given as if conditionals.

The driver behavior corresponding to behavior 1 is given in guard1.cpp. The drive behavior in this case is simple, the
driver starts in the start-up mode, stays in the start-up mode for 9.5 time units and then switches to normal mode.
The guard1.cpp file encodes this transition in the if conditional that is given in lines 42-61. By chaing the constant to
another value, the switching time for normal mode can be changed. Also note that corresponding to this guard condition,
there is an invariant condition in invariant1.cpp file lines 42-63 that check if the state satisfies the invariants.
The invariant specified currently requires that the execution stays in start-up mode until 9.5 time units and the execution 
stays in normal mode until 18 time units. Thus, in order to modify the drive behavior, one has to carefully make sure that
both these parameters specified in the invariant set and guard set ensure that the set of trajectories are not empty.

If any additional help is required for modifying these parameters, please do not hesitate to contact 
Parasara Sridhar Duggirala (duggira3@illinois.edu)