============================================================================ This directory contains a bounded LTL model checker and some experiments ============================================================================ This directory contains the following files: LPNMR2001-deadlock-experiments.tar.gz - The 1-safe nets (in PEP) format, and the smodels programs which correspond to the bounded model checking translations of these programs. (These are exactly the same as used in ASP2001.) LPNMR2001-LTL-demo-examples.tar.gz - A small set of LTL model checking examples, for demonstration use only. There are three 2 process mutex algorithms. The formulas are: + formula1: Two processes are never both in the critical section at the same time + formula2: Process 1 will not get to the critical section + formula3: Process 1 will not get into the critical section inifitely often The programs have been generated with small enough bounds to make smodels terminate quickly on my machine. boundsmodels-0.9.tar.gz - The boundsmodels tool, which can generate smodels programs which have a stable model if the net deadlocks / the LTL formula does not hold. (See the paper below for a better description.) The tar file contains smodels 2.26, so no need to dowload it. You also need the pparse tool, it can be directly obtained from: http://www.tcs.hut.fi/Software/smodels/src/pparse-1.17.tar.gz A sample session from deadlock checking with step semantics: %: boundsmodels -D -s -b=4 elevator_1.ll_net | pparse | smodels smodels version 2.26. Reading...done Answer: 1 Stable Model: p1(0) p12(0) p19(0) p28(0) t1(0) t7(0) t8(0) t9(0) p2(1) p13(1) p20(1) p29(1) t12(1) t51(1) p3(2) p14(2) p21(2) p30(2) t73(2) p3(3) p14(3) p26(3) p62(3) t11(3) t14(3) p5(4) p14(4) p27(4) p63(4) True Duration: 0.000 Number of choice points: 6 Number of wrong choices: 5 Number of atoms: 179 Number of rules: 277 Number of picked atoms: 879 Number of forced atoms: 60 Number of truth assignments: 19148 Size of searchspace (removed): 51 (0) A sample session from LTL model checking with interleaving semantics: %: boundsmodels -i -b=12 -O2 -f=dijkstra_2-formula2.ltl dijkstra_2.ll_net | pparse | smodels smodels version 2.26. Reading...done Answer: 1 Stable Model: p5(0) p23(0) p26(0) p44(0) p51(0) p55(0) p59(0) p63(0) p67(0) t84(0) p58(1) p5(1) p23(1) p26(1) p44(1) p51(1) p55(1) p63(1) p67(1) t82(1) p50(2) p58(2) p5(2) p23(2) p26(2) p44(2) p55(2) p63(2) p67(2) t34(2) p4(3) p50(3) p57(3) p23(3) p26(3) p44(3) p55(3) p63(3) p67(3) t68(3) p6(4) p50(4) p57(4) p23(4) p26(4) p44(4) p55(4) p63(4) p67(4) t14(4) p14(5) p50(5) p57(5) p23(5) p26(5) p44(5) p55(5) p63(5) p67(5) t85(5) p14(6) p50(6) p57(6) p62(6) p23(6) p26(6) p44(6) p55(6) p67(6) t83(6) p14(7) p50(7) p54(7) p57(7) p62(7) p23(7) p26(7) p44(7) p67(7) t26(7) p13(8) p50(8) p53(8) p57(8) p62(8) p23(8) p26(8) p44(8) p67(8) t67(8) p15(9) p50(9) p53(9) p57(9) p62(9) p23(9) p26(9) p44(9) p67(9) t42(9) p20(10) p50(10) p53(10) p57(10) p62(10) p23(10) p26(10) p44(10) p67(10) t69(10) p20(11) p21(11) p50(11) p53(11) p57(11) p62(11) p26(11) p44(11) p67(11) t59(11) p19(12) p22(12) p50(12) p53(12) p57(12) p62(12) p26(12) p44(12) p67(12) f1(12) f0(0) f0(1) f0(2) f0(3) f0(4) f0(5) f0(6) f0(7) f0(8) f0(9) f0(10) f0(11) f0(12) True Duration: 0.160 Number of choice points: 8 Number of wrong choices: 0 Number of atoms: 1000 Number of rules: 2657 Number of picked atoms: 3457 Number of forced atoms: 150 Number of truth assignments: 130552 Size of searchspace (removed): 193 (293) The syntax of the formula files is the PEP tool LTL format, the operators are: - = negation + = disjunction * = and G = box F = diamond U = until R = release Usage: %: boundsmodels ============================================================================ Bounded LTL model checker for 1-safe nets (generates smodels programs) Usage: boundsmodels [OPTION]... file1 [file2] Options: -b=num : The number of time steps -f=fname : Model check the LTL formula (in PEP format) in the file fname -D : Deadlock check the net -s : Use step semantics (default) -i : Use interleaved semantics -O0 : Do not optimize the translation -O1 : Do only simple optimizations -O2 : Do also duplicate rule removal (default) file1 : input file containing unfolding extension '.ll_net': PEP low level net file2 : output result file Copyright (c) 1998-2001 Keijo Heljanko (unfolder) Copyright (c) 1998-2000 Patrik Simons (smodels) Version 0.9, smodels version 2.26, (Apr 5 2001) ============================================================================ For more information, see the paper: Heljanko, K. and Niemelä, I.: Bounded LTL Model Checking with Stable Models. In Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'2001), pages 200-212, Lecture Notes in Computer Science 2173, Vienna, Austria, September 2001. Email me if you find the tool useful. Enjoy, Kepa -- Keijo.Heljanko@hut.fi Researcher Laboratory for Theoretical Computer Science Helsinki University of Technology Finland