From ac869503348a5e529c37658a279a4c53593d2f50 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 5 Nov 2010 14:34:12 +0000 Subject: [PATCH] NOTES. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2227 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES | 16 ++++++++++++---- prism/NOTES-PTAS.txt | 2 ++ 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/prism/NOTES b/prism/NOTES index d7262ead..4c2490c0 100644 --- a/prism/NOTES +++ b/prism/NOTES @@ -8,9 +8,9 @@ TODO (before any release) ------------------------- PTAs: +* Implement divergence fix +* Sort out "time-lock" error message * (Further) tidy of prism-examples/pta -* Clarify time divergence issues -* non-zeno checks? ======================================================= @@ -26,6 +26,9 @@ Filters, property semantics, etc. * Restructure Result class? e.g. separate bracketed comment? (done I think) - Errors (Exceptions) formatted properly? +Action labels: +* Check status of export/import trans wrt actions (alll models) + Sim: * tidy doSampling, looking at Vincent's code * seed issues (Vlad) @@ -40,8 +43,12 @@ PTAs: (see non-well-formed.nm/pctl for a test case) (if can't do that, syntax check using sat) - digital clocks: check invariants after transform/reach? -* Digital clocks: No time-bounded until yet -* Digital clocks: Translation done sep for each property (e.g. for cmax)? + (might be like non-pta case: doing before reach causes false alarms?) +* Digital clocks time-bounded + - will need to make sure cmax is updated accordingly + (currently just from temporal operator time bound since no clocks in formula) + - also might need to access property constants (see TODO in DC.java) + * Bug fix: action alphabet (syntactic) for sync lost in PTA object construction DOC (before public release) @@ -72,6 +79,7 @@ PTAs: - access to other local and global vars - system endsystem? (then test on Arnd's BRP model + others) +* Implement structurally non-zeno checks * BRP example * Translate non-convex guards to DNF and multiple transitions * Investigate whether non-convex invariants can be supported (look at zone ops) diff --git a/prism/NOTES-PTAS.txt b/prism/NOTES-PTAS.txt index 1d166754..0f0b10fd 100644 --- a/prism/NOTES-PTAS.txt +++ b/prism/NOTES-PTAS.txt @@ -9,6 +9,8 @@ In guards or invariants, references to clocks must be conjunctions of simple clo There are also some additional restrictions for PTA models. Modules cannot read the local variables of other modules and global variables are not permitted. The model must also have a single initial state (i.e. the init...endinit construct is not permitted). Again, when using digital clocks, the latter constraint does not apply. +Model checking requires several assumptions: we require PTAs to be well-formed and non-zeno (see e.g. [KNP09c] for details). Currently, PRISM does not check automatically that these assumptions are satisfied. + There are a set of PRISM PTA examples in the directory examples/pta. See the formats09.sh script in this directory for details of how to run the examples. * Properties