From 2d4907aa1f6ad6ae86e988a806afb1db45784019 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 11 Nov 2010 16:00:12 +0000 Subject: [PATCH] NOTES. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2237 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES | 14 +++++++------- prism/NOTES-PTAS.txt | 2 ++ 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/prism/NOTES b/prism/NOTES index 4c2490c0..43a65ad5 100644 --- a/prism/NOTES +++ b/prism/NOTES @@ -8,10 +8,12 @@ TODO (before any release) ------------------------- PTAs: -* Implement divergence fix -* Sort out "time-lock" error message * (Further) tidy of prism-examples/pta +DOC! + +timelock reported as deadlock for digital + ======================================================= TODO (before public release) @@ -28,6 +30,9 @@ Filters, property semantics, etc. Action labels: * Check status of export/import trans wrt actions (alll models) +* Finalise tra format with actions (needs to work with MCs too) + - also fix e.g. importtrans, prism-statra +* make action storage optional (when required e.g. for export) (especially for MCs) Sim: * tidy doSampling, looking at Vincent's code @@ -111,11 +116,6 @@ Simulator: * Traviendo export? * Code: Optimise/tidy Choices (ChoiceList/ChoiceSingleton/etc.) -Actions: -* Finalise tra format with actions (needs to work with MCs too) - - also fix e.g. importtrans, prism-statra -* make action storage optional (when required e.g. for export) (especially for MCs) - Adversary generation: * Add adversary generation for other engines diff --git a/prism/NOTES-PTAS.txt b/prism/NOTES-PTAS.txt index 0f0b10fd..73794303 100644 --- a/prism/NOTES-PTAS.txt +++ b/prism/NOTES-PTAS.txt @@ -11,6 +11,8 @@ There are also some additional restrictions for PTA models. Modules cannot read 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. +PRISM does check for timelocks, i.e. states in which it possible to get to a point where no transitions are available and time cannot elapse due to invariant conditions. + 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