From ebfee78ecc4c228b6471f34295259fb9fd7f3731 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 27 Sep 2018 11:44:35 +0200
Subject: [PATCH] Fixed compilation of tests
---
.../storm/modelchecker/CtmcCslModelCheckerTest.cpp | 10 ++--------
.../storm/modelchecker/DtmcPrctlModelCheckerTest.cpp | 10 ++--------
.../MarkovAutomatonCslModelCheckerTest.cpp | 5 +----
.../storm/modelchecker/MdpPrctlModelCheckerTest.cpp | 12 +++---------
4 files changed, 8 insertions(+), 29 deletions(-)
diff --git a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp
index 9e4cac7f9..b0bf313be 100644
--- a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp
@@ -205,11 +205,8 @@ namespace {
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
} else if (TestType::engine == CtmcEngine::JaniSparse || TestType::engine == CtmcEngine::JitSparse) {
- storm::converter::PrismToJaniConverterOptions options;
- options.allVariablesGlobal = true;
- options.janiOptions.standardCompliant = true;
- options.janiOptions.exportFlattened = true;
auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+ janiData.first.substituteFunctions();
result.second = storm::api::extractFormulasFromProperties(janiData.second);
result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second, TestType::engine == CtmcEngine::JitSparse)->template as<MT>();
}
@@ -226,11 +223,8 @@ namespace {
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
} else if (TestType::engine == CtmcEngine::JaniHybrid) {
- storm::converter::PrismToJaniConverterOptions options;
- options.allVariablesGlobal = true;
- options.janiOptions.standardCompliant = true;
- options.janiOptions.exportFlattened = true;
auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+ janiData.first.substituteFunctions();
result.second = storm::api::extractFormulasFromProperties(janiData.second);
result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
}
diff --git a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp
index b5d5c801b..f29c88859 100644
--- a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp
@@ -461,11 +461,8 @@ namespace {
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
} else if (TestType::engine == DtmcEngine::JaniSparse || TestType::engine == DtmcEngine::JitSparse) {
- storm::converter::PrismToJaniConverterOptions options;
- options.allVariablesGlobal = true;
- options.janiOptions.standardCompliant = true;
- options.janiOptions.exportFlattened = true;
auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+ janiData.first.substituteFunctions();
result.second = storm::api::extractFormulasFromProperties(janiData.second);
result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second, TestType::engine == DtmcEngine::JitSparse)->template as<MT>();
}
@@ -482,11 +479,8 @@ namespace {
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
} else if (TestType::engine == DtmcEngine::JaniDd) {
- storm::converter::PrismToJaniConverterOptions options;
- options.allVariablesGlobal = true;
- options.janiOptions.standardCompliant = true;
- options.janiOptions.exportFlattened = true;
auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+ janiData.first.substituteFunctions();
result.second = storm::api::extractFormulasFromProperties(janiData.second);
result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
}
diff --git a/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp
index 11d29b6b6..db6ca04f9 100644
--- a/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp
@@ -137,11 +137,8 @@ namespace {
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
} else if (TestType::engine == MaEngine::JaniSparse || TestType::engine == MaEngine::JitSparse) {
- storm::converter::PrismToJaniConverterOptions options;
- options.allVariablesGlobal = true;
- options.janiOptions.standardCompliant = true;
- options.janiOptions.exportFlattened = true;
auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+ janiData.first.substituteFunctions();
result.second = storm::api::extractFormulasFromProperties(janiData.second);
result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second, TestType::engine == MaEngine::JitSparse)->template as<MT>();
}
diff --git a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp
index fb0b135c4..67ae49920 100644
--- a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp
@@ -321,11 +321,8 @@ namespace {
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
} else if (TestType::engine == MdpEngine::JaniSparse || TestType::engine == MdpEngine::JitSparse) {
- storm::converter::PrismToJaniConverterOptions options;
- options.allVariablesGlobal = true;
- options.janiOptions.standardCompliant = true;
- options.janiOptions.exportFlattened = true;
auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+ janiData.first.substituteFunctions();
result.second = storm::api::extractFormulasFromProperties(janiData.second);
result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second, TestType::engine == MdpEngine::JitSparse)->template as<MT>();
}
@@ -342,11 +339,8 @@ namespace {
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
} else if (TestType::engine == MdpEngine::JaniDd) {
- storm::converter::PrismToJaniConverterOptions options;
- options.allVariablesGlobal = true;
- options.janiOptions.standardCompliant = true;
- options.janiOptions.exportFlattened = true;
auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+ janiData.first.substituteFunctions();
result.second = storm::api::extractFormulasFromProperties(janiData.second);
result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
}
@@ -588,7 +582,7 @@ namespace {
// This example considers a zero-reward end component that does not reach the target
// For some methods this requires end-component elimination which is (currently) not supported in the Dd engine
- if (TypeParam::engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
+ if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse || TypeParam::engine == MdpEngine::JitSparse || TypeParam::engine == MdpEngine::Hybrid) {
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("114/49"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
} else {