From 136cb194d1a1a602347f788ca1d934c12e26b39e Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 21 Dec 2016 18:01:04 +0100 Subject: [PATCH] fixed a bunch of unused variable warnings --- .../abstraction/ExpressionTranslator.cpp | 24 +++++------ src/storm/abstraction/MenuGame.cpp | 4 +- src/storm/abstraction/MenuGameRefiner.cpp | 6 +-- src/storm/abstraction/MenuGameRefiner.h | 2 +- src/storm/adapters/AddExpressionAdapter.cpp | 8 ++-- src/storm/adapters/MathsatExpressionAdapter.h | 8 ++-- src/storm/adapters/Smt2ExpressionAdapter.h | 2 +- src/storm/adapters/Z3ExpressionAdapter.cpp | 8 ++-- src/storm/builder/DdJaniModelBuilder.cpp | 4 +- src/storm/builder/DdPrismModelBuilder.cpp | 8 ++-- src/storm/builder/DdPrismModelBuilder.h | 4 +- src/storm/builder/RewardModelBuilder.cpp | 2 +- .../jit/ExplicitJitJaniModelBuilder.cpp | 2 +- .../MILPMinimalLabelSetGenerator.h | 24 +++++------ .../SMTMinimalCommandSetGenerator.h | 4 +- .../generator/JaniNextStateGenerator.cpp | 2 +- .../generator/PrismNextStateGenerator.cpp | 2 +- src/storm/logic/CloneVisitor.cpp | 14 +++---- src/storm/logic/Formula.cpp | 6 +-- src/storm/logic/FormulaInformationVisitor.cpp | 40 +++++++++---------- src/storm/logic/FragmentChecker.cpp | 14 +++---- src/storm/logic/LabelSubstitutionVisitor.cpp | 2 +- src/storm/logic/ToExpressionVisitor.cpp | 34 ++++++++-------- .../logic/VariableSubstitutionVisitor.cpp | 2 +- .../modelchecker/AbstractModelChecker.cpp | 12 +++--- .../abstraction/GameBasedMdpModelChecker.cpp | 6 +-- .../abstraction/GameBasedMdpModelChecker.h | 2 +- .../csl/HybridCtmcCslModelChecker.cpp | 6 +-- .../csl/SparseCtmcCslModelChecker.cpp | 12 +++--- .../SparseMarkovAutomatonCslModelChecker.cpp | 10 ++--- .../csl/helper/HybridCtmcCslHelper.cpp | 12 +++--- .../csl/helper/HybridCtmcCslHelper.h | 3 +- .../csl/helper/SparseCtmcCslHelper.cpp | 20 +++++----- .../csl/helper/SparseCtmcCslHelper.h | 4 +- .../helper/SparseMarkovAutomatonCslHelper.cpp | 15 +++---- .../helper/SparseMarkovAutomatonCslHelper.h | 8 ++-- .../prctl/HybridDtmcPrctlModelChecker.cpp | 2 +- .../prctl/SparseDtmcPrctlModelChecker.cpp | 2 +- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 4 +- .../prctl/helper/SparseDtmcPrctlHelper.h | 2 +- src/storm/utility/storm.h | 2 +- 41 files changed, 171 insertions(+), 177 deletions(-) diff --git a/src/storm/abstraction/ExpressionTranslator.cpp b/src/storm/abstraction/ExpressionTranslator.cpp index fb9d1f5fc..f97074bfd 100644 --- a/src/storm/abstraction/ExpressionTranslator.cpp +++ b/src/storm/abstraction/ExpressionTranslator.cpp @@ -26,7 +26,7 @@ namespace storm { } template - boost::any ExpressionTranslator::visit(IfThenElseExpression const& expression, boost::any const& data) { + boost::any ExpressionTranslator::visit(IfThenElseExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); } @@ -57,8 +57,8 @@ namespace storm { // At this point, none of the predicates was found to be equivalent, so we split the expression. } - storm::dd::Bdd left = boost::any_cast>(expression.getFirstOperand()->accept(*this, boost::none)); - storm::dd::Bdd right = boost::any_cast>(expression.getSecondOperand()->accept(*this, boost::none)); + storm::dd::Bdd left = boost::any_cast>(expression.getFirstOperand()->accept(*this, data)); + storm::dd::Bdd right = boost::any_cast>(expression.getSecondOperand()->accept(*this, data)); switch (expression.getOperatorType()) { case BinaryBooleanFunctionExpression::OperatorType::And: return left && right; case BinaryBooleanFunctionExpression::OperatorType::Or: return left || right; @@ -69,7 +69,7 @@ namespace storm { } template - boost::any ExpressionTranslator::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + boost::any ExpressionTranslator::visit(BinaryNumericalFunctionExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); } @@ -92,8 +92,8 @@ namespace storm { STORM_LOG_THROW(!hasLocationVariables || !hasAbstractedVariables, storm::exceptions::NotSupportedException, "Expressions with two types (location variables and abstracted variables) of variables are currently not supported by the abstraction expression translator."); if (hasLocationVariables) { - storm::dd::Add left = boost::any_cast>(expression.getFirstOperand()->accept(*this, boost::none)); - storm::dd::Add right = boost::any_cast>(expression.getSecondOperand()->accept(*this, boost::none)); + storm::dd::Add left = boost::any_cast>(expression.getFirstOperand()->accept(*this, data)); + storm::dd::Add right = boost::any_cast>(expression.getSecondOperand()->accept(*this, data)); switch (expression.getRelationType()) { case BinaryRelationExpression::RelationType::Equal: return left.equals(right); @@ -117,7 +117,7 @@ namespace storm { } template - boost::any ExpressionTranslator::visit(VariableExpression const& expression, boost::any const& data) { + boost::any ExpressionTranslator::visit(VariableExpression const& expression, boost::any const&) { if (abstractedVariables.find(expression.getVariable()) != abstractedVariables.end()) { for (uint64_t predicateIndex = 0; predicateIndex < abstractionInformation.get().getNumberOfPredicates(); ++predicateIndex) { if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), expression.toExpression())) { @@ -158,19 +158,19 @@ namespace storm { // At this point, none of the predicates was found to be equivalent, so we split the expression. } - storm::dd::Bdd sub = boost::any_cast>(expression.getOperand()->accept(*this, boost::none)); + storm::dd::Bdd sub = boost::any_cast>(expression.getOperand()->accept(*this, data)); switch (expression.getOperatorType()) { case UnaryBooleanFunctionExpression::OperatorType::Not: return !sub; } } template - boost::any ExpressionTranslator::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + boost::any ExpressionTranslator::visit(UnaryNumericalFunctionExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); } template - boost::any ExpressionTranslator::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any ExpressionTranslator::visit(BooleanLiteralExpression const& expression, boost::any const&) { if (expression.isTrue()) { return abstractionInformation.get().getDdManager().getBddOne(); } else { @@ -179,12 +179,12 @@ namespace storm { } template - boost::any ExpressionTranslator::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + boost::any ExpressionTranslator::visit(IntegerLiteralExpression const& expression, boost::any const&) { return abstractionInformation.get().getDdManager().template getConstant(expression.getValue()); } template - boost::any ExpressionTranslator::visit(RationalLiteralExpression const& expression, boost::any const& data) { + boost::any ExpressionTranslator::visit(RationalLiteralExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); } diff --git a/src/storm/abstraction/MenuGame.cpp b/src/storm/abstraction/MenuGame.cpp index eb203a48d..596f05b39 100644 --- a/src/storm/abstraction/MenuGame.cpp +++ b/src/storm/abstraction/MenuGame.cpp @@ -34,7 +34,7 @@ namespace storm { } template - storm::dd::Bdd MenuGame::getStates(std::string const& label) const { + storm::dd::Bdd MenuGame::getStates(std::string const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Menu games do not provide labels."); } @@ -75,7 +75,7 @@ namespace storm { } template - bool MenuGame::hasLabel(std::string const& label) const { + bool MenuGame::hasLabel(std::string const&) const { return false; } diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index a2458dd6d..453528427 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -231,7 +231,7 @@ namespace storm { } template - RefinementPredicates MenuGameRefiner::derivePredicatesFromDifferingChoices(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const { + RefinementPredicates MenuGameRefiner::derivePredicatesFromDifferingChoices(storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const { // Prepare result. storm::expressions::Expression newPredicate; bool fromGuard = false; @@ -389,7 +389,7 @@ namespace storm { bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); if (lowerChoicesDifferent) { STORM_LOG_TRACE("Deriving predicate based on lower choice."); - predicates = derivePredicatesFromDifferingChoices(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + predicates = derivePredicatesFromDifferingChoices((pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); } if (predicates && (!player1ChoicesDifferent || predicates.get().getSource() == RefinementPredicates::Source::Guard)) { @@ -404,7 +404,7 @@ namespace storm { bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); if (upperChoicesDifferent) { STORM_LOG_TRACE("Deriving predicate based on upper choice."); - additionalPredicates = derivePredicatesFromDifferingChoices(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + additionalPredicates = derivePredicatesFromDifferingChoices((pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); } if (additionalPredicates) { diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 1157a8985..8d55cecd6 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -100,7 +100,7 @@ namespace storm { bool addedAllGuards() const; private: - RefinementPredicates derivePredicatesFromDifferingChoices(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const; + RefinementPredicates derivePredicatesFromDifferingChoices(storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const; RefinementPredicates derivePredicatesFromPivotState(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& pivotState, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const; /*! diff --git a/src/storm/adapters/AddExpressionAdapter.cpp b/src/storm/adapters/AddExpressionAdapter.cpp index e1ff56d4e..b5731a3f3 100644 --- a/src/storm/adapters/AddExpressionAdapter.cpp +++ b/src/storm/adapters/AddExpressionAdapter.cpp @@ -142,7 +142,7 @@ namespace storm { } template - boost::any AddExpressionAdapter::visit(storm::expressions::VariableExpression const& expression, boost::any const& data) { + boost::any AddExpressionAdapter::visit(storm::expressions::VariableExpression const& expression, boost::any const&) { auto const& variablePair = variableMapping->find(expression.getVariable()); STORM_LOG_THROW(variablePair != variableMapping->end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains the variable '" << expression.getVariableName() << "' for which no DD counterpart is known."); if (expression.hasBooleanType()) { @@ -187,17 +187,17 @@ namespace storm { } template - boost::any AddExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any AddExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) { return expression.getValue() ? ddManager->getBddOne() : ddManager->getBddZero(); } template - boost::any AddExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) { + boost::any AddExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) { return ddManager->getConstant(static_cast(expression.getValue())); } template - boost::any AddExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) { + boost::any AddExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) { return ddManager->getConstant(static_cast(expression.getValueAsDouble())); } diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h index a7e5f2e22..63edcc371 100644 --- a/src/storm/adapters/MathsatExpressionAdapter.h +++ b/src/storm/adapters/MathsatExpressionAdapter.h @@ -176,15 +176,15 @@ namespace storm { } } - virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) override { + virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) override { return expression.getValue() ? msat_make_true(env) : msat_make_false(env); } - virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) override { + virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) override { return msat_make_number(env, std::to_string(expression.getValueAsDouble()).c_str()); } - virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) override { + virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) override { return msat_make_number(env, std::to_string(static_cast(expression.getValue())).c_str()); } @@ -218,7 +218,7 @@ namespace storm { } } - virtual boost::any visit(storm::expressions::VariableExpression const& expression, boost::any const& data) override { + virtual boost::any visit(storm::expressions::VariableExpression const& expression, boost::any const&) override { return translateExpression(expression.getVariable()); } diff --git a/src/storm/adapters/Smt2ExpressionAdapter.h b/src/storm/adapters/Smt2ExpressionAdapter.h index 7c5b6dce4..ad72269a6 100644 --- a/src/storm/adapters/Smt2ExpressionAdapter.h +++ b/src/storm/adapters/Smt2ExpressionAdapter.h @@ -24,7 +24,7 @@ namespace storm { * @param manager The manager that can be used to build expressions. * @param useReadableVarNames sets whether the expressions should use human readable names for the variables or the internal representation */ - Smt2ExpressionAdapter(storm::expressions::ExpressionManager& manager, bool useReadableVarNames) + Smt2ExpressionAdapter(storm::expressions::ExpressionManager&, bool useReadableVarNames) : useReadableVarNames(useReadableVarNames) { declaredVariables.emplace_back(std::set()); } diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index 77f3379ea..fa8e9721e 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -207,17 +207,17 @@ namespace storm { } } - boost::any Z3ExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any Z3ExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) { return context.bool_val(expression.getValue()); } - boost::any Z3ExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) { + boost::any Z3ExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) { std::stringstream fractionStream; fractionStream << expression.getValue(); return context.real_val(fractionStream.str().c_str()); } - boost::any Z3ExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) { + boost::any Z3ExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) { return context.int_val(static_cast(expression.getValue())); } @@ -261,7 +261,7 @@ namespace storm { return z3::expr(context, Z3_mk_ite(context, conditionResult, thenResult, elseResult)); } - boost::any Z3ExpressionAdapter::visit(storm::expressions::VariableExpression const& expression, boost::any const& data) { + boost::any Z3ExpressionAdapter::visit(storm::expressions::VariableExpression const& expression, boost::any const&) { return this->translateExpression(expression.getVariable()); } diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index a6006a009..929595495 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -222,7 +222,7 @@ namespace storm { return createVariables(); } - boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { + boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const&) override { auto it = automata.find(composition.getAutomatonName()); STORM_LOG_THROW(it == automata.end(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition that refers to the automaton '" << composition.getAutomatonName() << "' multiple times."); automata.insert(it, composition.getAutomatonName()); @@ -231,7 +231,7 @@ namespace storm { boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { for (auto const& subcomposition : composition.getSubcompositions()) { - subcomposition->accept(*this, boost::none); + subcomposition->accept(*this, data); } return boost::none; } diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 099c0fba5..988335cbb 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -424,7 +424,7 @@ namespace storm { action.second = emptyAction; } else { // Otherwise, the actions of the modules are synchronized. - action.second = DdPrismModelBuilder::combineSynchronizingActions(generationInfo, action.second, right.synchronizingActionToDecisionDiagramMap[action.first]); + action.second = DdPrismModelBuilder::combineSynchronizingActions(action.second, right.synchronizingActionToDecisionDiagramMap[action.first]); } } else { // If we don't synchronize over this action, we need to construct the interleaving. @@ -893,7 +893,7 @@ namespace storm { } template - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2) { + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineSynchronizingActions(ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2) { std::set assignedGlobalVariables; std::set_union(action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), action2.assignedGlobalVariables.begin(), action2.assignedGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin())); return ActionDecisionDiagram(action1.guardDd * action2.guardDd, action1.transitionsDd * action2.transitionsDd, assignedGlobalVariables, std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables)); @@ -1107,7 +1107,7 @@ namespace storm { } template - storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd) { + storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd) { // Start by creating the state reward vector. boost::optional> stateRewards; @@ -1384,7 +1384,7 @@ namespace storm { std::unordered_map> rewardModels; for (auto const& rewardModel : selectedRewardModels) { - rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, transitionMatrix, reachableStatesAdd, stateActionDd)); + rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, reachableStatesAdd, stateActionDd)); } // Build the labels that can be accessed as a shortcut. diff --git a/src/storm/builder/DdPrismModelBuilder.h b/src/storm/builder/DdPrismModelBuilder.h index d60cbcaee..5b1db357f 100644 --- a/src/storm/builder/DdPrismModelBuilder.h +++ b/src/storm/builder/DdPrismModelBuilder.h @@ -218,7 +218,7 @@ namespace storm { static ActionDecisionDiagram combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector& commandDds, uint_fast64_t nondeterminismVariableOffset); - static ActionDecisionDiagram combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2); + static ActionDecisionDiagram combineSynchronizingActions(ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2); static ActionDecisionDiagram combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2, storm::dd::Add const& identityDd1, storm::dd::Add const& identityDd2); @@ -230,7 +230,7 @@ namespace storm { static storm::dd::Add createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); - static storm::models::symbolic::StandardRewardModel createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd); + static storm::models::symbolic::StandardRewardModel createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd); static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo); diff --git a/src/storm/builder/RewardModelBuilder.cpp b/src/storm/builder/RewardModelBuilder.cpp index 0200207bc..75dece593 100644 --- a/src/storm/builder/RewardModelBuilder.cpp +++ b/src/storm/builder/RewardModelBuilder.cpp @@ -16,7 +16,7 @@ namespace storm { } template - storm::models::sparse::StandardRewardModel RewardModelBuilder::build(uint_fast64_t rowCount, uint_fast64_t columnCount, uint_fast64_t rowGroupCount) { + storm::models::sparse::StandardRewardModel RewardModelBuilder::build(uint_fast64_t rowCount, uint_fast64_t, uint_fast64_t rowGroupCount) { boost::optional> optionalStateRewardVector; if (hasStateRewards()) { stateRewardVector.resize(rowGroupCount); diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index bf96e1e23..7d20342e5 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -2405,7 +2405,7 @@ namespace storm { } template - std::vector getParameters(storm::jani::Model const& model, std::shared_ptr>> cache) { + std::vector getParameters(storm::jani::Model const&, std::shared_ptr>> cache) { STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "This function must not be called for this type."); } diff --git a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h index bcf18eb0e..c50ac3472 100644 --- a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h @@ -262,11 +262,9 @@ namespace storm { * Creates the variable for the probability of the virtual initial state. * * @param solver The MILP solver. - * @param maximizeProbability If set to true, the objective function is constructed in a way that a - * label-minimal subsystem of maximal probability is computed. * @return The index of the variable for the probability of the virtual initial state. */ - static std::pair createVirtualInitialStateVariable(storm::solver::LpSolver& solver, bool maximizeProbability = false) { + static std::pair createVirtualInitialStateVariable(storm::solver::LpSolver& solver) { std::stringstream variableNameBuffer; variableNameBuffer << "pinit"; storm::expressions::Variable variable = solver.addBoundedContinuousVariable(variableNameBuffer.str(), 0, 1); @@ -415,13 +413,12 @@ namespace storm { * exceeds the given threshold. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. * @param variableInformation A struct with information about the variables of the model. * @param probabilityThreshold The probability that the subsystem must exceed. * @param strictBound A flag indicating whether the threshold must be exceeded or only matched. * @return The total number of constraints that were created. */ - static uint_fast64_t assertProbabilityGreaterThanThreshold(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& labeledMdp, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound) { + static uint_fast64_t assertProbabilityGreaterThanThreshold(storm::solver::LpSolver& solver, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound) { storm::expressions::Expression constraint; if (strictBound) { constraint = variableInformation.virtualInitialStateVariable > solver.getConstant(probabilityThreshold); @@ -506,11 +503,10 @@ namespace storm { * * @param solver The MILP solver. * @param stateInformation The information about the states in the model. - * @param choiceInformation The information about the choices in the model. * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertZeroProbabilityWithoutChoice(storm::solver::LpSolver& solver, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertZeroProbabilityWithoutChoice(storm::solver::LpSolver& solver, StateInformation const& stateInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; for (auto state : stateInformation.relevantStates) { storm::expressions::Expression constraint = variableInformation.stateToProbabilityVariableMap.at(state); @@ -624,13 +620,11 @@ namespace storm { * Asserts that labels that are on all paths from initial to target states are definitely taken. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. - * @param psiStates A bit vector characterizing the psi states in the model. * @param choiceInformation The information about the choices in the model. * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertKnownLabels(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertKnownLabels(storm::solver::LpSolver& solver, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; for (auto label : choiceInformation.knownLabels) { @@ -815,7 +809,7 @@ namespace storm { */ static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) { // Assert that the reachability probability in the subsystem exceeds the given threshold. - uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold(solver, labeledMdp, variableInformation, probabilityThreshold, strictBound); + uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold(solver, variableInformation, probabilityThreshold, strictBound); STORM_LOG_DEBUG("Asserted that reachability probability exceeds threshold."); // Add constraints that assert the policy takes at most one action in each state. @@ -828,7 +822,7 @@ namespace storm { // Add constraints that encode that the reachability probability from states which do not pick any action // is zero. - numberOfConstraints += assertZeroProbabilityWithoutChoice(solver, stateInformation, choiceInformation, variableInformation); + numberOfConstraints += assertZeroProbabilityWithoutChoice(solver, stateInformation, variableInformation); STORM_LOG_DEBUG("Asserted that reachability probability is zero if no choice is taken."); // Add constraints that encode the reachability probabilities for states. @@ -840,7 +834,7 @@ namespace storm { STORM_LOG_DEBUG("Asserted that unproblematic state reachable from problematic states."); // Add constraints that express that certain labels are already known to be taken. - numberOfConstraints += assertKnownLabels(solver, labeledMdp, psiStates, choiceInformation, variableInformation); + numberOfConstraints += assertKnownLabels(solver, choiceInformation, variableInformation); STORM_LOG_DEBUG("Asserted known labels are taken."); // If required, assert additional constraints that reduce the number of possible policies. @@ -923,7 +917,7 @@ namespace storm { } public: - static boost::container::flat_set getMinimalLabelSet(storm::logic::Formula const& pathFormula, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { + static boost::container::flat_set getMinimalLabelSet(storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { // (0) Check whether the MDP is indeed labeled. if (!labeledMdp.hasChoiceLabeling()) { throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model."; @@ -1015,7 +1009,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - boost::container::flat_set usedLabelSet = getMinimalLabelSet(probabilityOperator.getSubformula(), labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isUseSchedulerCutsSet()); + boost::container::flat_set usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isUseSchedulerCutsSet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h index ecc82ad25..7a0b7b232 100644 --- a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1593,7 +1593,7 @@ namespace storm { * @param checkThresholdFeasible If set, it is verified that the model can actually achieve/exceed the given probability value. If this check * is made and fails, an exception is thrown. */ - static boost::container::flat_set getMinimalCommandSet(storm::logic::Formula const& pathFormula, storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { + static boost::container::flat_set getMinimalCommandSet(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { #ifdef STORM_HAVE_Z3 // Set up all clocks used for time measurement. auto totalClock = std::chrono::high_resolution_clock::now(); @@ -1791,7 +1791,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto labelSet = getMinimalCommandSet(probabilityOperator.getSubformula(), program, constantDefinitionString, labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isEncodeReachabilitySet()); + auto labelSet = getMinimalCommandSet(program, constantDefinitionString, labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isEncodeReachabilitySet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 625e4cd8e..c7fe2497c 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -23,7 +23,7 @@ namespace storm { } template - JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(model.getExpressionManager(), options), model(model), rewardVariables(), hasStateActionRewards(false) { + JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator(model.getExpressionManager(), options), model(model), rewardVariables(), hasStateActionRewards(false) { STORM_LOG_THROW(model.hasStandardComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables."); STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support assignment levels."); diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index d9c3b4293..6b4c4c7d4 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -22,7 +22,7 @@ namespace storm { } template - PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(program.getManager(), options), program(program), rewardModels() { + PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool) : NextStateGenerator(program.getManager(), options), program(program), rewardModels() { STORM_LOG_TRACE("Creating next-state generator for PRISM program: " << program); STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index b3981e62a..e1d41edff 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -10,11 +10,11 @@ namespace storm { return boost::any_cast>(result); } - boost::any CloneVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const { + boost::any CloneVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - boost::any CloneVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const { + boost::any CloneVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } @@ -24,7 +24,7 @@ namespace storm { return std::static_pointer_cast(std::make_shared(f.getOperator(), left, right)); } - boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const { + boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } @@ -44,7 +44,7 @@ namespace storm { return std::static_pointer_cast(std::make_shared(subformula, conditionFormula, f.getContext())); } - boost::any CloneVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { + boost::any CloneVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } @@ -63,7 +63,7 @@ namespace storm { return std::static_pointer_cast(std::make_shared(subformula)); } - boost::any CloneVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const { + boost::any CloneVisitor::visit(InstantaneousRewardFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } @@ -72,7 +72,7 @@ namespace storm { return std::static_pointer_cast(std::make_shared(subformula, f.getOperatorInformation())); } - boost::any CloneVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { + boost::any CloneVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } @@ -99,7 +99,7 @@ namespace storm { return std::static_pointer_cast(std::make_shared(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation())); } - boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { + boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared()); } diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index e253da4fb..d61129914 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -460,15 +460,15 @@ namespace storm { return this->shared_from_this(); } - void Formula::gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const { + void Formula::gatherAtomicExpressionFormulas(std::vector>&) const { return; } - void Formula::gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const { + void Formula::gatherAtomicLabelFormulas(std::vector>&) const { return; } - void Formula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { + void Formula::gatherReferencedRewardModels(std::set&) const { return; } diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp index ed0a461b1..69226031d 100644 --- a/src/storm/logic/FormulaInformationVisitor.cpp +++ b/src/storm/logic/FormulaInformationVisitor.cpp @@ -9,88 +9,88 @@ namespace storm { return boost::any_cast(result); } - boost::any FormulaInformationVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const { + boost::any FormulaInformationVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const { return FormulaInformation(); } - boost::any FormulaInformationVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const { + boost::any FormulaInformationVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const { return FormulaInformation(); } - boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { + boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const&) const { return FormulaInformation(); } - boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const { + boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const { return FormulaInformation(); } boost::any FormulaInformationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { - return boost::any_cast(f.getLeftSubformula().accept(*this)).join(boost::any_cast(f.getRightSubformula().accept(*this))).setContainsBoundedUntilFormula(); + return boost::any_cast(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast(f.getRightSubformula().accept(*this))).setContainsBoundedUntilFormula(); } boost::any FormulaInformationVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { - return boost::any_cast(f.getSubformula().accept(*this)).join(boost::any_cast(f.getConditionFormula().accept(*this))); + return boost::any_cast(f.getSubformula().accept(*this, data)).join(boost::any_cast(f.getConditionFormula().accept(*this))); } - boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { + boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { return FormulaInformation(); } boost::any FormulaInformationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { - return f.getSubformula().accept(*this); + return f.getSubformula().accept(*this, data); } boost::any FormulaInformationVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { - return f.getSubformula().accept(*this); + return f.getSubformula().accept(*this, data); } boost::any FormulaInformationVisitor::visit(GloballyFormula const& f, boost::any const& data) const { - return f.getSubformula().accept(*this); + return f.getSubformula().accept(*this, data); } - boost::any FormulaInformationVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const { + boost::any FormulaInformationVisitor::visit(InstantaneousRewardFormula const& f, boost::any const&) const { return FormulaInformation(); } boost::any FormulaInformationVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { - return f.getSubformula().accept(*this); + return f.getSubformula().accept(*this, data); } - boost::any FormulaInformationVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { + boost::any FormulaInformationVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const&) const { return FormulaInformation(); } boost::any FormulaInformationVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const { FormulaInformation result; for(auto const& subF : f.getSubformulas()){ - result.join(boost::any_cast(subF->accept(*this))); + result.join(boost::any_cast(subF->accept(*this, data))); } return result; } boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const { - return boost::any_cast(f.getSubformula().accept(*this)).setContainsNextFormula(); + return boost::any_cast(f.getSubformula().accept(*this, data)).setContainsNextFormula(); } boost::any FormulaInformationVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { - return f.getSubformula().accept(*this); + return f.getSubformula().accept(*this, data); } boost::any FormulaInformationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { - return boost::any_cast(f.getSubformula().accept(*this)).setContainsRewardOperator(); + return boost::any_cast(f.getSubformula().accept(*this, data)).setContainsRewardOperator(); } - boost::any FormulaInformationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { + boost::any FormulaInformationVisitor::visit(TotalRewardFormula const& f, boost::any const&) const { return FormulaInformation(); } boost::any FormulaInformationVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { - return f.getSubformula().accept(*this); + return f.getSubformula().accept(*this, data); } boost::any FormulaInformationVisitor::visit(UntilFormula const& f, boost::any const& data) const { - return boost::any_cast(f.getLeftSubformula().accept(*this)).join(boost::any_cast(f.getRightSubformula().accept(*this))); + return boost::any_cast(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast(f.getRightSubformula().accept(*this))); } } diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 0b2b1a81b..3dc27fe5f 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -28,12 +28,12 @@ namespace storm { return result; } - boost::any FragmentChecker::visit(AtomicExpressionFormula const& f, boost::any const& data) const { + boost::any FragmentChecker::visit(AtomicExpressionFormula const&, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); return inherited.getSpecification().areAtomicExpressionFormulasAllowed(); } - boost::any FragmentChecker::visit(AtomicLabelFormula const& f, boost::any const& data) const { + boost::any FragmentChecker::visit(AtomicLabelFormula const&, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); return inherited.getSpecification().areAtomicLabelFormulasAllowed(); } @@ -46,7 +46,7 @@ namespace storm { return result; } - boost::any FragmentChecker::visit(BooleanLiteralFormula const& f, boost::any const& data) const { + boost::any FragmentChecker::visit(BooleanLiteralFormula const&, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); return inherited.getSpecification().areBooleanLiteralFormulasAllowed(); } @@ -88,7 +88,7 @@ namespace storm { return result; } - boost::any FragmentChecker::visit(CumulativeRewardFormula const& f, boost::any const& data) const { + boost::any FragmentChecker::visit(CumulativeRewardFormula const&, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); return inherited.getSpecification().areCumulativeRewardFormulasAllowed(); } @@ -137,7 +137,7 @@ namespace storm { return result; } - boost::any FragmentChecker::visit(InstantaneousRewardFormula const& f, boost::any const& data) const { + boost::any FragmentChecker::visit(InstantaneousRewardFormula const&, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); return inherited.getSpecification().areInstantaneousRewardFormulasAllowed(); } @@ -154,7 +154,7 @@ namespace storm { return result; } - boost::any FragmentChecker::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { + boost::any FragmentChecker::visit(LongRunAverageRewardFormula const&, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); return inherited.getSpecification().areLongRunAverageRewardFormulasAllowed(); } @@ -219,7 +219,7 @@ namespace storm { return result; } - boost::any FragmentChecker::visit(TotalRewardFormula const& f, boost::any const& data) const { + boost::any FragmentChecker::visit(TotalRewardFormula const&, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); return inherited.getSpecification().areTotalRewardFormulasAllowed(); } diff --git a/src/storm/logic/LabelSubstitutionVisitor.cpp b/src/storm/logic/LabelSubstitutionVisitor.cpp index 6a245aab8..9794b2530 100644 --- a/src/storm/logic/LabelSubstitutionVisitor.cpp +++ b/src/storm/logic/LabelSubstitutionVisitor.cpp @@ -14,7 +14,7 @@ namespace storm { return boost::any_cast>(result); } - boost::any LabelSubstitutionVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const { + boost::any LabelSubstitutionVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const { auto it = labelToExpressionMapping.find(f.getLabel()); if (it != labelToExpressionMapping.end()) { return std::static_pointer_cast(std::make_shared(it->second)); diff --git a/src/storm/logic/ToExpressionVisitor.cpp b/src/storm/logic/ToExpressionVisitor.cpp index a223a45da..aabfbcb97 100644 --- a/src/storm/logic/ToExpressionVisitor.cpp +++ b/src/storm/logic/ToExpressionVisitor.cpp @@ -15,11 +15,11 @@ namespace storm { return boost::any_cast(result); } - boost::any ToExpressionVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const { return f.getExpression(); } - boost::any ToExpressionVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression, because the undefined atomic label '" << f.getLabel() << "' appears in the formula."); } @@ -46,59 +46,59 @@ namespace storm { return result; } - boost::any ToExpressionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(BoundedUntilFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(ConditionalFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(CumulativeRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(EventuallyFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(TimeOperatorFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(GloballyFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(GloballyFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(LongRunAverageOperatorFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(MultiObjectiveFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(NextFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(NextFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(ProbabilityOperatorFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(RewardOperatorFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - boost::any ToExpressionVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(TotalRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } @@ -111,7 +111,7 @@ namespace storm { } } - boost::any ToExpressionVisitor::visit(UntilFormula const& f, boost::any const& data) const { + boost::any ToExpressionVisitor::visit(UntilFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index 8f0d09faf..916542b39 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -14,7 +14,7 @@ namespace storm { return boost::any_cast>(result); } - boost::any VariableSubstitutionVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const { + boost::any VariableSubstitutionVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f.getExpression().substitute(substitution))); } } diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 0eba3911b..e564aa0f6 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -105,27 +105,27 @@ namespace storm { } template - std::unique_ptr AbstractModelChecker::computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr AbstractModelChecker::computeConditionalRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } template - std::unique_ptr AbstractModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr AbstractModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } template - std::unique_ptr AbstractModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr AbstractModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } template - std::unique_ptr AbstractModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr AbstractModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } template - std::unique_ptr AbstractModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr AbstractModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } @@ -144,7 +144,7 @@ namespace storm { } template - std::unique_ptr AbstractModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr AbstractModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 4609c5853..37404b867 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -368,12 +368,12 @@ namespace storm { } // #ifdef LOCAL_DEBUG - abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); + // abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); // #endif // (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). auto qualitativeStart = std::chrono::high_resolution_clock::now(); - QualitativeResultMinMax qualitativeResult = computeProb01States(checkTask, previousQualitativeResult, game, player1Direction, transitionMatrixBdd, initialStates, constraintStates, targetStates); + QualitativeResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates); std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); if (result) { printStatistics(*abstractor, game); @@ -527,7 +527,7 @@ namespace storm { } template - QualitativeResultMinMax GameBasedMdpModelChecker::computeProb01States(CheckTask const& checkTask, boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { + QualitativeResultMinMax GameBasedMdpModelChecker::computeProb01States(boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { QualitativeResultMinMax result; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index de6fd8fc8..ae63f96df 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -71,7 +71,7 @@ namespace storm { * Performs a qualitative check on the the given game to compute the (player 1) states that have probability * 0 or 1, respectively, to reach a target state and only visiting constraint states before. */ - QualitativeResultMinMax computeProb01States(CheckTask const& checkTask, boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); + QualitativeResultMinMax computeProb01States(boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); void printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game) const; diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 62f789332..b94d4d14e 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -52,7 +52,7 @@ namespace storm { template - std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -81,13 +81,13 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); return storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); } diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index e554e7997..22aa11c1e 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -94,21 +94,21 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -124,17 +124,17 @@ namespace storm { ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), this->getModel().getInitialStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 16ccd6162..cb5275abc 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -80,14 +80,14 @@ namespace storm { } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } @@ -100,19 +100,19 @@ namespace storm { std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute expected times in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index 19d6755c7..e48b436a7 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -28,17 +28,17 @@ namespace storm { template std::unique_ptr HybridCtmcCslHelper::computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - return HybridDtmcPrctlHelper::computeReachabilityRewards(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), rewardModel.divideStateRewardVector(exitRateVector), targetStates, qualitative, linearEquationSolverFactory); + return HybridDtmcPrctlHelper::computeReachabilityRewards(model, computeProbabilityMatrix(rateMatrix, exitRateVector), rewardModel.divideStateRewardVector(exitRateVector), targetStates, qualitative, linearEquationSolverFactory); } template std::unique_ptr HybridCtmcCslHelper::computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates) { - return HybridDtmcPrctlHelper::computeNextProbabilities(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), nextStates); + return HybridDtmcPrctlHelper::computeNextProbabilities(model, computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates); } template std::unique_ptr HybridCtmcCslHelper::computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - return HybridDtmcPrctlHelper::computeUntilProbabilities(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), phiStates, psiStates, qualitative, linearEquationSolverFactory); + return HybridDtmcPrctlHelper::computeUntilProbabilities(model, computeProbabilityMatrix(rateMatrix, exitRateVector), phiStates, psiStates, qualitative, linearEquationSolverFactory); } template @@ -277,7 +277,7 @@ namespace storm { template std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - storm::dd::Add probabilityMatrix = computeProbabilityMatrix(model, rateMatrix, exitRateVector); + storm::dd::Add probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); // Create ODD for the translation. storm::dd::Odd odd = model.getReachableStates().createOdd(); @@ -285,7 +285,7 @@ namespace storm { storm::storage::SparseMatrix explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd); std::vector explicitExitRateVector = exitRateVector.toVector(odd); - std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector, qualitative, linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector, linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } @@ -309,7 +309,7 @@ namespace storm { } template - storm::dd::Add HybridCtmcCslHelper::computeProbabilityMatrix(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector) { + storm::dd::Add HybridCtmcCslHelper::computeProbabilityMatrix(storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector) { return rateMatrix / exitRateVector; } diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h index d8bc0fc66..df5cd60a3 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h @@ -40,12 +40,11 @@ namespace storm { * @param exitRateVector The exit rate vector of the model. * @return The probability matrix. */ - static storm::dd::Add computeProbabilityMatrix(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector); + static storm::dd::Add computeProbabilityMatrix(storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector); /*! * Computes the matrix representing the transitions of the uniformized CTMC. * - * @param model The symbolic model. * @param transitionMatrix The matrix to uniformize. * @param exitRateVector The exit rate vector. * @param maybeStates The states that need to be considered. diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index d616ac806..f2235e755 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -192,7 +192,7 @@ namespace storm { } template ::SupportsExponential, int>::type> - std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const&, storm::storage::SparseMatrix const&, storm::storage::BitVector const&, storm::storage::BitVector const&, std::vector const&, bool, double, double, storm::solver::LinearEquationSolverFactory const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type."); } @@ -233,7 +233,7 @@ namespace storm { } template ::SupportsExponential, int>::type> - std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const&, std::vector const&, RewardModelType const&, double, storm::solver::LinearEquationSolverFactory const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing instantaneous rewards is unsupported for this value type."); } @@ -274,7 +274,7 @@ namespace storm { } template - std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Compute expected time on CTMC by reduction to DTMC with rewards. storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); @@ -330,7 +330,7 @@ namespace storm { } template - std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // If there are no goal states, we avoid the computation and directly return zero. uint_fast64_t numberOfStates = probabilityMatrix.getRowCount(); if (psiStates.empty()) { @@ -695,11 +695,11 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); @@ -720,14 +720,14 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h index cfb56b375..80aa68130 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -43,10 +43,10 @@ namespace storm { static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template - static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template - static std::vector computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); /*! * Computes the matrix representing the transitions of the uniformized CTMC. diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index d720555be..89f6f76ae 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -31,7 +31,7 @@ namespace storm { namespace helper { template - void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Start by computing four sparse matrices: // * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states. @@ -145,7 +145,7 @@ namespace storm { std::vector vProbabilistic(probabilisticNonGoalStates.getNumberOfSetBits()); std::vector vMarkovian(markovianNonGoalStates.getNumberOfSetBits()); - computeBoundedReachabilityProbabilities(dir, transitionMatrix, exitRateVector, markovianStates, psiStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory); + computeBoundedReachabilityProbabilities(dir, transitionMatrix, exitRateVector, psiStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory); // (4) If the lower bound of interval was non-zero, we need to take the current values as the starting values for a subsequent value iteration. if (lowerBound != storm::utility::zero()) { @@ -163,7 +163,7 @@ namespace storm { STORM_LOG_INFO("Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [0, " << lowerBound << "]." << std::endl); // Compute the bounded reachability for interval [0, b-a]. - computeBoundedReachabilityProbabilities(dir, transitionMatrix, exitRateVector, markovianStates, storm::storage::BitVector(numberOfStates), markovianStates, ~markovianStates, vAllMarkovian, vAllProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory); + computeBoundedReachabilityProbabilities(dir, transitionMatrix, exitRateVector, storm::storage::BitVector(numberOfStates), markovianStates, ~markovianStates, vAllMarkovian, vAllProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory); // Create the result vector out of vAllProbabilistic and vAllMarkovian and return it. std::vector result(numberOfStates, storm::utility::zero()); @@ -189,12 +189,13 @@ namespace storm { template template - std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix.getRowCount(), transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, totalRewardVector, minMaxLinearEquationSolverFactory); } + template - std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // If there are no goal states, we avoid the computation and directly return zero. @@ -349,7 +350,7 @@ namespace storm { } template - std::vector SparseMarkovAutomatonCslHelper::computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); std::vector rewardValues(numberOfStates, storm::utility::zero()); storm::utility::vector::setVectorValues(rewardValues, markovianStates, storm::utility::one()); @@ -505,7 +506,7 @@ namespace storm { } template class SparseMarkovAutomatonCslHelper; - template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); } } diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 081ee7313..ba8223b60 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -19,15 +19,15 @@ namespace storm { static std::vector computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template - static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static std::vector computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static std::vector computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); private: - static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); /*! * Computes the long-run average value for the given maximal end component of a Markov automaton. diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index b84c6eb10..03e4f1194 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -112,7 +112,7 @@ namespace storm { storm::storage::SparseMatrix explicitProbabilityMatrix = this->getModel().getTransitionMatrix().toMatrix(odd, odd); - std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), *this->linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().template getAddZero(), this->getModel().getReachableStates(), std::move(odd), std::move(result))); } diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index dda0cd248..83566192c 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -111,7 +111,7 @@ namespace storm { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, checkTask.isQualitativeSet(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 1e98585ae..89d5c538e 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -232,8 +232,8 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - return SparseCtmcCslHelper::computeLongRunAverageProbabilities(transitionMatrix, psiStates, nullptr, qualitative, linearEquationSolverFactory); + std::vector SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return SparseCtmcCslHelper::computeLongRunAverageProbabilities(transitionMatrix, psiStates, nullptr, linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index e248de563..0709aba11 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -38,7 +38,7 @@ namespace storm { static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint = boost::none); - static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::vector computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 1784e44c7..b91b1f7b3 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -113,7 +113,7 @@ namespace storm { std::vector> parseFormulasForJaniModel(std::string const& inputString, storm::jani::Model const& model); template - std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { storm::builder::BuilderOptions options(formulas); if (storm::settings::getModule().isBuildFullModelSet()) {