From 83556362ba96f90dd8ddbbfa0ba348097f298bd8 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 30 Nov 2010 23:36:10 +0000 Subject: [PATCH] Brief notes on the structure of the source directory. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2309 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES | 5 +++-- prism/src/NOTES.txt | 24 ++++++++++++++++++++++++ 2 files changed, 27 insertions(+), 2 deletions(-) create mode 100644 prism/src/NOTES.txt diff --git a/prism/NOTES b/prism/NOTES index b6228892..2dbae30d 100644 --- a/prism/NOTES +++ b/prism/NOTES @@ -15,6 +15,7 @@ DOC! timelock reported as deadlock for digital verbose has new behaviour now?! (wrt filters) pta rewards with digital clocks (just F) - no clocks in rew strs though +filters: {} always range, even if single value (allow "single"?) ======================================================= @@ -22,10 +23,10 @@ TODO (before public release) ---------------------------- Filters, property semantics, etc. -* {}-filters should be "first", not "range" for 1-state filters - (need to move invisible filter creation into StateModelChecker I think) * Integer-valued props displayed as doubles when printed as vector * Intervals (e.g. for multiple initial states) plotted in graphs +* Add "single" filter - throws error if filter states > 1? +* Allow other filter types to be spec with {} notation? Action labels: * Check status of export/import trans wrt actions (alll models) diff --git a/prism/src/NOTES.txt b/prism/src/NOTES.txt new file mode 100644 index 00000000..8cb82c2b --- /dev/null +++ b/prism/src/NOTES.txt @@ -0,0 +1,24 @@ +Brief notes on the structure of this source directory. +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