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.
