NOW/NEXT: add path manip methods - autochoice, backtrack etc. but need to sort out loop detection first? embedded into Path*? TODO: add support "deadlock" and "init" (new EvaluationContext, model *and* state dependent) explicitbuildtest doesn't handle dupes in mdps (e.g. consensus) explicit build doesn't handle multiple initial states seed issues (currently twice in one second = same seed) traviendo export? 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) GUI transition box: "true" updates don't display correctly