From ab9fa27411e70b57766ebb7f3d2c2c0df2fbaf53 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 27 Dec 2011 00:55:38 +0000 Subject: [PATCH] Automatically switch to another engine if numerical computation not supported. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4282 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModelChecker.java | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 3160ffad..a50986b6 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1085,6 +1085,8 @@ public class NondetModelChecker extends NonProbModelChecker JDDNode rewardsMTBDD; DoubleVector rewardsDV; StateValues rewards = null; + // Local copy of setting + int engine = this.engine; // a trivial case: "=0" if (time == 0) { @@ -1095,6 +1097,11 @@ public class NondetModelChecker extends NonProbModelChecker else { // compute the rewards mainLog.println("\nComputing rewards..."); + // switch engine, if necessary + if (engine == Prism.HYBRID) { + mainLog.println("Switching engine since hybrid engine does yet support this computation..."); + engine = Prism.SPARSE; + } mainLog.println("Engine: " + Prism.getEngineString(engine)); try { switch (engine) { @@ -1127,6 +1134,8 @@ public class NondetModelChecker extends NonProbModelChecker JDDNode rewardsMTBDD; DoubleVector rewardsDV; StateValues rewards = null; + // Local copy of setting + int engine = this.engine; Vector zeroCostEndComponents = null; @@ -1213,6 +1222,11 @@ public class NondetModelChecker extends NonProbModelChecker else { // compute the rewards mainLog.println("\nComputing remaining rewards..."); + // switch engine, if necessary + if (engine == Prism.HYBRID) { + mainLog.println("Switching engine since hybrid engine does yet support this computation..."); + engine = Prism.SPARSE; + } mainLog.println("Engine: " + Prism.getEngineString(engine)); try { switch (engine) {