www.prismmodelchecker.org

Other Downloads

PRISM includes or adapts several pieces of software developed elsewhere:

CUDD

PRISM includes a modified version of the CUDD package, a BDD/MTBDD library developed by Fabio Somenzi at Colorado University. Currently, this is based on version 2.5.0. You can download an unmodified copy of this version here:

For more up-to-date information or versions, see the CUDD website.

PEPA-to-PRISM Compiler

PRISM includes a translator from PEPA to PRISM, developed by Stephen Gilmore at the University of Edinburgh. PRISM includes a pre-compiled copy of version 0.03.2. The compiler is released under the GPL and you can download the full source code version here:

JFreeChart

The PRISM GUI includes a graph-plotting component based on JFreeChart. PRISM includes binary versions (JAR files) for version 1.0.13 of JFreeChart and version 1.0.16 of its dependency JCommon. You can download full source code versions of these here:

JFreeChart/JCommon are released under the LGPL. For more up-to-date information or versions, see the JFree website.

EPS Graphics

The PRISM GUI uses the EPS Graphics library to provide export of graphs to EPS files. PRISM includes a binary version (JAR file) for version 1.0.0 of the library. You can download a full source code version here:

This version of the library is released under the GPL. For more up-to-date information or versions, see the EPS Graphics website.

LTL 2 BA and ltl2dstar

PRISM's LTL model checking functionality includes Java ports, by Carlos Bederian, of LTL 2 BA (by Denis Oddoux & Paul Gastin) and ltl2dstar (by Joachim Klein), GPL-licensed tools for LTL-to-automata translation.

jhoafparser

PRISM supports the Hanoi Omega Automaton (HOA) format for importing deterministic omega automata. To to do this, it uses the jhoafparser HOA parser (by Joachim Klein and David Müller), released under the LGPL. PRISM includes a JAR file (also including source) for version 1.1.0.

Colt

PRISM's simulator uses parts of Colt, a free numerical library in Java, developed at CERN by Wolfgang Hoschek and released under under a BSD-style license (we include only packages cern.colt*, cern.jet*, cern.clhep). PRISM includes a binary version (JAR file) for version 1.2.0 of the library. You can download source code version for that version here:

Java Algebra System (JAS)

PRISM's parametric model checking functionality uses parts of JAS (the Java Algebra System), a library for algebraic computations in Java released under the GPL. PRISM includes a binary version (JAR file) for version 2.5.5246 of the library. You can download source code for that version here:

We also include its dependency, the Apache log4j package.

Downloads


63,270 downloads of PRISM to date.