sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Fixed compilation of tests

tempestpy_adaptions
TimQu 6 years ago
parent
ec3881e502
commit
ebfee78ecc
4 changed files with 8 additions and 29 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp
  2. 10
      src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp
  3. 5
      src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp
  4. 12
      src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp

10
src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp
View File

@ -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>();
}

10
src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp
View File

@ -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>();
}

5
src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp
View File

@ -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>();
}

12
src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp
View File

@ -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 {
Write Preview
Loading…
Cancel
Save