Browse Source

Fixed compile issues

tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
dfd1fec8c5
  1. 2
      src/storm-pars-cli/storm-pars.cpp
  2. 4
      src/storm-pars/api/region.h
  3. 10
      src/storm/api/transformation.h

2
src/storm-pars-cli/storm-pars.cpp

@ -145,7 +145,7 @@ namespace storm {
} }
if (parametricSettings.transformContinuousModel() && (result.first->isOfType(storm::models::ModelType::Ctmc) || result.first->isOfType(storm::models::ModelType::MarkovAutomaton))) { if (parametricSettings.transformContinuousModel() && (result.first->isOfType(storm::models::ModelType::Ctmc) || result.first->isOfType(storm::models::ModelType::MarkovAutomaton))) {
result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as<storm::models::sparse::Model<ValueType>>()), storm::api::extractFormulasFromProperties(input.properties));
result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as<storm::models::sparse::Model<ValueType>>()), storm::api::extractFormulasFromProperties(input.properties)).first;
result.second = true; result.second = true;
} }

4
src/storm-pars/api/region.h

@ -91,7 +91,7 @@ namespace storm {
if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model..."); STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() }; std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector);
consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector).first;
STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed."); STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
} }
@ -121,7 +121,7 @@ namespace storm {
if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model..."); STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() }; std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector);
consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector).first;
STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed."); STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
} }

10
src/storm/api/transformation.h

@ -24,7 +24,7 @@ namespace storm {
while(model->hasRewardModel(timeRewardName)) { while(model->hasRewardModel(timeRewardName)) {
timeRewardName += "_"; timeRewardName += "_";
} }
auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName)
auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName);
STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties."); STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties.");
if (model->isOfType(storm::models::ModelType::Ctmc)) { if (model->isOfType(storm::models::ModelType::Ctmc)) {
@ -34,7 +34,7 @@ namespace storm {
} else { } else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model->getType() << " to a discrete time model is not supported"); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model->getType() << " to a discrete time model is not supported");
} }
return nullptr;
return std::make_pair(nullptr, newFormulas);;
} }
/*! /*!
@ -51,8 +51,8 @@ namespace storm {
while(model.hasRewardModel(timeRewardName)) { while(model.hasRewardModel(timeRewardName)) {
timeRewardName += "_"; timeRewardName += "_";
} }
auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName)
STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties.");
auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName);
STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model.getType() << " to a discrete time model does not preserve all properties.");
if (model.isOfType(storm::models::ModelType::Ctmc)) { if (model.isOfType(storm::models::ModelType::Ctmc)) {
return std::make_pair(transformer.transform(std::move(*model.template as<storm::models::sparse::Ctmc<ValueType>>())), newFormulas); return std::make_pair(transformer.transform(std::move(*model.template as<storm::models::sparse::Ctmc<ValueType>>())), newFormulas);
@ -61,7 +61,7 @@ namespace storm {
} else { } else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported.");
} }
return nullptr;
return std::make_pair(nullptr, newFormulas);;
} }

Loading…
Cancel
Save