VeriSiMPL Files

% Verification via biSimulations of MPL models (VeriSiMPL) Toolbox
% Version 2.0 (8-Dec-2014)

Webpages:
http://sourceforge.net/projects/verisimpl
http://www.dcsc.tudelft.nl/~aabate/VeriSiMPL.html

Authors:
Dieky Adzkiya and Alessandro Abate

Emails contacts:
{d.adzkiya,a.abate}@tudelft.nl
alessandro.abate@cs.ox.ac.uk

Mail contacts: 
1) Delft Center for Systems and Control
   TU Delft - Delft University of Technology
   Mekelweg 2, 2628CD Delft, 
   The Netherlands
2) Department of Computer Science
   University of Oxford
   Wolfson Building, Parks Road, Oxford, OX1 3QD,
   United Kingdom

Main bibliographical references:
1) D. Adzkiya and A. Abate,
   ``VeriSiMPL: Verification via biSimulations of MPL Models''
   In Proceedings of the 10th Quantitative Evaluation of Systems
   volume 8054 of Lecture Notes in Computer Science, pages 253-256, Springer, Heidelberg
   Buenos Aires, September 2013.
2) D. Adzkiya, B. De Schutter, and A. Abate,
   ``Finite Abstractions of Max-Plus-Linear Systems''
   IEEE Transactions on Automatic Control 58(12), pages 3039-3053, December 2013.
3) G. Holzmann, 
   ``The SPIN Model Checker''
   Addison-Wesley, 2003. 

Additional bibliographical references:
1) D. Adzkiya, B. De Schutter, and A. Abate,
   ``Abstraction and Verification of Autonomous Max-Plus-Linear Systems''
   In Proceedings of the 31st American Control Conference, pages 721-726
   Montreal - CA, June 2012.
2) D. Adzkiya, B. De Schutter, and A. Abate,
   ``Finite Abstractions of Nonautonomous Max-Plus-Linear Systems''
   In Proceedings of the 32nd American Control Conference, pages 4387-4392
   Washington, June 2013.
3) D. Adzkiya, B. De Schutter, and A. Abate,
   ``Forward Reachability Computation for Autonomous Max-Plus-Linear Systems''
   In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
   volume 8413 of Lecture Notes in Computer Science, pages 248-262, Springer, Heidelberg
   Grenoble, April 2014.
4) D. Adzkiya, B. De Schutter, and A. Abate,
   ``Backward Reachability of Autonomous Max-Plus-Linear Systems''
   Proceedings of the 12th IFAC - IEEE International Workshop on Discrete Event Systems, pages 117-122, May 2014, Paris.

Description
===========

This toolbox is used to generate finite abstractions of autonomous
Max-Plus-Linear (MPL) models over R^n. Abstractions are 
characterized as finite-state Labeled Transition Systems (LTS). 
The LTS finite abstractions are shown to either simulate or to bisimulate
the original MPL model. LTS models are to be verified against given 
specifications expressed as formulae in Linear Temporal Logic (LTL) and
Computation Tree Logic (CTL). The toolbox intends to leverage the NuSMV model checker. 

Models are to be expressed in the JAVA language. 
The abstraction procedure runs in JAVA. 
The generated LTS is exported to the NuSMV language. 
As such, it can be fed, along with a specification of interest, to the NuSMV model checker.

If you are more familiar with MATLAB models, we suggest you to try VeriSiMPL version 1.4.

Installation
============

This toolbox consists of the following main files: 

PartAgainstAP               - generate a proposition-preserving partition
Maxpl2pwa                   - generate a PWA system from an autonomous max-plus-linear system
Maxpl2pwa_refine            - refine the regions in the PWA system such that the regions become a dynamics-based partition
Maxpl2ts_part               - determine the initial partition (refinement of proposition-preserving partition and dynamics-based partition)
Maxpl2ts_trans              - compute the transition relation
Maxpl2ts_trans_refine       - determinize the transition system
CalInitStates               - determine the initial states of the transition system
Ts2nusmv                    - generate NuSMV code and execute NuSMV
Maxpl2ts_trans_bench        - compute the transition relation (with the assumption that the partition is proposition preserving)
Maxpl2ts_bench              - the function used in the benchmark against VeriSiMPL 1
Main                        - an interactive abstraction procedure of autonomous max-plus-linear systems
PartAgainstAP_tree          - construct space-partitioning tree associated with the proposition-preserving partition
Maxpl2ts_part_tree          - construct space-partitioning tree associated with the initial partition
Maxpl2ts_trans_tree         - compute the transition relation by using the tree structure
Maxpl2ts_bench_tree         - benchmark for the tree-based abstraction procedure

Eclipse can be used to run this toolbox.
Firstly, we import the project in the workspace as follows:
go to 'File'->'Import'->'General'->'Existing project' and select the folder of VeriSiMPL.
Secondly, the classes (each class is a java file) in DBM or MPL or MATLAB package with 'void main()' function at the end can be run.
These 'main()' functions contain some simple examples.
Notice that we can change the matrices written in the 'main()' functions.
To run the classes, right click on the class you want to run, 'Run as'->'Java application'. Then it will be run.

If, after you import the project, there are crosses (indicating errors) at the bottom right corner of the all packages,
it means the project cannot find the external matrix library 'jblas'.
In this case, we right click on the project name 'VeriSiMPL' -> 'Build Path' -> 'Configure build path' -> tab 'library' -> remove 'jblas' -> then re-add it by 'add external JARs' and select the jblas.jar file in the VeriSiMPL folder.

If you are more familiar with MATLAB models, we suggest you to try VeriSiMPL version 1.4 which is fully based on MATLAB.

Support
=======

There is no support! This toolbox is made freely available in the hope 
that you find it useful in solving whatever problems you have to hand.
We are happy to correspond with people who have found genuine bugs. 
If you have any questions or comments, or you observe buggy behavior 
of this toolbox, please send your reports by email to the authors.