Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add --not-graph-preserving flag #588

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Add --not-graph-preserving flag #588

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f739523
Add --not-graph-preserving flag
glatteis Aug 1, 2024
b3aebb6
Preserve reward models in graph-preserving bisim
glatteis Aug 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/storm-cli-utilities/model-handling.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -572,14 +572,14 @@ std::shared_ptr<storm::models::sparse::Model<ValueType>> preprocessSparseMarkovA
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> preprocessSparseModelBisimulation(
std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input,
storm::settings::modules::BisimulationSettings const& bisimulationSettings) {
storm::settings::modules::BisimulationSettings const& bisimulationSettings, bool graphPreserving = true) {
storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
if (bisimulationSettings.isWeakBisimulationSet()) {
bisimType = storm::storage::BisimulationType::Weak;
}

STORM_LOG_INFO("Performing bisimulation minimization...");
return storm::api::performBisimulationMinimization<ValueType>(model, createFormulasToRespect(input.properties), bisimType);
return storm::api::performBisimulationMinimization<ValueType>(model, createFormulasToRespect(input.properties), bisimType, graphPreserving);
}

template<typename ValueType>
Expand Down
20 changes: 18 additions & 2 deletions src/storm-pars-cli/storm-pars.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,19 @@ std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::shared
} else if (regionSettings.isRegionBoundSet()) {
result = storm::api::createRegion<ValueType>(regionSettings.getRegionBoundString(), *model);
}
if (!regionSettings.isNotGraphPreservingSet()) {
for (auto const& region : result) {
for (auto const& variable : region.getVariables()) {
if (region.getLowerBoundary(variable) <= storm::utility::zero<typename storm::utility::parametric::CoefficientType<ValueType>::type>() ||
region.getUpperBoundary(variable) >= storm::utility::one<typename storm::utility::parametric::CoefficientType<ValueType>::type>()) {
STORM_LOG_WARN(
"Region" << region
<< " appears to not preserve the graph structure of the parametric model. If this is the case, --not-graph-preserving.");
break;
}
}
}
}
return result;
}

Expand Down Expand Up @@ -202,6 +215,7 @@ PreprocessResult preprocessSparseModel(std::shared_ptr<storm::models::sparse::Mo
auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
auto monSettings = storm::settings::getModule<storm::settings::modules::MonotonicitySettings>();
auto regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();

PreprocessResult result(model, false);
// TODO: why only simplify in these modes
Expand All @@ -218,8 +232,8 @@ PreprocessResult preprocessSparseModel(std::shared_ptr<storm::models::sparse::Mo
}

if (mpi.applyBisimulation) {
result.model =
storm::cli::preprocessSparseModelBisimulation(result.model->template as<storm::models::sparse::Model<ValueType>>(), input, bisimulationSettings);
result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as<storm::models::sparse::Model<ValueType>>(), input,
bisimulationSettings, !regionSettings.isNotGraphPreservingSet());
result.changed = true;
}

Expand Down Expand Up @@ -394,6 +408,7 @@ void processInputWithValueTypeAndDdlib(cli::SymbolicInput& input, storm::cli::Mo
auto parSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
auto monSettings = storm::settings::getModule<storm::settings::modules::MonotonicitySettings>();
auto sampleSettings = storm::settings::getModule<storm::settings::modules::SamplingSettings>();
auto regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();

STORM_LOG_THROW(mpi.engine == storm::utility::Engine::Sparse || mpi.engine == storm::utility::Engine::Hybrid || mpi.engine == storm::utility::Engine::Dd,
storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models.");
Expand Down Expand Up @@ -457,6 +472,7 @@ void processInputWithValueTypeAndDdlib(cli::SymbolicInput& input, storm::cli::Mo
STORM_LOG_INFO("Solution function mode started.");
STORM_LOG_THROW(regions.empty(), storm::exceptions::InvalidSettingsException,
"Solution function computations cannot be restricted to specific regions");
STORM_LOG_ERROR_COND(!regionSettings.isNotGraphPreservingSet(), "Solution function computations assume graph preservation.");

if (model->isSparseModel()) {
computeSolutionFunctionsWithSparseEngine(model->as<storm::models::sparse::Model<ValueType>>(), input);
Expand Down
9 changes: 9 additions & 0 deletions src/storm-pars/settings/modules/RegionSettings.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ const std::string RegionSettings::moduleName = "region";
const std::string regionOptionName = "region";
const std::string regionShortOptionName = "reg";
const std::string regionBoundOptionName = "regionbound";
const std::string notGraphPreservingName = "not-graph-preserving";

RegionSettings::RegionSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, regionOptionName, false, "Sets the region(s) considered for analysis.")
Expand All @@ -28,6 +29,10 @@ RegionSettings::RegionSettings() : ModuleSettings(moduleName) {
"regionbound", "The bound for the region result for all variables: 0+bound <= var <=1-bound")
.build())
.build());

this->addOption(storm::settings::OptionBuilder(moduleName, notGraphPreservingName, false,
"Enables mode in which the region might not preserve the graph structure of the parametric model.")
.build());
}

