README

Golok is an automated tool for discovering the cut-off system instance size of parameterized systems.

FILES

README this file examples/ various example inputs to the program bin/ contains golok binary lib/ support files

AUTHOR

David Samuelson [email protected]

Please include "[Golok]" in the subject line.

INSTALL

Unpack golok-vx.x.tar.bz2.

The binary was built on a Fedora 10 (Cambridge) x86 machine. It should work on most modern x86 GNU/Linux distributions.

To run an example and output the simulating subset of the system instance, execute

./golok --sys <example file>

You probably want to use GraphViz (http://www.graphviz.org) to convert the .dot output files to images. Then you can run a command like

dot -Tsvg -o pretty_picture.svg golok_output.dot

to see the simulating subgraph of the solution as an svg graphic.

Execute

./golok --help

to see all command line options, and see the documentation at http://www.cs.iastate.edu/~slede/golok/ for more detailed usage of the tool.

NEWS

v1.2

• input format modified

• many new command line options

• internals cleaned

• default behavior changed

v1.1.2

• moved to sourceforge

• complete rewrite of low-level logic

v1.1.1

• added support for multiple parameterized processes

• input format and topology specification redesigned

• (slightly) improved system state space exploration

v1.1.0

• many internal changes

• input file format modified to match what is referenced in "Behavioral Automata Composition for Automatic Topology Independent Verification of Parameterized Systems" as published in the proceedings of ESEC 2009

v1.0.1

• changed initial-config to use behavioral automata names instead of entry index

v1.0

• first release

COPYING/LICENSE

Copyright (C) 2009, Iowa State University of Science and Technology. All rights reserved.

The Golok framework is available for free for non-profit research and educational purposes. For commercial licensing please contact Hridesh Rajan by sending an e-mail to [email protected]. The compiler, tools, libraries and sources are licensed according to the following license: Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software") for non-profit research and educational purposes, to use this Software subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

BUGS

None known.

Please file a bug report at http://sourceforge.net/projects/golok/support if you discover a problem.