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<storm::models::sparse::Model<ValueType>>();
+ auto matrix = sparseModel->getTransitionMatrix();
+ auto backwardsTransitionMatrix = matrix.transpose();
+
+ auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(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<uint_fast64_t> 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<ValueType> flexibleMatrix(matrix);
+ storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(backwardsTransitionMatrix, true);
+ auto actionRewards = std::vector<ValueType>(matrix.getRowCount(), storm::utility::zero<ValueType>());
+ storm::solver::stateelimination::NondeterministicModelStateEliminator<ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, actionRewards);
+ for(auto state : selectedStates) {
+ stateEliminator.eliminateState(state, true);
+ }
+ selectedStates.complement();
+ auto keptRows = matrix.getRowFilter(selectedStates);
+ storm::storage::SparseMatrix<ValueType> newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates);
+ // TODO: rewards get lost
+ // obtain the reward model for the resulting system
+// std::unordered_map<std::string, RewardModelType> 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<storm::models::sparse::Dtmc<ValueType>>(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<ValueType>(model, formulas, parSettings.isValidateAssumptionsSet());
+ auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>(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<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(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<ValueType>(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 <typename ValueType>
- MonotonicityChecker<ValueType>::MonotonicityChecker(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, bool validate) {
+ MonotonicityChecker<ValueType>::MonotonicityChecker(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> 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<carl::Variable, std::pair<bool, bool>>();
if (model != nullptr) {
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
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<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, bool validate);
+ MonotonicityChecker(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> 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<std::shared_ptr<storm::logic::Formula const>> formulas;
bool validate;
+
+ bool sccElimination;
std::map<carl::Variable, std::pair<bool, bool>> 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;
};