From ed3fa3f82b7d252e3629a3c13855aa1cf94a619e Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Thu, 17 Oct 2019 11:14:31 +0200 Subject: [PATCH] Fix TODOs --- src/storm-pars-cli/storm-pars.cpp | 110 +++++++++--------- src/storm-pars/analysis/AssumptionChecker.cpp | 2 - .../analysis/MonotonicityChecker.cpp | 5 - src/storm-pars/analysis/OrderExtender.cpp | 29 ----- src/storm-pars/api/region.h | 30 ----- 5 files changed, 58 insertions(+), 118 deletions(-) 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>(); - auto matrix = sparseModel->getTransitionMatrix(); - auto backwardsTransitionMatrix = matrix.transpose(); - - storm::storage::StronglyConnectedComponentDecompositionOptions const options; - auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(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 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>(); + auto matrix = sparseModel->getTransitionMatrix(); + auto backwardsTransitionMatrix = matrix.transpose(); + + storm::storage::StronglyConnectedComponentDecompositionOptions const options; + auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(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 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 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); + } + for (auto state : selfLoopStates) { + auto row = flexibleMatrix.getRow(state); + stateEliminator.eliminateLoop(state); } + selectedStates.complement(); + auto keptRows = matrix.getRowFilter(selectedStates); + storm::storage::SparseMatrix newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates); + // TODO: note that rewards get lost + model = std::make_shared>(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 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); - } - for (auto state : selfLoopStates) { - auto row = flexibleMatrix.getRow(state); - stateEliminator.eliminateLoop(state); - } - selectedStates.complement(); - auto keptRows = matrix.getRowFilter(selectedStates); - storm::storage::SparseMatrix newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates); - // TODO: rewards get lost - model = std::make_shared>(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> regions = parseRegions(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(); - // 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 minValues = minRes.getValueVector(); std::vector maxValues = maxRes.getValueVector(); - // TODO: zijn de value vectors nu precies omgedraaid? - // Create initial order std::tuple criticalTuple = extender->toOrder(formulas, minValues, maxValues); -// std::tuple criticalTuple = extender->toOrder(formulas); - - // Continue based on not (yet) sorted states std::map>> 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 std::tuple OrderExtender::toOrder(std::vector> formulas, std::vector minValues, std::vector 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> 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 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 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 - std::shared_ptr, ConstantType>> initializeParameterLiftingDtmcModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask 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> 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> 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, ConstantType>> checker; - if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) { - checker = std::make_shared, 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 std::shared_ptr> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) {