PROD TOOL
PROD is a reachability analysis tool for Pr/T nets.
- Environment:
- Unix, MS-DOS (C compiler and linker required)
- Origin:
- Digital Systems Laboratory, Helsinki University of Technology, Finland
- Kind of Nets supported:
- Predicate/Transition Nets
- Functionalities:
- Nets are described in the C preprocessor language extended with net description directives (prpp)
- ANALYSIS:
- generation of the REACHABILITY GRAPH
- UNFOLDING of the Pr/T net to a P/T net
- Stubborn Set Method for reduced state space generation (on the Unfolding)
- Graph Query Program (probe)
- Computation of the strongly connected components of the graph (strong)
- Graph Query Language CTL (Computation Tree Logic) for inspecting the generated state space
- Availability:
-
- References:
- P. Grönberg, M. Tiusanen, K. Varpaaniemi: PROD - A Pr/T-Net Reachability Analysis Tool [gtv93]
- K. Varpaaniemi: On Computing symmetries and Stubborn Sets [var94]
- K. Varpaaniemi: Efficent Detection of Deadlocks of Petri Nets [var93]
- J. Haalme, K. Hiekkanen, T. Pyssysalo, K. Varpaaniemi: PROD Reference Manual
- K. Varpaaniemi, M. Rauhamaa: The Stubborn Set Method in Practice [vr92]
- Tool description at DAIMI
- Notes:
- References available at saturn.hut.fi
