www.prismmodelchecker.org

Other Downloads

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.

Integrated components

The following are incorporated within the PRISM codebase:

Java libraries

PRISM includes various pre-compiled Java libraries, usually as JAR files. To check the version numbers of libraries included in a particular release, check the file lib/README.md.

  • 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: colt-1.2.0.tar.gz.
  • EPS Graphics: The PRISM GUI uses the EPS Graphics library to provide export of graphs to EPS files. PRISM includes a pre-compiled copy of version 1.0.0 of the library, which was released under the GPL. You can download a full source code version here: epsgraphics-1.0.0-src.zip.
  • 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.7.90 of the library. You can download source code for that version here: jas-2.7.90-src.zip.
  • Log4j: The Apache Log4j package (version 2.16.0) is included as a dependency of JAS.
  • JCommon and JFreeChart: The PRISM GUI includes a graph-plotting component based on JFreeChart. PRISM includes pre-compiled copies fofor version 1.0.13 of JFreeChart and version 1.0.16 of its dependency JCommon. JFreeChart/JCommon are released under the LGPL and you can download full source code versions of these here: jfreechart-1.0.13.tar.gz, jcommon-1.0.16.tar.gz.
  • 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.1.
  • JUnit: 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: junit-platform-console-standalone-1.7.2-sources.jar.
  • Nailgun: PRISM can use the Nailgun server to avoid JVM start-up overhead. PRISM includes a pre-compiled copy of version 0.9.2-SNAPSHOT. It was released under the Apache License and source code can be found here.
  • 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: pepa2prism-0.03.2.tar.gz.

Other libraries

PRISM and/or PRISM-games include various other libraries, mostly written in C/C++ but including Java interfaces.

  • lp_solve: PRISM includes a modified version of lp_solve, an LGPL-licensed Mixed Integer Linear Programming (MILP) solver. It builds on version 5.5.2.0 of lp_solve and version 5.5.0.14 of the lp_solve Java wrapper. Modifications can be found on GitHub: lp_solve_5.5 and lp_solve_5.5_java.
  • Z3: PRISM-games can use the Z3 solver by Microsoft Research, released under the MIT license. It currently includes version 4.12.4.
  • Yices 2: PRISM-games can use the Yices 2 SMT solver via its Java interface, which are released under the GPL and MIT license, respectively. It currently includes version 2.6.4 and version 1.0.1 (approximately), respectively.
  • Parma Polyhedron Library (PPL): PRISM-games can use the Parma Polyhedron Library (PPL), which is released under the GPL. A modified version, based on PPL 2.1, is at https://github.com/prismmodelchecker/ppl, which eases the build process.

More information on building and integrating these dependencies can be found on the PRISM developer wiki.

Downloads