diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 79c2284f2..c2679770d 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -668,66 +668,72 @@ namespace storm {
if (model && monSettings.isSccEliminationSet()) {
storm::utility::Stopwatch eliminationWatch(true);
- // TODO: check for correct Model type
- STORM_PRINT("Applying scc elimination" << std::endl);
- auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
- auto matrix = sparseModel->getTransitionMatrix();
- auto backwardsTransitionMatrix = matrix.transpose();
-
- storm::storage::StronglyConnectedComponentDecompositionOptions const options;
- auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(matrix, options);
-
- storm::storage::BitVector selectedStates(matrix.getRowCount());
- storm::storage::BitVector selfLoopStates(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 (model->isOfType(storm::models::ModelType::Dtmc)) {
+ STORM_PRINT("Applying scc elimination" << std::endl);
+ auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
+ auto matrix = sparseModel->getTransitionMatrix();
+ auto backwardsTransitionMatrix = matrix.transpose();
+
+ storm::storage::StronglyConnectedComponentDecompositionOptions const options;
+ auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(matrix, options);
+
+ storm::storage::BitVector selectedStates(matrix.getRowCount());
+ storm::storage::BitVector selfLoopStates(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);
+ selfLoopStates.set(state);
+ } else {
+ selectedStates.set(state);
}
}
- if (found) {
- entryStates.push_back(state);
- selfLoopStates.set(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");
}
}
+ }
- 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);
+ }
+ for (auto state : selfLoopStates) {
+ auto row = flexibleMatrix.getRow(state);
+ stateEliminator.eliminateLoop(state);
}
+ selectedStates.complement();
+ auto keptRows = matrix.getRowFilter(selectedStates);
+ storm::storage::SparseMatrix<ValueType> newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates);
+ // TODO: note that rewards get lost
+ model = std::make_shared<storm::models::sparse::Dtmc<ValueType>>(std::move(newTransitionMatrix), sparseModel->getStateLabeling().getSubLabeling(selectedStates));
+
+ eliminationWatch.stop();
+ STORM_PRINT(std::endl << "Time for scc elimination: " << eliminationWatch << "." << std::endl << std::endl);
+ model->printModelInformationToStream(std::cout);
+ } else if (model->isOfType(storm::models::ModelType::Mdp)) {
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Unable to perform SCC elimination for monotonicity analysis on MDP: Not mplemented");
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type.");
}
- 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);
- }
- for (auto state : selfLoopStates) {
- auto row = flexibleMatrix.getRow(state);
- stateEliminator.eliminateLoop(state);
- }
- selectedStates.complement();
- auto keptRows = matrix.getRowFilter(selectedStates);
- storm::storage::SparseMatrix<ValueType> newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates);
- // TODO: rewards get lost
- model = std::make_shared<storm::models::sparse::Dtmc<ValueType>>(std::move(newTransitionMatrix), sparseModel->getStateLabeling().getSubLabeling(selectedStates));
-
- eliminationWatch.stop();
- STORM_PRINT(std::endl << "Time for scc elimination: " << eliminationWatch << "." << std::endl << std::endl);
- model->printModelInformationToStream(std::cout);
}
std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);
diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp
index 43d0e75e4..e90b8e913 100644
--- a/src/storm-pars/analysis/AssumptionChecker.cpp
+++ b/src/storm-pars/analysis/AssumptionChecker.cpp
@@ -32,9 +32,7 @@ namespace storm {
for (auto i = 0; i < numberOfSamples; ++i) {
auto valuation = utility::parametric::Valuation<ValueType>();
- // TODO: samplen over de region
for (auto var: variables) {
-
auto lb = region.getLowerBoundary(var.name());
auto ub = region.getUpperBoundary(var.name());
// Creates samples between lb and ub, that is: lb, lb + (ub-lb)/(#samples -1), lb + 2* (ub-lb)/(#samples -1), ..., ub
diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp
index 8687a0566..62bbc02e2 100644
--- a/src/storm-pars/analysis/MonotonicityChecker.cpp
+++ b/src/storm-pars/analysis/MonotonicityChecker.cpp
@@ -194,13 +194,8 @@ namespace storm {
std::vector<double> minValues = minRes.getValueVector();
std::vector<double> maxValues = maxRes.getValueVector();
- // TODO: zijn de value vectors nu precies omgedraaid?
-
// Create initial order
std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toOrder(formulas, minValues, maxValues);
-// std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toOrder(formulas);
-
-
// Continue based on not (yet) sorted states
std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
diff --git a/src/storm-pars/analysis/OrderExtender.cpp b/src/storm-pars/analysis/OrderExtender.cpp
index 991f88f35..d9f109777 100644
--- a/src/storm-pars/analysis/OrderExtender.cpp
+++ b/src/storm-pars/analysis/OrderExtender.cpp
@@ -38,10 +38,8 @@ namespace storm {
uint_fast64_t numberOfStates = this->model->getNumberOfStates();
// Build stateMap
- // TODO: is dit wel nodig
for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
stateMap[i] = new storm::storage::BitVector(numberOfStates, false);
-
auto row = matrix.getRow(i);
for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) {
// ignore self-loops when there are more transitions
@@ -129,33 +127,6 @@ namespace storm {
template <typename ValueType>
std::tuple<Order*, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::toOrder(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, std::vector<double> minValues, std::vector<double> maxValues) {
uint_fast64_t numberOfStates = this->model->getNumberOfStates();
-//
-// // Compare min/max for all states
-// STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis");
-// STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula()
-// && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()
-// || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until or eventually formula");
-//
-// // TODO: dit moet anders kunnen
-// storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*model);
-// storm::storage::BitVector phiStates;
-// storm::storage::BitVector psiStates;
-// if ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()) {
-// phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
-// psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
-// } else {
-// phiStates = storm::storage::BitVector(numberOfStates, true);
-// psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
-// }
-//
-// // Get the maybeStates
-// std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->model->getBackwardTransitions(), phiStates, psiStates);
-// storm::storage::BitVector topStates = statesWithProbability01.second;
-// storm::storage::BitVector bottomStates = statesWithProbability01.first;
-//
-// STORM_LOG_THROW(topStates.begin() != topStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no 1 states");
-// STORM_LOG_THROW(bottomStates.begin() != bottomStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no zero states");
-//
uint_fast64_t bottom = numberOfStates;
uint_fast64_t top = numberOfStates;
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(matrix);
diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h
index f0315f45d..0ee310b39 100644
--- a/src/storm-pars/api/region.h
+++ b/src/storm-pars/api/region.h
@@ -110,36 +110,6 @@ namespace storm {
return checker;
}
- // TODO: make more generic
- template <typename ParametricType, typename ConstantType>
- std::shared_ptr<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>> initializeParameterLiftingDtmcModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) {
-
- STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
-
- std::shared_ptr<storm::models::sparse::Model<ParametricType>> consideredModel = model;
-
- // Treat continuous time models
- 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).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.");
- }
-
- // Obtain the region model checker
- std::shared_ptr<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>> checker;
- if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) {
- checker = std::make_shared<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>>();
- } else {
- STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
- }
-
- checker->specify(env, consideredModel, task, generateSplitEstimates, allowModelSimplification);
-
- return checker;
- }
-
-
template <typename ParametricType, typename ImpreciseType, typename PreciseType>
std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) {