Browse Source

Auto-switch to spatrse engine when asked to generate adversraries.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6827 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
commit
bba7710a6f
  1. 3
      prism/src/prism/NondetModelChecker.java

3
prism/src/prism/NondetModelChecker.java

@ -93,7 +93,8 @@ public class NondetModelChecker extends NonProbModelChecker
boolean advGenNeeded = (prism.getExportAdv() != Prism.EXPORT_ADV_NONE); boolean advGenNeeded = (prism.getExportAdv() != Prism.EXPORT_ADV_NONE);
if (advGenNeeded) { if (advGenNeeded) {
if (engine != Prism.SPARSE) { if (engine != Prism.SPARSE) {
mainLog.printWarning("Adversary generation is only implemented for the sparse engine");
mainLog.println("Switching engine since only sparse engine currently supports this computation...");
engine = Prism.SPARSE;
} }
if (precomp && prob1) { if (precomp && prob1) {
mainLog.printWarning("Disabling Prob1 since this is needed for adversary generation"); mainLog.printWarning("Disabling Prob1 since this is needed for adversary generation");

Loading…
Cancel
Save