|
|
|
@ -1,24 +1,27 @@ |
|
|
|
Brief notes on the structure of this source directory. |
|
|
|
Further details on packages are in the Javadoc. |
|
|
|
Dave Parker. |
|
|
|
|
|
|
|
----------- |
|
|
|
|
|
|
|
* prism/ - main Prism API, the command-line tool, and Java classes for symbolic data structures and algorithms |
|
|
|
* parser/ - JavaCC parser files and accompanying abstract syntax tree data structures and tools |
|
|
|
* settings/ - generic 'settings' libraries |
|
|
|
* simulator/ - the discrete event simulation engine and approximate model checking code |
|
|
|
* dd/ - a C/C++ library of BDD/MTBDD functions, mostly just wrappers for the CUDD library |
|
|
|
* jdd/ - a Java library providing a wrapper around the dd librar and hence Java access to CUDD via JNI |
|
|
|
* odd/ - "offset-labelled BDDs", used to facilitate indexing of states between BDDs and explicit-state data structures |
|
|
|
* dv/ - "double vector" - utility functions for operations on vectors of doubles |
|
|
|
* mtbdd/ - the "MTBDD" engine: fully symbolic implementations of model checking algorithms |
|
|
|
* sparse/ - the "Sparse" engine: sparse matrix data structures and corresponding implementations of model checking algorithms |
|
|
|
* hybrid/ - the "Hybrid" engine: data structures and model checking algorithms that mix MTBDDs and explicit-state techniques |
|
|
|
* jltl2ba/ and jltl2dstar/ - Java ports of the LTL-to-automata libraries |
|
|
|
* explicit/ - explicit-state probabilistic model checking, implemented in Java |
|
|
|
* pta/ - probabilistic timed automata (PTA) model checking, including DBM library |
|
|
|
* userinterface/ - the GUI |
|
|
|
* pepa/ - PEPA-to-PRISM model translation |
|
|
|
* bin/ - OS-specific build scripts, customised and installed by make |
|
|
|
* scripts/ - schell script(s) used from within make |
|
|
|
* nsis_script.nsi - Script to build Windows binaries with NSIS |
|
|
|
* bin/ - OS-specific build scripts, customised and installed by make. |
|
|
|
* dd/ - A C/C++ library of BDD/MTBDD functions, mostly just wrappers for the CUDD library. |
|
|
|
* dv/ - Utility functions for operations on vectors of doubles (stored in C++ through JNI). |
|
|
|
* explicit/ - Explicit-state probabilistic model checking engine, implemented in Java. |
|
|
|
* hybrid/ - The "Hybrid" engine: data structures and model checking algorithms that mix MTBDDs and explicit-state techniques. |
|
|
|
* jdd/ - A Java library providing a wrapper around the dd library and hence Java access to CUDD via JNI. |
|
|
|
* jltl2ba/ - Java port of the LTL to Buchi automata conversion library. |
|
|
|
* jltl2dstar/ - Java port of the LTL to deterministic Rabin automata conversion library. |
|
|
|
* mtbdd/ - The "MTBDD" engine: fully symbolic implementations of model checking algorithms. |
|
|
|
* odd/ - ODDs (offset-labelled BDDs), used to facilitate indexing of states between BDDs and explicit-state data structures. |
|
|
|
* parser/ - The PRISM model/properties parser, accompanying abstract syntax tree data structures and tools (and JavaCC parser files). |
|
|
|
* pepa/ - PEPA-to-PRISM model translation. |
|
|
|
* prism/ - The main Prism API, the command-line tool, and Java classes for symbolic data structures and algorithms. |
|
|
|
* pta/ - Probabilistic timed automata (PTA) model checking, including DBM library. |
|
|
|
* scripts/ - Shell script(s) used from within make. |
|
|
|
* settings/ - Generic 'settings' functionality. |
|
|
|
* simulator/ - The discrete event simulation engine and approximate (statistical) model checking code. |
|
|
|
* sparse/ - The "Sparse" engine: sparse matrix data structures and corresponding implementations of model checking algorithms. |
|
|
|
* userinterface/ - PRISM's graphical user interface (GUI). |
|
|
|
|
|
|
|
* nsis_script.nsi - Script to build Windows binaries with NSIS. |