[  overview | download | License ]

Overview

The finite state machine calculator FSMCalc implements data structures and algorithms of Formal Models (FG3) and Model Checking (Systemtheory 1). The input language allows to model classical finite state machines as well as some simple form of process algebra. Algorithms include power construction, complementation, language emptiness check and partial order reduction. More information on the tool and the input language can be found in the bachelor thesis FSMCalc.pdf by Leopold Haller.

Download

[ FSMCalc.zip | FSMCalc.jar | FSMCalc.pdf | jgraph.jar ]

FSMCalc is written in Java with generic programming. You need a newer Java run time environment which supports generics, such as version 1.5, in order to use FSMCalc. The ZIP archive FSMCalc.zip contains the class files of FSMCalc as well as the class files of JGraph. These class files are needed to run the tool and are available as two JAR files FSMCalc.jar and jgraph.jar seperately. The ZIP file also contains the bachelor thesis FSMCalc.pdf by Leopold Haller which serves as reference manual and tutorial.

License

FSMCalc is distributed under the GPL LICENSE. Note that JGraph has a BSD, GPL, and LGPL LICENSE.