From 45c1f3f367b761f82ccdf29d2d4b01bdb5ba32b1 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 15 Oct 2010 20:42:55 +0000 Subject: [PATCH] NOTES. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2161 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES | 171 +++++++++++++++++++++++++++++++---------------- prism/NOTES-PTAS | 90 ------------------------- prism/NOTES-SIM | 40 ----------- prism/TODO | 30 --------- 4 files changed, 115 insertions(+), 216 deletions(-) delete mode 100644 prism/NOTES-PTAS delete mode 100644 prism/NOTES-SIM delete mode 100644 prism/TODO diff --git a/prism/NOTES b/prism/NOTES index 83eca48c..d1347837 100644 --- a/prism/NOTES +++ b/prism/NOTES @@ -1,27 +1,31 @@ - -Last stable version of PRISM on svn (3.3 plus some fixes) is rev 1405 -(there is a copy of this, e.g. to get working old simulator, in ~/prism-old) - ------------------------------------------------------------------------ - -Stuff to remove when distributing early copies to people: +Remove for beta distributions: +------------------------------ * NOTES* * TODO? -* examples/des -* examples/explicit ------------------------------------------------------------------------ +======================================================= -See also: -* NOTES-PTAS -* NOTES-SIM -* NOTES-ABSTR +TODO (before any release) +------------------------- ------------------------------------------------------------------------ +PTAs: +* GUI +* Tidy prism-examples/pta, incl. delete brp +* 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 -Filters, property semantics, etc. +======================================================= + +TODO (before public release) +---------------------------- -TODO: +Filters, property semantics, etc. * Integer-valued props displayed as doubles - need to give types to StateValues? - lots of other places too e.g. GUI results) * Intervals for multiple initial states @@ -30,51 +34,106 @@ TODO: * Restructure Result class? e.g. separate bracketed comment? (done I think) - Errors (Exceptions) formatted properly? -Doc: -* Filters - no longer allowed minmax (or encode as range?) -* P>=p[...{filter}] means & not print (didn't print in 3.3 anyway, despite manual) - ------------------------------------------------------------------------ - -TODO: - -- remove colons from @params +PTAs: +* Enforce well-formedness checks (i.e. guards/resets imply target invariants) + (as opposed to say supporting strong invariants, + where targets with false invariants cannot be entered) + - zone-based: check during reach using valids + (or just during FW reach?) (nb: need to split dpost to do check) + (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? -- fix adversary generation (de alfaro thesis) -- add adversary generation for other engines -- make action storage optional (when required e.g. for export) (especially for MCs) -- lp stuff - plugin support for eclipse/lpsolve (in prism-multi?) -- also look up lrs? -- finalise tra format with actions (needs to work with actions too) - - so also fix e.g. importtrans, prism-statra +DOC (before public release) +--------------------------- ------------------------------------------------------------------------ - -Abstraction/refinement: - -TODO: -* exp reach for games - -Other notes/ideas: -* refine opt: don't add ubsets of player1 choices - ------------------------------------------------------------------------ - -LTL... - -bug: +Filters: +* Filters - no longer allowed minmax (or encode as range?) +* P>=p[...{filter}] means & not print (didn't print in 3.3 anyway, despite manual) -prism ~/prism-examples/dice/dice.pm \ +PTAs: +* Where can clocks be used + - clock constraints (just (some) binops) + - in guards + - in invariants + - resets (normal updates, but to ints only) + - var decl.s + - generally must be convex (i.e. just conj of constraints) (can be relaxed a bit for digital clocks) +* Currently, modules cannot access non-local vars (and there are no globals) + (this is too restrictive, e.g. for message passing) +* Must have single initial state (is this true for digital clocks too?) +* Invariants must come straight after var decls + +======================================================= + +BUG (some time) +--------------- + +Simulator: +* approx mc of a property loses any current simulator path in gui. + is that ok? (seems to be buggy in 3.3.1 anyway) + +* prism ~/prism-examples/dice/dice.pm \ -pctl '(s=0|s=1)=>P>=1 [ (P>=0.9 [ F<=1 s=3 ])=>(P>=0.5 [ F<=2 s=4 ]) ]' -time-bounds should be ok in inner pctl but are not +(time-bounds should be ok in inner pctl but are not) + +TODO (some time) +---------------- + +PTAs: +* On-the-fly global reachability to allow (for A-R engine): + - access to other local and global vars + - system endsystem? + (then test on Arnd's BRP model + others) +* BRP example +* Translate non-convex guards to DNF and multiple transitions +* Investigate whether non-convex invariants can be supported (look at zone ops) + +* Games: Optimise number of states in time-bounded PTAs + (extras added in old target states) using until in forwards reach? +* Fix: Creation of new names (adding extra _s) doesn't take into account prop file ot consts etc. +* Digital clocks: urgency? +* Digital clocks: optimisations? + +* New version of valid2 (inv/g push outside) +* Combined complement + intersection (terminating early) for when dbm lists get big +* Are we ok to have non-diagonal c-closure algorithm? + (or is it ok if only use this on initial reach graph construction?) + +Simulator: +* Investigate efficiency wrt old simulator +* Add (back) support for full loop detection? (embedded into Path*?) +* Add (back) early manual termination of sampling (thru expt stop?) +* Random initial state +* Variable overflow etc. +* Add support for "deadlock" and "init" (new EvaluationContext, model *and* state dependent) +* Seed issues (currently twice in one second = same seed) +* explicitbuildtest doesn't handle dupes in mdps (e.g. consensus) +* Explicit build doesn't handle multiple initial states +* GUI sim - add context menu to transition list with e.g. "show in model" +* 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 -bscc stuff -- regression testing on ltl stuff with 3 diff options - ------------------------------------------------------------------------ +Abstraction/refinement: +* Exp reach for games +* Poss. refine opt: don't add ubsets of player1 choices -prism-multi +BSCC stuff: +* regression testing + perf. on ltl stuff with 3 diff options -DOC: no state rewards +Code tidy: +* remove colons from @params +DOC (some time) +--------------- +Prism-multi: +* No state rewards diff --git a/prism/NOTES-PTAS b/prism/NOTES-PTAS deleted file mode 100644 index 4a583bcd..00000000 --- a/prism/NOTES-PTAS +++ /dev/null @@ -1,90 +0,0 @@ - -TODO (before any release) -------------------------- - -* GUI - -* Tidy prism-examples/pta, incl. delete brp - -* 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 - - -TODO (later) ------------- - -* Enforce well-formedness checks (i.e. guards/resets imply target invariants) - (as opposed to say supporting strong invariants, - where targets with false invariants cannot be entered) - - zone-based: check during reach using valids - (or just during FW reach?) (nb: need to split dpost to do check) - (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? - -* On-the-fly global reachability to allow (for A-R engine): - - access to other local and global vars - - system endsystem? - (then test on Arnd's BRP model + others) - -* BRP example - -* Translate non-convex guards to DNF and multiple transitions - -* Investigate whether non-convex invariants can be supported (look at zone ops) - - - -Bugs ----- - - -Maybe todo ----------- - -* Games: Optimise number of states in time-bounded PTAs - (extras added in old target states) using until in forwards reach? - -* Fix: Creation of new names (adding extra _s) doesn't take into account prop file ot consts etc. - -* Digital clocks: urgency? - -* Digital clocks: optimisations? - - -Tidy ----- - -* Remove unneeded files from examples (prism-benchmark, rewards stuff) - - -Documentation -------------- - -Where can clocks be used -* clock constraints (just (some) binops) - - in guards - - in invariants -* resets (normal updates, but to ints only) -* var decl.s -* generally must be convex (i.e. just conj of constraints) (can be relaxed a bit for digital clocks) - -Currently, modules cannot access non-local vars (and there are no globals) -(this is too restrictive, e.g. for message passing) - -Must have single initial state (is this true for digital clocks too?) - -Invariants must come straight after var decls - diff --git a/prism/NOTES-SIM b/prism/NOTES-SIM deleted file mode 100644 index 17539828..00000000 --- a/prism/NOTES-SIM +++ /dev/null @@ -1,40 +0,0 @@ - -NOW/NEXT --------- - - -TODO (before any release) -------------------------- - - -TODO (later) ------------- - -* investigate efficiency wrt old simulator - -* add (back) support for full loop detection? (embedded into Path*?) -* add (back) early manual termination of sampling (thru expt stop?) - -* random initial state -* variable overflow etc. -* add support for "deadlock" and "init" (new EvaluationContext, model *and* state dependent) -* seed issues (currently twice in one second = same seed) - -* explicitbuildtest doesn't handle dupes in mdps (e.g. consensus) -* explicit build doesn't handle multiple initial states - -* GUI sim - add context menu to transition list with e.g. "show in model" - -* traviendo export? - -CODE: -* Optimise/tidy Choices (ChoiceList/ChoiceSingleton/etc.) - - -BUGS (later) ------------- - -* approx mc of a property loses any current simulator path in gui. - is that ok? (seems to be buggy in 3.3.1 anyway) - - diff --git a/prism/TODO b/prism/TODO deleted file mode 100644 index a73740dd..00000000 --- a/prism/TODO +++ /dev/null @@ -1,30 +0,0 @@ - - -TODO: - -new version of valid2 (inv/g push outside) - -combined complement + intersection (terminating early) for when dbm lists get big - ----------------------- - -BUGS: - ----------------------- ----------------------- - -./forwardreach examples/repudiation/originator.des examples/repudiation/recipient.des examples/repudiation/honest_deadline40.des '*:*:before' 'true' -min -opt -nopre -Final TPSG: 416 states, 1813 distribution sets, 2221 distributions, 3751 transitions, p1max/avg = 3/4.4, p2max/avg = 2/1.2 -(avg > max) - ----------------------- - -Questions: - -is it safe to split (refine) multiple states concurrently in the way that we do? - -do we want to check for duplicate sym states when creating new ones through refinement? - - is this safe? - -are we ok to have non-diagonal c-closure algorithm? -or is it ok if only use this on initial reach graph construction?