readme.txt

一个matlab的将军模型

Current Version: CheckMate 3.6
Update information is appended consecutively to this file
*******************************************************************
3.61 Release: 04/05/2004
*******************************************************************
* Added capability of using gradient function of linear dynamics in the 
   optimization routines.


*******************************************************************
3.6 Release: 02/23/2004
*******************************************************************
* New routines in polylib (using cddmex).
* Fixed type conversion bugs in SCSB.
* Added interface to SVM.
* Updated procedures to get rid of the second pass of compute_mapping.

*******************************************************************
3.5 Release: 06/04/2003
*******************************************************************

This version is compatible with Matlab R13. To solve the type 
conversion issues we changed the following:

* The PTHB has as output type 'boolean'
* We introduced a new start event block for continuous systems. This block 
has output type boolean.
* For sample data models matters remain a bit more complicated. To avoid 
problems do the following
    - Use the sample data start event block (output type double)
    - Use proper types in the fsm block. This means that all input condition 
    are of type 'boolean' and the output type is 'double'.
    - Open the preferences of the statflow model (Tools>Explore>Edit>Properties) 
    and select strong data typing.
* Other minor changes to in the code solved a few other type conversion issues.
* We fixed a problem in the bounding box routine.
* CheckMate now facilitates the use of non-square transforamtion matrices.
* The distribution includes now documentation of the main data structure GLOBAL_PIHA.
* The distribution includes now documetation on the VCT demo.    
    
*******************************************************************
3.4 Release: 11/21/2002
*******************************************************************

_ A problem with unconnected inputs, that appeared incidentally when 
a model as opened has been resolved. The related problem of additional 
input ports remains. This is not really a problem, since it does affect 
neither simulation, exploration nor verification.

- This version does support the use of conditions in the FSMBs of the 
model rather than events. Note that due to the semantics of Stateflow, 
either all transition of a FSMB must be triggered by events, or all 
conditions must be guarded by conditions. The boing demo includes 
an example of a model that uses conditions.

*******************************************************************
3.4.13 Release: 01/19/2003
*******************************************************************

This release contains a few fixes of type conversion errors in Matlab R13.

------------------Previous Releases--------------------------------------


*******************************************************************
3.01 Release: 3/6/2002
*******************************************************************

Changes in this release:

-Bugs fixed in the refinement procedure.  Thanks to Howard Wong-Toi
for reporting the bug.

-State space partitioning procedure updated.  A hard-coded parameter
that was used to test which vertices correspond to which hyperplanes
was removed.  The parameter is now taken from the 'paramters.m' file.
Also, a bug relating to the bookkeeping of hyperplanes was fixed.

-Another demo example was added, the electronic throttle control (ETC)
example.  This is a 5th order version of the ETC example from the 
MoBIES project.  The example is meant for simulation/exploration
purposes.  Verification should not be attempted on this model.

-The documentation from the previous release was fixed.  The documentation
should now work in any browser.  Also, new documentation was added for 
the ETC example.

-The switched continuous system block (SCSB) in the CheckMate library
was fixed.  The blocks should no longer cause a warning when a CheckMate
model is simulated.  The user should be aware that the 'Apply' button
must be hit after properties in the SCSB are changed in order for them
to take effect.

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

Changes in this release:

-A bug was fixed which involved the way that the reachability routine
dealt with non-determinism in the finite state machine. 

*******************************************************************
3.01b Release: 3/12/2002  
*******************************************************************

Changes in this release:

-A bug was fixed (in compute_mapping_no_SD.m) that incorrectly dealt with
assigned multiple terminal state mappings.  (Thanks to Howard Wong-Toi for
reporting this).

-Documentation for the ETC examples was added and previous documentation has
been updated.

-ETC regulation example was added that verifies an ETC system.  Also the 5d ETC
model was updated.

-A new splash page was added.

-Change was made (in check_overall_dynamics.m) to allow equality constraints 
for parameters.

-Changed optimization warning (in seg_approx_ode.m) so that the user knows that
the optimization did not improve on the original convex hull of the simulation points
during reachability analysis.

-Changed the flowpipe 'shrink wrapping' procedure (in seg_approx_ode.m) to accomodate
lower dimensional polyhedral regions.  This was introduced specifically to accomodate
lower dimensional paramter regions.

*******************************************************************
3.01c Release: 3/21/2002  
*******************************************************************

-Changed "apply_reset.m" to handle the case where one SCSB is reset while the others
are not.  Also, "apply_reset.m" now calls "grow_polytope.m".

-"seg_approx_ode.m" was changed to accomodate the case when it is passed an
empty parameter constraint set.

-SCSB block changed.  The block is now implemented with a mex function.
"trace_pthb_input.m" and "trace_scsb_input.m" was changed to accomodate the fact
that the SCSB block is now an s-function instead of a subsystem.

-SCSB's in demo's were updated to point to the new SCSB in the CheckMate/Simulink
library.

*******************************************************************
3.01c Release: 3/22/2002  
*******************************************************************

-New SCSB functions incorporated.  This one does not cause Matlab to crash
when the user debugs a Stateflow diagram.

-Note: users must manually update the SCSB's in their old CheckMate models with
the new SCSB. 

*******************************************************************
3.01d Release: 4/4/2002  
*******************************************************************

-Minor bugs with the Switched Continuous System Block were fixed.

-A user-setable flag was added that tells the verification procedure whether
to perform initial reachability or not. 

*******************************************************************
3.01e Release: 4/12/2002  
*******************************************************************

-Minor documentation changes

-Installation instructions added to root directory

-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.