From 5a13c4cf57f1beba6a4b2a37d4e455c6f2488fd2 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 15 Apr 2008 15:09:39 +0000 Subject: [PATCH] Bugfix: in detection of whether there is room for DRA DD vars before row/col. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@758 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 6e44a0b1..4a937776 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -146,7 +146,7 @@ public class LTLModelChecker // and whether there is room to put them before rather than after the existing vars n = (int) Math.ceil(PrismUtils.log2(dra.size())); before = true; - if (allDDRowVars.getMinVarIndex() - ((NondetModel) model).getAllDDNondetVars().getMaxVarIndex() < 2 * n) { + if ((allDDRowVars.getMinVarIndex() - ((NondetModel) model).getAllDDNondetVars().getMaxVarIndex()) - 1 < 2 * n) { before = false; } @@ -191,9 +191,9 @@ public class LTLModelChecker newAllDDRowVars.addVars(draDDRowVars); newAllDDColVars.addVars(draDDColVars); } - newVarList = (VarList)varList.clone(); + newVarList = (VarList) varList.clone(); newVarList.addVar(before ? 0 : varList.getNumVars(), draVar, 0, dra.size() - 1, 0, 1, Expression.INT); - + // Extra references (because will get derefed when new model is done with) // TODO: tidy this up, make it corresond to model.clear() allDDRowVars.refAll();