From 20721f74d424ca98345e07a47e8e4d14965c72ae Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 8 Dec 2009 13:50:48 +0000 Subject: [PATCH] Bugfix: crash on DRAs with only 1 state, e.g. for F F false. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1628 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 568ee8d9..0fc8e71e 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -147,7 +147,9 @@ public class LTLModelChecker // See how many new dd vars will be needed for DRA // and whether there is room to put them before rather than after the existing vars + // (if DRA only has one state, we add an extra dummy state) n = (int) Math.ceil(PrismUtils.log2(dra.size())); + n = Math.max(n, 1); before = true; if (allDDRowVars.getMinVarIndex() - 1 < 2 * n) { before = false; @@ -195,7 +197,8 @@ public class LTLModelChecker newAllDDColVars.addVars(draDDColVars); } newVarList = (VarList) varList.clone(); - Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(dra.size() - 1))); + // NB: if DRA only has one state, we add an extra dummy state + Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(dra.size() - 1, 1)))); newVarList.addVar(before ? 0 : varList.getNumVars(), decl, 1, model.getConstantValues()); // Extra references (because will get derefed when new model is done with) @@ -292,7 +295,9 @@ public class LTLModelChecker // See how many new dd vars will be needed for DRA // and whether there is room to put them before rather than after the existing vars + // (if DRA only has one state, we add an extra dummy state) n = (int) Math.ceil(PrismUtils.log2(dra.size())); + n = Math.max(n, 1); before = true; if ((allDDRowVars.getMinVarIndex() - model.getAllDDNondetVars().getMaxVarIndex()) - 1 < 2 * n) { before = false; @@ -340,7 +345,8 @@ public class LTLModelChecker newAllDDColVars.addVars(draDDColVars); } newVarList = (VarList) varList.clone(); - Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(dra.size() - 1))); + // NB: if DRA only has one state, we add an extra dummy state + Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(dra.size() - 1, 1)))); newVarList.addVar(before ? 0 : varList.getNumVars(), decl, 1, model.getConstantValues()); // Extra references (because will get derefed when new model is done with)