ParAd: Parallel Adriana, version 1.2.3 released - the fastest tool to compute PN invariants on parallel architectures https://github.com/dazeorgacm/ParAd Solve a linear Diophantine homogeneous (sparse) system via composition of its clans Compatibility:-------------- Source code: C (gcc version 5.4.1) with OpenMP (version 4.0) and libc (version 2.23) functions.Operating system: Linux (tested on Ubuntu 18.04).Libraries: MPI -- Message Passing Interface (tested on MPICH 3.2, www.mpich.org ); SuiteSparse:GraphBLAS -- a set of sparse matrix operations on an extended algebra of semirings using an almost unlimited variety of operators and types (version 1.1.2, http://faculty.cse.tamu.edu/davis/suitesparse.html ); METIS -- A Software Package for Partitioning Unstructured Graphs, Partitioning Meshes, and Computing Fill-Reducing Orderings of Sparse Matrices (version 5.1.0, http://glaros.dtc.umn.edu/gkhome/views/metis).Solvers: zsolve from 4ti2 package ( www.4ti2.de ).Data formats: (sparse) matrix in a simple coordinate format; import a Petri net in .net/.ndr format of system Tina ( www.laas.fr/tina ).ParAd launches external executables named: zsolve -- to solve a Diaphantine system and gpmetis -- to partition decomposition graph (aggregate clans), their launch should be provided. New features:------------- Load balancing via clan aggregation with: (i) graph partitioning using METIS; (ii) bin packing with the first fit on a sorted array algorithm. Description:------------ Solving a sparse linear Diophantine homogeneous system is a widespread task for manifold application areas. Sometimes systems are rather big, and gaining some speed-up, employing useful properties of a sparse system [1,2], is a good idea. Besides, in a Petri net domain, solving such a system in nonnegative integer numbers is required that constitutes an intractable task. For Petri nets, the technique of using decomposition into clans (functional subnets) for solving linear systems [3,4] has been implemented as a software tool Adriana in 2005. ParAd [1], in essence, is a remake of Adriana which uses multi-core clusters to gain a considerable speed-up of computations. We implement two schemes of clans composition (simultaneous and parallel-sequential) independently from a linear system solver. We implement one internal solver ParTou using OpenMP to find solutions in nonnegative domain that is valuable for Petri net applications. We also implement an interface routine to launch zsolve from 4ti2 ( www.4ti2.de ) package to solve a system in the entire integer domain. Besides, we provide an option to attach a new external solver. To be consistent with general theory and tools for solving linear Diophantine systems, we provide a simple coordinate format to input/output a (sparse) matrix. Note that at present we use 32-bits representation of integer numbers which can be easily extended or replaced by some variable length representation. Since Adriana had been implemented as a plug-in of system Tina ( www.laas.fr/tina ) to draw and analyse Petri nets, historically we provide import from its formats of data, namely .net and .ndr types for logical and graphical specification of a Petri net, respectively. Besides, Tina implements import/export of nets in some other formats including the recent standard for Petri nets exchange -- .pnml. Actually we solve a system `xC=0` (or `Cy=0`),in integer numbers: c_{i,j} and x_i (y_i) are integer numbers. Note that the task corresponds to finding Petri net place (or transition) invariants, respectively, in case matrix C is a Petri net incidence matrix; for Petri nets, nonnegative integer invariants are of some use usually. To apply composition of clans to speed-up solving a system, the matrix should be decomposable into clans that supposes it is, at first, sparse. Matrices of clans obtained in the process of solution can be either dense or sparse; usually they are more dense than the source matrix. Let us remind that decomposition into clans is represented by a union of a block column matrix with a block diagonal matrix: | A1 C1 0 ... 0 | | A2 0 C2 ... 0 | | ... | | Ak 0 0 ... Ck | Clans are represented with block-rows of the matrix, where block-matrices C1 ... Ck specify internal parts of each clan, while block-matrices A1 ... Ak define connection of clans. Thus, matrix of i-th clan is represented as (Ai,Ci). Analysis of about a hundred of real-life Petri net models from Model Checking Contest ( https://mcc.lip6.fr/ ) collection shows that about 3/4 of them are rather good decomposable into clans.
References:----------- 1. Zaitsev D.A., Tomov S., Dongarra J. Solving Linear Diophantine Systems on Parallel Architectures, IEEE Transactions on Parallel and Distributed Systems, 30(5) 2019, 1158-1169, http://dx.doi.org/10.1109/TPDS.2018.2873354 2. Zaitsev D.A. Sequential composition of linear systems307. Online 12 February 2016, http://dx.doi.org/10.1016/j.ins.2016.02.016 3. Zaitsev D.A. Compositional analysis of Petri nets, Cybernetics and Systems Analysis, Volume 42, Number 1 (2006), 126-136, http://dx.doi.org/10.1007/s10559-006-0044-0 4. Zaitsev D.A. Decomposition of Petri Nets, Cybernetics and Systems Analysis, Volume 40, Number 5 (2004), 739-746, http://dx.doi.org/10.1007/s10559-005-0012-0 ++
---- [[ Petri Nets World: ]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ: ]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies: ]] [[ [email protected] ]]
