============================================================================
This directory contains a LTL model checker using net unfoldings
============================================================================

The tool is free software under the GPL license, see file COPYING.


This directory contains the following files:


unfsmodels-0.9.tar.gz

- The unfsmodels 0.9 LTL model checker (beta).
  The unfsmodels is a prototype tool. If you need something fast
  for conventional prefix generation, I suggest you try ERVunfold
  by S.Römer. (You can get it e.g. from the Model Checking kit:
  http://wwwbrauer.informatik.tu-muenchen.de/gruppen/theorie/KIT/ )



See the following URL for example some nets and formulas:

http://www.tcs.hut.fi/~kepa/experiments/spin2001/



PLEASE NOTE: If you want to check other LTL formulas, you also need the
"qq" model checker tool by F.Wallner, and the "Spin" tool. You can still
test unfsmodels with the supplied examples by going directly to step 4
in the instructions below.

The "qq" tool can be dowloaded from:
http://www7.in.tum.de/gruppen/theorie/QQ

The "Spin" tool is available from:
http://netlib.bell-labs.com/netlib/spin/whatispin.html



LTL model checking use is as follows:

1. Make a (1-safe) net system foo.ll_net (in PEP format)

2. Make an LTL-formula foo.ltl (in PEP format)

3. Synchronize them using (see note above):
qq foo.ll_net foo.ltl -S

4. Model check the synchronization result:
unfsmodels -v -l foo.sync.ll_net


If you want to generate a conventional prefix:

1. Make a (1-safe) net system foo.ll_net (in PEP format)

2. Generate a conventional prefix (in PEP .mci format):
unfsmodels -v -m=foo.mci foo.ll_net



Please email me if you find the tool useful. 

Usage:

============================================================================
Safe net unfolder and LTL checker (Smodels based)
Usage: /home/kepa/bin/unfsmodels-0.9 [OPTION]... file1 [file2]

Options:
        -m=<mci_file> : Output the prefix in '.mci' file format
        -l            : Do LTL model checking
        -v            : Give verbose statistics

        file1         : input file containing unfolding
                        extension '.ll_net': PEP low level net
        file2         : output result file

Copyright (c) 1998-2001 Keijo Heljanko <Keijo.Heljanko@hut.fi> (unfolder)
Copyright (c) 1998-2000 Patrik Simons <Patrik.Simons@hut.fi> (smodels)

Version 0.9, smodels version 2.26, (Feb 19 2001)
============================================================================


For the theory behind this tool, see the technical report:

J.Esparza and K.Heljanko: Implementing LTL Model Checking with
Net Unfoldings. Research Report A68, Laboratory for Theoretical
Computer Science, Helsinki University of Technology, Espoo,
Finland, March 2001, 29p. Available at:

http://www.tcs.hut.fi/Publications/reports/A68abstract.html



Enjoy,

                Kepa

--
Keijo.Heljanko@hut.fi
Researcher
Laboratory for Theoretical Computer Science
Helsinki University of Technology
Finland