README

sf2dve - Stateflow to DVE transformation tool
=============================================

Licence: GNU LGPL 2.1 or any later version (more in LGPL.txt)
Copyright: Pavla Kratochvilova, 2015

Overview

	Sf2dve is a tool transforming Stateflow diagrams into DVE,
	the native input language of DiVinE model checker
	(https://divine.fi.muni.cz/), in order to enable automated
	formal verification of the Stateflow systems. The program takes
	either MathWorks SLX file format or XML document and generates
	DVE source code to either standard output or a file.

	Because of the Stateflow format being proprietary, formal
	correctness of the transformation cannot be guaranteed.
	The algorithm is based on informal specification contained in User's
	Guide (http://www.mathworks.com/help/pdf_doc/stateflow/sf_ug.pdf)
	and on observations of Stateflow behaviour.

Supported Stateflow features:

	* states with 'entry', 'during' and 'exit' actions
	* transitions with conditions, 'condition' and 'transition' actions
	* hierarchy of the states
	* labelled default transitions
	* implicit tick event
	* variables of integer and boolean types
	* C as action language

Unsupported Stateflow features:

	* events (including 'on event' actions, transitions guarded with
	  events, event broadcasting)
	* bind actions
	* AND decomposition of states
	* connective and history junctions
	* functions, boxes
	* variables of float types
	* MATLAB as action language

Limitations:

	The range of integer types differ in Stateflow and DVE. Also boolean
	variables from Stateflow are translated as byte variables in DVE.

Dependencies:

	Sf2dve is written in python3 and uses libraries lxml a ply.
	Following fedora or debian packages are required for running sf2dve:
		* python3 (version >=3.2)
		* python3-lxml
		* python3-ply

Usage examples:

	python3 sf2dve.py lift.slx lift.dve
	python3 sf2dve.py lift.xml lift.dve

	Full usage: python3 sf2dve.py --help

	The program is also able to generate an additional process that
	models simplified environment for the model. The variables with the
	scope 'input' are then nondeterministically assigned values within
	given range.


This tool was created as part of a bachelor's thesis on Masaryk 
University Faculty of Informatics, Brno.