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

using some template magic to make it compile again 

Former-commit-id: 69888cac45
main
dehnert 10 years ago
parent
11b04c7940
commit
40a75baee7
4 changed files with 41 additions and 20 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. 1
      src/models/symbolic/Model.h
  2. 2
      src/storage/bisimulation/BisimulationDecomposition.cpp
  3. 2
      src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
  4. 50
      src/utility/storm.h

1
src/models/symbolic/Model.h
View File

@ -38,6 +38,7 @@ namespace storm {
template<storm::dd::DdType Type> template<storm::dd::DdType Type>
class Model : public storm::models::ModelBase { class Model : public storm::models::ModelBase {
public: public:
static const storm::dd::DdType DdType = Type;
typedef StandardRewardModel<Type, double> RewardModelType; typedef StandardRewardModel<Type, double> RewardModelType;
Model(Model<Type> const& other) = default; Model(Model<Type> const& other) = default;

2
src/storage/bisimulation/BisimulationDecomposition.cpp
View File

@ -276,9 +276,11 @@ namespace storm {
} }
template class BisimulationDecomposition<storm::models::sparse::Dtmc<double>>; template class BisimulationDecomposition<storm::models::sparse::Dtmc<double>>;
template class BisimulationDecomposition<storm::models::sparse::Ctmc<double>>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class BisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>>; template class BisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>>;
template class BisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>>;
#endif #endif
} }
} }

2
src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
View File

@ -364,9 +364,11 @@ namespace storm {
} }
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>; template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>;
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>>; template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>>;
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>>;
#endif #endif
} }
} }

50
src/utility/storm.h
View File

@ -113,33 +113,49 @@ namespace storm {
return result; return result;
} }
template<typename ValueType>
std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
template<typename ModelType>
std::shared_ptr<ModelType> performSparseBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::cout << "Performing bisimulation minimization... ";
typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options options;
if (!formulas.empty()) {
options = typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas);
}
if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
options.type = storm::storage::BisimulationType::Weak;
options.bounded = false;
}
storm::storage::DeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
model = bisimulationDecomposition.getQuotient();
std::cout << "done." << std::endl << std::endl;
return model;
}
template<typename ModelType, typename ValueType = typename ModelType::ValueType, typename std::enable_if<std::is_base_of<storm::models::sparse::Model<ValueType>, ModelType>::value, bool>::type = 0>
std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
if (storm::settings::generalSettings().isBisimulationSet()) { if (storm::settings::generalSettings().isBisimulationSet()) {
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models.");
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs.");
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = sparseModel->template as<storm::models::sparse::Dtmc<ValueType>>();
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs and CTMCs.");
dtmc->reduceToStateBasedRewards();
model->reduceToStateBasedRewards();
std::cout << "Performing bisimulation minimization... ";
typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options;
if (!formulas.empty()) {
options = typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options(*sparseModel, formulas);
}
if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
options.type = storm::storage::BisimulationType::Weak;
options.bounded = false;
if (model->isOfType(storm::models::ModelType::Dtmc)) {
return performSparseBisimulationMinimization<storm::models::sparse::Dtmc<ValueType>>(model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas);
} else {
return performSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas);
} }
storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options);
model = bisimulationDecomposition.getQuotient();
std::cout << "done." << std::endl << std::endl;
} }
return model; return model;
} }
template<typename ModelType, storm::dd::DdType DdType = ModelType::DdType, typename std::enable_if< std::is_base_of< storm::models::symbolic::Model<DdType>, ModelType >::value, bool>::type = 0>
std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
// No preprocessing available yet.
return model;
}
template<typename ValueType> template<typename ValueType>
void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> const& formula) { void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) { if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {

Write Preview
Loading…
Cancel
Save