============================================================================ This directory contains a bounded LTL model checker and some experiments ============================================================================ This directory contains the following files: boundsmodels-experiments.tar.gz - The experiments used to benchmark boundsmodels 1.0. The top directory is called "boundsmodels-experiments", and the subdirectories are: "boundsmodels-deadlock-experiments": - The 1-safe nets (in PEP format), and the smodels programs which correspond to the bounded model checking translations of these programs. Look at the file "list" how the programs have been generated from nets. Example run: %: boundsmodels1.0 -D -O2 -s -b=1 dp_6.fsa.ll_net | pparse-1.17 | smodels-2.26 smodels version 2.26. Reading...done Answer: 1 Stable Model: p1(0) p3(0) p5(0) p7(0) p9(0) p11(0) p13(0) p17(0) p21(0) p25(0) p29(0) p33(0) t2(0) t6(0) t10(0) t14(0) t18(0) t21(0) p2(1) p4(1) p6(1) p8(1) p10(1) p12(1) p14(1) p18(1) p22(1) p26(1) p30(1) p34(1) True Duration: 0.010 Number of choice points: 0 Number of wrong choices: 0 Number of atoms: 44 Number of rules: 54 Number of picked atoms: 2 Number of forced atoms: 1 Number of truth assignments: 75 Size of searchspace (removed): 0 (0) "nusmv-deadlock-experiments": - NuSMV models and command files for deadlock checking. Example usage: %: NuSMV -int < dp_6.bmc.commands %: NuSMV -int < dp_6.bdd.commands "boundsmodels-ltl-experiments": - The 1-safe nets and formulas (in PEP format), and the smodels programs which correspond to the bounded LTL model checking translations of these programs. Look at the file "ltl-list" how the programs have been generated from nets and formulas. Example run: %: boundsmodels1.0 -s -b=7 -O2 -f=dp_6.net.formula1 dp_6.ltl.ll_net | pparse-1.17 | smodels-2.26 smodels version 2.26. Reading...done Answer: 1 Stable Model: p1(0) p3(0) p5(0) p7(0) p9(0) p11(0) p13(0) p17(0) p21(0) p25(0) p29(0) p33(0) t21(0) p12(1) p14(1) p1(1) p3(1) p5(1) p7(1) p9(1) p17(1) p21(1) p25(1) p29(1) p33(1) t1(1) t6(1) p2(2) p4(2) p12(2) p15(2) p22(2) p5(2) p7(2) p9(2) p17(2) p25(2) p29(2) p33(2) t9(2) p2(3) p4(3) p6(3) p7(3) p9(3) p12(3) p15(3) p23(3) p17(3) p25(3) p29(3) p33(3) t14(3) p2(4) p4(4) p6(4) p8(4) p9(4) p12(4) p15(4) p17(4) p23(4) p25(4) p30(4) p33(4) t17(4) p2(5) p4(5) p6(5) p8(5) p10(5) p12(5) p15(5) p17(5) p23(5) p25(5) p31(5) p33(5) t16(5) p2(6) p4(6) p6(6) p7(6) p10(6) p12(6) p15(6) p17(6) p23(6) p25(6) p32(6) p33(6) t19(6) p2(7) p4(7) p6(7) p7(7) p9(7) p12(7) p15(7) p17(7) p23(7) p25(7) p29(7) p33(7) live el(3) l nl(4) il(4) il(5) il(6) il(7) f3(0) f3(1) f5(2) f5(3) f5(4) f5(5) f5(6) f5(7) f7(0) f7(1) f7(2) f9(3) f9(4) f9(5) f9(6) f9(7) f11(0) f11(1) f11(2) f11(3) f11(4) f11(7) f12(5) f10(0) f10(1) f10(2) f10(8) f10(3) f10(4) f10(5) f10(7) f8(3) f8(4) f8(5) f8(7) f6(0) f6(1) f6(2) f6(8) f6(3) f6(4) f6(5) f6(7) f4(2) f4(3) f4(4) f4(5) f4(7) f2(0) f2(1) f2(2) f2(8) f2(3) f2(4) f2(5) f2(7) f1(0) f1(1) f1(2) f1(8) f1(3) f1(4) f1(5) f1(6) f1(7) f0(0) f0(1) f0(2) f0(3) f0(4) f0(5) f0(6) f0(7) f0(8) True Duration: 0.200 Number of choice points: 15 Number of wrong choices: 10 Number of atoms: 528 Number of rules: 1327 Number of picked atoms: 9569 Number of forced atoms: 380 Number of truth assignments: 207282 Size of searchspace (removed): 139 (240) "nusmv-ltl-experiments": - NuSMV models and command files for LTL model checking. Example usage: %: NuSMV -int < dp_6.ltl.bmc.commands %: NuSMV -int < dp_6.ltl.bdd.commands "nusmv-2.1.0.bdd.deadlock.checking.patch": - A patch to NuSMV 2.1.0 (a kludge) we used during BDD based deadlock checking runs. It disables the initialization of fairness sets in NuSMV, and thus renders the CTL and LTL model checkers unusable. (All other runs used an unpatched version of NuSMV 2.1.0.) "corbett-original-specifications": - Original deadlock checking models by corbett, FSA and SMV models. boundsmodels-1.0.tar.gz - The boundsmodels tool, which can generate smodels programs which have a stable model if the net deadlocks. The tar file contains smodels 2.26, so no need to download 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.010 Number of choice points: 3 Number of wrong choices: 2 Number of atoms: 184 Number of rules: 284 Number of picked atoms: 668 Number of forced atoms: 61 Number of truth assignments: 17314 Size of searchspace (removed): 51 (2) Usage: %: boundsmodels ============================================================================ Bounded LTL model checker for 1-safe nets (generates smodels programs) Usage: boundsmodels1.0 [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 1.0, smodels version 2.26, (Jan 15 2002) ============================================================================ Enjoy, Kepa -- Keijo.Heljanko@hut.fi Researcher Laboratory for Theoretical Computer Science Helsinki University of Technology Finland