From 48cba66d96f7e2fa3573693888e80c76fbf66a6e Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Thu, 31 Jan 2019 13:10:51 +0100 Subject: [PATCH] Add scc elimination --- src/storm-pars-cli/storm-pars.cpp | 67 ++++++++++++++++++- src/storm-pars/analysis/LatticeExtender.cpp | 1 + .../analysis/MonotonicityChecker.cpp | 3 +- src/storm-pars/analysis/MonotonicityChecker.h | 4 +- .../settings/modules/ParametricSettings.cpp | 6 ++ .../settings/modules/ParametricSettings.h | 3 + 6 files changed, 79 insertions(+), 5 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 572562302..60fda624b 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -29,7 +29,7 @@ #include "storm/settings/SettingsManager.h" -#include "storm/solver/stateelimination/PrioritizedStateEliminator.h" +#include "storm/solver/stateelimination/NondeterministicModelStateEliminator.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/storage/SymbolicModelDescription.h" @@ -562,6 +562,67 @@ namespace storm { } } + if (parSettings.isSccEliminationSet()) { + // TODO: check for correct Model type + std::cout << "Applying scc elimination" << std::endl; + auto sparseModel = model->as>(); + auto matrix = sparseModel->getTransitionMatrix(); + auto backwardsTransitionMatrix = matrix.transpose(); + + auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, false, false); + + storm::storage::BitVector selectedStates(matrix.getRowCount()); + for (auto i = 0; i < decomposition.size(); ++i) { + auto scc = decomposition.getBlock(i); + if (scc.size() > 1) { + auto nrInitial = 0; + auto statesScc = scc.getStates(); + std::vector entryStates; + for (auto state : statesScc) { + auto row = backwardsTransitionMatrix.getRow(state); + bool found = false; + for (auto backState : row) { + if (!scc.containsState(backState.getColumn())) { + found = true; + } + } + if (found) { + entryStates.push_back(state); + } else { + selectedStates.set(state); + } + } + + if (entryStates.size() != 1) { + STORM_LOG_THROW(entryStates.size() > 1, storm::exceptions::NotImplementedException, + "state elimination not implemented for scc with more than 1 entry points"); + } + } + } + + storm::storage::FlexibleSparseMatrix flexibleMatrix(matrix); + storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardsTransitionMatrix, true); + auto actionRewards = std::vector(matrix.getRowCount(), storm::utility::zero()); + storm::solver::stateelimination::NondeterministicModelStateEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions, actionRewards); + for(auto state : selectedStates) { + stateEliminator.eliminateState(state, true); + } + selectedStates.complement(); + auto keptRows = matrix.getRowFilter(selectedStates); + storm::storage::SparseMatrix newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates); + // TODO: rewards get lost + // obtain the reward model for the resulting system +// std::unordered_map rewardModels; +// if(rewardModelName) { +// storm::utility::vector::filterVectorInPlace(actionRewards, keptRows); +// rewardModels.insert(std::make_pair(*rewardModelName, RewardModelType(boost::none, std::move(actionRewards)))); +// } + model = std::make_shared>(std::move(newTransitionMatrix), sparseModel->getStateLabeling().getSubLabeling(selectedStates)); + + + std::cout << "SCC Elimination applied" << std::endl; + } + if (parSettings.isMonotonicityAnalysisSet()) { std::cout << "Hello, Jip2" << std::endl; @@ -571,7 +632,7 @@ namespace storm { std::ofstream outfile; outfile.open("results.txt", std::ios_base::app); storm::utility::Stopwatch monotonicityWatch(true); - auto monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, parSettings.isValidateAssumptionsSet()); + auto monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, parSettings.isValidateAssumptionsSet(), parSettings.isSccEliminationSet()); monotonicityChecker.checkMonotonicity(); monotonicityWatch.stop(); STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl @@ -581,7 +642,7 @@ namespace storm { outfile.close(); std::cout << "Bye, Jip2" << std::endl; - return; +// return; } std::vector> regions = parseRegions(model); diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index 639ec0e20..97f4ce9c9 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -70,6 +70,7 @@ namespace storm { auto initialMiddleStates = storm::storage::BitVector(numberOfStates); // Check if MC contains cycles + // TODO maybe move to other place auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(model->getTransitionMatrix(), false, false); acyclic = true; for (auto i = 0; acyclic && i < decomposition.size(); ++i) { diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 8f1a4efa0..21ae0057e 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -30,11 +30,12 @@ namespace storm { namespace analysis { template - MonotonicityChecker::MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate) { + MonotonicityChecker::MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate, bool sccElimination) { outfile.open(filename, std::ios_base::app); this->model = model; this->formulas = formulas; this->validate = validate; + this->sccElimination = sccElimination; this->resultCheckOnSamples = std::map>(); if (model != nullptr) { std::shared_ptr> sparseModel = model->as>(); diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index b4b6db84c..f40f301bb 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -26,7 +26,7 @@ namespace storm { class MonotonicityChecker { public: - MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate); + MonotonicityChecker(std::shared_ptr model, std::vector> formulas, bool validate, bool sccElimination); /*! * Checks for all lattices in the map if they are monotone increasing or monotone decreasing. * @@ -71,6 +71,8 @@ namespace storm { std::vector> formulas; bool validate; + + bool sccElimination; std::map> resultCheckOnSamples; diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp index 8c1be78d4..967d83ef8 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.cpp +++ b/src/storm-pars/settings/modules/ParametricSettings.cpp @@ -22,6 +22,7 @@ namespace storm { const std::string ParametricSettings::samplesGraphPreservingOptionName = "samples-graph-preserving"; const std::string ParametricSettings::sampleExactOptionName = "sample-exact"; const std::string ParametricSettings::monotonicityAnalysis = "monotonicity-analysis"; + const std::string ParametricSettings::sccElimination = "elim-scc"; const std::string ParametricSettings::validateAssumptions = "validate-assumptions"; ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) { @@ -35,6 +36,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, samplesGraphPreservingOptionName, false, "Sets whether it can be assumed that the samples are graph-preserving.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, sampleExactOptionName, false, "Sets whether to sample using exact arithmetic.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, monotonicityAnalysis, false, "Sets whether monotonicity analysis is done").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, sccElimination, false, "Sets whether SCCs should be eliminated").build()); this->addOption(storm::settings::OptionBuilder(moduleName, validateAssumptions, false, "Sets whether assumptions made in monotonicity analysis are validated").build()); } @@ -74,6 +76,10 @@ namespace storm { return this->getOption(monotonicityAnalysis).getHasOptionBeenSet(); } + bool ParametricSettings::isSccEliminationSet() const { + return this->getOption(sccElimination).getHasOptionBeenSet(); + } + bool ParametricSettings::isValidateAssumptionsSet() const { return this->getOption(validateAssumptions).getHasOptionBeenSet(); } diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h index 2fc386471..29cbb81bf 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.h +++ b/src/storm-pars/settings/modules/ParametricSettings.h @@ -65,6 +65,8 @@ namespace storm { bool isSampleExactSet() const; bool isMonotonicityAnalysisSet() const; + // TODO: maybe move to other place + bool isSccEliminationSet() const; bool isValidateAssumptionsSet() const; @@ -80,6 +82,7 @@ namespace storm { const static std::string samplesGraphPreservingOptionName; const static std::string sampleExactOptionName; const static std::string monotonicityAnalysis; + const static std::string sccElimination; const static std::string validateAssumptions; };