Browse Source
NOTES.
NOTES.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2161 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
15 years ago
4 changed files with 115 additions and 216 deletions
-
171prism/NOTES
-
90prism/NOTES-PTAS
-
40prism/NOTES-SIM
-
30prism/TODO
@ -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 |
|
||||
|
|
||||
@ -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) |
|
||||
|
|
||||
|
|
||||
@ -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? |
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue