------------------------------------------------------------------------------- This directory contains the 1-safe Petri net deadlock checking tutorial demo nets and tools for the Advanced Tutorial at ACSD 2006 / Petri Nets 2006 - Bounded Model Checking Keijo Heljanko and Tommi Junttila Turku, Finland, June 26, 2006 Example runs for the small net from the slides: $ cat running.net P = ['p1','p2','p3','p4','p5','p6'] T = ['t1','t2','t3','t4','t5','t6'] F = [['p1','t1'],['t1','p3'], ['p2','t2'],['t2','p4'], ['p4','t3'],['t3','p5'], ['p3','t4'],['p5','t4'],['t4','p1'],['t4','p2'], ['p5','t5'],['t5','p2'], ['p5','t6'],['t6','p6']] M_0 = ['p1','p2'] bound = 4 semantics = "interleaving" $ ./1b-pn-bmc < running.net | bczchaff -v| ./cex-print {p1, p2}[t1>{p2, p3}[t2>{p3, p4}[t3>{p3, p5}[t6>{p3, p6} $ cat step-running.net P = ['p1','p2','p3','p4','p5','p6'] T = ['t1','t2','t3','t4','t5','t6'] F = [['p1','t1'],['t1','p3'], ['p2','t2'],['t2','p4'], ['p4','t3'],['t3','p5'], ['p3','t4'],['p5','t4'],['t4','p1'],['t4','p2'], ['p5','t5'],['t5','p2'], ['p5','t6'],['t6','p6']] M_0 = ['p1','p2'] bound = 3 semantics = "step" $ ./1b-pn-bmc < step-running.net | bczchaff -v | ./cex-print {p1, p2}[t2>{p1, p4}[t1, t3>{p3, p5}[t6>{p3, p6} $ cat process-running.net P = ['p1','p2','p3','p4','p5','p6'] T = ['t1','t2','t3','t4','t5','t6'] F = [['p1','t1'],['t1','p3'], ['p2','t2'],['t2','p4'], ['p4','t3'],['t3','p5'], ['p3','t4'],['p5','t4'],['t4','p1'],['t4','p2'], ['p5','t5'],['t5','p2'], ['p5','t6'],['t6','p6']] M_0 = ['p1','p2'] bound = 3 semantics = "process" $ ./1b-pn-bmc < process-running.net | bczchaff -v | ./cex-print {p1, p2}[t1, t2>{p3, p4}[t3>{p3, p5}[t6>{p3, p6} The licence for the "1b-pn-bmc" and "cex-print" Python scripts is the GNU General Public License (GPL), version 2, see: http://www.gnu.org/licenses/gpl.txt The sources for the circuit bczchaff extension for zChaff are from: http://www.tcs.hut.fi/~tjunttil/circuits/index.html Almost all deadlock checking examples are the ones used by Toni Jussila for his PhD Thesis: Toni Jussila. On bounded model checking of asynchronous systems. Research Report A97, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, October 2005. Doctoral dissertation. Available from: http://lib.tkk.fi/Diss/2005/isbn9512279045/ They were generated with a tool by Toni Jussila from FSA descriptions by James C. Corbett [Co95] (They differ from earlier models by the same name used e.g., by Melzer and Römer [MR97] and Heljanko [Hel01], the ones here match the original FSA models in statespace size.): The only exception to the above rule is the "byzagr4_2a" example, which is from [Me97]. [Co95] Corbett, J. C.: Evaluating Deadlock Detection Methods for Concurrent Software, Technical Report, Department of Information and Computer Science, University of Hawaii at Manoa, 1995. [MR97] Stephan Melzer, Stefan Römer: Deadlock Checking Using Net Unfoldings. CAV 1997: 352-363, LNCS 1254. [Hel01] Keijo Heljanko. Bounded reachability checking with process semantics. In Kim Guldstrand Larsen and Mogens Nielsen, editors, Proceedings of the 12th International Conference on Concurrency Theory (Concur'2001), volume 2154 of Lecture Notes in Computer Science, pages 218\u2013232, Aalborg, Denmark, August 2001. Springer-Verlag [Me97] Merkel, S.: Verification of Fault Tolerant Algorithms Using PEP, Technical report, Technische Universität München, TUM-19734, SFB-Bericht Nr. 342/23/97 A, München, Germany, 1997. -------------------------------------------------------------------------------