From 0070e79fa02c2d832eea4b654714736c4d81325b Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 19 Oct 2010 08:58:02 +0000 Subject: [PATCH] NOTES. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2172 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/prism/NOTES b/prism/NOTES index 5d700915..843b6da1 100644 --- a/prism/NOTES +++ b/prism/NOTES @@ -9,15 +9,12 @@ TODO (before any release) PTAs: * GUI -* Tidy prism-examples/pta +* (Further) tidy of prism-examples/pta * Clarify semantic/type checks (consistency with games/digital) * Check guards/invariants for convexity (for now, neither can be non-convex, see below) * Clarify time divergence issues * non-zeno checks? * Sort VarList (two types - before and after constants evaluated). Need for simulator too. -* Digital clocks: No time-bounded until yet -* Digital clocks: Translation done sep for each property (e.g. for cmax)? -* Bug fix: action alphabet (syntactic) for sync lost in PTA object construction ======================================================= @@ -42,6 +39,9 @@ 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)? +* Bug fix: action alphabet (syntactic) for sync lost in PTA object construction DOC (before public release) ---------------------------