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(program, result.second)->template as(); } 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(janiData.first, result.second, TestType::engine == CtmcEngine::JitSparse)->template as(); } @@ -226,11 +223,8 @@ namespace { result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); } 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(janiData.first, result.second)->template as(); } 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(program, result.second)->template as(); } 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(janiData.first, result.second, TestType::engine == DtmcEngine::JitSparse)->template as(); } @@ -482,11 +479,8 @@ namespace { result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); } 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(janiData.first, result.second)->template as(); } 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(program, result.second)->template as(); } 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(janiData.first, result.second, TestType::engine == MaEngine::JitSparse)->template as(); } 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(program, result.second)->template as(); } 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(janiData.first, result.second, TestType::engine == MdpEngine::JitSparse)->template as(); } @@ -342,11 +339,8 @@ namespace { result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); } 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(janiData.first, result.second)->template as(); } @@ -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 {