Skip to content

Home

Jump to bottom
Dave Parker edited this page Jan 12, 2024 · 31 revisions

PRISM Developer Resources

PRISM and PRISM-games are open-source software and we encourage developers to adapt and extend them.

Here, we collate information and resources for developers of these tools, or of code that extends/connects to them.

If you have questions or want to discuss issues relating to PRISM/PRISM-games development, please use the PRISM developers forum on Google Groups first. For anything else, please email Dave Parker at david.parker@cs.ox.ac.uk.

Source code

The source code for PRISM and PRISM-games can be found at:

These are the most up-to-date version of the code. If you plan to extend/adapt them, create a fork from that repo. Public releases (both binaries and source) are published on the PRISM download and PRISM-games download pages, and also on the GitHub PRISM releases and PRISM-games releases pages.

The prism-api repo contains examples of how to connect to PRISM programmatically:

Compilation

The manual has PRISM installation instructions and there are some extra PRISM-games installation instructions.

In short, you need GNU make, a C/C++ compiler (e.g. gcc/g++) and a Java Development Kit (version 9 or above). And, from within the downloaded PRISM distribution, compilation should just require:

cd prism && make

These scripts install required packages and compile PRISM on a fresh install/VM for various OSs:

Useful one-liners for clean installs. Linux (Unbuntu):

/bin/bash <(curl -fsSL https://raw.githubusercontent.com/prismmodelchecker/prism/master/prism/etc/scripts/prism-install-ubuntu) --nobuild

Windows (in a Command Prompt and Cygwin shell respectively:

"%SystemRoot%\System32\WindowsPowerShell\v1.0\powershell.exe" -Command "wget -Uri https://raw.githubusercontent.com/prismmodelchecker/prism/master/prism/etc/scripts/prism-install-windows.bat -Outfile prism-install-windows.bat" && cmd /K .\prism-install-windows.bat

/bin/bash <(curl -fsSL https://raw.githubusercontent.com/prismmodelchecker/prism/master/prism/etc/scripts/prism-install-cygwin) --nobuild

Dependencies

PRISM uses various libraries, but aims for the install to have minimal pre-requisites so these libraries are generally built from source at compile time or are included in binary form for various OSs.

  • CUDD: PRISM needs (a customised version of) the CUDD library for BDDs and MTBDD. This is in ../cudd and is compiled by the main build process. The CUDD repo is used to keep track of modifications made.

  • Java libraries: PRISM uses various Java libraries, which are included, pre-compiled, as JAR files in the lib directory. See lib/README.md for a list of libraries and versions and this page for further details and links.

Several external libraries are contained in the ext directory, which are either compiled from source or provided as pre-compiled binaries, and are copied to lib at compile time. See ext/README.md or this page for version info.

  • lp_solve: PRISM includes a modified version of lp_solve and the lp_solve Java wrapper. Modifications can be found in the main Git repo: lp_solve_5.5 and lp_solve_5.5_java. These are compiled by PRISM, called from the main Makefile, except for Windows where pre-compiled binaries are included.

  • Z3: PRISM-games includes the Z3 solver by Microsoft Research, and its Java interface, in the form of pre-compiled binary files.

  • Yices 2: PRISM-games includes the Yices 2 SMT solver and its Java interface, in the form of pre-compiled binary files (we statically include GMP). Notes on compilation are in ext/yices/README.md.

  • PPL: PRISM-games includes the Parma Polyhedron Library (PPL) including its Java interface, in the form of pre-compiled binary files (we statically include GMP). Notes on compilation are in ext/ppl/README.md, and a version modified for easier building is in the PPL repo.

Branches and merging

For the main PRISM repo, we use a linear git history, rebasing rather than merging when feature branches are incorporated. There is no specific policy for retaining/updating the timestamps of the original commits.

The PRISM-games repo is periodically updated to incorporate updates from the main PRISM repo. This is done via merging, not rebasing, since some parts of the codebase have diverged a little.

The prism-ext repo is used for hosting public snapshots (e.g. for tool competitions) or publicly released extensions (e.g. PRISM-pomdps, before it was integrated to the main repo).

Parsers

The (modelling and property) languages in PRISM are processed using parsers generated by JavaCC. We use version 7.0. You do not need this to build a normal version of PRISM, only if you have made your own modifications to the parsers. (In that case, note that make parser re-compiles just the parser code)

Clone this wiki locally