Browse Source

Bug fix: LHS of until was being ignored in explicit CTMC model checking.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5760 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
commit
08b5f75aa4
  1. 2
      prism/src/explicit/CTMCModelChecker.java

2
prism/src/explicit/CTMCModelChecker.java

@ -216,7 +216,7 @@ public class CTMCModelChecker extends DTMCModelChecker
{ {
mainLog.println("Building embedded DTMC..."); mainLog.println("Building embedded DTMC...");
DTMC dtmcEmb = ((CTMC) dtmc).buildImplicitEmbeddedDTMC(); DTMC dtmcEmb = ((CTMC) dtmc).buildImplicitEmbeddedDTMC();
return super.computeReachProbs(dtmcEmb, null, target, init, known);
return super.computeReachProbs(dtmcEmb, remain, target, init, known);
} }
/** /**

Loading…
Cancel
Save