?? readme.txt
字號:
*******************************************************************
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.
--------------------------------------------
Bruce Krogh
krogh@ece.cmu.edu
Zhi Han
zhih@ece.cmu.edu
Rajesh Kumar
rajeshk@ece.cmu.edu
Jim Kapinski
jpk3@andrew.cmu.edu
?? 快捷鍵說明
復制代碼
Ctrl + C
搜索代碼
Ctrl + F
全屏模式
F11
切換主題
Ctrl + Shift + D
顯示快捷鍵
?
增大字號
Ctrl + =
減小字號
Ctrl + -