============================================================================ This directory contains a model 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 prefix from a 1-safe Petri net e.g. by the PEP command: EVunfold mynet.ll_net -m=mynet.mci -c -n=1 -s -@ 2. mcsmodels is used to check whether the net can deadlock (FALSE) or not (TRUE). If a deadlock can be reached, a sequence of events leading to the deadlock will be printed: mcsmodels mynet.mci 3. mcsmodels can also be used to check for reachability properties i.e. formulas in PEP-syntax which contain only one diamond or box operator. An example would be: %: cat example_formula #(P1 + P2+ P3 + P4 + P5 + P6 + P7) %: mcsmodels -f=example_formula gas_station.mci FALSE E2(T13), E3(T15), E4(T16), E5(T17), E6(T18), E7(T7). Time needed: 0.010 s (Notice PEP formula notation: ^ = diamond = EF in CTL # = box = AG in CTL + = OR * = AND - = negation ) ============================================================================ The files in this directory are : ============================================================================ CHANGES - Changes since version 1.0, with tips on command line options. mcsmodels-1.7.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. All the parts of the tool are under GPL, see the file COPYING for details. See file CHANGES for changes since first release. 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: ============================================================================ Safe net model checker (Smodels reachability translation) Usage: ./mcsmodels [OPTION]... file1 [file2] Options: -f=fname : Model check the formula in the file fname -D : Deadlock check the net (default) -O0 : Do not optimize the translation -O1 : Do only guaranteed linear time optimizations -O2 : Do cheap polynomial time optimizations -O3 : Do also enabledness closure (default) -O4 : Do expensive optimizations (much slower than O3) -n : Use smodels with no lookahead (fast for easy examples) -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-9 Keijo Heljanko (translation) Copyright (c) 1998-9 Patrik Simons (smodels) Version 1.4, smodels version 2.23, (Sep 7 1999) ============================================================================ Example use: %: mcsmodels dme2.mci TRUE Time needed: 0.050 s %: mcsmodels -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.010 s Smodels statistics: Duration: 0.010 Number of choice points: 1 Number of wrong choices: 0 Number of atoms: 136 Number of rules: 206 Number of picked atoms: 174 Number of forced atoms: 69 Number of truth assignments: 2329 Size of searchspace (removed): 18 (0) ============================================================================ 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)}, pages={240--254}, year={1999}, publisher={Springer-Verlag, Berlin}, month=mar, note={LNCS 1579}, IGNOREnote={Available at http://\linebreak[3]www.tcs.hut.fi/\~{ }kepa/publications/KH-tacas99.ps.gz} } @article{Heljanko:Fundamenta99, author={Heljanko, K.}, title={Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe {Petri} Nets}, journal={Fundamenta Informaticae}, volume={37}, number={3}, pages={247--268}, year={1999}, publisher={IOS Press} } ============================================================================ Enjoy, Kepa -- Keijo.Heljanko@hut.fi Researcher Laboratory for Theoretical Computer Science Helsinki University of Technology Finland