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

Merge branch 'master' into dft

tempestpy_adaptions
Matthias Volk 6 years ago
parent
04164d8b02 8fbc8d56c0
commit
47b2cb737d
10 changed files with 259 additions and 79 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. 137
      src/storm-pars-cli/storm-pars.cpp
  2. 4
      src/storm-pars/api/region.h
  3. 4
      src/storm-parsers/parser/DirectEncodingParser.cpp
  4. 75
      src/storm/analysis/GraphConditions.cpp
  5. 34
      src/storm/api/transformation.h
  6. 28
      src/storm/logic/ExpectedTimeToExpectedRewardVisitor.cpp
  7. 25
      src/storm/logic/ExpectedTimeToExpectedRewardVisitor.h
  8. 2
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
  9. 19
      src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp
  10. 10
      src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h

137
src/storm-pars-cli/storm-pars.cpp
View File

@ -45,6 +45,16 @@ namespace storm {
bool graphPreserving;
bool exact;
};
struct PreprocessResult {
PreprocessResult(std::shared_ptr<storm::models::ModelBase> const& model, bool changed) : changed(changed), model(model) {
// Intentionally left empty.
}
bool changed;
std::shared_ptr<storm::models::ModelBase> model;
boost::optional<std::vector<std::shared_ptr<storm::logic::Formula const>>> formulas;
};
template <typename ValueType>
std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::shared_ptr<storm::models::ModelBase> const& model) {
@ -127,64 +137,76 @@ namespace storm {
}
template <typename ValueType>
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
PreprocessResult preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
PreprocessResult result(model, false);
if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) {
result.first = storm::cli::preprocessSparseMarkovAutomaton(result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
result.second = true;
if (result.model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
result.model = storm::cli::preprocessSparseMarkovAutomaton(result.model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
result.changed = true;
}
if (generalSettings.isBisimulationSet()) {
result.first = storm::cli::preprocessSparseModelBisimulation(result.first->template as<storm::models::sparse::Model<ValueType>>(), input, bisimulationSettings);
result.second = true;
result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as<storm::models::sparse::Model<ValueType>>(), input, bisimulationSettings);
result.changed = true;
}
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.second = true;
if (parametricSettings.transformContinuousModel() && (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton))) {
auto transformResult = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*model->template as<storm::models::sparse::Model<ValueType>>()), storm::api::extractFormulasFromProperties(input.properties));
result.model = transformResult.first;
// Set transformed properties as new properties in input
result.formulas = transformResult.second;
result.changed = true;
}
return result;
}
template <storm::dd::DdType DdType, typename ValueType>
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) {
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
PreprocessResult preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) {
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
PreprocessResult result(model, false);
if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) {
// Currently, hybrid engine for parametric models just referrs to building the model symbolically.
// Currently, hybrid engine for parametric models just refers to building the model symbolically.
STORM_LOG_INFO("Translating symbolic model to sparse model...");
result.first = storm::api::transformSymbolicToSparseModel(model);
result.second = true;
result.model = storm::api::transformSymbolicToSparseModel(model);
result.changed = true;
// Invoke preprocessing on the sparse model
auto sparsePreprocessingResult = storm::pars::preprocessSparseModel<ValueType>(result.first->as<storm::models::sparse::Model<ValueType>>(), input);
if (sparsePreprocessingResult.second) {
result.first = sparsePreprocessingResult.first;
PreprocessResult sparsePreprocessingResult = storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), input);
if (sparsePreprocessingResult.changed) {
result.model = sparsePreprocessingResult.model;
result.formulas = sparsePreprocessingResult.formulas;
}
} else {
STORM_LOG_ASSERT(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Dd, "Expected Dd engine.");
if (generalSettings.isBisimulationSet()) {
result.model = storm::cli::preprocessDdModelBisimulation(result.model->template as<storm::models::symbolic::Model<DdType, ValueType>>(), input, bisimulationSettings);
result.changed = true;
}
}
return result;
}
template <storm::dd::DdType DdType, typename ValueType>
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
PreprocessResult preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
storm::utility::Stopwatch preprocessingWatch(true);
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
PreprocessResult result(model, false);
if (model->isSparseModel()) {
result = storm::pars::preprocessSparseModel<ValueType>(result.first->as<storm::models::sparse::Model<ValueType>>(), input);
result = storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), input);
} else {
STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
result = storm::pars::preprocessDdModel<DdType, ValueType>(result.first->as<storm::models::symbolic::Model<DdType, ValueType>>(), input);
result = storm::pars::preprocessDdModel<DdType, ValueType>(result.model->as<storm::models::symbolic::Model<DdType, ValueType>>(), input);
}
if (result.second) {
if (result.changed) {
STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl);
}
return result;
@ -353,6 +375,11 @@ namespace storm {
boost::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath());
}
else if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Ctmc)) {
auto ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
boost::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*ctmc), parametricSettings.exportResultPath());
}
});
} else {
STORM_LOG_TRACE("Sampling the model at given points.");
@ -461,11 +488,47 @@ namespace storm {
}
}
}
template <storm::dd::DdType DdType, typename ValueType>
void verifyPropertiesWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
if (samples.empty()) {
verifyProperties<ValueType>(input.properties,
[&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithDdEngine<DdType, ValueType>(model, storm::api::createTask<ValueType>(formula, true));
if (result) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
}
return result;
},
[&model] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) {
//auto dtmc = model->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>();
//boost::optional<ValueType> rationalFunction = result->asSymbolicQuantitativeCheckResult<DdType, ValueType>().sum();
//storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath());
}
});
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is not supported in the symbolic engine.");
}
}
template <storm::dd::DdType DdType, typename ValueType>
void verifyWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, SampleInformation<ValueType> const& samples) {
if (regions.empty()) {
storm::pars::verifyPropertiesWithSymbolicEngine(model, input, samples);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Region verification is not supported in the symbolic engine.");
}
}
template <storm::dd::DdType DdType, typename ValueType>
void verifyParametricModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, SampleInformation<ValueType> const& samples) {
STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type.");
storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples);
if (model->isSparseModel()) {
storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples);
} else {
storm::pars::verifyWithDdEngine<DdType, ValueType>(model->as<storm::models::symbolic::Model<DdType, ValueType>>(), input, regions, samples);
}
}
template <storm::dd::DdType DdType, typename ValueType>
@ -492,8 +555,20 @@ namespace storm {
if (model) {
auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input);
if (preprocessingResult.second) {
model = preprocessingResult.first;
if (preprocessingResult.changed) {
model = preprocessingResult.model;
if (preprocessingResult.formulas) {
std::vector<storm::jani::Property> newProperties;
for (size_t i = 0; i < preprocessingResult.formulas.get().size(); ++i) {
auto formula = preprocessingResult.formulas.get().at(i);
STORM_LOG_ASSERT(i < input.properties.size(), "Index " << i << " greater than number of properties.");
storm::jani::Property property = input.properties.at(i);
newProperties.push_back(storm::jani::Property(property.getName(), formula, property.getUndefinedConstants(), property.getComment()));
}
input.properties = newProperties;
}
model->printModelInformationToStream(std::cout);
}
}

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

@ -91,7 +91,7 @@ namespace storm {
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...");
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.");
}
@ -121,7 +121,7 @@ namespace storm {
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...");
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.");
}

4
src/storm-parsers/parser/DirectEncodingParser.cpp
View File

@ -106,13 +106,13 @@ namespace storm {
// Initialize
auto modelComponents = std::make_shared<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>();
bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton || type == storm::models::ModelType::Pomdp);
bool continousTime = (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton);
bool continuousTime = (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton);
storm::storage::SparseMatrixBuilder<ValueType> builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, nonDeterministic, 0);
modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize);
modelComponents->observabilityClasses = std::vector<uint32_t>();
modelComponents->observabilityClasses->resize(stateSize);
std::vector<std::vector<ValueType>> stateRewards;
if (continousTime) {
if (continuousTime) {
modelComponents->exitRates = std::vector<ValueType>(stateSize);
if (type == storm::models::ModelType::MarkovAutomaton) {
modelComponents->markovianStates = storm::storage::BitVector(stateSize);

75
src/storm/analysis/GraphConditions.cpp
View File

@ -56,47 +56,70 @@ namespace storm {
template <typename ValueType>
void ConstraintCollector<ValueType>::process(storm::models::sparse::Model<ValueType> const& model) {
for(uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) {
ValueType sum = storm::utility::zero<ValueType>();
for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) {
auto const& transition = *transitionIt;
sum += transition.getValue();
if (!storm::utility::isConstant(transition.getValue())) {
auto const& transitionVars = transition.getValue().gatherVariables();
variableSet.insert(transitionVars.begin(), transitionVars.end());
// Assert: 0 <= transition <= 1
if (model.getType() != storm::models::ModelType::Ctmc) {
for(uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) {
ValueType sum = storm::utility::zero<ValueType>();
for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) {
auto const& transition = *transitionIt;
sum += transition.getValue();
if (!storm::utility::isConstant(transition.getValue())) {
auto const& transitionVars = transition.getValue().gatherVariables();
variableSet.insert(transitionVars.begin(), transitionVars.end());
// Assert: 0 <= transition <= 1
if (transition.getValue().denominator().isConstant()) {
assert(transition.getValue().denominator().constantPart() != 0);
if (transition.getValue().denominator().constantPart() > 0) {
// Assert: nom <= denom
wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::LEQ);
// Assert: nom >= 0
wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
} else if (transition.getValue().denominator().constantPart() < 0) {
// Assert nom >= denom
wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::GEQ);
// Assert: nom <= 0
wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
} else {
STORM_LOG_ASSERT(false, "Denominator must not equal 0.");
}
} else {
// Assert: denom != 0
wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
// Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0
wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType<ValueType>::val(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
// TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0
}
// Assert: transition > 0
graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
}
}
STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1.");
if(!storm::utility::isConstant(sum)) {
// Assert: sum == 1
wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ);
}
}
} else {
for (auto const& transition : model.getTransitionMatrix()) {
if(!transition.getValue().isConstant()) {
if (transition.getValue().denominator().isConstant()) {
assert(transition.getValue().denominator().constantPart() != 0);
if (transition.getValue().denominator().constantPart() > 0) {
// Assert: nom <= denom
wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::LEQ);
// Assert: nom >= 0
wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
} else if (transition.getValue().denominator().constantPart() < 0) {
// Assert nom >= denom
wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::GEQ);
// Assert: nom <= 0
wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
} else {
STORM_LOG_ASSERT(false, "Denominator must not equal 0.");
assert(false); // Should fail before.
}
} else {
// Assert: denom != 0
wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
// Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0
wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType<ValueType>::val(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
// TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0
}
// Assert: transition > 0
graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
}
}
STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1.");
if(!storm::utility::isConstant(sum)) {
// Assert: sum == 1
wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ);
}
}
if (model.getType() == storm::models::ModelType::Ctmc) {

34
src/storm/api/transformation.h
View File

@ -13,25 +13,28 @@ namespace storm {
/*!
* Transforms the given continuous model to a discrete time model.
* If such a transformation does not preserve one of the given formulas, an error is issued.
* If such a transformation does not preserve one of the given formulas, a warning is issued.
*/
template <typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType> transformer;
for (auto const& formula : formulas) {
STORM_LOG_THROW(transformer.preservesFormula(*formula), storm::exceptions::InvalidOperationException, "Transformation to discrete time model does not preserve formula " << *formula << ".");
std::string timeRewardName = "_time";
while(model->hasRewardModel(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.");
if (model->isOfType(storm::models::ModelType::Ctmc)) {
return transformer.transform(*model->template as<storm::models::sparse::Ctmc<ValueType>>());
return std::make_pair(transformer.transform(*model->template as<storm::models::sparse::Ctmc<ValueType>>(), timeRewardName), newFormulas);
} else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
return transformer.transform(*model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
return std::make_pair(transformer.transform(*model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(), timeRewardName), newFormulas);
} else {
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);;
}
/*!
@ -40,22 +43,25 @@ namespace storm {
* If such a transformation does not preserve one of the given formulas, an error is issued.
*/
template <typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model<ValueType>&& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model<ValueType>&& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType> transformer;
for (auto const& formula : formulas) {
STORM_LOG_THROW(transformer.preservesFormula(*formula), storm::exceptions::InvalidOperationException, "Transformation to discrete time model does not preserve formula " << *formula << ".");
std::string timeRewardName = "_time";
while(model.hasRewardModel(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.");
if (model.isOfType(storm::models::ModelType::Ctmc)) {
return transformer.transform(std::move(*model.template as<storm::models::sparse::Ctmc<ValueType>>()));
return std::make_pair(transformer.transform(std::move(*model.template as<storm::models::sparse::Ctmc<ValueType>>()), timeRewardName), newFormulas);
} else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) {
return transformer.transform(std::move(*model.template as<storm::models::sparse::MarkovAutomaton<ValueType>>()));
return std::make_pair(transformer.transform(std::move(*model.template as<storm::models::sparse::MarkovAutomaton<ValueType>>()), timeRewardName), newFormulas);
} else {
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);;
}

28
src/storm/logic/ExpectedTimeToExpectedRewardVisitor.cpp
View File

@ -0,0 +1,28 @@
#include "storm/logic/ExpectedTimeToExpectedRewardVisitor.h"
#include "storm/logic/Formulas.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidPropertyException.h"
namespace storm {
namespace logic {
ExpectedTimeToExpectedRewardVisitor::ExpectedTimeToExpectedRewardVisitor(std::string const& timeRewardModelName) : timeRewardModelName(timeRewardModelName) {
// Intentionally left empty
}
std::shared_ptr<Formula> ExpectedTimeToExpectedRewardVisitor::substitute(Formula const& f) const {
boost::any result = f.accept(*this, boost::any());
return boost::any_cast<std::shared_ptr<Formula>>(result);
}
boost::any ExpectedTimeToExpectedRewardVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
STORM_LOG_THROW(f.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected eventually formula within time operator. Got " << f << " instead.");
std::shared_ptr<Formula> subsubformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
STORM_LOG_THROW(f.getSubformula().isReachabilityTimeFormula(), storm::exceptions::InvalidPropertyException, "Expected time path formula within time operator. Got " << f << " instead.");
std::shared_ptr<Formula> subformula = std::make_shared<EventuallyFormula>(subsubformula, storm::logic::FormulaContext::Reward);
return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, timeRewardModelName, f.getOperatorInformation()));
}
}
}

25
src/storm/logic/ExpectedTimeToExpectedRewardVisitor.h
View File

@ -0,0 +1,25 @@
#pragma once
#include <map>
#include "storm/logic/CloneVisitor.h"
#include "storm/storage/expressions/Expression.h"
namespace storm {
namespace logic {
class ExpectedTimeToExpectedRewardVisitor : public CloneVisitor {
public:
ExpectedTimeToExpectedRewardVisitor(std::string const& timeRewardModelName);
std::shared_ptr<Formula> substitute(Formula const& f) const;
virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
private:
std::string const& timeRewardModelName;
};
}
}

2
src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
View File

@ -998,6 +998,8 @@ namespace storm {
// Check quotient matrix for sanity.
if (std::is_same<ValueType, storm::RationalNumber>::value) {
STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>()).isZero(), "Illegal entries in quotient matrix.");
} else if (std::is_same<ValueType, storm::RationalFunction>::value) {
// No comparison for rational functions
} else {
STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>() + storm::utility::convertNumber<ValueType>(1e-6)).isZero(), "Illegal entries in quotient matrix.");
}

19
src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp
View File

@ -5,7 +5,7 @@
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/logic/Formulas.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/logic/CloneVisitor.h"
#include "storm/logic/ExpectedTimeToExpectedRewardVisitor.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
@ -93,7 +93,22 @@ namespace storm {
fragment.setReachabilityRewardFormulasAllowed(true);
return formula.isInFragment(fragment);
}
template <typename ValueType, typename RewardModelType>
std::vector<std::shared_ptr<storm::logic::Formula const>> ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::checkAndTransformFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& timeRewardName) {
std::vector<std::shared_ptr<storm::logic::Formula const>> result;
storm::logic::ExpectedTimeToExpectedRewardVisitor v(timeRewardName);
for (auto const& f : formulas) {
// Translate expected time formulas
auto newF = v.substitute(*f);
if(preservesFormula(*newF)) {
result.push_back(newF);
} else {
STORM_LOG_INFO("Continuous to discrete time transformation does not preserve formula " << *f);
}
}
return result;
}
template <typename ValueType, typename RewardModelType>
std::shared_ptr<storm::models::sparse::Mdp<ValueType, RewardModelType>> ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::transform(storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType> const& ma, boost::optional<std::string> const& timeRewardModelName) {

10
src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h
View File

@ -16,9 +16,15 @@ namespace storm {
class ContinuousToDiscreteTimeModelTransformer {
public:
// If this method returns true, the given formula is preserced by the transformation
// If this method returns true, the given formula is preserved by the transformation
static bool preservesFormula(storm::logic::Formula const& formula);
// Checks whether the given formulas are preserved.
// Expected time formulas are translated to expected reward formulas.
// The returned vector only contains formulas that are preserved by the transformation.
static std::vector<std::shared_ptr<storm::logic::Formula const>> checkAndTransformFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& timeRewardName);
// Transforms the given CTMC to its underlying (aka embedded) DTMC.
// A reward model for time is added if a corresponding reward model name is given
static std::shared_ptr<storm::models::sparse::Dtmc<ValueType, RewardModelType>> transform(storm::models::sparse::Ctmc<ValueType, RewardModelType> const& ctmc, boost::optional<std::string> const& timeRewardModelName = boost::none);

Write Preview
Loading…
Cancel
Save