The Petri Net API A collection of Petri net-related functions Niels Lohmann, Stephan Mennicke, and Christian Sura Universität Rostock, Institut für Informatik,  Rostock, Germany pnapi@service-technology.org Abstract. This paper introduces the Petri Net API, a C++ library of Petri net-related functions. The Petri Net API is currently used in more than a dozen Petri net tools, ranging from compilers to verification tools. 1 Introduction Algorithms to reason about the correctness of distributed systems usually have devastating worst-case complexities. Nevertheless, experiences in the field of model checking show that the feared state space explosion can be alleviated by state space reduction techniques or symbolic representations [5]. Therefore, novel techniques to verify correctness often require a proof-of-concept implementation to conduct experiments or to demonstrate feasibility on realistic input data. We recently investigated the academic software development process [14] and claimed that single purpose tools have the right granularity to be implemented using rapid prototyping techniques. A prerequisite for this is the encapsulation of frequently recurring functionality into reusable libraries to avoid an unnecessary “reinvention of the wheel” and to minimize the amount of untested ad-hoc code. This paper introduces with the Petri Net API such a reusable library. It was originally derived from the back-end of the compiler BPEL2oWFN [12] and offered simple net management functionality and the file output in several formats. In the last years, the functions of the Petri Net API have been revised and collected into a consistent C++ library. The main focus of the API is to organize Petri nets, rather than to implement verification algorithms (i.e., to build and analyze state spaces) or to provide a graphical front-end. We claim that these tasks should be part of a dedicated tool rather than a library that is designed to be shared by several tools. As of September , the Petri Net API is used by  tools, see http://service-technology.org/tools for an overview. The rest of this paper is organized as follows. The next section presents the features that are implemented by the Petri Net API. Then Sect. 3 shows how the Petri Net API can be used in novel tools, discusses its availability, and the integration in third-party tools. Section 4 presents a small case study in which the Petri Net API is used to perform some structural modifications to check a correctness notion for workflow nets. Section 5 briefly compares the Petri Net API to existing frameworks, before Sect. 6 concludes the paper. 2 Features The Petri Net API implements the following features to organize Petri nets. – Petri net creation and manipulation (creation, modification, deletion, copying, and search of nodes and arcs), – file import and export of Petri nets in various file formats (PNML [9], LoLA [22] file format, Fiona [15] open net format, Woflan [21] workflow nets), – generation of graphical representation using Graphviz dot, – efficient application of structural reduction rules [17,19,18], – structural checks (e.g., workflow net structure, free-choice property), – import from automata (using the region theory tools Petrify [6] or Genet [3]), – export to automata, – support for open nets [23] (ports, net composition) – organization of final markings, and – support for role annotations. The Petri Net API can be easily extended to new features. As of now, we only moved features from a tool into the Petri Net API when this feature is used by at least one other tool. This avoids a cluttered API full of too specific functions. At the same time, it ensures a high test case coverage of the features. 3 Usage Integration as C++ library. The API itself is written in C++ and can be integrated into other tools with no more effort than including a header file. Listing 1.1 shows example code to read a file in PNML format, structurally reduce it using the Murata rules [17], and output a graphical representation. Listing 1.1. Example using the Petri Net API as C++ library. # include < pnapi / pnapi .h > using namespace pnapi ; int main () { // read PNML net from file std :: istream in ( " file . pnml " , std :: ios_base :: in ) ; in >> io :: pnml >> net ; // apply r e d u c t i o n rules net . reduce ( PetriNet :: SET_MURATA ) ; // output the Petri net in G r a p h v i z dot format std :: cout << io :: dot << net ; return 0; } The Petri Net API complies with the 1998 ANSI/ISO C++ standard and can be compiled on many platforms, including Microsoft Windows, Sun Solaris, GNU/Linux, Mac OS X, and other UNIX-based operating systems. Command-line tool. Beside the direct integration, we implemented a command- line tool petri (part of the Petri Net API distribution) for the most common operations. The call petri *. pnml -- input = pnml -- reduce = murata -- output = png performs a similar transformation as the code in Listing 1.1, but is also able to read multiple files and to directly create graphics files. This front-end tool is very useful in shell scripts to process large libraries of nets. Integration into third-party tools. The Petri Net API is currently indirectly (as front-end tool or library) integrated into the business process modeling tool Oryx [7], the process mining toolkit ProM [20], and the YAWL workflow editor [2]. In all tools, the Petri Net API organizes the exchange of Petri Net models in PNML format. 3.1 Availability The Petri Net API is free open source software, licensed under the GNU LGPL 3.1 The most recent version together with its manual can be downloaded at http://service-technology.org/pnapi. 4 Case study: Checking relaxed soundness To demonstrate the usage of the Petri net API in a realistic setting, we discuss a small case study in this section. We show how relaxed soundness [8], a correctness property of workflow nets [1], can be translated into a series of reachability problems that can be checked by LoLA [22]. Relaxed soundness requires for every transition of the workflow net to occur in at least one successful firing sequence from the initial marking [i] to the final marking [o]. Dehnert and Aalst [8] provided a verification algorithm for this property in which builds the state space of the workflow net and then analyzes its runs. This algorithm is implemented in the tool Woflan [21]. It is, however, not clear whether state space reduction techniques are applicable. Alternatively, we can reformulate the above requirement in a reachability problem as follows. Given a workflow net N and a transition t of N , we can construct a Petri net Nt which only reaches a final marking iff N reaches a final marking by a transition sequence which includes t. We create Nt by adding to N a transition t0 and two places p1 and p2 . Figure 1 illustrates the construction. Thereby, p1 is marked as long t has not yet fired, and p2 is marked after t has fired at least once. We then can check wether the marking [o, p2 ] is reachable from the initial marking [i, p1 ]. If this check succeeds for all nets Nt , we can conclude relaxed soundness of N . 1 GNU Lesser General Public License, http://www.gnu.org/licenses/lgpl.html p1 t t p2 t� (a) subnet of N (b) subnet of Nt Fig. 1. Transforming relaxed soundness into a reachability problem. Listing 1.2. Construction of Nt using the Petri Net API. # include < pnapi / pnapi .h > using namespace pnapi ; void c o n s t r u c t A n a l y s i s N e t s ( PetriNet & N ) { // iterate t r a n s i t i o n s PNAPI_FOREACH ( trans , N . getTra nsition s () ) { // create copy of the net PetriNet Nt ( N ) ; // create a n a l y s i s subnet for current t r a n s i t i o n ( see Fig . 1) Place & p1 = Nt . createPlace () ; Place & p2 = Nt . createPlace () ; Transition * t = Nt . findTra nsition ((* trans ) -> getName () ) ; Transition & tprime = Nt . c r ea t e T r a n s i t i o n () ; // connect a n a l y s i s subnet PNAPI_FOREACH (p , t - > getPreset () ) { Nt . createArc (** p , tprime ) ; } PNAPI_FOREACH (p , t - > getPostset () ) { Nt . createArc ( tprime , ** p ) ; } p1 . setTokenCount (1) ; Nt . createArc ( p1 , * t ) ; Nt . createArc (* t , p2 ) ; Nt . createArc ( p2 , tprime ) ; Nt . createArc ( tprime , p2 ) ; // write nets into LoLA files std :: ofstream o ; o . open ( " N_ " + (* trans ) -> getName () + " . lola " , std :: ios_base :: trunc ) ; o << pnapi :: io :: lola << Nt << std :: endl ; o << " FORMULA ( " << pnapi :: io :: lola << Nt . g e t F i n a l C o n d i t i o n () << " AND " << p2 . getName () << " = 1 ) " << std :: endl ; } } Listing 1.2 shows a function implementing this construction. It assumes a Petri net N is given and writes, for each transition t of N , a Petri net Nt in LoLA file format together with a formula expressing the final marking to disk. The implementation is straightforward and is — due the encapsulation of the Petri net functions — nearly on a pseudocode level. The Petri net model checker LoLA can read these generated files and check whether the included formula can be satisfied by a reachable marking. The described transformation and check is implemented as service-oriented extension of the business process editor Oryx [7]. 5 Related work The idea to collect Petri net-related functions in a library or toolbox is not new (see [16,4] and the Petri Net World Website2 listing hundreds of tools). We discuss two prominent examples. The Petri Net Kernel [11] was designed as a modular kernel that is designed to integrate Petri net algorithms. Petri net types are not fixed, but can be freely defined and extended. Similarly, the PNML framework [10] is a reference implementation of the PNML standard. It is designed to facilitate import and export of PNML standard compliant files and provides a complex meta model to support different kinds of Petri nets. Again, its focus lies on flexibility. In contrast, the Petri net API has a fixed feature set and new features are only added when they are also used by other tools. Furthermore, it was not originally designed as a generic Petri net framework, but was created by “outsourcing” Petri net-related code from actual tools. Finally, it is implemented in C++ due to performance considerations. 6 Conclusion This paper introduced the Petri Net API, a library of Petri net-related functions. We observed that the Petri Net API greatly simplified rapid prototyping. The encapsulation of Petri net-related functions lead to smaller tools which could focus on their main functionality; see [13] for a discussion. After four years of development and a consolidated feature set, we claim that this API is useful to other researchers in the Petri net community. The main advantage of the Petri Net API is that its implemented functions are heavily used for several years and thus has a well-tested and justified feature set. Acknowledgments. The authors thank Christian Gierds, Dennis Reinert, Georg Straube, Robert Waltemath, and Martin Znamirowski for their work on earlier versions of the Petri Net API. References 1. Aalst, W.M.P.v.d.: The application of Petri nets to workflow management. Journal of Circuits, Systems and Computers 8(1), 21–66 (1998) 2. Aalst, W.M.P.v.d., Hofstede, A.H.M.t.: YAWL: yet another workflow language. Inf. Syst. 30(4), 245–275 (2005) 2 http://www.informatik.uni-hamburg.de/TGI/PetriNets/tools/ 3. Carmona, J., Cortadella, J., Kishinevsky, M.: Genet: a tool for the synthesis and mining of Petri nets. In: ACSD 2009. pp. 181–185. IEEE (2009) 4. Chouikha, A., Fay, A., Schnieder, E.: Konzept eines Frame- works für Petrinetz- Editoren. In: AWPN 1998. pp. 32–37. No. 694 in Research Reports, Universität Dortmund, Fachbereich Informatik (1998) 5. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999) 6. Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Petrify: A tool for manipulating concurrent specifications and synthesis of asynchronous controllers. Trans. Inf. and Syst. E80-D(3), 315–325 (1997) 7. Decker, G., Overdick, H., Weske, M.: Oryx - an open modeling platform for the bpm community. In: BPM 2008. pp. 382–385. LNCS 5240, Springer (2008) 8. Dehnert, J., Aalst, W.M.P.v.d.: Bridging the gap between business models and workflow specifications. Int. J. Cooperative Inf. Syst. 13(3), 289–332 (2004) 9. Hillah, L.M., Kindler, E., Kordon, F., Petrucci, L., Trèves, N.: A primer on the Petri Net Markup Language and ISO/IEC 15909-2. Petri Net Newsletter 76, 9–28 (2009) 10. Hillah, L.M., Kordon, F., Petrucci, L., Trèves, N.: PNML framework: An extendable reference implementation of the Petri Net Markup Language. In: PETRI NETS 2010. pp. 318–327. LNCS 6128, Springer (2010) 11. Kindler, E., Weber, M.: The Petri Net Kernel - an infrastructure for building Petri net tools. STTT 3(4), 486–497 (2001) 12. Lohmann, N.: A feature-complete Petri net semantics for WS-BPEL 2.0 and its compiler BPEL2oWFN. Informatik-Berichte 212, Humboldt-Universität zu Berlin, Berlin, Germany (2007) 13. Lohmann, N., Weinberg, D.: Wendy: A tool to synthesize partners for services. In: PETRI NETS 2010. pp. 297–307. LNCS 6128, Springer (2010) 14. Lohmann, N., Wolf, K.: How to implement a theory of correctness in the area of business processes and services. In: BPM 2010. pp. 61–77. LNCS 6336, Springer (2010) 15. Massuthe, P., Weinberg, D.: Fiona: A tool to analyze interacting open nets. In: AWPN 2008. pp. 99–104. CEUR Workshop Proceedings Vol. 380, CEUR-WS.org (2008) 16. Menzel, T.: Entwurf und Implementierung eines objektorientierten Frameworks zur Petrinetzbasierten Modellierung. In: AWPN 1997. pp. 25–30. No. 85 in Informatik- Berichte, Humboldt-Universität zu Berlin, Institut für Informatik (1997) 17. Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (1989) 18. Pillat, T.: Gegenüberstellung struktureller Reduktionstechniken für Petrinetze. Diplomarbeit, Humboldt-Universität zu Berlin (2008), (in German) 19. Starke, P.H.: Analyse von Petri-Netz-Modellen. Teubner Verlag (1990) 20. Verbeek, E., Buijs, J., Dongen, B.v., Aalst, W.M.P.v.d.: Prom 6: The process mining toolkit. In: BPM 2010 Demos. CEUR Workshop Proceedings Vol. 615, CEUR-WS.org (2010) 21. Verbeek, H.M.W., Basten, T., Aalst, W.M.P.v.d.: Diagnosing workflow processes using Woflan. Comput. J. 44(4), 246–279 (2001) 22. Wolf, K.: Generating Petri net state spaces. In: ICATPN 2007. pp. 29–42. LNCS 4546, Springer (2007) 23. Wolf, K.: Does my service have partners? LNCS T. Petri Nets and Other Models of Concurrency 5460(2), 152–171 (2009)