PRISM includes or adapts several pieces of software developed elsewhere. This pages lists them, and provides links and downloads.
Typically, the version numbers given here refer to the libraries currently distributed with the latest development version on GitHub. To check the version numbers of libraries included in a particular release, check the file lib/README.md.
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.
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:
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.
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.
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.
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.1.
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:
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.7.90 of the library. You can download source code for that version here:
We also include its dependency, the Apache Log4j package (version 2.16.0).
PRISM-games uses the Parma Polyhedron Library (PPL) and its Java interface, which is released under the GPL. Building PRISM-games from source requires PPL to be available. Binary releases of PRISM-games include binary versions of the native libraries and JAR file for version 1.2 or later. You can download source code for 1.2 here:
The most up-to-date code for PPL is available from the Git repo git://git.cs.unipr.it/ppl/ppl.git, browsable here.
PRISM uses JUnit for regression tests, which is released under a GPL-compatible license. PRISM includes a binary version (JAR file) for version 1.7.2 of the library. You can download a source code version for that release here:
Site hosted at the Department of Computer Science, University of Oxford