readme.txt

CheckMate is a MATLAB-based tool for modeling, simulating and investigating properties of hybrid dyn

-A bug was fixed in our convex hull routine (convex_hull.m).  The program now
returns the correct solution for the case where it is given less unique points
than there are dimensions.  Thanks to Howard Wong-Toi for pointing this out to us.

-A bug was fixed in the Ph-Plant demo.  The model was opening and assigning illegal
values to the initial condition field of the SCSB.  This has been rectified.

*******************************************************************
3.01f Release: 5/9/2002  
*******************************************************************

-Apply_reset was changed.  It no linger explicitly performs a 'grow polytope' operation.
It relies on the convex hull routine to grow the polytope if it is 'flat'.  The idea being
that if a reset was applied that was degenerate, the convex hull routine would have been called
to construct the reset region.

*******************************************************************
3.01g Release: 5/17/2002  
*******************************************************************

-A minor bug in iauto_part was fixed.  

*******************************************************************
3.01h Release: 6/7/2002
*******************************************************************

-Bug was fixed in partition_ss.m.  the clean_up procedure at the end was not correctly
 testing each of the pthb's to see which one was satisfied for each SSTREE region.  
This was corrected.  

-Convex hull routine updated.

*******************************************************************
3.01i Release: 6/17/2002
*******************************************************************

-CheckMate no longer attempts to allow PTHB names in ACTL expressions.
The change was made to 'build_ap.m'.

-Bug was fixed in partition_ss.  Program was not always associating the inside of the
PTHB with the correct side of a hyperplane in 'split_region' routine.  This has been
fixed.

-A new global variable has been introduced, GLOBAL_APPROX_PARAM.  This variable
holds all of the numerical parameters used for the verification.  Using this global
variable is much more efficient than the function calls that were used before.  Hence
significant increase in the speed of verifications has been achieved.

*******************************************************************
3.01j Release: 7/3/2002
*******************************************************************

-There was a bug in Piha.m.  The 'is_repeat' routine was testing to see if a newly
created cell was a copy of an existing cell by only testing if the boundary HP's were
identical.  This is not enough; the 'side' of each of the HP's is also important 
(iformation that is contained in hpflags).  This has been fixed.

-Several unused 'bouding_box' routines were removed.  Some of these existed as functions 
inside m-files and some of them were unused stand alone m-files.

-A new routine has been introduced which provides an alternative to the convex_hull 
routine used previously, performing a rectangular hull instead.  The function, 'rect_hull', 
produces a set of 2*n hyperplanes which are either parallel or orthogonal to each other 
and which bound a given set of points.  The hyperplanes are oriented in directions such 
that the total volume of the object returned is relatively small.  This provides a more 
conservative hull of the points given (in the sense that the polyhedral object returned 
contains more points than the convex hull would), but results in a smaller number of faces 
and takes much less time.  Note that this rectangular hull is now the default option (set 
by specifying the '.hull_flag' in the user-defined parameter file as either 'hyperrectangle' 
or 'convexhull'). 

*******************************************************************
3.01k Release: 7/23/2002
*******************************************************************

-CheckMate has been changed to be more verbose, when verifying non-linear systems. This 
should help the user to determine whether CheckMate got stuck, or whether there is any progress.

All 'clc' commands that remove feedback as soon as the next stage of the verification starts. 
This change affect all verifications. In addtition to this a approx_param.verbosity flag was 
introduced (default 0), with values from 0 (standard) to 2 (very verbose). This change will 
only effect the feedback for the verification of nonlinear systems. It is also possible to 
use the commandline option "verify -verbose". This sets verbosity to 1.

-The function fs_nonlin-map was changed, and will now detect certain null events. If a flowpipe 
segment lies completely inside the initial set, it is assumed that some states may stay in that 
location forever. 

-The private routine polyhedron.m was changed, to accmodate the change between rectangular hull 
and convex hull also for the case that the polyhedron is derived from a matrix of vertices. All 
other ways to create polyhedra already took care of this.

-The routine seg_aprox_ode has been changed such that, in case that the flowpipe approximation 
uses rectangular hull approximation of polyhedra, it adds the normals of the invariants to the 
set of normals. this gives a tighter approximation.

*******************************************************************
3.01L Release: 8/12/2002
*******************************************************************

-Line 548 of piha.m was changed.  'n' loop began with NAR where as it should begin with
NAR+1

-'number' field in the transition structure that is in the GLOBAL_PIHA was changed
to 'id'.  This is to reflect the fact that the transition number was given by Stateflow and
is not a sequential numbering of the transitions.

-'find_cond_expr' routine in piha.m was changed.  It should correctly parse the Stateflow
condition expressions now.

-'load_parameters.m' was added.  Running this function loads the default parameters into
a global variable.  This allows the user to use CheckMate functions that require parameters
without having defined a specific set of parameters. 

-Significant changes were made to 'partition_ss.m'.  The method used to partition the state
space was replaced with a new method that uses 'linprog' to discover when a cell region should
be divided.  The new method is much more efficient. 

*******************************************************************
3.01m Release: 8/28/2002
*******************************************************************

-Preliminary work on a sampled data difference equation analysis reachability
technique, called discrete-time flow analysis (DTFA) has been included in this 
release.  This type of analysis is not currently supported and documentation 
for it has yet to be written.  Its presence, however, should not affect the 
normal operation of CheckMate.  Several functions in CheckMate 
have been altered/added to accomodate the new capability, and three demos have been
added to illustrate the capability of DTFA.  For a description of DTFA, 
see J. Kapinski and B. Krogh, "Verifying Switched Mode Computer
 Controlled Systems", In Proceedings of the 2002 Conference on Computer
Aided Control System Design, to appear.   

-An unused function, transform.m, has been removed from the 'approximation'
folder.  The function that this file was to perform is already implemented
as a linearcon object method by the same name.

-Line 81 in apply_reset.m was uncommented.  This line 'bloats' the result
of the reset operation.  In some cases, the result is flattened and needs
to be restored to full dimension.

-The unused parameter Tsim was removed from the release.

-The method in which the user specifies the reset inside the user defined
dynamics file has been changed.  Now the user specifies an A and a B matrix
for the transformation.  See the boing example file boingfunc.m for an
example of the new reset method.

*******************************************************************
3.2 Release: 9/12/2002
*******************************************************************

- The function fs_lin_map was revised. It now computes the first segment
of the flowpipe, and translates this to obtain the other segments. The
function now only test for the timelimit if neither the system has an
attractive equilibrium, nor the system is unstable. Some unused sub-functions 
have been removed.

- The new way to define the reset may cause backward compatibility
problems. We now test whether the user uses an old type of reset or a new 
type of reset. If the reset is defined in the old fashion, CheckMate
produces a warning.

- To ensure backward compatibility, we include the obsolete field "np"
in the mask. This field is not used anywhere. It is just kept to
maintain backwards compatibility.

- Several unused function have been removed, as well as inconsistencies
in file names have been resolved.

*******************************************************************
3.3 Release: 10/17/2002
*******************************************************************

- The function piha.m was revised. Some flaws in the construction of the
composition of the FSM have been straightened out. Also some obsolete code 
has been removed.

- An obsolete function in flow_reach has been removed.

- The distinction between 'face' and 'init' in the standard case was no 
longer needed if the model is linear or nonlinear. This has been fixed.

- the function grow_polytope had a minor bug that was caused by an 
superfluous input.