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

@@ -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<State> 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) {