From 46d8ec3d8b9527c8f7afe8bc791dd26e9913be3b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 9 May 2018 18:45:25 +0200 Subject: [PATCH] explicit.LTLModelChecker: protect against int overflow if product state space can not be indexed by int The state information of the model-automaton product are stored as an int array, with one entry for every combination of model state index and automaton state index. Thus, |S|*|A| has to be less than INT_MAX, even if the reachable state space could be index with an int. Thus, we use Math.multiplyExact to catch the case that the product of the two numbers of states overflows the int range and throw an Exception. --- prism/src/explicit/LTLModelChecker.java | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 4d6a5333..eb396142 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -433,11 +433,17 @@ public class LTLModelChecker extends PrismComponent int daSize = da.size(); int numAPs = da.getAPList().size(); int modelNumStates = model.getNumStates(); - int prodNumStates = modelNumStates * daSize; + int prodNumStates; int s_1, s_2, q_1, q_2; BitSet s_labels = new BitSet(numAPs); List prodStatesList = null, daStatesList = null; + try { + prodNumStates = Math.multiplyExact(modelNumStates, daSize); + } catch (ArithmeticException e) { + throw new PrismException("Size of product state space of model and automaton is too large for explicit engine"); + } + VarList newVarList = null; if (model.getVarList() != null) {