============================================================================
This directory contains the example nets and programs used in my paper:
============================================================================

Using Logic Programs with Stable Model Semantics
to Solve Deadlock and Reachability Problems
for 1-Safe Petri Nets

Keijo Heljanko

P.O.Box 5400
FIN-02015 HUT
Finland

Keijo.Heljanko@hut.fi

============================================================================
The files are:
============================================================================

dlsmodels.tar.gz

- C++ source code for a deadlock checker using PEP generated complete
finite prefixes as input and a constraint-based logic programming
tool, the smodels system as the computational engine. Also contains
a statically linked Linux x86 binary of the tool dlsmodels. All the parts
of the tool are under GPL, see the file COPYING in the dlsmodels_src
directory for details. It shouldn't be too hard to add input capabilities
for also other prefix input formats, please contact me.

Please email me if you find the tool useful. 

Usage:

============================================================================
Determination of deadlocks (Smodels reachability translation)
Usage: dlsmodels_bin/dlsmodels [OPTION]... file1 [file2]

Options:
        -O0 : Do not optimize the translation
        -O1 : Do only guaranteed linear time optimizations
        -O2 : Do cheap polynomial time optimizations (default)
        -O3 : Do expensive optimizations (much slower than O2)
        -d  : Produce smodels translation only (for debugging)
        -v  : Give verbose translation statistics

        file1 : input file containing unfolding
                extension '.mci': binary coded format
        file2 : output result file

Copyright (c) 1998 Keijo Heljanko <Keijo.Heljanko@hut.fi> (translation)
Copyright (c) 1998 Patrik Simons <Patrik.Simons@hut.fi> (smodels)

Version 1.0, smodels version pre-2.0.30, (Sep 11 1998)
============================================================================

Example use:

%: dlsmodels dme2.mci
TRUE

Time needed:      0.130 s
%: dlsmodels -v elevator_1.fsa.mci
FALSE
E1(000010000000000000001), E2(000020000000000000001),
  E5(000030000000000000001), E6(000040000000000000001),
  E7(000050000000000000001), E9(000050000000000000053),
  E28(000050000000000000070), E34(000050000000000000004),
  E39(000010000000000000008), E44(000050000000000000084),
  E52(000050000000000000060), E62(000050000000000000041),
  E84(000050000000000000062), E108(000040000000000000063).

Time needed:      0.030 s

Smodels statistics:

Duration: 0.020
Number of choice points: 1
Number of wrong choices: 0
Number of atoms: 136
Number of rules: 234
Number of picked atoms: 175
Number of forced atoms: 69
Number of truth assignments: 2355

============================================================================

example_nets.tar.gz

- A gzipped compressed file containg the example nets in PEP format.
It also includes two additional examples, DARTES(1) and DME(12).
We were not able to generate prefixes for these examples on a
machine with 512MB ram, so you might want to skip them.

Credits for the examples:

- The DME series of examples by Ken McMillan.
- The HART series of examples modeled by Stephan Melzer and Stefan Römer.
- All other examples by James C. Corbett, with translation to PEP by
  Stephan Melzer and Stefan Römer.

Thanks to Stefan Römer for letting me redistribute these examples.


Further references in bibtex format:

@inproceedings{McM92,
  AUTHOR = {McMillan, K. L.},
  TITLE = {Using Unfoldings to Avoid the State Space Explosion Problem in the verification of Asynchronous Circuits},
  BOOKTITLE = {Proceeding of 4th Workshop on Computer Aided Verification (CAV'92)},
  YEAR = {1992}, 
  Editor = {},
  Pages = {164--174},
  Organization = {},
  Publisher = {},
  Address = {},
  Month = {},
  Note ={LNCS 663}}

@inproceedings{McM95,
  AUTHOR = {McMillan, K. L.},
  TITLE = {A Technique of a State Space Search Based on Unfolding},
  BOOKTITLE = {Formal Methods is System Design 6(1)},
  YEAR = {1995}, 
  Editor = {},
  Pages = {45--65},
  Organization = {},
  Publisher = {},
  Address = {},
  Month = {},
  Note ={}	}

@techreport{Corbett94:deadlock,
        author = {Corbett, J. C.},
        title = {Evaluating Deadlock Detection Methods for Concurrent Software},
        institution = {Department of Information and Computer Science, University of Hawaii at Manoa},
        year = {1995}
}

@inproceedings{MR:cav97,
  AUTHOR = {Melzer, S. and R\"omer, S.},
  TITLE = {Deadlock Checking Using Net Unfoldings},
  BOOKTITLE = {Proceeding of 9th International Conference on Computer Aided Verification (CAV'97)},
  YEAR = {1997}, 
  Editor = {},
  Pages = {352--363},
  Organization = {},
  Publisher = {Springer-Verlag},
  Address = {Haifa, Israel},
  Month = {Jun},
  Note ={LNCS 1254}}

@inproceedings{Best96:pomiv,
author={Best, E.},
title={Partial Order Verification with {P}{E}{P}},
booktitle={Proceedings of POMIV'96, Workshop on Partial Order Methods in Verification},
year={1996},
editor={Holzmann, G. and Peled, D. and Pratt, V.},
publisher={American Mathematical Society},
month=jul,
}

============================================================================

example_prefixes.tar.gz

- Prefix files generated by PEP for the examples. If you have access
to PEP, you can unfold the nets yourself, and then you don't need
this file.

============================================================================

Enjoy,


		Kepa

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