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

fix for command line invokation of PLA

tempestpy_adaptions
TimQu 8 years ago
parent
da90719097
commit
3430a66335
1 changed files with 4 additions and 3 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 7
      src/storm/utility/storm.h

7
src/storm/utility/storm.h
View File

@ -324,17 +324,18 @@ namespace storm {
auto refinementThreshold = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(storm::settings::getModule<storm::settings::modules::CoreSettings>().getParameterLiftingThreshold()); auto refinementThreshold = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(storm::settings::getModule<storm::settings::modules::CoreSettings>().getParameterLiftingThreshold());
std::vector<std::pair<storm::storage::ParameterRegion<storm::RationalFunction>, storm::modelchecker::parametric::RegionCheckResult>> result; std::vector<std::pair<storm::storage::ParameterRegion<storm::RationalFunction>, storm::modelchecker::parametric::RegionCheckResult>> result;
std::cout << "Performing parameter lifting for property " << formula << " on initial region " << initialRegion.toString(true) << " with refinementThreshold " << storm::utility::convertNumber<double>(refinementThreshold) << " ...";
std::cout << "Performing parameter lifting for property " << *formula << " on initial region " << initialRegion.toString(true) << " with refinementThreshold " << storm::utility::convertNumber<double>(refinementThreshold) << " ...";
std::cout.flush(); std::cout.flush();
storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction> task(*formula, true);
if (markovModel->isOfType(storm::models::ModelType::Dtmc)) { if (markovModel->isOfType(storm::models::ModelType::Dtmc)) {
storm::modelchecker::parametric::ParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>()); storm::modelchecker::parametric::ParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
parameterLiftingContext.specifyFormula(*formula);
parameterLiftingContext.specifyFormula(task);
result = parameterLiftingContext.performRegionRefinement(initialRegion, refinementThreshold); result = parameterLiftingContext.performRegionRefinement(initialRegion, refinementThreshold);
} else if (markovModel->isOfType(storm::models::ModelType::Mdp)) { } else if (markovModel->isOfType(storm::models::ModelType::Mdp)) {
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>()); storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
parameterLiftingContext.specifyFormula(*formula);
parameterLiftingContext.specifyFormula(task);
result = parameterLiftingContext.performRegionRefinement(initialRegion, refinementThreshold); result = parameterLiftingContext.performRegionRefinement(initialRegion, refinementThreshold);
} else { } else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting on the provided model type."); STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting on the provided model type.");

Write Preview
Loading…
Cancel
Save