From 197c242bb16006cf7f2bb45e31a55ff61c86adb3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 8 Feb 2015 13:40:32 +0100 Subject: [PATCH 1/5] Some minor changes. Former-commit-id: 4ba2abac632aad498ccae9bbb548524a54672f05 --- .../SparseDtmcEliminationModelChecker.cpp | 72 +++++++++---------- src/settings/modules/ParametricSettings.cpp | 7 ++ src/settings/modules/ParametricSettings.h | 8 +++ src/stormParametric.cpp | 19 +++++ 4 files changed, 70 insertions(+), 36 deletions(-) diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index d21a154da..5bee46f8b 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -231,18 +231,18 @@ namespace storm { storm::storage::BitVector statesReachingPhi = storm::utility::graph::performProbGreater0(backwardTransitions, trueStates, phiStates); // The set of states we need to consider are those that have a non-zero probability to satisfy the condition or are on some path that has a psi state in it. - STORM_LOG_DEBUG("Initial state: " << model.getInitialStates()); - STORM_LOG_DEBUG("Phi states: " << phiStates); - STORM_LOG_DEBUG("Psi state: " << psiStates); - STORM_LOG_DEBUG("States with probability greater 0 of satisfying the condition: " << statesWithProbabilityGreater0); - STORM_LOG_DEBUG("States with psi predecessor: " << statesWithPsiPredecessor); - STORM_LOG_DEBUG("States reaching phi: " << statesReachingPhi); + STORM_LOG_TRACE("Initial state: " << model.getInitialStates()); + STORM_LOG_TRACE("Phi states: " << phiStates); + STORM_LOG_TRACE("Psi state: " << psiStates); + STORM_LOG_TRACE("States with probability greater 0 of satisfying the condition: " << statesWithProbabilityGreater0); + STORM_LOG_TRACE("States with psi predecessor: " << statesWithPsiPredecessor); + STORM_LOG_TRACE("States reaching phi: " << statesReachingPhi); storm::storage::BitVector maybeStates = statesWithProbabilityGreater0 | (statesWithPsiPredecessor & statesReachingPhi); - STORM_LOG_DEBUG("Found " << maybeStates.getNumberOfSetBits() << " relevant states: " << maybeStates); + STORM_LOG_TRACE("Found " << maybeStates.getNumberOfSetBits() << " relevant states: " << maybeStates); // Determine the set of initial states of the sub-DTMC. storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates; - STORM_LOG_DEBUG("Found new initial states: " << newInitialStates << " (old: " << model.getInitialStates() << ")"); + STORM_LOG_TRACE("Found new initial states: " << newInitialStates << " (old: " << model.getInitialStates() << ")"); // Create a dummy vector for the one-step probabilities. std::vector oneStepProbabilities(maybeStates.getNumberOfSetBits(), storm::utility::zero()); @@ -264,10 +264,10 @@ namespace storm { // Keep only the states that we do not eliminate in the maybe states. maybeStates = phiStates | psiStates; - STORM_LOG_DEBUG("Phi states in reduced model " << phiStates); - STORM_LOG_DEBUG("Psi states in reduced model " << psiStates); + STORM_LOG_TRACE("Phi states in reduced model " << phiStates); + STORM_LOG_TRACE("Psi states in reduced model " << psiStates); storm::storage::BitVector statesToEliminate = ~maybeStates & ~newInitialStates; - STORM_LOG_DEBUG("Eliminating the states " << statesToEliminate); + STORM_LOG_TRACE("Eliminating the states " << statesToEliminate); // Before starting the model checking process, we assign priorities to states so we can use them to // impose ordering constraints later. @@ -301,10 +301,10 @@ namespace storm { for (auto const& trans1 : flexibleMatrix.getRow(*newInitialStates.begin())) { auto initialStateSuccessor = trans1.getColumn(); - STORM_LOG_DEBUG("Exploring successor " << initialStateSuccessor << " of the initial state."); + STORM_LOG_TRACE("Exploring successor " << initialStateSuccessor << " of the initial state."); if (phiStates.get(initialStateSuccessor)) { - STORM_LOG_DEBUG("Is a phi state."); + STORM_LOG_TRACE("Is a phi state."); // If the state is both a phi and a psi state, we do not need to eliminate chains. if (psiStates.get(initialStateSuccessor)) { @@ -327,7 +327,7 @@ namespace storm { typename FlexibleSparseMatrix::row_type const& successorRow = flexibleMatrix.getRow(element.getColumn()); // Eliminate the successor only if there possibly is a psi state reachable through it. if (successorRow.size() > 1 || (!successorRow.empty() && successorRow.front().getColumn() != element.getColumn())) { - STORM_LOG_DEBUG("Found non-psi successor " << element.getColumn() << " that needs to be eliminated."); + STORM_LOG_TRACE("Found non-psi successor " << element.getColumn() << " that needs to be eliminated."); eliminateState(flexibleMatrix, oneStepProbabilities, element.getColumn(), flexibleBackwardTransitions, missingStateRewards, false, true, phiStates); hasNonPsiSuccessor = true; } @@ -338,7 +338,7 @@ namespace storm { } } else { STORM_LOG_ASSERT(psiStates.get(initialStateSuccessor), "Expected psi state."); - STORM_LOG_DEBUG("Is a psi state."); + STORM_LOG_TRACE("Is a psi state."); // At this point, we know that the state satisfies psi and not phi. // This means, we must compute the probability to reach phi states, which in turn means that we need @@ -356,7 +356,7 @@ namespace storm { if (!phiStates.get(element.getColumn())) { typename FlexibleSparseMatrix::row_type const& successorRow = flexibleMatrix.getRow(element.getColumn()); if (successorRow.size() > 1 || (!successorRow.empty() && successorRow.front().getColumn() != element.getColumn())) { - STORM_LOG_DEBUG("Found non-phi successor " << element.getColumn() << " that needs to be eliminated."); + STORM_LOG_TRACE("Found non-phi successor " << element.getColumn() << " that needs to be eliminated."); eliminateState(flexibleMatrix, oneStepProbabilities, element.getColumn(), flexibleBackwardTransitions, missingStateRewards, false, true, psiStates); hasNonPhiSuccessor = true; } @@ -464,15 +464,15 @@ namespace storm { std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; }); } - STORM_LOG_INFO("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); + STORM_LOG_DEBUG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); for (auto const& state : states) { eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); } - STORM_LOG_INFO("Eliminated " << states.size() << " states." << std::endl); + STORM_LOG_DEBUG("Eliminated " << states.size() << " states." << std::endl); } else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) { // When using the hybrid technique, we recursively treat the SCCs up to some size. std::vector entryStateQueue; - STORM_LOG_INFO("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); + STORM_LOG_DEBUG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::sparseDtmcEliminationModelCheckerSettings().getMaximalSccSize(), entryStateQueue, stateRewards, statePriorities); // If the entry states were to be eliminated last, we need to do so now. @@ -482,7 +482,7 @@ namespace storm { eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); } } - STORM_LOG_INFO("Eliminated " << subsystem.size() << " states." << std::endl); + STORM_LOG_DEBUG("Eliminated " << subsystem.size() << " states." << std::endl); } // Finally eliminate initial state. @@ -503,7 +503,7 @@ namespace storm { STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).front().getColumn() == *initialStates.begin(), "Remaining entry should be a self-loop, but it is not."); ValueType loopProbability = flexibleMatrix.getRow(*initialStates.begin()).front().getValue(); loopProbability = storm::utility::one() / (storm::utility::one() - loopProbability); - STORM_LOG_INFO("Scaling the reward of the initial state " << stateRewards.get()[(*initialStates.begin())] << " with " << loopProbability); + STORM_LOG_DEBUG("Scaling the reward of the initial state " << stateRewards.get()[(*initialStates.begin())] << " with " << loopProbability); stateRewards.get()[(*initialStates.begin())] *= loopProbability; flexibleMatrix.getRow(*initialStates.begin()).clear(); } @@ -596,11 +596,11 @@ namespace storm { // If the SCCs are large enough, we try to split them further. if (scc.getNumberOfSetBits() > maximalSccSize) { - STORM_LOG_DEBUG("SCC is large enough (" << scc.getNumberOfSetBits() << " states) to be decomposed further."); + STORM_LOG_TRACE("SCC is large enough (" << scc.getNumberOfSetBits() << " states) to be decomposed further."); // Here, we further decompose the SCC into sub-SCCs. storm::storage::StronglyConnectedComponentDecomposition decomposition(forwardTransitions, scc & ~entryStates, false, false); - STORM_LOG_DEBUG("Decomposed SCC into " << decomposition.size() << " sub-SCCs."); + STORM_LOG_TRACE("Decomposed SCC into " << decomposition.size() << " sub-SCCs."); // Store a bit vector of remaining SCCs so we can be flexible when it comes to the order in which // we eliminate the SCCs. @@ -621,15 +621,15 @@ namespace storm { std::sort(trivialSccs.begin(), trivialSccs.end(), [&statePriorities] (std::pair const& a, std::pair const& b) { return statePriorities.get()[a.first] < statePriorities.get()[b.first]; }); } - STORM_LOG_DEBUG("Eliminating " << trivialSccs.size() << " trivial SCCs."); + STORM_LOG_TRACE("Eliminating " << trivialSccs.size() << " trivial SCCs."); for (auto const& stateIndexPair : trivialSccs) { eliminateState(matrix, oneStepProbabilities, stateIndexPair.first, backwardTransitions, stateRewards); remainingSccs.set(stateIndexPair.second, false); } - STORM_LOG_DEBUG("Eliminated all trivial SCCs."); + STORM_LOG_TRACE("Eliminated all trivial SCCs."); // And then recursively treat the remaining sub-SCCs. - STORM_LOG_DEBUG("Eliminating " << remainingSccs.getNumberOfSetBits() << " remaining SCCs on level " << level << "."); + STORM_LOG_TRACE("Eliminating " << remainingSccs.getNumberOfSetBits() << " remaining SCCs on level " << level << "."); for (auto sccIndex : remainingSccs) { storm::storage::StronglyConnectedComponent const& newScc = decomposition.getBlock(sccIndex); @@ -653,7 +653,7 @@ namespace storm { } else { // In this case, we perform simple state elimination in the current SCC. - STORM_LOG_DEBUG("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly."); + STORM_LOG_TRACE("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly."); storm::storage::BitVector remainingStates = scc & ~entryStates; std::vector states(remainingStates.begin(), remainingStates.end()); @@ -669,16 +669,16 @@ namespace storm { eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards); } - STORM_LOG_DEBUG("Eliminated all states of SCC."); + STORM_LOG_TRACE("Eliminated all states of SCC."); } // Finally, eliminate the entry states (if we are required to do so). if (eliminateEntryStates) { - STORM_LOG_DEBUG("Finally, eliminating/adding entry states."); + STORM_LOG_TRACE("Finally, eliminating/adding entry states."); for (auto state : entryStates) { eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards); } - STORM_LOG_DEBUG("Eliminated/added entry states."); + STORM_LOG_TRACE("Eliminated/added entry states."); } else { for (auto state : entryStates) { entryStateQueue.push_back(state); @@ -698,7 +698,7 @@ namespace storm { auto eliminationStart = std::chrono::high_resolution_clock::now(); ++counter; - STORM_LOG_DEBUG("Eliminating state " << state << "."); + STORM_LOG_TRACE("Eliminating state " << state << "."); if (counter > matrix.getNumberOfRows() / 10) { ++chunkCounter; STORM_LOG_INFO("Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl); @@ -744,7 +744,7 @@ namespace storm { } } - STORM_LOG_DEBUG((hasSelfLoop ? "State has self-loop." : "State does not have a self-loop.")); + STORM_LOG_TRACE((hasSelfLoop ? "State has self-loop." : "State does not have a self-loop.")); // Now connect the predecessors of the state being eliminated with its successors. typename FlexibleSparseMatrix::row_type& currentStatePredecessors = backwardTransitions.getRow(state); @@ -767,10 +767,10 @@ namespace storm { // Skip the state if the elimination is constrained, but the predecessor is not in the constraint. if (constrained && !predecessorConstraint.get(predecessor)) { newCurrentStatePredecessors.emplace_back(predecessor, storm::utility::one()); - STORM_LOG_DEBUG("Not eliminating predecessor " << predecessor << ", because it does not fit the filter."); + STORM_LOG_TRACE("Not eliminating predecessor " << predecessor << ", because it does not fit the filter."); continue; } - STORM_LOG_DEBUG("Eliminating predecessor " << predecessor << "."); + STORM_LOG_TRACE("Eliminating predecessor " << predecessor << "."); // First, find the probability with which the predecessor can move to the current state, because // the other probabilities need to be scaled with this factor. @@ -834,7 +834,7 @@ namespace storm { if (!stateRewards) { // Add the probabilities to go to a target state in just one step if we have to compute probabilities. oneStepProbabilities[predecessor] += storm::utility::simplify(multiplyFactor * oneStepProbabilities[state]); - STORM_LOG_DEBUG("Fixed new next-state probabilities of predecessor states."); + STORM_LOG_TRACE("Fixed new next-state probabilities of predecessor states."); } else { // If we are computing rewards, we basically scale the state reward of the state to eliminate and // add the result to the state reward of the predecessor. @@ -914,7 +914,7 @@ namespace storm { // Now move the new predecessors in place. successorBackwardTransitions = std::move(newPredecessors); } - STORM_LOG_DEBUG("Fixed predecessor lists of successor states."); + STORM_LOG_TRACE("Fixed predecessor lists of successor states."); if (removeForwardTransitions) { // Clear the eliminated row to reduce memory consumption. diff --git a/src/settings/modules/ParametricSettings.cpp b/src/settings/modules/ParametricSettings.cpp index f2480e029..89a62a008 100644 --- a/src/settings/modules/ParametricSettings.cpp +++ b/src/settings/modules/ParametricSettings.cpp @@ -10,6 +10,7 @@ namespace storm { const std::string ParametricSettings::encodeSmt2StrategyOptionName = "smt2strategy"; const std::string ParametricSettings::exportSmt2DestinationPathOptionName = "smt2path"; const std::string ParametricSettings::exportResultDestinationPathOptionName = "resultfile"; + const std::string ParametricSettings::derivativesOptionName = "derivatives"; ParametricSettings::ParametricSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, encodeSmt2StrategyOptionName, true, "Set the smt2 encoding strategy.") @@ -18,6 +19,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportResultDestinationPathOptionName, true, "A path to a file where the smt2 encoding should be saved.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, derivativesOptionName, false, "Sets whether to generate the derivatives of the resulting rational function.").build()); } bool ParametricSettings::exportResultToFile() const { @@ -47,6 +49,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown smt2encoding strategy '" << strategy << "'."); } } + + bool ParametricSettings::isDerivativesSet() const { + return this->getOption(derivativesOptionName).getHasOptionBeenSet(); + } + } // namespace modules } // namespace settings } // namespace storm \ No newline at end of file diff --git a/src/settings/modules/ParametricSettings.h b/src/settings/modules/ParametricSettings.h index 3586e2d5f..28789c95f 100644 --- a/src/settings/modules/ParametricSettings.h +++ b/src/settings/modules/ParametricSettings.h @@ -58,6 +58,13 @@ namespace storm { * @return The encoding strategy to be used. */ Smt2EncodingStrategy smt2EncodingStrategy() const; + + /*! + * Retrieves whether or not derivatives of the resulting rational function are to be generated. + * + * @return True if the derivatives are to be generated. + */ + bool isDerivativesSet() const; const static std::string moduleName; @@ -65,6 +72,7 @@ namespace storm { const static std::string encodeSmt2StrategyOptionName; const static std::string exportSmt2DestinationPathOptionName; const static std::string exportResultDestinationPathOptionName; + const static std::string derivativesOptionName; }; } // namespace modules diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 09cfa47d5..40388cca6 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -208,6 +208,25 @@ void check() { printApproximateResult(valueFunction); } std::cout << std::endl; + + // Generate derivatives for sensitivity analysis if requested. + if (std::is_same::value && storm::settings::parametricSettings().isDerivativesSet()) { + ValueType function = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; + + auto allVariables = function.gatherVariables(); + + if (!allVariables.empty()) { + std::map derivatives; + for (auto const& variable : allVariables) { + derivatives[variable] = function.derivative(variable); + } + + std::cout << std::endl << "Derivatives (variable; derivative):" << std::endl; + for (auto const& variableDerivativePair : derivatives) { + std::cout << "(" << variableDerivativePair.first << "; " << variableDerivativePair.second << ")" << std::endl; + } + } + } } /*! From 43a1d0bc73ff4d1ce56d77281af7c1be1acd9da8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 8 Feb 2015 13:52:36 +0100 Subject: [PATCH 2/5] Added debug output. Former-commit-id: 20ee3ec777ff3491d1a8bc2eeae4a962351ce1ff --- .../reachability/SparseDtmcEliminationModelChecker.cpp | 1 + src/stormParametric.cpp | 8 ++++---- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 5bee46f8b..1a3e54ab2 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -538,6 +538,7 @@ namespace storm { } // Now, we return the value for the only initial state. + STORM_LOG_DEBUG("Simplifying and returning result."); if (stateRewards) { return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]); } else { diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 40388cca6..ade3e3451 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -197,10 +197,6 @@ void check() { std::unique_ptr result = modelchecker.check(*formula); ValueType valueFunction = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; - if (storm::settings::parametricSettings().exportResultToFile()) { - storm::utility::exportParametricMcResult(valueFunction, constraintCollector); - } - // Report the result. STORM_PRINT_AND_LOG(std::endl << "Result (initial state): "); result->writeToStream(std::cout, model->getInitialStates()); @@ -209,6 +205,10 @@ void check() { } std::cout << std::endl; + if (storm::settings::parametricSettings().exportResultToFile()) { + storm::utility::exportParametricMcResult(valueFunction, constraintCollector); + } + // Generate derivatives for sensitivity analysis if requested. if (std::is_same::value && storm::settings::parametricSettings().isDerivativesSet()) { ValueType function = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; From a602cecb262960049ba3f5a14a4c89072e22df78 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 8 Feb 2015 15:14:22 +0100 Subject: [PATCH 3/5] removed simplification of final result. Former-commit-id: d5a1f5f28cbd2d2576e64a8ad7ef4aebb70fd35c --- .../SparseDtmcEliminationModelChecker.cpp | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 1a3e54ab2..7f5ea4ea5 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -536,13 +536,21 @@ namespace storm { STORM_PRINT_AND_LOG(" * maximal depth of SCC decomposition: " << maximalDepth << std::endl); } } - + // Now, we return the value for the only initial state. STORM_LOG_DEBUG("Simplifying and returning result."); if (stateRewards) { - return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]); +// if (storm::settings::parametricSettings().isSimplifySet()) { +// return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]); +// } else { + return stateRewards.get()[*initialStates.begin()]; +// } } else { - return storm::utility::simplify(oneStepProbabilities[*initialStates.begin()]); +// if (storm::settings::parametricSettings().isSimplifySet()) { +// return storm::utility::simplify(oneStepProbabilities[*initialStates.begin()]); +// } else { + return oneStepProbabilities[*initialStates.begin()]; +// } } } From e32482b7a99c0d89ca1030032e2e6842804d3446 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 8 Feb 2015 16:22:27 +0100 Subject: [PATCH 4/5] Added debug output. Former-commit-id: 247b615c1e7c5b4c0a7681457966c8e10fe8f34f --- .../reachability/SparseDtmcEliminationModelChecker.cpp | 2 +- src/stormParametric.cpp | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 7f5ea4ea5..f7cc0a274 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -543,7 +543,7 @@ namespace storm { // if (storm::settings::parametricSettings().isSimplifySet()) { // return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]); // } else { - return stateRewards.get()[*initialStates.begin()]; + return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]); // } } else { // if (storm::settings::parametricSettings().isSimplifySet()) { diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index ade3e3451..1d44a79cf 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -194,9 +194,16 @@ void check() { storm::modelchecker::reachability::CollectConstraints constraintCollector; constraintCollector(*dtmc); + STORM_LOG_DEBUG("Computing function..."); + std::unique_ptr result = modelchecker.check(*formula); + + STORM_LOG_DEBUG("Computed the final result."); + ValueType valueFunction = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; + STORM_LOG_DEBUG("Extracted value function."); + // Report the result. STORM_PRINT_AND_LOG(std::endl << "Result (initial state): "); result->writeToStream(std::cout, model->getInitialStates()); From 534c8c8a449ff9e491c5fe8742eb9e8f8e0e6222 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 8 Feb 2015 21:29:30 +0100 Subject: [PATCH 5/5] Set more sensible default value for elimination order. Former-commit-id: 1f7651f9c61c10351f3a6424e6ce605e56f92d19 --- .../modules/SparseDtmcEliminationModelCheckerSettings.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp b/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp index fe4b63068..ce4221c7d 100644 --- a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp +++ b/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp @@ -14,7 +14,7 @@ namespace storm { SparseDtmcEliminationModelCheckerSettings::SparseDtmcEliminationModelCheckerSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { std::vector orders = {"fw", "fwrev", "bw", "bwrev", "rand"}; - this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(orders)).setDefaultValueString("bw").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(orders)).setDefaultValueString("fwrev").build()).build()); std::vector methods = {"state", "hybrid"}; this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use. Available are {state, hybrid}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("hybrid").build()).build());