What is DiPro?
Current stochastic model checkers do not make counterexamples for property violations readily available. DiPro is a tool, that applies directed explicit state space search to discrete- and continuous-time Markov chains in order to compute counterexamples for the violation of PCTL or CSL properties.
Directed explicit state space search algorithms explore the state space on-the-fly which makes DiPro very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method.
Counterexamples provided by DiPro have two important properties. First, they include those traces which contribute the most amount of probability to the property violation. Hence, they show the most probable offending execution scenarios of the system. Second, the obtained counterexamples tend to be small. Hence, they can be effectively analyzed by a human user. Both properties make the counterexamples obtained by our method very useful for debugging purposes.
DiPro allows for the computation of counterexamples for the stochastic model checkers PRISM or MRMC.
Download
To download DiPro, please proceed to the download page.
Q: If I try to run DiPro from source code I receive the error message "java.lang.UnsatisfiedLinkError: no prism in java.library.path".
A: You need to set the java.library.path to the lib folder of your PRISM dir where the prism.jar is located (check whether the prism.jar is in the lib folder, if not see next question). You can either set the path for the dynamic linker in an environment variable of your system (LD_LIBRARY_PATH on most Linux systems, DYLD_LIBRARY_PATH on Mac OS X, and PATH on Windows) or you use "java -Djava.library.path=$PRISM_DIR/lib" when running DiPro.
Q: There is no prism.jar file in the lib folder, how do I generate it?
A: To generate the prism.jar you need the source code version of PRISM. Run 'make binary' form the command line in the PRISM folder and the prism.jar is generated
Q: What kind of properties are supported by DiPro?
A: At the DiPro supports reachability properties of the form "P<> [() U ()]" and time-bounded reachability properties of the form "P<> [() U<=T ()]" and properties of the form "P=? [() U ()]" or "P=? [() U<=T ()]". Note that the property "P<> [F "something"]" can be rewritten to "P=? [(true) U ("something")]".