s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

imported patch symb-MET-LTLModelChecker-rabin-darowcol-optional.patch

accumulation-v4.7
Joachim Klein 7 years ago
committed by Joachim Klein
parent
1043d51ccf
commit
418b5e7bd6
1 changed files with 36 additions and 26 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 62
      prism/src/prism/LTLModelChecker.java

62
prism/src/prism/LTLModelChecker.java
View File

@ -1206,13 +1206,18 @@ public class LTLModelChecker extends PrismComponent
acceptanceVector_K = JDD.Or(acceptanceVector_K, tmpK);
}
JDD.Ref(model.getTrans01());
JDD.Ref(acceptanceVector_L_not);
candidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), acceptanceVector_L_not);
acceptanceVector_L_not = JDD.PermuteVariables(acceptanceVector_L_not, draDDRowVars, draDDColVars);
candidateStates = JDD.Apply(JDD.TIMES, candidateStates, acceptanceVector_L_not);
candidateStates = JDD.ThereExists(candidateStates, model.getAllDDColVars());
candidateStates = JDD.ThereExists(candidateStates, model.getAllDDNondetVars());
if (draDDRowVars != null && draDDColVars != null) {
JDD.Ref(model.getTrans01());
JDD.Ref(acceptanceVector_L_not);
candidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), acceptanceVector_L_not);
acceptanceVector_L_not = JDD.PermuteVariables(acceptanceVector_L_not, draDDRowVars, draDDColVars);
candidateStates = JDD.Apply(JDD.TIMES, candidateStates, acceptanceVector_L_not);
candidateStates = JDD.ThereExists(candidateStates, model.getAllDDColVars());
candidateStates = JDD.ThereExists(candidateStates, model.getAllDDNondetVars());
} else {
JDD.Ref(model.getReach());
candidateStates = JDD.And(model.getReach(), acceptanceVector_L_not);
}
// find all maximal end components
List<JDDNode> allecs = findMECStates(model, candidateStates, acceptanceVector_K);
JDD.Deref(acceptanceVector_K);
@ -1265,13 +1270,15 @@ public class LTLModelChecker extends PrismComponent
continue;
} else { // recompute maximal end components
//mainLog.println(" ------------- ec is recomputed ------------- ");
JDD.Ref(model.getTrans01());
JDD.Ref(candidateStates);
JDDNode newcandidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), candidateStates);
candidateStates = JDD.PermuteVariables(candidateStates, draDDRowVars, draDDColVars);
newcandidateStates = JDD.Apply(JDD.TIMES, candidateStates, newcandidateStates);
newcandidateStates = JDD.ThereExists(newcandidateStates, model.getAllDDColVars());
candidateStates = JDD.ThereExists(newcandidateStates, model.getAllDDNondetVars());
if (draDDRowVars != null && draDDColVars != null) {
JDD.Ref(model.getTrans01());
JDD.Ref(candidateStates);
JDDNode newcandidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), candidateStates);
candidateStates = JDD.PermuteVariables(candidateStates, draDDRowVars, draDDColVars);
newcandidateStates = JDD.Apply(JDD.TIMES, candidateStates, newcandidateStates);
newcandidateStates = JDD.ThereExists(newcandidateStates, model.getAllDDColVars());
candidateStates = JDD.ThereExists(newcandidateStates, model.getAllDDNondetVars());
}
ecs = findMECStates(model, candidateStates, acceptanceVector_K);
}
JDD.Deref(candidateStates);
@ -1299,18 +1306,21 @@ public class LTLModelChecker extends PrismComponent
JDDNode statesK_i = acceptance.get(i).getK();
// 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)
// TODO: I don't think this next step is needed,
// since the ECComputer restricts the model in this way anyway.
// However, for fairness, the restriction of the candidateStates
// to statesLi_not has to happen for correctness.
JDD.Ref(model.getTrans01());
JDD.Ref(statesLi_not);
candidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), statesLi_not);
statesLi_not = JDD.PermuteVariables(statesLi_not, draDDRowVars, draDDColVars);
candidateStates = JDD.Apply(JDD.TIMES, candidateStates, statesLi_not);
candidateStates = JDD.ThereExists(candidateStates, model.getAllDDColVars());
candidateStates = JDD.ThereExists(candidateStates, model.getAllDDNondetVars());
// Normal case (no fairness): find accepting MECs within !L_i
if (draDDRowVars != null && draDDColVars != null) {
// 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(statesLi_not);
candidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), statesLi_not);
statesLi_not = JDD.PermuteVariables(statesLi_not, draDDRowVars, draDDColVars);
candidateStates = JDD.Apply(JDD.TIMES, candidateStates, statesLi_not);
candidateStates = JDD.ThereExists(candidateStates, model.getAllDDColVars());
candidateStates = JDD.ThereExists(candidateStates, model.getAllDDNondetVars());
} else {
JDD.Ref(model.getReach());
candidateStates = JDD.And(model.getReach(), statesLi_not);
}
// Normal case (no fairness): find accepting MECs within !L_i
if (!fairness) {
List<JDDNode> ecs = findMECStates(model, candidateStates);
JDD.Deref(candidateStates);

Write Preview
Loading…
Cancel
Save