============================================================================ This directory contains a bounded reachability checker for 1-safe Petri nets ============================================================================ This directory contains the following files: - punroll-0.3.tar.gz A process unroller version 0.3 (beta). Given a 1-safe Petri net and a bound n, it generates a constrained Boolean circuit which is satisfiable iff the net system has an execution of length n in (process, step, interleaving) semantics. It can also add a part to the circuit which requires that the execution ends in a deadlocked state. (If you need other reachability properties to be checked, add them by hand or contact me for an updated version.) The tool is free software under GPL license, see file COPYING. - Concur2001-nets.tar.gz Nets used in experiments, in PEP low-level net format. - Concur2001-circuits.tar.gz Boolean circuits generated from nets, in BCSat format. - Concur2001-exp-list A list of commands which generates all the circuits from the nets. To check whether the circuits are satisfiable you'll need the BCSat tool, which is available from: http://www.tcs.hut.fi/~tjunttil/bcsat/ A sample session works as follows: %: punroll-0.3 -b=4 -p -D -O1 elevator_1.ll_net | bcsat-0.3 -v parsing from stdin Original circuit has 510 gates Max-min height of the circuit is 6 Shared circuit has 377 gates Simplified circuit has 337 gates Shared circuit has 297 gates Simplified circuit has 296 gates Shared circuit has 296 gates Simplified circuit has 294 gates Shared circuit has 286 gates Simplified circuit has 286 gates Shared circuit has 286 gates Simplified circuit has 286 gates Lookahead determined the value of 183 gates Shared circuit has 286 gates Simplified circuit has 208 gates Shared circuit has 61 gates Simplified circuit has 61 gates Shared circuit has 61 gates Simplified circuit has 61 gates Max-min height of the reduced circuit is 1 COI-reduced circuit has 53 gates Choice points: 3 Wrong choices: 0 Circuit is satisfiable Solution: ~p54_3 ~t79_2 ~p54_4 ~t67_2 ~fp55_3 ~p55_2 ~t52_1 ~t61_2 ~t59_2 ~t57_2 ~t4_0 ~gp20_2 ncp17_2 ~t71_2 ~t69_2 ~p58_2 ~t63_1 ~p58_3 ~fp58_3 ~t80_2 ~p58_4 ~t63_3 ~gfp28_3 ~gp28_3 ~p28_2 ~fp28_2 p28_1 t8_0 ~t64_1 ~t62_1 ~t54_1 ~t53_1 t50_1 ~p31_4 ~gfp53_4 ~t53_3 ~p53_3 ~fp53_3 ~p53_2 tt64_1 ~p16_1 ~gp28_1 ~gp16_1 tt64_3 ~t64_3 ~p28_3 ~p16_3 ~gp16_3 ~p16_2 ~fp16_2 tt12_3 ~t12_3 ~p23_3 ~gp23_3 ~t76_2 ~t74_2 p2_3 p2_2 t11_1 ~p35_4 ~gp1_1 ~gp53_2 ~p60_2 ~p60_3 ~fp60_3 ~p60_4 ~t62_3 ~fp61_4 p61_3 t72_2 t10_3 ~p39_2 ~p39_3 ~fp39_3 ~p39_4 ~t54_3 p12_1 t6_0 ~p12_2 ~fp12_2 ~p12_3 ~gp12_3 ~p12_4 ~fp12_4 ~t50_3 ~p2_4 ~fp2_4 ~t14_3 t13_3 ~p16_4 ~fp16_4 ~fp17_3 ~p17_2 ~gp17_2 ~p41_4 ~p6_4 tt74_2 p20_2 ~gp39_2 ~p45_4 tt0_0 t0_0 p0_0 ~gfp15_4 ~gp15_4 ~t52_3 ~p15_3 ~fp15_3 ~p15_2 ~gp15_2 ~p49_4 tt4_0 p11_0 ~p22_3 ~gp22_3 ~p22_4 ~fp22_4 ~fp23_4 tt8_0 p27_0 gp19_1 tt80_2 ~gp58_2 p26_4 ~fp27_1 ~p51_4 tt59_2 ~gp55_2 ~live_4 ~p0_4 ~p0_3 ~p0_2 ~p0_1 ~fp0_1 ~p3_4 ~p7_4 ~p9_4 ~p11_4 ~p11_3 ~p11_2 ~p11_1 ~fp11_1 ~t5_0 ~p18_4 ~p18_3 ~p18_2 ~p18_1 ~fp18_1 p18_0 t7_0 ~p27_4 ~p27_3 ~p27_2 ~p27_1 ~p36_4 ~p61_4 ~p19_4 ~p19_3 ~p19_2 ~fp19_2 p19_1 ~p1_4 ~p1_3 ~p1_2 ~fp1_2 p1_1 ~p23_4 ~p25_4 ~fp25_4 p25_3 ~p28_4 ~fp28_4 ~p5_4 ~p42_4 ~p33_4 ~p46_4 ~p30_4 ~p43_4 ~p52_4 ~p8_4 ~p10_4 ~p14_4 ~fp14_4 ~p14_3 ~gp14_3 ~p14_2 ~fp14_2 ~p14_1 ~p15_4 ~p55_4 ~p55_3 ~p17_4 ~gp17_4 ~p17_3 ~p29_4 ~p29_3 ~fp29_3 p29_2 ~p20_4 ~p20_3 ~fp20_3 ~p44_4 ~p56_4 ~p56_3 ~fp56_3 ~p56_2 ~p37_4 ~p53_4 ~p34_4 ~p47_4 ~p48_4 ~p38_4 ~p21_4 ~p50_4 ~p59_4 ~p59_3 ~p32_4 ~p24_4 ~p40_4 ~p40_3 ~p57_4 ~p57_3 ncp14_1 ncp14_3 tt61_2 ~gfp29_4 gp25_3 non_idle_0 non_idle_1 non_idle_2 gp29_2 non_idle_3 tt13_3 ~gfp58_4 ncp20_2 tt69_2 ~gp60_2 p13_2 p13_3 p13_4 ~gfp60_4 ncp28_1 ncp28_3 tt71_2 ~gfp39_4 ~gfp12_3 ~gfp16_3 gp12_1 tt79_2 tt5_0 tt52_1 ~gp14_1 tt52_3 ncp11_0 ncp15_2 tt62_1 ncp2_3 tt62_3 tt10_3 gp61_3 ~gfp55_4 tt14_3 p62_4 p4_4 tt72_2 ~gfp13_4 tt76_2 ~gp56_2 ~gfp17_4 tt6_0 tt53_1 tt53_3 ncp60_2 tt57_2 ncp16_1 ncp16_3 tt63_1 tt63_3 tt11_1 ~gfp56_4 tt67_2 ncp55_2 ~gfp14_3 tt50_1 tt50_3 tt7_0 tt54_1 tt54_3 Please email me if you find the tool useful. Usage: %: punroll ============================================================================ Process unroller for 1-safe nets (Outputs boolean circuits) Usage: punroll [OPTION]... file1 [file2] Options: -R : Give transition relation and initial predicate (default) -b=num : The number of time steps to unroll -D : Deadlock check the net -p : Use process semantics (default) -s : Use step semantics -i : Use interleaved semantics -n : Do not allow empty timesteps (default) -e : Allow empty timesteps -O0 : Do not optimize the translation -O1 : Do optimizations (default) file1 : input file containing unfolding extension '.ll_net': PEP low level net file2 : output result file Copyright 2001 Keijo Heljanko Version 0.3, (Mar 25 2001) ============================================================================ Enjoy, Kepa -- Keijo.Heljanko@hut.fi Researcher Laboratory for Theoretical Computer Science Helsinki University of Technology Finland