s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
3499 Commits
5 Branches
0 Tags
31 MiB
 
 
 
 
 
 
Tree: ca9309d18e
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'ca9309d18e'
${ noResults }
prism-accumulation/prism/src
Steffen Märcker ca9309d18e
Harmonize log output after steady-state power iteration between engines 		8 years ago
..
acceptance symbolic acceptance: provide intersect() method to allow restriction of the state sets 9 years ago
automata HOAF2DA.labelExpressionToAPMonom: fix missing return in switch statement (for FALSE) 8 years ago
bin Removed -d64 and -d32 from Mac launch scripts. 8 years ago
cex Makefiles: add Makefiles for common, cex package; update for simulator 8 years ago
common Makefiles: add Makefiles for common, cex package; update for simulator 8 years ago
dd Makefiles: inhibit parallel building (-j n mode) 8 years ago
dv Makefiles: inhibit parallel building (-j n mode) 8 years ago
explicit Harmonize log output after steady-state power iteration between engines 8 years ago
hybrid hybrid.cc: initialise col_offset in hdd_negative_row_sums 8 years ago
jdd Makefiles: inhibit parallel building (-j n mode) 8 years ago
jltl2ba SimpleLTL.simplified: Don't use fall-through in switch statement 8 years ago
jltl2dstar NBA.print: add missing break in switch for 'lbtt' printing 8 years ago
mtbdd mtbdd/hybrid/sparse: Generate PrismNotSupportedExceptions if native error message contains 'not supported' 8 years ago
odd Makefiles: inhibit parallel building (-j n mode) 8 years ago
param param/Makefile: ignore package-info.java 8 years ago
parser Rewrite Values#clone for readability and efficiency 8 years ago
pepa/compiler Makefiles: inhibit parallel building (-j n mode) 8 years ago
prism Tidy some w3c imports; was causing compile issues in Eclipse+Java10. 8 years ago
pta PTAParser.jj: update to include changes from PTAParser.java (fixes #32) 8 years ago
scripts The "r" is prepended to svn revision numbers automatically (in prism.getVersion and printversion.sh). 13 years ago
settings FileSetting: On-first-use allocation of file selector 8 years ago
simulator Statistical MC: Fix infinite sampling for lower bounded P[F]/P[U] 8 years ago
sparse mtbdd/hybrid/sparse: Generate PrismNotSupportedExceptions if native error message contains 'not supported' 8 years ago
strat Makefiles: inhibit parallel building (-j n mode) 8 years ago
userinterface Tidy some w3c imports; was causing compile issues in Eclipse+Java10. 8 years ago
README.txt Improved documentation (JavaDoc mostly). 15 years ago
authors.txt Update authors list used for git-svn migration. 8 years ago
manifest.txt Edited makefile to create Jar files which can be double-clicked. Also added a manifest.txt in the src directory which is required to realise this behaviour. 19 years ago
nsis_script.nsi Make NSIS installer creator use correct "Program Files" depending on 32/64-bit-ness. 12 years ago
overview.html Improved documentation (JavaDoc mostly). 15 years ago

README.txt 

Brief notes on the structure of this source directory.

Further details on packages are in the Javadoc.

Dave Parker.



-----------



* 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 facilitat