============================================================================
This directory contains a deadlock checker using finite complete prefixes:
============================================================================

It is currently and add-on tool to the PEP toolset, but other prefix based
tools could also be supported. The use of this tool goes as follows:

1. PEP is used to generate a complete finite perix from a 1-safe Petri net
e.g. by the PEP command:

EVunfold mynet.ll_net -m=mynet.mci  -b -c -n=1 -s -@

2. dlsmodels is used to check whether the net can deadlock (FALSE) or
not (TRUE). It a deadlock can be reached, a sequence of events leading to
the deadlock will be printed:

dlsmodels mynet.mci

============================================================================
The files in this directory are :
============================================================================

dlsmodels-1.0.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

============================================================================
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 ={}	}

@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,
}

@inproceedings{Heljanko:CSP98,
author={Heljanko, K.},
title={Deadlock Checking for Complete Finite Prefixes Using Logic Programs with
Stable Model Semantics (Extended Abstract)},
booktitle={Proceedings of the Workshop Concurrency, Specification \& Programming 1998},
series={Informatik-Bericht Nr. 110},
pages={106--115},
year={1998},
publisher={Humboldt-University, Berlin},
month=sep,
IGNOREnote={Available at http://\linebreak[3]www.tcs.hut.fi/\~{ }kepa/publications/KH_csp98.ps.gz}
}

@inproceedings{Heljanko:Tacas99,
author={Heljanko, K.},
title={Using Logic Programs with Stable Model Semantics to Solve
Deadlock and Reachability Problems for 1-Safe Petri Nets},
booktitle={Proceedings of Fifth International Conference on
Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99)},
addlaterpages={},
year={1998},
publisher={Springer-Verlag, Berlin},
month=mar,
note={Accepted for publication}
}

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

Enjoy,


		Kepa

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