PRISM is free and open source software. You can download both the tool and its source code for free from below.
Distribution is under the GNU General Public License (GPL), version 2.
Latest version: 4.5
The current version of PRISM is 4.5 (first released 19 Apr 2019).
The main changes since the last public release (4.4) are listed below.
More details for individual releases are in the CHANGELOG.
- New features
- add round function to language (rounds to nearest integer)
- Java stack size can be set via command-line switch -javastack (or PRISM_JAVASTACKSIZE)
- fractional values allowed for constants in -const switch and in GUI
- allow rewards to be included in simulation paths exported from GUI (like for -simpath)
- Enhancements and fixes:
- PRISM GUI settings file (.prism) moved to more standard locations
- ITE supported in exact/parametric mode
- various improvements to model checking in "exact" mode
- bugfix for incorrect model construction during fast adaptive uniformisation
- faster explicit construction of models with no labels
- command-line -exportsteadystates switch implies -steadystate
- GUI shortcuts: double-clicks for addition of constants, labels
- fixed Mac launch scripts for Java 10 (removed -d64 and -d32)
- improved auto switching between model checking engines in some cases
- many minor bugfixes
- Development changes and enhancements:
- alignment of source code releases and GitHub repos (some files moved to top-level)
- move/simplify release building Makefile scripts (see GitHub wiki)
- utility scripts for installing PRISM on fresh OSs (in etc/scripts)
- HTML copy of manual now included in repo
- make clean_all cleans external libs too, e.g. lpsolve
- switch from javah (deprecated since Java 8) to javac for JNI header generation
- launch scripts now use exec to start Java by default (PRISM_NO_EXEC=yes to revert)
- Benchmarking/testing changes and enhancements:
- integration of prism-tests into main repo
- fractions/exact numbers allowed in testing RESULT specs
- Travis build config for continuous integration testing
- prism-auto guesses ngprism location
- prism-auto options: --skip-export-runs, --skip-duplicate-runs, --timeout
- Makefile targets/settings: test, testsecho, testsfull, TESTS_ARGS, source-jar
- NG_MAINCLASS setting for running PRISM in Nailgun server mode (prism -ng)
To access more recently developed features, get the latest code from GitHub.
PRISM should run on 32/64-bit versions of all major operating systems.
We distribute pre-built binary versions for various architectures.
But for non-Windows platforms, it is usually easy to build from source code.
Your version (32- vs 64-bit) of Java must match that of PRISM.
In particular, to use the 32-bit Windows binary,
make sure you are running a 32-bit version of Java.
See the installation instructions,
included in the PRISM manual (which is also distributed with the tool).
If you have any problems, first check the list of
common problems and questions.
If you are still stuck, post a message in the
Once you have installed PRISM, you might want to look at: