From 8525fdc43a4c9ad8b3e48170b66f173b17c5bb43 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 30 Jun 2010 20:37:20 +0000 Subject: [PATCH] NOTES. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1965 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES-SIM | 31 +++++++++++++------------------ 1 file changed, 13 insertions(+), 18 deletions(-) diff --git a/prism/NOTES-SIM b/prism/NOTES-SIM index c2b7fbdc..7ca4d080 100644 --- a/prism/NOTES-SIM +++ b/prism/NOTES-SIM @@ -2,40 +2,35 @@ NOW/NEXT -------- -add path manip methods - autochoice, backtrack etc. -but need to sort out loop detection first? -embedded into Path*? +DTMC with local nondet and actions (~/prism-models/dave-test.nm) + +GUI transition box: "true" updates don't display correctly TODO (before any release) ------------------------- -* variable overflow? TODO (later) ------------ +* add (back) support for loop detection (embedded into Path*?) +* add (back) early termination of sampling (thru expt stop?) + * random initial state +* variable overflow etc. +* add support for "deadlock" and "init" (new EvaluationContext, model *and* state dependent) * explicitbuildtest doesn't handle dupes in mdps (e.g. consensus) * seed issues (currently twice in one second = same seed) * traviendo export? -add support for "deadlock" and "init" (new EvaluationContext, model *and* state dependent) - - -explicit build doesn't handle multiple initial states - +* explicit build doesn't handle multiple initial states -approx mc of a property loses any current simulator path in gui. -is that ok? (seems to be buggy in 3.3.1 anyway) - -TEST CASES - -[t,t'] examples sent as MRMC bug fix? - -DTMC with local nondet and actions (~/prism-models/dave-test.nm) +BUGS (later) +------------ -GUI transition box: "true" updates don't display correctly +* approx mc of a property loses any current simulator path in gui. + is that ok? (seems to be buggy in 3.3.1 anyway)