Browse Source

Rmin/max[C]: Switch from -hybrid (default) engine to -sparse

As currently there is no support for Rmin/max[C] computations using hybrid engine, and hybrid is the default engine, automatically switch to the sparse engine, similar to what is done for other computations.
accumulation-v4.7
Joachim Klein 7 years ago
committed by GitHub
parent
commit
837bdc601d
No known key found for this signature in database GPG Key ID: 4AEE18F83AFDEB23
  1. 7
      prism/src/prism/NondetModelChecker.java

7
prism/src/prism/NondetModelChecker.java

@ -2174,9 +2174,16 @@ public class NondetModelChecker extends NonProbModelChecker
{
DoubleVector rewardsDV;
StateValues rewards = null;
// Local copy of setting
int engine = this.engine;
// compute 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) {

Loading…
Cancel
Save