From 06fa11172d7f2be2efad5a1afd0efc47577c8ef9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 18 Apr 2008 22:20:26 +0000 Subject: [PATCH] Bug fix: LTL DRA start states for reachability. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@760 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 4a937776..a545072e 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -214,10 +214,11 @@ public class LTLModelChecker newTrans = buildTransMask(dra, labelDDs, allDDRowVars, allDDColVars, draDDRowVars, draDDColVars); JDD.Ref(model.getTrans()); newTrans = JDD.Apply(JDD.TIMES, model.getTrans(), newTrans); - + + // Note: ... TODO newStart = buildStartMask(dra, labelDDs); - JDD.Ref(model.getStart()); - newStart = JDD.And(model.getStart(), newStart); + JDD.Ref(model.getReach()); + newStart = JDD.And(model.getReach(), newStart); // Create a new model model object to store the product model NondetModel modelProd = new NondetModel(