|
|
@ -806,6 +806,8 @@ public class LTLModelChecker extends PrismComponent |
|
|
JDDNode statesK_i = buildKStatesForRabinPair(draDDRowVars, dra, i); |
|
|
JDDNode statesK_i = buildKStatesForRabinPair(draDDRowVars, dra, i); |
|
|
// Find states in the model for which there are no transitions leaving !L_i |
|
|
// Find states in the model for which there are no transitions leaving !L_i |
|
|
// (this will allow us to reduce the problem to finding MECs, not ECs) |
|
|
// (this will allow us to reduce the problem to finding MECs, not ECs) |
|
|
|
|
|
// TODO: I don't think this next step is needed, |
|
|
|
|
|
// since the ECComputer restricts the model in this way anyway |
|
|
JDD.Ref(model.getTrans01()); |
|
|
JDD.Ref(model.getTrans01()); |
|
|
JDD.Ref(statesLi_not); |
|
|
JDD.Ref(statesLi_not); |
|
|
candidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), statesLi_not); |
|
|
candidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), statesLi_not); |
|
|
|