From a744b15a7e69f51c813bd7e5805ff90b7fca1b4f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 19 May 2015 01:14:41 +0000 Subject: [PATCH] Fix (again) computation of number of nondet choices for symbolic models (did not work for large number of nondet DD vars). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9848 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModel.java | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index b305988c..1fa26bfb 100644 --- a/prism/src/prism/NondetModel.java +++ b/prism/src/prism/NondetModel.java @@ -268,15 +268,18 @@ public class NondetModel extends ProbModel transInd = JDD.Or(transInd, JDD.ThereExists(tmp, allDDColVars)); } JDD.Deref(tmp); - // update mask - JDD.Deref(nondetMask); + // update transition count + numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); + // re-build mask for nondeterminstic choices + // (and work out number of choices) JDD.Ref(trans01); JDD.Ref(reach); - nondetMask = JDD.And(JDD.Not(JDD.ThereExists(trans01, allDDColVars)), reach); - // update model stats - numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); - double d = JDD.GetNumMinterms(nondetMask, getNumDDRowVars() + getNumDDNondetVars()); - numChoices = ((Math.pow(2, getNumDDNondetVars())) * numStates) - d; + if (this.nondetMask != null) + JDD.Deref(this.nondetMask); + nondetMask = JDD.And(JDD.ThereExists(trans01, allDDColVars), reach); + numChoices = JDD.GetNumMinterms(nondetMask, getNumDDRowVars() + getNumDDNondetVars()); + JDD.Ref(reach); + nondetMask = JDD.And(JDD.Not(nondetMask), reach); } }