VeriSiMPL Files

% Verification via biSimulations of MPL models (VeriSiMPL) Toolbox
% Version 3.0 (17-May-2017)

Webpages:
sourceforge.net/projects/verisimpl
sites.google.com/site/diekyadzkiya
www.cs.ox.ac.uk/people/alessandro.abate/home.html

Authors:
Dieky Adzkiya and Alessandro Abate

Email contacts:
dieky@matematika.its.ac.id
alessandro.abate@cs.ox.ac.uk

Mail contacts: 
1) Department of Mathematics
   Institut Teknologi Sepuluh Nopember
   Kampus ITS Sukolilo, Surabaya 60111 
   Indonesia
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) D. Adzkiya, B. De Schutter and A. Abate,
   ``Computational Techniques for Reachability Analysis of Max-Plus-Linear Systems''
   Automatica 53(0), pages 293-302, 2015.
4) D. Adzkiya, Y. Zhang and A. Abate,
   ``VeriSiMPL 2: An open-source software for the verification of max-plus-linear systems''
   Discrete Event Dynamic Systems 26(1), pages 109-145, 2016.
5) 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.
5) Muhammadun, D. Adzkiya and I. Mukhlash,
   ``Object Oriented Design of Software Tool for Finite Abstractions of Max-Plus-Linear Systems using Unified Modeling Language''
   International Journal of Computing Science and Applied Mathematics 3(1), pages 32-39, 2017.

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

This toolbox is used to generate finite abstractions of autonomous
Max-Plus-Linear (MPL) systems 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 system. 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 C++ language. 
The abstraction procedure runs in C++. 
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 JAVA language,
we suggest you to try VeriSiMPL version 2.0 which is fully based on JAVA.
If you are more familiar with MATLAB language,
we suggest you to try VeriSiMPL version 1.4 which is fully based on MATLAB.

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

This toolbox consists of the following main classes: 

1) StateMatrix
   This class is used to store the state matrix of an MPL system.
2) AffineDynamics
   This class is used to store an affine dynamics generated from an MPL dynamics.
3) DBM
   This class is used to represent a DBM and its operations, such as
   computing the canonical-form representation, intersection of two DBM,
   complement of a DBM, emptiness checking, computing the image of a DBM w.r.t. an affine dynamics
   and computing the inverse image of a DBM w.r.t. an affine dynamics.
4) AbstractionTree
   This is the main class that is used to store the abstract transition system.

This toolbox calls the executable file of NuSMV model checker.
Please make sure that the NuSMV executable file is named "NuSMV.exe" (in windows) and "NuSMV" (in linux).
Furthermore the NuSMV executable has to be accessible from any location,
which can be done by inserting the location of NuSMV executable in the PATH.

There are two ways to run this toolbox:
1) Binary file
If your operating system is windows,
you should execute the file "VeriSiMPL.exe" in the "windows\bin\Debug" folder.
If your operating system is linux,
you should execute the file "VeriSiMPL" in the "linux/bin/Debug" folder.
2) Source file
We suggest to use Code::Blocks run the source code of this toolbox.
Firstly, we open project file "VeriSiMPL.cbp".
If your operating system is windows,
you should open the file in the "windows" folder.
If your operating system is linux,
you should open the file in the "linux" folder.
Lastly, you can execute the toolbox by using the command "Build and Run".

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