bool RegionSettings::isRegionSet() const {
Expand All @@ -46,6 +51,10 @@ std::string RegionSettings::getRegionBoundString() const {
return this->getOption(regionBoundOptionName).getArgumentByName("regionbound").getValueAsString();
}

bool RegionSettings::isNotGraphPreservingSet() const {
return this->getOption(notGraphPreservingName).getHasOptionBeenSet();
}

} // namespace modules
} // namespace settings
} // namespace storm
5 changes: 5 additions & 0 deletions src/storm-pars/settings/modules/RegionSettings.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,11 @@ class RegionSettings : public ModuleSettings {
*/
std::string getRegionBoundString() const;

/*!
* Retrieves whether non-graph-preserving mode is enabled
*/
bool isNotGraphPreservingSet() const;

const static std::string moduleName;
};

Expand Down
31 changes: 23 additions & 8 deletions src/storm/api/bisimulation.h
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
#pragma once

#include <any>
#include "storm/models/sparse/Ctmc.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
Expand All @@ -19,11 +20,18 @@ namespace api {
template<typename ModelType>
std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model,
std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
storm::storage::BisimulationType type) {
storm::storage::BisimulationType type, bool graphPreserving = true) {
typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options options;
if (!formulas.empty()) {
if (!formulas.empty() && graphPreserving) {
options = typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas);
}
// If we cannot use formula-based decomposition because of
// non-graph-preserving regions but there are reward models, we need to
// preserve those
if (!graphPreserving &&
std::any_of(formulas.begin(), formulas.end(), [](auto const& formula) { return formula->getReferencedRewardModels().size() > 0; })) {
options.setKeepRewards(true);
}
options.setType(type);

storm::storage::DeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
Expand All @@ -34,11 +42,18 @@ std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(st
template<typename ModelType>
std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model,
std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
storm::storage::BisimulationType type) {
storm::storage::BisimulationType type, bool graphPreserving = true) {
typename storm::storage::NondeterministicModelBisimulationDecomposition<ModelType>::Options options;
if (!formulas.empty()) {
if (!formulas.empty() && graphPreserving) {
options = typename storm::storage::NondeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas);
}
// If we cannot use formula-based decomposition because of
// non-graph-preserving regions but there are reward models, we need to
// preserve those
if (!graphPreserving &&
std::any_of(formulas.begin(), formulas.end(), [](auto const& formula) { return formula->getReferencedRewardModels().size() > 0; })) {
options.setKeepRewards(true);
}
options.setType(type);

storm::storage::NondeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
Expand All @@ -49,7 +64,7 @@ std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulationMinimization(
std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
storm::storage::BisimulationType type = storm::storage::BisimulationType::Strong) {
storm::storage::BisimulationType type = storm::storage::BisimulationType::Strong, bool graphPreserving = true) {
STORM_LOG_THROW(
model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp),
storm::exceptions::NotSupportedException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs.");
Expand All @@ -59,13 +74,13 @@ std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulationMini

if (model->isOfType(storm::models::ModelType::Dtmc)) {
return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Dtmc<ValueType>>(
model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas, type);
model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas, type, graphPreserving);
} else if (model->isOfType(storm::models::ModelType::Ctmc)) {
return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(
model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, type);
model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, type, graphPreserving);
} else {
return performNondeterministicSparseBisimulationMinimization<storm::models::sparse::Mdp<ValueType>>(
model->template as<storm::models::sparse::Mdp<ValueType>>(), formulas, type);
model->template as<storm::models::sparse::Mdp<ValueType>>(), formulas, type, graphPreserving);
}
}

Expand Down
4 changes: 4 additions & 0 deletions src/storm/storage/bisimulation/BisimulationDecomposition.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,10 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
return this->keepRewards;
}

void setKeepRewards(bool keepRewards) {
this->keepRewards = keepRewards;
}

bool isOptimizationDirectionSet() const {
return static_cast<bool>(optimalityType);
}
Expand Down
Loading