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

parameter lifting with hybrid engine

tempestpy_adaptions
TimQu 8 years ago
parent
bb3c2bd556
commit
367b8f0a3e
4 changed files with 40 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
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 12
      src/storm/cli/entrypoints.h
  2. 27
      src/storm/transformer/SymbolicToSparseTransformer.cpp
  3. 3
      src/storm/transformer/SymbolicToSparseTransformer.h
  4. 1
      src/storm/utility/storm.h

12
src/storm/cli/entrypoints.h
View File

@ -290,7 +290,17 @@ namespace storm {
// Then select the correct engine.
if (hybrid) {
verifySymbolicModelWithHybridEngine<LibraryType, ValueType>(markovModel, properties, onlyInitialStatesRelevant);
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isParameterLiftingSet()) {
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet(), storm::exceptions::InvalidSettingsException, "Invoked parameter lifting without enabling the parametric engine.");
STORM_PRINT_AND_LOG("Transforming symbolic model to sparse model ...");
auto sparseModel = storm::transformer::transformSymbolicToSparseModel(markovModel);
STORM_PRINT_AND_LOG(" done" << std::endl);
sparseModel->printModelInformationToStream(std::cout);
auto formulas = extractFormulasFromProperties(properties);
storm::performParameterLifting<ValueType>(sparseModel, formulas);
} else {
verifySymbolicModelWithHybridEngine<LibraryType, ValueType>(markovModel, properties, onlyInitialStatesRelevant);
}
} else {
verifySymbolicModelWithDdEngine<LibraryType, ValueType>(markovModel, properties, onlyInitialStatesRelevant);
}

27
src/storm/transformer/SymbolicToSparseTransformer.cpp
View File

@ -4,12 +4,29 @@
#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/NotImplementedException.h"
namespace storm {
namespace transformer {
template<storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> transformSymbolicToSparseModel(std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> const& symbolicModel) {
switch (symbolicModel->getType()) {
case storm::models::ModelType::Dtmc:
return SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>().translate(*symbolicModel->template as<storm::models::symbolic::Dtmc<Type, ValueType>>());
case storm::models::ModelType::Mdp:
return SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Mdp<Type, ValueType>>());
case storm::models::ModelType::Ctmc:
return SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Ctmc<Type, ValueType>>());
default:
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Transformation of symbolic " << symbolicModel->getType() << " to sparse model is not implemented.");
}
return nullptr;
}
template<storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>::translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc) {
this->odd = symbolicDtmc.getReachableStates().createOdd();
@ -106,19 +123,25 @@ namespace storm {
return std::make_shared<storm::models::sparse::Ctmc<ValueType>>(transitionMatrix, labelling, rewardModels);
}
template std::shared_ptr<storm::models::sparse::Model<double>> transformSymbolicToSparseModel<storm::dd::DdType::CUDD, double>(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>> const& symbolicModel);
template std::shared_ptr<storm::models::sparse::Model<double>> transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, double>(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>> const& symbolicModel);
template std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, storm::RationalNumber>(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalNumber>> const& symbolicModel);
template std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, storm::RationalFunction>(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction>> const& symbolicModel);
template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::CUDD, double>;
template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, double>;
template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalFunction>;
template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::CUDD, double>;
template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, double>;
template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, storm::RationalFunction>;
template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::CUDD, double>;
template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::Sylvan, double>;
template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;
template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalFunction>;
}
}

3
src/storm/transformer/SymbolicToSparseTransformer.h
View File

@ -12,6 +12,9 @@
namespace storm {
namespace transformer {
template<storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> transformSymbolicToSparseModel(std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> const& symbolicModel);
template<storm::dd::DdType Type, typename ValueType>
class SymbolicDtmcToSparseDtmcTransformer {
public:

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

@ -332,6 +332,7 @@ namespace storm {
STORM_PRINT_AND_LOG("Transforming continuous model to discrete model...");
storm::transformer::transformContinuousToDiscreteModelInPlace(markovModel, consideredFormula);
STORM_PRINT_AND_LOG(" done!" << std::endl);
markovModel->printModelInformationToStream(std::cout);
}
auto modelParameters = storm::models::sparse::getProbabilityParameters(*markovModel);

Write Preview
Loading…
Cancel
Save