From 5b09b91ae1f4d1abc9d25951263c5b606a6181f0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 22 Dec 2016 11:07:13 +0100 Subject: [PATCH] fixed more warnings --- .../abstraction/ExpressionTranslator.cpp | 3 + .../jit/ExplicitJitJaniModelBuilder.cpp | 2 +- .../MILPMinimalLabelSetGenerator.h | 2 +- .../SMTMinimalCommandSetGenerator.h | 6 +- src/storm/logic/CloneVisitor.cpp | 2 +- src/storm/logic/FormulaInformationVisitor.cpp | 16 +-- src/storm/logic/ToExpressionVisitor.cpp | 2 + .../abstraction/GameBasedMdpModelChecker.cpp | 4 +- .../csl/HybridCtmcCslModelChecker.cpp | 2 +- .../csl/helper/HybridCtmcCslHelper.cpp | 2 +- .../csl/helper/HybridCtmcCslHelper.h | 2 +- .../csl/helper/SparseCtmcCslHelper.cpp | 6 +- .../helper/SparseMarkovAutomatonCslHelper.cpp | 2 +- .../SparseExplorationModelChecker.cpp | 2 +- .../pcaa/SparsePcaaWeightVectorChecker.cpp | 2 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 2 +- src/storm/solver/GurobiLpSolver.cpp | 2 +- src/storm/solver/SmtSolver.cpp | 8 +- src/storm/solver/SolverSelectionOptions.cpp | 4 + .../StandardMinMaxLinearEquationSolver.cpp | 1 + .../TopologicalMinMaxLinearEquationSolver.cpp | 4 + .../stateelimination/EliminatorBase.cpp | 8 +- src/storm/storage/SparseMatrix.cpp | 2 +- .../BisimulationDecomposition.cpp | 4 +- .../bisimulation/BisimulationDecomposition.h | 3 +- src/storm/storage/dd/Add.cpp | 4 +- src/storm/storage/dd/Add.h | 4 +- src/storm/storage/dd/Bdd.cpp | 1 + src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 2 +- .../storage/dd/sylvan/InternalSylvanAdd.cpp | 42 +++---- .../storage/dd/sylvan/InternalSylvanBdd.cpp | 8 +- .../storage/expressions/BaseExpression.cpp | 6 +- .../expressions/BooleanLiteralExpression.cpp | 4 +- .../expressions/ChangeManagerVisitor.cpp | 8 +- .../expressions/IntegerLiteralExpression.cpp | 4 +- .../expressions/LinearCoefficientVisitor.cpp | 16 +-- .../expressions/LinearityCheckVisitor.cpp | 16 +-- .../expressions/RationalLiteralExpression.cpp | 4 +- .../expressions/SubstitutionVisitor.cpp | 8 +- .../storage/expressions/ToCppVisitor.cpp | 2 +- .../expressions/ToExprtkStringVisitor.cpp | 8 +- .../expressions/ToRationalFunctionVisitor.cpp | 18 +-- .../expressions/ToRationalNumberVisitor.cpp | 20 ++-- .../VariableSetPredicateSplitter.cpp | 16 +-- src/storm/storage/jani/JSONExporter.cpp | 106 +++++++++--------- src/storm/storage/jani/Model.cpp | 13 +-- src/storm/storage/jani/ModelType.cpp | 1 + src/storm/storage/prism/BooleanVariable.cpp | 2 +- .../prism/CompositionToJaniVisitor.cpp | 2 +- src/storm/storage/prism/IntegerVariable.cpp | 2 +- src/storm/storage/prism/Program.cpp | 2 +- src/storm/storage/prism/Variable.cpp | 2 +- src/storm/storage/prism/Variable.h | 4 +- src/storm/utility/ConstantsComparator.cpp | 6 +- src/storm/utility/constants.cpp | 22 ++-- src/storm/utility/graph.cpp | 70 +++--------- src/storm/utility/graph.h | 5 +- src/storm/utility/numerical.h | 2 +- src/storm/utility/shortestPaths.cpp | 8 +- src/test/utility/GraphTest.cpp | 34 ++++-- 60 files changed, 267 insertions(+), 298 deletions(-) diff --git a/src/storm/abstraction/ExpressionTranslator.cpp b/src/storm/abstraction/ExpressionTranslator.cpp index f97074bfd..fe2d28f97 100644 --- a/src/storm/abstraction/ExpressionTranslator.cpp +++ b/src/storm/abstraction/ExpressionTranslator.cpp @@ -66,6 +66,7 @@ namespace storm { case BinaryBooleanFunctionExpression::OperatorType::Implies: return !left || right; case BinaryBooleanFunctionExpression::OperatorType::Iff: return (left && right) || (!left && !right); } + return boost::any(); } template @@ -114,6 +115,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); } + return boost::any(); } template @@ -162,6 +164,7 @@ namespace storm { switch (expression.getOperatorType()) { case UnaryBooleanFunctionExpression::OperatorType::Not: return !sub; } + return boost::any(); } template diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 7d20342e5..7c215dfbe 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -2400,7 +2400,7 @@ namespace storm { } template> = carl::dummy> - RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable, std::shared_ptr>> cache) { + RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable, std::shared_ptr>>) { return RationalFunctionType(variable); } diff --git a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h index c50ac3472..537b844d6 100644 --- a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h @@ -94,7 +94,7 @@ namespace storm { */ static struct StateInformation determineRelevantAndProblematicStates(storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { StateInformation result; - result.relevantStates = storm::utility::graph::performProbGreater0E(labeledMdp.getTransitionMatrix(), labeledMdp.getNondeterministicChoiceIndices(), labeledMdp.getBackwardTransitions(), phiStates, psiStates); + result.relevantStates = storm::utility::graph::performProbGreater0E(labeledMdp.getBackwardTransitions(), phiStates, psiStates); result.relevantStates &= ~psiStates; result.problematicStates = storm::utility::graph::performProb0E(labeledMdp.getTransitionMatrix(), labeledMdp.getNondeterministicChoiceIndices(), labeledMdp.getBackwardTransitions(), phiStates, psiStates); result.problematicStates &= result.relevantStates; diff --git a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h index 7a0b7b232..6971992d4 100644 --- a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h @@ -95,7 +95,7 @@ namespace storm { // Compute all relevant states, i.e. states for which there exists a scheduler that has a non-zero // probabilitiy of satisfying phi until psi. storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); - relevancyInformation.relevantStates = storm::utility::graph::performProbGreater0E(labeledMdp.getTransitionMatrix(), labeledMdp.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates); + relevancyInformation.relevantStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates); relevancyInformation.relevantStates &= ~psiStates; STORM_LOG_DEBUG("Found " << relevancyInformation.relevantStates.getNumberOfSetBits() << " relevant states."); @@ -1410,7 +1410,7 @@ namespace storm { } storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; - storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getTransitionMatrix(), subMdp.getNondeterministicChoiceIndices(), subMdp.getBackwardTransitions(), phiStates, psiStates); + storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getBackwardTransitions(), phiStates, psiStates); boost::container::flat_set locallyRelevantLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); @@ -1530,7 +1530,7 @@ namespace storm { STORM_LOG_DEBUG("Successfully determined reachable state space."); storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; - storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getTransitionMatrix(), subMdp.getNondeterministicChoiceIndices(), subMdp.getBackwardTransitions(), phiStates, psiStates); + storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getBackwardTransitions(), phiStates, psiStates); boost::container::flat_set locallyRelevantLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index e1d41edff..adb6c4cb3 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -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&) const { + boost::any CloneVisitor::visit(TotalRewardFormula const&, boost::any const&) const { return std::static_pointer_cast(std::make_shared()); } diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp index 69226031d..319fbf2f8 100644 --- a/src/storm/logic/FormulaInformationVisitor.cpp +++ b/src/storm/logic/FormulaInformationVisitor.cpp @@ -9,19 +9,19 @@ namespace storm { return boost::any_cast(result); } - boost::any FormulaInformationVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const { + boost::any FormulaInformationVisitor::visit(AtomicExpressionFormula const&, boost::any const&) const { return FormulaInformation(); } - boost::any FormulaInformationVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const { + boost::any FormulaInformationVisitor::visit(AtomicLabelFormula const&, boost::any const&) const { return FormulaInformation(); } - boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const&) const { + boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const { return FormulaInformation(); } - boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const { + boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const { return FormulaInformation(); } @@ -33,7 +33,7 @@ namespace storm { 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&) const { + boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const&, boost::any const&) const { return FormulaInformation(); } @@ -49,7 +49,7 @@ namespace storm { return f.getSubformula().accept(*this, data); } - boost::any FormulaInformationVisitor::visit(InstantaneousRewardFormula const& f, boost::any const&) const { + boost::any FormulaInformationVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const { return FormulaInformation(); } @@ -57,7 +57,7 @@ namespace storm { return f.getSubformula().accept(*this, data); } - boost::any FormulaInformationVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const&) const { + boost::any FormulaInformationVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const { return FormulaInformation(); } @@ -81,7 +81,7 @@ namespace storm { return boost::any_cast(f.getSubformula().accept(*this, data)).setContainsRewardOperator(); } - boost::any FormulaInformationVisitor::visit(TotalRewardFormula const& f, boost::any const&) const { + boost::any FormulaInformationVisitor::visit(TotalRewardFormula const&, boost::any const&) const { return FormulaInformation(); } diff --git a/src/storm/logic/ToExpressionVisitor.cpp b/src/storm/logic/ToExpressionVisitor.cpp index aabfbcb97..ddfe0ea6d 100644 --- a/src/storm/logic/ToExpressionVisitor.cpp +++ b/src/storm/logic/ToExpressionVisitor.cpp @@ -34,6 +34,7 @@ namespace storm { return left || right; break; } + return boost::any(); } boost::any ToExpressionVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const { @@ -109,6 +110,7 @@ namespace storm { return !subexpression; break; } + return boost::any(); } boost::any ToExpressionVisitor::visit(UntilFormula const&, boost::any const&) const { diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 37404b867..8249fe7d8 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -214,7 +214,7 @@ namespace storm { } template - std::unique_ptr checkForResultAfterQuantitativeCheck(CheckTask const& checkTask, ValueType const& minValue, ValueType const& maxValue, storm::utility::ConstantsComparator const& comparator) { + std::unique_ptr checkForResultAfterQuantitativeCheck(ValueType const& minValue, ValueType const& maxValue, storm::utility::ConstantsComparator const& comparator) { std::unique_ptr result; // If the lower and upper bounds are close enough, we can return the result. @@ -440,7 +440,7 @@ namespace storm { STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.initialStatesRange.first << ", " << quantitativeResult.max.initialStatesRange.second << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. - result = checkForResultAfterQuantitativeCheck(checkTask, quantitativeResult.min.initialStatesRange.first, quantitativeResult.max.initialStatesRange.second, comparator); + result = checkForResultAfterQuantitativeCheck(quantitativeResult.min.initialStatesRange.first, quantitativeResult.max.initialStatesRange.second, comparator); if (result) { printStatistics(*abstractor, game); return result; diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index b94d4d14e..ca07fbc07 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -98,7 +98,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), *linearEquationSolverFactory); } // Explicitly instantiate the model checker. diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index e48b436a7..e3e301f68 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -276,7 +276,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) { + 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, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { storm::dd::Add probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); // Create ODD for the translation. diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h index df5cd60a3..70f8a5c1d 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h @@ -28,7 +28,7 @@ namespace storm { static std::unique_ptr 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); - static std::unique_ptr 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); + static std::unique_ptr computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::unique_ptr computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index f2235e755..b8f0f527a 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -269,7 +269,7 @@ namespace storm { } template ::SupportsExponential, int>::type> - std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const&, std::vector const&, RewardModelType const&, double, storm::solver::LinearEquationSolverFactory const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing cumulative rewards is unsupported for this value type."); } @@ -325,7 +325,7 @@ namespace storm { } template ::SupportsExponential, int>::type> - std::vector SparseCtmcCslHelper::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) { + std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const&, storm::storage::SparseMatrix const&, std::vector const&, RewardModelType const&, storm::storage::BitVector const&, bool, storm::solver::LinearEquationSolverFactory const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing reachability rewards is unsupported for this value type."); } @@ -591,7 +591,7 @@ namespace storm { } // Use Fox-Glynn to get the truncation points and the weights. - std::tuple> foxGlynnResult = storm::utility::numerical::getFoxGlynnCutoff(lambda, 1e-300, 1e+300, storm::settings::getModule().getPrecision() / 8.0); + std::tuple> foxGlynnResult = storm::utility::numerical::getFoxGlynnCutoff(lambda, 1e+300, storm::settings::getModule().getPrecision() / 8.0); STORM_LOG_DEBUG("Fox-Glynn cutoff points: left=" << std::get<0>(foxGlynnResult) << ", right=" << std::get<1>(foxGlynnResult)); // Scale the weights so they add up to one. diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 89f6f76ae..4bbc92e73 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -402,7 +402,7 @@ namespace storm { if (!unionOfNonGoalMaximalEndComponents.empty()) { // Now we need to check for which states there exists a scheduler that reaches one of the previously computed states. - infinityStates = storm::utility::graph::performProbGreater0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, storm::storage::BitVector(numberOfStates, true), unionOfNonGoalMaximalEndComponents); + infinityStates = storm::utility::graph::performProbGreater0E(backwardTransitions, storm::storage::BitVector(numberOfStates, true), unionOfNonGoalMaximalEndComponents); } else { // Otherwise, we have no infinity states. infinityStates = storm::storage::BitVector(numberOfStates); diff --git a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp index 3fd18a49a..de099d655 100644 --- a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp +++ b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp @@ -440,7 +440,7 @@ namespace storm { // duplicate work is the following. Optimally, we would only do the MEC decomposition, because we need // it anyway. However, when only detecting (accepting) MECs, we do not infer which of the other states // (not contained in MECs) also have probability 0/1. - statesWithProbability0 = storm::utility::graph::performProb0A(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates); + statesWithProbability0 = storm::utility::graph::performProb0A(transposedMatrix, allStates, targetStates); targetStates.set(sink, true); statesWithProbability1 = storm::utility::graph::performProb1E(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index f3cb80ff5..d18146b40 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -133,7 +133,7 @@ namespace storm { nonZeroRewardStates.set(state); } } - storm::storage::BitVector subsystemStates = storm::utility::graph::performProbGreater0E(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getTransitionMatrix().transpose(true), storm::storage::BitVector(model.getNumberOfStates(), true), nonZeroRewardStates); + storm::storage::BitVector subsystemStates = storm::utility::graph::performProbGreater0E(model.getTransitionMatrix().transpose(true), storm::storage::BitVector(model.getNumberOfStates(), true), nonZeroRewardStates); // Remove neutral end components, i.e., ECs in which no reward is earned. auto ecEliminatorResult = storm::transformer::EndComponentEliminator::transform(model.getTransitionMatrix(), subsystemStates, ecActions & zeroRewardActions, possiblyRecurrentStates); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index f27629133..0657330f2 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -35,7 +35,7 @@ namespace storm { if (dir == OptimizationDirection::Minimize) { maybeStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, stepBound); } else { - maybeStates = storm::utility::graph::performProbGreater0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, stepBound); + maybeStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates, true, stepBound); } maybeStates &= ~psiStates; STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); diff --git a/src/storm/solver/GurobiLpSolver.cpp b/src/storm/solver/GurobiLpSolver.cpp index 4cc3af6be..2754cc292 100644 --- a/src/storm/solver/GurobiLpSolver.cpp +++ b/src/storm/solver/GurobiLpSolver.cpp @@ -455,7 +455,7 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } - void GurobiLpSolver::toggleOutput(bool set) const { + void GurobiLpSolver::toggleOutput(bool) const { throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } diff --git a/src/storm/solver/SmtSolver.cpp b/src/storm/solver/SmtSolver.cpp index 50645510c..b9e2605dc 100644 --- a/src/storm/solver/SmtSolver.cpp +++ b/src/storm/solver/SmtSolver.cpp @@ -48,15 +48,15 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } - std::vector SmtSolver::allSat(std::vector const& important) { + std::vector SmtSolver::allSat(std::vector const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } - uint_fast64_t SmtSolver::allSat(std::vector const& important, std::function const& callback) { + uint_fast64_t SmtSolver::allSat(std::vector const&, std::function const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } - uint_fast64_t SmtSolver::allSat(std::vector const& important, std::function const& callback) { + uint_fast64_t SmtSolver::allSat(std::vector const&, std::function const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); } @@ -72,7 +72,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of interpolants."); } - storm::expressions::Expression SmtSolver::getInterpolant(std::vector const& groupsA) { + storm::expressions::Expression SmtSolver::getInterpolant(std::vector const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of interpolants."); } diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp index edf8a8e61..125ed2461 100644 --- a/src/storm/solver/SolverSelectionOptions.cpp +++ b/src/storm/solver/SolverSelectionOptions.cpp @@ -12,6 +12,7 @@ namespace storm { return "topological"; } + return "invalid"; } std::string toString(LpSolverType t) { @@ -21,6 +22,7 @@ namespace storm { case LpSolverType::Glpk: return "Glpk"; } + return "invalid"; } std::string toString(EquationSolverType t) { @@ -34,6 +36,7 @@ namespace storm { case EquationSolverType::Elimination: return "Elimination"; } + return "invalid"; } std::string toString(SmtSolverType t) { @@ -43,6 +46,7 @@ namespace storm { case SmtSolverType::Mathsat: return "Mathsat"; } + return "invalid"; } } } diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 765162a00..7a6e54df5 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -91,6 +91,7 @@ namespace storm { case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration: return solveEquationsPolicyIteration(dir, x, b); } + return true; } template diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index ab3b0ab48..c29b0452c 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -288,7 +288,11 @@ namespace storm { template std::vector> TopologicalMinMaxLinearEquationSolver::getOptimalGroupingFromTopologicalSccDecomposition(storm::storage::StronglyConnectedComponentDecomposition const& sccDecomposition, std::vector const& topologicalSort, storm::storage::SparseMatrix const& matrix) const { + + (void)matrix; + std::vector> result; + #ifdef STORM_HAVE_CUDA // 95% to have a bit of padding size_t const cudaFreeMemory = static_cast(getFreeCudaMemory() * 0.95); diff --git a/src/storm/solver/stateelimination/EliminatorBase.cpp b/src/storm/solver/stateelimination/EliminatorBase.cpp index 989ebc5ad..7da485d54 100644 --- a/src/storm/solver/stateelimination/EliminatorBase.cpp +++ b/src/storm/solver/stateelimination/EliminatorBase.cpp @@ -252,22 +252,22 @@ namespace storm { } template - void EliminatorBase::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { + void EliminatorBase::updateValue(storm::storage::sparse::state_type const&, ValueType const&) { // Intentionally left empty. } template - void EliminatorBase::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { + void EliminatorBase::updatePredecessor(storm::storage::sparse::state_type const&, ValueType const&, storm::storage::sparse::state_type const&) { // Intentionally left empty. } template - void EliminatorBase::updatePriority(storm::storage::sparse::state_type const& state) { + void EliminatorBase::updatePriority(storm::storage::sparse::state_type const&) { // Intentionally left empty. } template - bool EliminatorBase::filterPredecessor(storm::storage::sparse::state_type const& state) { + bool EliminatorBase::filterPredecessor(storm::storage::sparse::state_type const&) { STORM_LOG_ASSERT(false, "Must not filter predecessors."); return false; } diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 1d5291666..8794ac759 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1274,7 +1274,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void SparseMatrix::performSuccessiveOverRelaxationStep(Interval omega, std::vector& x, std::vector const& b) const { + void SparseMatrix::performSuccessiveOverRelaxationStep(Interval, std::vector&, std::vector const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported."); } #endif diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.cpp b/src/storm/storage/bisimulation/BisimulationDecomposition.cpp index cab2bfdce..e7a3fab50 100644 --- a/src/storm/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storm/storage/bisimulation/BisimulationDecomposition.cpp @@ -41,7 +41,7 @@ namespace storm { this->preserveSingleFormula(model, *formulas.front()); } else { for (auto const& formula : formulas) { - preserveFormula(model, *formula); + preserveFormula(*formula); } } } @@ -52,7 +52,7 @@ namespace storm { } template - void BisimulationDecomposition::Options::preserveFormula(ModelType const& model, storm::logic::Formula const& formula) { + void BisimulationDecomposition::Options::preserveFormula(storm::logic::Formula const& formula) { // Disable the measure driven initial partition. measureDrivenInitialPartition = false; phiStates = boost::none; diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.h b/src/storm/storage/bisimulation/BisimulationDecomposition.h index 142555bfe..6617715f7 100644 --- a/src/storm/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storm/storage/bisimulation/BisimulationDecomposition.h @@ -83,10 +83,9 @@ namespace storm { /*! * Changes the options in a way that the given formula is preserved. * - * @param model The model for which to preserve the formula. * @param formula The only formula to check. */ - void preserveFormula(ModelType const& model, storm::logic::Formula const& formula); + void preserveFormula(storm::logic::Formula const& formula); /** * Sets the bisimulation type. If the bisimulation type is set to weak, diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 8bf7a41a4..2e72e8329 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -749,7 +749,7 @@ namespace storm { } template - AddIterator Add::end(bool enumerateDontCareMetaVariables) const { + AddIterator Add::end() const { return internalAdd.end(this->getDdManager()); } @@ -786,7 +786,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template - Add Add::replaceLeaves(std::map>> const& replacementMap) const { + Add Add::replaceLeaves(std::map>> const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Not yet implemented: replaceLeaves"); } diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 2654a8c91..a0db0be76 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -610,11 +610,9 @@ namespace storm { /*! * Retrieves an iterator that points past the end of the container. * - * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even - * if a meta variable does not at all influence the the function value. * @return An iterator that points past the end of the container. */ - AddIterator end(bool enumerateDontCareMetaVariables = true) const; + AddIterator end() const; template friend std::ostream & operator<<(std::ostream& out, Add const& add); diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index b1a83d226..809d7d512 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -38,6 +38,7 @@ namespace storm { case storm::logic::ComparisonType::GreaterEqual: return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal(), value, std::placeholders::_1)); } + return Bdd(); } template diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 0dc5316ff..58d8b5bf3 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -332,7 +332,7 @@ namespace storm { } template - AddIterator InternalAdd::begin(DdManager const& fullDdManager, InternalBdd const& variableCube, uint_fast64_t numberOfDdVariables, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { + AddIterator InternalAdd::begin(DdManager const& fullDdManager, InternalBdd const&, uint_fast64_t, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { int* cube; double value; DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index ff5461296..4a23680d8 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -140,7 +140,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalBdd InternalAdd::equals(InternalAdd const& other) const { + InternalBdd InternalAdd::equals(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Equals"); } #endif @@ -152,7 +152,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalBdd InternalAdd::notEquals(InternalAdd const& other) const { + InternalBdd InternalAdd::notEquals(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Not Equals"); } #endif @@ -164,7 +164,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalBdd InternalAdd::less(InternalAdd const& other) const { + InternalBdd InternalAdd::less(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Less"); } #endif @@ -176,7 +176,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { + InternalBdd InternalAdd::lessOrEqual(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Less or Equal"); } #endif @@ -188,7 +188,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalBdd InternalAdd::greater(InternalAdd const& other) const { + InternalBdd InternalAdd::greater(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Greater"); } #endif @@ -200,7 +200,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalBdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { + InternalBdd InternalAdd::greaterOrEqual(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Greater or Equal"); } #endif @@ -212,7 +212,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::pow(InternalAdd const& other) const { + InternalAdd InternalAdd::pow(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Pow"); } #endif @@ -224,7 +224,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::mod(InternalAdd const& other) const { + InternalAdd InternalAdd::mod(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Mod"); } #endif @@ -236,7 +236,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::logxy(InternalAdd const& other) const { + InternalAdd InternalAdd::logxy(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: logxy"); } #endif @@ -272,7 +272,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::minimum(InternalAdd const& other) const { + InternalAdd InternalAdd::minimum(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Minimum"); } #endif @@ -284,13 +284,13 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::maximum(InternalAdd const& other) const { + InternalAdd InternalAdd::maximum(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Maximum"); } #endif template - InternalAdd InternalAdd::replaceLeaves(std::map>> const& replacementMap) const { + InternalAdd InternalAdd::replaceLeaves(std::map>> const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: replaceLeaves"); } @@ -337,19 +337,19 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { + InternalAdd InternalAdd::minAbstract(InternalBdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstract"); } #endif template - InternalAdd InternalAdd::minAbstractExcept0(InternalBdd const& cube) const { + InternalAdd InternalAdd::minAbstractExcept0(InternalBdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractExcept0"); } #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::minAbstractExcept0(InternalBdd const& cube) const { + InternalAdd InternalAdd::minAbstractExcept0(InternalBdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractExcept0"); } #endif @@ -366,7 +366,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { + InternalAdd InternalAdd::maxAbstract(InternalBdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: maxAbstract"); } #endif @@ -382,7 +382,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - bool InternalAdd::equalModuloPrecision(InternalAdd const& other, double precision, bool relative) const { + bool InternalAdd::equalModuloPrecision(InternalAdd const&, double, bool) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: equalModuloPrecision"); } #endif @@ -416,7 +416,7 @@ namespace storm { } template<> - InternalBdd InternalAdd::greater(storm::RationalFunction const& value) const { + InternalBdd InternalAdd::greater(storm::RationalFunction const& ) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } @@ -426,7 +426,7 @@ namespace storm { } template<> - InternalBdd InternalAdd::greaterOrEqual(storm::RationalFunction const& value) const { + InternalBdd InternalAdd::greaterOrEqual(storm::RationalFunction const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } @@ -451,7 +451,7 @@ namespace storm { } template - InternalAdd InternalAdd::restrict(InternalAdd const& constraint) const { + InternalAdd InternalAdd::restrict(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } @@ -519,7 +519,7 @@ namespace storm { } template - void InternalAdd::exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const { + void InternalAdd::exportToDot(std::string const& filename, std::vector const&) const { // Open the file, dump the DD and close it again. FILE* filePointer = fopen(filename.c_str() , "w"); this->sylvanMtbdd.PrintDot(filePointer); diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index 65c7cca7a..e6a51eb23 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -89,11 +89,11 @@ namespace storm { return sylvanBdd != other.sylvanBdd; } - InternalBdd InternalBdd::relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables, std::vector> const& columnVariables) const { + InternalBdd InternalBdd::relationalProduct(InternalBdd const& relation, std::vector> const&, std::vector> const&) const { return InternalBdd(ddManager, this->sylvanBdd.RelNext(relation.sylvanBdd, sylvan::Bdd(sylvan_false))); } - InternalBdd InternalBdd::inverseRelationalProduct(InternalBdd const& relation, std::vector> const& rowVariables, std::vector> const& columnVariables) const { + InternalBdd InternalBdd::inverseRelationalProduct(InternalBdd const& relation, std::vector> const&, std::vector> const&) const { return InternalBdd(ddManager, this->sylvanBdd.RelPrev(relation.sylvanBdd, sylvan::Bdd(sylvan_false))); } @@ -144,7 +144,7 @@ namespace storm { } InternalBdd InternalBdd::implies(InternalBdd const& other) const { - return InternalBdd(ddManager, !this->sylvanBdd | other.sylvanBdd); + return InternalBdd(ddManager, (!this->sylvanBdd) | other.sylvanBdd); } InternalBdd InternalBdd::operator!() const { @@ -230,7 +230,7 @@ namespace storm { return this->getIndex(); } - void InternalBdd::exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const { + void InternalBdd::exportToDot(std::string const& filename, std::vector const&) const { FILE* filePointer = fopen(filename.c_str() , "w"); this->sylvanBdd.PrintDot(filePointer); fclose(filePointer); diff --git a/src/storm/storage/expressions/BaseExpression.cpp b/src/storm/storage/expressions/BaseExpression.cpp index 761264074..7780351eb 100644 --- a/src/storm/storage/expressions/BaseExpression.cpp +++ b/src/storm/storage/expressions/BaseExpression.cpp @@ -40,15 +40,15 @@ namespace storm { return this->getType().isRationalType(); } - int_fast64_t BaseExpression::evaluateAsInt(Valuation const* valuation) const { + int_fast64_t BaseExpression::evaluateAsInt(Valuation const*) const { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer."); } - bool BaseExpression::evaluateAsBool(Valuation const* valuation) const { + bool BaseExpression::evaluateAsBool(Valuation const*) const { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean."); } - double BaseExpression::evaluateAsDouble(Valuation const* valuation) const { + double BaseExpression::evaluateAsDouble(Valuation const*) const { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double."); } diff --git a/src/storm/storage/expressions/BooleanLiteralExpression.cpp b/src/storm/storage/expressions/BooleanLiteralExpression.cpp index 7aea9570e..409cd4b19 100644 --- a/src/storm/storage/expressions/BooleanLiteralExpression.cpp +++ b/src/storm/storage/expressions/BooleanLiteralExpression.cpp @@ -8,7 +8,7 @@ namespace storm { // Intentionally left empty. } - bool BooleanLiteralExpression::evaluateAsBool(Valuation const* valuation) const { + bool BooleanLiteralExpression::evaluateAsBool(Valuation const*) const { return this->getValue(); } @@ -24,7 +24,7 @@ namespace storm { return this->getValue() == false; } - void BooleanLiteralExpression::gatherVariables(std::set& variables) const { + void BooleanLiteralExpression::gatherVariables(std::set&) const { return; } diff --git a/src/storm/storage/expressions/ChangeManagerVisitor.cpp b/src/storm/storage/expressions/ChangeManagerVisitor.cpp index d650131e3..d2ab51341 100644 --- a/src/storm/storage/expressions/ChangeManagerVisitor.cpp +++ b/src/storm/storage/expressions/ChangeManagerVisitor.cpp @@ -38,7 +38,7 @@ namespace storm { return std::shared_ptr(new BinaryRelationExpression(manager, expression.getType(), newFirstOperand, newSecondOperand, expression.getRelationType())); } - boost::any ChangeManagerVisitor::visit(VariableExpression const& expression, boost::any const& data) { + boost::any ChangeManagerVisitor::visit(VariableExpression const& expression, boost::any const&) { return std::shared_ptr(new VariableExpression(manager.getVariable(expression.getVariableName()))); } @@ -52,15 +52,15 @@ namespace storm { return std::shared_ptr(new UnaryNumericalFunctionExpression(manager, expression.getType(), newOperand, expression.getOperatorType())); } - boost::any ChangeManagerVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any ChangeManagerVisitor::visit(BooleanLiteralExpression const& expression, boost::any const&) { return std::shared_ptr(new BooleanLiteralExpression(manager, expression.getValue())); } - boost::any ChangeManagerVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + boost::any ChangeManagerVisitor::visit(IntegerLiteralExpression const& expression, boost::any const&) { return std::shared_ptr(new IntegerLiteralExpression(manager, expression.getValue())); } - boost::any ChangeManagerVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { + boost::any ChangeManagerVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) { return std::shared_ptr(new RationalLiteralExpression(manager, expression.getValue())); } diff --git a/src/storm/storage/expressions/IntegerLiteralExpression.cpp b/src/storm/storage/expressions/IntegerLiteralExpression.cpp index 41597bb3d..1e8a56f23 100644 --- a/src/storm/storage/expressions/IntegerLiteralExpression.cpp +++ b/src/storm/storage/expressions/IntegerLiteralExpression.cpp @@ -9,7 +9,7 @@ namespace storm { // Intentionally left empty. } - int_fast64_t IntegerLiteralExpression::evaluateAsInt(Valuation const* valuation) const { + int_fast64_t IntegerLiteralExpression::evaluateAsInt(Valuation const*) const { return this->getValue(); } @@ -21,7 +21,7 @@ namespace storm { return true; } - void IntegerLiteralExpression::gatherVariables(std::set& variables) const { + void IntegerLiteralExpression::gatherVariables(std::set&) const { return; } diff --git a/src/storm/storage/expressions/LinearCoefficientVisitor.cpp b/src/storm/storage/expressions/LinearCoefficientVisitor.cpp index d180f258d..6f3e45c80 100644 --- a/src/storm/storage/expressions/LinearCoefficientVisitor.cpp +++ b/src/storm/storage/expressions/LinearCoefficientVisitor.cpp @@ -88,11 +88,11 @@ namespace storm { return boost::any_cast(expression.getBaseExpression().accept(*this, boost::none)); } - boost::any LinearCoefficientVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { + boost::any LinearCoefficientVisitor::visit(IfThenElseExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); } - boost::any LinearCoefficientVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + boost::any LinearCoefficientVisitor::visit(BinaryBooleanFunctionExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); } @@ -114,11 +114,11 @@ namespace storm { return leftResult; } - boost::any LinearCoefficientVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { + boost::any LinearCoefficientVisitor::visit(BinaryRelationExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); } - boost::any LinearCoefficientVisitor::visit(VariableExpression const& expression, boost::any const& data) { + boost::any LinearCoefficientVisitor::visit(VariableExpression const& expression, boost::any const&) { VariableCoefficients coefficients; if (expression.getType().isNumericalType()) { coefficients.setCoefficient(expression.getVariable(), 1); @@ -128,7 +128,7 @@ namespace storm { return coefficients; } - boost::any LinearCoefficientVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + boost::any LinearCoefficientVisitor::visit(UnaryBooleanFunctionExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); } @@ -143,15 +143,15 @@ namespace storm { } } - boost::any LinearCoefficientVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any LinearCoefficientVisitor::visit(BooleanLiteralExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); } - boost::any LinearCoefficientVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + boost::any LinearCoefficientVisitor::visit(IntegerLiteralExpression const& expression, boost::any const&) { return VariableCoefficients(static_cast(expression.getValue())); } - boost::any LinearCoefficientVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { + boost::any LinearCoefficientVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) { return VariableCoefficients(expression.getValueAsDouble()); } } diff --git a/src/storm/storage/expressions/LinearityCheckVisitor.cpp b/src/storm/storage/expressions/LinearityCheckVisitor.cpp index 328d633d1..44cb70728 100644 --- a/src/storm/storage/expressions/LinearityCheckVisitor.cpp +++ b/src/storm/storage/expressions/LinearityCheckVisitor.cpp @@ -17,12 +17,12 @@ namespace storm { return result == LinearityStatus::LinearWithoutVariables || result == LinearityStatus::LinearContainsVariables; } - boost::any LinearityCheckVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { + boost::any LinearityCheckVisitor::visit(IfThenElseExpression const&, boost::any const&) { // An if-then-else expression is never linear. return LinearityStatus::NonLinear; } - boost::any LinearityCheckVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + boost::any LinearityCheckVisitor::visit(BinaryBooleanFunctionExpression const&, boost::any const&) { // Boolean function applications are not allowed in linear expressions. return LinearityStatus::NonLinear; } @@ -56,15 +56,15 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal binary numerical expression operator."); } - boost::any LinearityCheckVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { + boost::any LinearityCheckVisitor::visit(BinaryRelationExpression const&, boost::any const&) { return LinearityStatus::NonLinear; } - boost::any LinearityCheckVisitor::visit(VariableExpression const& expression, boost::any const& data) { + boost::any LinearityCheckVisitor::visit(VariableExpression const&, boost::any const&) { return LinearityStatus::LinearContainsVariables; } - boost::any LinearityCheckVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + boost::any LinearityCheckVisitor::visit(UnaryBooleanFunctionExpression const&, boost::any const&) { // Boolean function applications are not allowed in linear expressions. return LinearityStatus::NonLinear; } @@ -78,15 +78,15 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal unary numerical expression operator."); } - boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const&, boost::any const&) { return LinearityStatus::NonLinear; } - boost::any LinearityCheckVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + boost::any LinearityCheckVisitor::visit(IntegerLiteralExpression const&, boost::any const&) { return LinearityStatus::LinearWithoutVariables; } - boost::any LinearityCheckVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { + boost::any LinearityCheckVisitor::visit(RationalLiteralExpression const&, boost::any const&) { return LinearityStatus::LinearWithoutVariables; } } diff --git a/src/storm/storage/expressions/RationalLiteralExpression.cpp b/src/storm/storage/expressions/RationalLiteralExpression.cpp index 919a032a5..242489c0a 100644 --- a/src/storm/storage/expressions/RationalLiteralExpression.cpp +++ b/src/storm/storage/expressions/RationalLiteralExpression.cpp @@ -18,7 +18,7 @@ namespace storm { // Intentionally left empty. } - double RationalLiteralExpression::evaluateAsDouble(Valuation const* valuation) const { + double RationalLiteralExpression::evaluateAsDouble(Valuation const*) const { return this->getValueAsDouble(); } @@ -26,7 +26,7 @@ namespace storm { return true; } - void RationalLiteralExpression::gatherVariables(std::set& variables) const { + void RationalLiteralExpression::gatherVariables(std::set&) const { return; } diff --git a/src/storm/storage/expressions/SubstitutionVisitor.cpp b/src/storm/storage/expressions/SubstitutionVisitor.cpp index b154f6835..e835806c6 100644 --- a/src/storm/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storm/storage/expressions/SubstitutionVisitor.cpp @@ -71,7 +71,7 @@ namespace storm { } template - boost::any SubstitutionVisitor::visit(VariableExpression const& expression, boost::any const& data) { + boost::any SubstitutionVisitor::visit(VariableExpression const& expression, boost::any const&) { // If the variable is in the key set of the substitution, we need to replace it. auto const& nameExpressionPair = this->variableToExpressionMapping.find(expression.getVariable()); if (nameExpressionPair != this->variableToExpressionMapping.end()) { @@ -106,17 +106,17 @@ namespace storm { } template - boost::any SubstitutionVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any SubstitutionVisitor::visit(BooleanLiteralExpression const& expression, boost::any const&) { return expression.getSharedPointer(); } template - boost::any SubstitutionVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + boost::any SubstitutionVisitor::visit(IntegerLiteralExpression const& expression, boost::any const&) { return expression.getSharedPointer(); } template - boost::any SubstitutionVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { + boost::any SubstitutionVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) { return expression.getSharedPointer(); } diff --git a/src/storm/storage/expressions/ToCppVisitor.cpp b/src/storm/storage/expressions/ToCppVisitor.cpp index 61d4bd4db..717317d0e 100644 --- a/src/storm/storage/expressions/ToCppVisitor.cpp +++ b/src/storm/storage/expressions/ToCppVisitor.cpp @@ -271,7 +271,7 @@ namespace storm { return boost::none; } - boost::any ToCppVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any ToCppVisitor::visit(BooleanLiteralExpression const& expression, boost::any const&) { stream << std::boolalpha << expression.getValue(); return boost::none; } diff --git a/src/storm/storage/expressions/ToExprtkStringVisitor.cpp b/src/storm/storage/expressions/ToExprtkStringVisitor.cpp index a47c0f608..fe46e8ca5 100644 --- a/src/storm/storage/expressions/ToExprtkStringVisitor.cpp +++ b/src/storm/storage/expressions/ToExprtkStringVisitor.cpp @@ -166,7 +166,7 @@ namespace storm { return boost::any(); } - boost::any ToExprtkStringVisitor::visit(VariableExpression const& expression, boost::any const& data) { + boost::any ToExprtkStringVisitor::visit(VariableExpression const& expression, boost::any const&) { stream << expression.getVariableName(); return boost::any(); } @@ -202,17 +202,17 @@ namespace storm { return boost::any(); } - boost::any ToExprtkStringVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any ToExprtkStringVisitor::visit(BooleanLiteralExpression const& expression, boost::any const&) { stream << expression.getValue(); return boost::any(); } - boost::any ToExprtkStringVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + boost::any ToExprtkStringVisitor::visit(IntegerLiteralExpression const& expression, boost::any const&) { stream << expression.getValue(); return boost::any(); } - boost::any ToExprtkStringVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { + boost::any ToExprtkStringVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) { stream << expression.getValue(); return boost::any(); } diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp index 32a557ed4..9dff8b060 100644 --- a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp @@ -21,12 +21,12 @@ namespace storm { } template - boost::any ToRationalFunctionVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { + boost::any ToRationalFunctionVisitor::visit(IfThenElseExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); } template - boost::any ToRationalFunctionVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + boost::any ToRationalFunctionVisitor::visit(BinaryBooleanFunctionExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); } @@ -62,12 +62,12 @@ namespace storm { } template - boost::any ToRationalFunctionVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { + boost::any ToRationalFunctionVisitor::visit(BinaryRelationExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); } template - boost::any ToRationalFunctionVisitor::visit(VariableExpression const& expression, boost::any const& data) { + boost::any ToRationalFunctionVisitor::visit(VariableExpression const& expression, boost::any const&) { auto variablePair = variableToVariableMap.find(expression.getVariable()); if (variablePair != variableToVariableMap.end()) { return convertVariableToPolynomial(variablePair->second); @@ -79,27 +79,27 @@ namespace storm { } template - boost::any ToRationalFunctionVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + boost::any ToRationalFunctionVisitor::visit(UnaryBooleanFunctionExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); } template - boost::any ToRationalFunctionVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + boost::any ToRationalFunctionVisitor::visit(UnaryNumericalFunctionExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); } template - boost::any ToRationalFunctionVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any ToRationalFunctionVisitor::visit(BooleanLiteralExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); } template - boost::any ToRationalFunctionVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + boost::any ToRationalFunctionVisitor::visit(IntegerLiteralExpression const& expression, boost::any const&) { return RationalFunctionType(carl::rationalize(static_cast(expression.getValue()))); } template - boost::any ToRationalFunctionVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { + boost::any ToRationalFunctionVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) { return storm::utility::convertNumber(expression.getValue()); } diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp index 441913fd5..4ff7db433 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp @@ -18,12 +18,12 @@ namespace storm { } template - boost::any ToRationalNumberVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { + boost::any ToRationalNumberVisitor::visit(IfThenElseExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template - boost::any ToRationalNumberVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + boost::any ToRationalNumberVisitor::visit(BinaryBooleanFunctionExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } @@ -63,32 +63,33 @@ namespace storm { } template - boost::any ToRationalNumberVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { + boost::any ToRationalNumberVisitor::visit(BinaryRelationExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template - boost::any ToRationalNumberVisitor::visit(VariableExpression const& expression, boost::any const& data) { + boost::any ToRationalNumberVisitor::visit(VariableExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot transform expressions containing variables to a rational number."); } template - boost::any ToRationalNumberVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + boost::any ToRationalNumberVisitor::visit(UnaryBooleanFunctionExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template - boost::any ToRationalNumberVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + boost::any ToRationalNumberVisitor::visit(UnaryNumericalFunctionExpression const&, boost::any const& ) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template - boost::any ToRationalNumberVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any ToRationalNumberVisitor::visit(BooleanLiteralExpression const&, boost::any const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template - boost::any ToRationalNumberVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + boost::any ToRationalNumberVisitor::visit(IntegerLiteralExpression const& expression, boost::any const&) { + (void)expression; #ifdef STORM_HAVE_CARL return RationalNumberType(carl::rationalize(static_cast(expression.getValue()))); #else @@ -97,7 +98,8 @@ namespace storm { } template - boost::any ToRationalNumberVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { + boost::any ToRationalNumberVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) { + (void)expression; #ifdef STORM_HAVE_CARL return expression.getValue(); #else diff --git a/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp b/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp index a6906ac8a..3e3da7650 100644 --- a/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp +++ b/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp @@ -31,7 +31,7 @@ namespace storm { return resultPredicates; } - boost::any VariableSetPredicateSplitter::visit(IfThenElseExpression const& expression, boost::any const& data) { + boost::any VariableSetPredicateSplitter::visit(IfThenElseExpression const& expression, boost::any const&) { std::set conditionVariables; expression.getCondition()->gatherVariables(conditionVariables); bool conditionOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), conditionVariables.begin(), conditionVariables.end()); @@ -103,11 +103,11 @@ namespace storm { return boost::any(); } - boost::any VariableSetPredicateSplitter::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + boost::any VariableSetPredicateSplitter::visit(BinaryNumericalFunctionExpression const& expression, boost::any const&) { return boost::any(); } - boost::any VariableSetPredicateSplitter::visit(BinaryRelationExpression const& expression, boost::any const& data) { + boost::any VariableSetPredicateSplitter::visit(BinaryRelationExpression const& expression, boost::any const&) { std::set leftContainedVariables; expression.getFirstOperand()->gatherVariables(leftContainedVariables); bool leftOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), leftContainedVariables.begin(), leftContainedVariables.end()); @@ -132,7 +132,7 @@ namespace storm { return boost::any(); } - boost::any VariableSetPredicateSplitter::visit(VariableExpression const& expression, boost::any const& data) { + boost::any VariableSetPredicateSplitter::visit(VariableExpression const& expression, boost::any const&) { if (expression.hasBooleanType() && irrelevantVariables.find(expression.getVariable()) == irrelevantVariables.end()) { resultPredicates.push_back(expression.toExpression()); } @@ -160,19 +160,19 @@ namespace storm { return boost::any(); } - boost::any VariableSetPredicateSplitter::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + boost::any VariableSetPredicateSplitter::visit(UnaryNumericalFunctionExpression const&, boost::any const&) { return boost::any(); } - boost::any VariableSetPredicateSplitter::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any VariableSetPredicateSplitter::visit(BooleanLiteralExpression const&, boost::any const&) { return boost::any(); } - boost::any VariableSetPredicateSplitter::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + boost::any VariableSetPredicateSplitter::visit(IntegerLiteralExpression const&, boost::any const&) { return boost::any(); } - boost::any VariableSetPredicateSplitter::visit(RationalLiteralExpression const& expression, boost::any const& data) { + boost::any VariableSetPredicateSplitter::visit(RationalLiteralExpression const&, boost::any const&) { return boost::any(); } diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 889496265..ea6de1ba2 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -43,7 +43,7 @@ namespace storm { return boost::any_cast(comp.accept(visitor, boost::none)); } - virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) { + virtual boost::any visit(AutomatonComposition const& composition, boost::any const&) { modernjson::json compDecl; modernjson::json autDecl; autDecl["automaton"] = composition.getAutomatonName(); @@ -63,7 +63,7 @@ namespace storm { elemDecl["automaton"] = std::static_pointer_cast(subcomp)->getAutomatonName(); } else { STORM_LOG_THROW(allowRecursion, storm::exceptions::InvalidJaniException, "Nesting composition " << *subcomp << " is not supported by JANI."); - elemDecl = boost::any_cast(subcomp->accept(*this, boost::none)); + elemDecl = boost::any_cast(subcomp->accept(*this, data)); } elems.push_back(elemDecl); } @@ -144,11 +144,11 @@ namespace storm { return boost::any_cast(formula.accept(translator)); } - boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const { + boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const&) const { return ExpressionToJson::translate(f.getExpression()); } - boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const { + boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const&) const { modernjson::json opDecl(f.getLabel()); return opDecl; } @@ -156,19 +156,19 @@ namespace storm { modernjson::json opDecl; storm::logic::BinaryBooleanStateFormula::OperatorType op = f.getOperator(); opDecl["op"] = op == storm::logic::BinaryBooleanStateFormula::OperatorType::And ? "∧" : "∨"; - opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, boost::none)); - opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, boost::none)); + opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, data)); + opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, data)); return opDecl; } - boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const { + boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const&) const { modernjson::json opDecl(f.isTrueFormula() ? true : false); return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const { modernjson::json opDecl; opDecl["op"] = "U"; - opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, boost::none)); - opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, boost::none)); + opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, data)); + opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, data)); if(f.hasDiscreteTimeBound()) { opDecl["step-bounds"] = constructPropertyInterval(0, f.getDiscreteTimeBound()); } else { @@ -177,19 +177,19 @@ namespace storm { return opDecl; } - boost::any FormulaToJaniJson::visit(storm::logic::ConditionalFormula const& f, boost::any const& data) const { + boost::any FormulaToJaniJson::visit(storm::logic::ConditionalFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); } - boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const { + boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm currently does not support translating cummulative reward formulae"); } boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const { modernjson::json opDecl; opDecl["op"] = "U"; - opDecl["left"] = boost::any_cast(f.getTrueFormula()->accept(*this, boost::none)); - opDecl["right"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["left"] = boost::any_cast(f.getTrueFormula()->accept(*this, data)); + opDecl["right"] = boost::any_cast(f.getSubformula().accept(*this, data)); return opDecl; } @@ -202,10 +202,10 @@ namespace storm { opDecl["op"] = comparisonTypeToJani(bound.comparisonType); if(f.hasOptimalityType()) { opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; - opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().accept(*this, data)); } else { opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin"; - opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().accept(*this, data)); } opDecl["left"]["exp"] = modernjson::json(1); opDecl["left"]["accumulate"] = modernjson::json(tvec); @@ -213,12 +213,12 @@ namespace storm { } else { if(f.hasOptimalityType()) { opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; - opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, data)); } else { // TODO add checks opDecl["op"] = "Emin"; - opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, data)); } opDecl["exp"] = modernjson::json(1); opDecl["accumulate"] = modernjson::json(tvec); @@ -226,11 +226,11 @@ namespace storm { return opDecl; } - boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const { + boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a globally formulae"); } - boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const { + boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an instanteneous reward formula"); } @@ -241,21 +241,21 @@ namespace storm { opDecl["op"] = comparisonTypeToJani(bound.comparisonType); if(f.hasOptimalityType()) { opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; - opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, data)); } else { opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Smax" : "Smin"; - opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, data)); } opDecl["right"] = numberToJson(bound.threshold); } else { if(f.hasOptimalityType()) { opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; - opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, data)); } else { // TODO add checks opDecl["op"] = "Pmin"; - opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, data)); } } return opDecl; @@ -292,15 +292,15 @@ namespace storm { } - boost::any FormulaToJaniJson::visit(storm::logic::MultiObjectiveFormula const& f, boost::any const& data) const { + boost::any FormulaToJaniJson::visit(storm::logic::MultiObjectiveFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a multi-objective formula"); } boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const { modernjson::json opDecl; opDecl["op"] = "U"; - opDecl["left"] = boost::any_cast(f.getTrueFormula()->accept(*this, boost::none)); - opDecl["right"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["left"] = boost::any_cast(f.getTrueFormula()->accept(*this, data)); + opDecl["right"] = boost::any_cast(f.getSubformula().accept(*this, data)); opDecl["step-bounds"] = constructPropertyInterval((uint64_t)1, (uint64_t)1); return opDecl; } @@ -316,21 +316,21 @@ namespace storm { opDecl["op"] = comparisonTypeToJani(bound.comparisonType); if(f.hasOptimalityType()) { opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax"; - opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, data)); } else { opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Pmax" : "Pmin"; - opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, data)); } opDecl["right"] = numberToJson(bound.threshold); } else { if(f.hasOptimalityType()) { opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax"; - opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, data)); } else { // TODO add checks opDecl["op"] = "Pmin"; - opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, data)); } } return opDecl; @@ -349,10 +349,10 @@ namespace storm { opDecl["op"] = comparisonTypeToJani(bound.comparisonType); if(f.hasOptimalityType()) { opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; - opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, boost::none)); + opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); } else { opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin"; - opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, boost::none)); + opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); } STORM_LOG_THROW(f.hasRewardModelName(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion"); opDecl["left"]["exp"] = f.getRewardModelName(); @@ -361,12 +361,12 @@ namespace storm { } else { if(f.hasOptimalityType()) { opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; - opDecl["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, boost::none)); + opDecl["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); } else { // TODO add checks opDecl["op"] = "Emin"; - opDecl["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, boost::none)); + opDecl["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); } STORM_LOG_THROW(f.hasRewardModelName(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion"); opDecl["exp"] = f.getRewardModelName(); @@ -375,7 +375,7 @@ namespace storm { return opDecl; } - boost::any FormulaToJaniJson::visit(storm::logic::TotalRewardFormula const& f, boost::any const& data) const { + boost::any FormulaToJaniJson::visit(storm::logic::TotalRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support a total reward formula"); } @@ -385,15 +385,15 @@ namespace storm { storm::logic::UnaryBooleanStateFormula::OperatorType op = f.getOperator(); assert(op == storm::logic::UnaryBooleanStateFormula::OperatorType::Not); opDecl["op"] = "¬"; - opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, data)); return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const { modernjson::json opDecl; opDecl["op"] = "U"; - opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, boost::none)); - opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, boost::none)); + opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, data)); + opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, data)); return opDecl; } @@ -459,54 +459,54 @@ namespace storm { boost::any ExpressionToJson::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) { modernjson::json opDecl; opDecl["op"] = "ite"; - opDecl["if"] = boost::any_cast(expression.getCondition()->accept(*this, boost::none)); - opDecl["then"] = boost::any_cast(expression.getThenExpression()->accept(*this, boost::none)); - opDecl["else"] = boost::any_cast(expression.getElseExpression()->accept(*this, boost::none)); + opDecl["if"] = boost::any_cast(expression.getCondition()->accept(*this, data)); + opDecl["then"] = boost::any_cast(expression.getThenExpression()->accept(*this, data)); + opDecl["else"] = boost::any_cast(expression.getElseExpression()->accept(*this, data)); return opDecl; } boost::any ExpressionToJson::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) { modernjson::json opDecl; opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); - opDecl["left"] = boost::any_cast(expression.getOperand(0)->accept(*this, boost::none)); - opDecl["right"] = boost::any_cast(expression.getOperand(1)->accept(*this, boost::none)); + opDecl["left"] = boost::any_cast(expression.getOperand(0)->accept(*this, data)); + opDecl["right"] = boost::any_cast(expression.getOperand(1)->accept(*this, data)); return opDecl; } boost::any ExpressionToJson::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) { modernjson::json opDecl; opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); - opDecl["left"] = boost::any_cast(expression.getOperand(0)->accept(*this, boost::none)); - opDecl["right"] = boost::any_cast(expression.getOperand(1)->accept(*this, boost::none)); + opDecl["left"] = boost::any_cast(expression.getOperand(0)->accept(*this, data)); + opDecl["right"] = boost::any_cast(expression.getOperand(1)->accept(*this, data)); return opDecl; } boost::any ExpressionToJson::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) { modernjson::json opDecl; opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); - opDecl["left"] = boost::any_cast(expression.getOperand(0)->accept(*this, boost::none)); - opDecl["right"] = boost::any_cast(expression.getOperand(1)->accept(*this, boost::none)); + opDecl["left"] = boost::any_cast(expression.getOperand(0)->accept(*this, data)); + opDecl["right"] = boost::any_cast(expression.getOperand(1)->accept(*this, data)); return opDecl; } - boost::any ExpressionToJson::visit(storm::expressions::VariableExpression const& expression, boost::any const& data) { + boost::any ExpressionToJson::visit(storm::expressions::VariableExpression const& expression, boost::any const&) { return modernjson::json(expression.getVariableName()); } boost::any ExpressionToJson::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) { modernjson::json opDecl; opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); - opDecl["exp"] = boost::any_cast(expression.getOperand()->accept(*this, boost::none)); + opDecl["exp"] = boost::any_cast(expression.getOperand()->accept(*this, data)); return opDecl; } boost::any ExpressionToJson::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) { modernjson::json opDecl; opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); - opDecl["exp"] = boost::any_cast(expression.getOperand()->accept(*this, boost::none)); + opDecl["exp"] = boost::any_cast(expression.getOperand()->accept(*this, data)); return opDecl; } - boost::any ExpressionToJson::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any ExpressionToJson::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) { return modernjson::json(expression.getValue()); } - boost::any ExpressionToJson::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) { + boost::any ExpressionToJson::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) { return modernjson::json(expression.getValue()); } - boost::any ExpressionToJson::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) { + boost::any ExpressionToJson::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) { return modernjson::json(expression.getValueAsDouble()); } diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index d13c823ca..53d3e84dc 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -282,14 +282,7 @@ namespace storm { conditionalMetaEdge.components = components; // Set the action index. - conditionalMetaEdge.actionIndex = Model::SILENT_ACTION_INDEX; - if (vector.getOutput() != Model::SILENT_ACTION_NAME) { - if (newModel.hasAction(vector.getOutput())) { - conditionalMetaEdge.actionIndex = newModel.getActionIndex(vector.getOutput()); - } else { - conditionalMetaEdge.actionIndex = newModel.addAction(Action(vector.getOutput())); - } - } + conditionalMetaEdge.actionIndex = resultingActionIndex; result.push_back(conditionalMetaEdge); @@ -321,7 +314,7 @@ namespace storm { } } - void addEdgesToReachableLocations(Model const& model, std::vector> const& composedAutomata, Automaton& newAutomaton, std::vector const& conditionalMetaEdges) { + void addEdgesToReachableLocations(std::vector> const& composedAutomata, Automaton& newAutomaton, std::vector const& conditionalMetaEdges) { // Maintain a stack of locations that still need to be to explored. std::vector> locationsToExplore; @@ -507,7 +500,7 @@ namespace storm { // Now that all meta edges have been built, we can explore the location space and add all edges based // on the templates. - addEdgesToReachableLocations(*this, composedAutomata, newAutomaton, conditionalMetaEdges); + addEdgesToReachableLocations(composedAutomata, newAutomaton, conditionalMetaEdges); // Fix all variables mentioned in assignments by applying the constructed remapping. newAutomaton.changeAssignmentVariables(variableRemapping); diff --git a/src/storm/storage/jani/ModelType.cpp b/src/storm/storage/jani/ModelType.cpp index f131f313e..287a48953 100644 --- a/src/storm/storage/jani/ModelType.cpp +++ b/src/storm/storage/jani/ModelType.cpp @@ -36,6 +36,7 @@ namespace storm { case ModelType::SHA: return "sha"; } + return "invalid"; } ModelType getModelType(std::string const& input) { diff --git a/src/storm/storage/prism/BooleanVariable.cpp b/src/storm/storage/prism/BooleanVariable.cpp index e51cdb589..4207f91fb 100644 --- a/src/storm/storage/prism/BooleanVariable.cpp +++ b/src/storm/storage/prism/BooleanVariable.cpp @@ -4,7 +4,7 @@ namespace storm { namespace prism { - BooleanVariable::BooleanVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, false, filename, lineNumber) { + BooleanVariable::BooleanVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, filename, lineNumber) { // Nothing to do here. } diff --git a/src/storm/storage/prism/CompositionToJaniVisitor.cpp b/src/storm/storage/prism/CompositionToJaniVisitor.cpp index 43f777936..01988020a 100644 --- a/src/storm/storage/prism/CompositionToJaniVisitor.cpp +++ b/src/storm/storage/prism/CompositionToJaniVisitor.cpp @@ -13,7 +13,7 @@ namespace storm { return result; } - boost::any CompositionToJaniVisitor::visit(ModuleComposition const& composition, boost::any const& data) { + boost::any CompositionToJaniVisitor::visit(ModuleComposition const& composition, boost::any const&) { std::shared_ptr result = std::make_shared(composition.getModuleName()); return result; } diff --git a/src/storm/storage/prism/IntegerVariable.cpp b/src/storm/storage/prism/IntegerVariable.cpp index 0101cf72c..5a67dd1bd 100644 --- a/src/storm/storage/prism/IntegerVariable.cpp +++ b/src/storm/storage/prism/IntegerVariable.cpp @@ -2,7 +2,7 @@ namespace storm { namespace prism { - IntegerVariable::IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, false, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) { + IntegerVariable::IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) { // Intentionally left empty. } diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 75fe1181f..bc44cf59b 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -40,7 +40,7 @@ namespace storm { } } - virtual boost::any visit(ModuleComposition const& composition, boost::any const& data) override { + virtual boost::any visit(ModuleComposition const& composition, boost::any const&) override { bool isValid = program.hasModule(composition.getModuleName()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "The module \"" << composition.getModuleName() << "\" referred to in the system composition does not exist."); isValid = appearingModules.find(composition.getModuleName()) == appearingModules.end(); diff --git a/src/storm/storage/prism/Variable.cpp b/src/storm/storage/prism/Variable.cpp index 2bdd7ba08..656b9566f 100644 --- a/src/storm/storage/prism/Variable.cpp +++ b/src/storm/storage/prism/Variable.cpp @@ -5,7 +5,7 @@ namespace storm { namespace prism { - Variable::Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), initialValueExpression(initialValueExpression) { + Variable::Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), initialValueExpression(initialValueExpression) { // Nothing to do here. } diff --git a/src/storm/storage/prism/Variable.h b/src/storm/storage/prism/Variable.h index 795707030..3d379cd25 100644 --- a/src/storm/storage/prism/Variable.h +++ b/src/storm/storage/prism/Variable.h @@ -77,12 +77,10 @@ namespace storm { * * @param variable The associated expression variable. * @param initialValueExpression The constant expression that defines the initial value of the variable. - * @param hasDefaultInitialValue A flag indicating whether the initial value of the variable is its default - * value. * @param filename The filename in which the variable is defined. * @param lineNumber The line number in which the variable is defined. */ - Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename = "", uint_fast64_t lineNumber = 0); + Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Creates a copy of the given variable and performs the provided renaming. diff --git a/src/storm/utility/ConstantsComparator.cpp b/src/storm/utility/ConstantsComparator.cpp index 4d4486872..d212d8874 100644 --- a/src/storm/utility/ConstantsComparator.cpp +++ b/src/storm/utility/ConstantsComparator.cpp @@ -31,7 +31,7 @@ namespace storm { } template - bool ConstantsComparator::isInfinity(ValueType const& value) const { + bool ConstantsComparator::isInfinity(ValueType const&) const { return false; } @@ -60,7 +60,7 @@ namespace storm { return std::abs(value1 - value2) <= precision; } - bool ConstantsComparator::isConstant(float const& value) const { + bool ConstantsComparator::isConstant(float const&) const { return true; } @@ -96,7 +96,7 @@ namespace storm { return std::abs(value1 - value2) <= precision; } - bool ConstantsComparator::isConstant(double const& value) const { + bool ConstantsComparator::isConstant(double const&) const { return true; } diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 22954dc65..b29ed4da1 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -39,7 +39,7 @@ namespace storm { } template - bool isConstant(ValueType const& a) { + bool isConstant(ValueType const&) { return true; } @@ -47,7 +47,7 @@ namespace storm { bool isInteger(ValueType const& number) { ValueType iPart; ValueType result = std::modf(number, &iPart); - return result = zero(); + return result == zero(); } template @@ -56,12 +56,12 @@ namespace storm { } template<> - bool isInteger(int const& number) { + bool isInteger(int const&) { return true; } template<> - bool isInteger(uint_fast64_t const& number) { + bool isInteger(uint_fast64_t const&) { return true; } @@ -196,8 +196,7 @@ namespace storm { } template<> - storm::RationalFunction minimum(std::vector const& values) - { + storm::RationalFunction minimum(std::vector const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined"); } @@ -214,12 +213,10 @@ namespace storm { } template<> - storm::RationalFunction maximum(std::vector const& values) - { + storm::RationalFunction maximum(std::vector const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); } - template ValueType maximum(std::vector const& values) { assert(!values.empty()); @@ -233,8 +230,7 @@ namespace storm { } template<> - storm::RationalFunction minimum(std::map const& values) - { + storm::RationalFunction minimum(std::map const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined"); } @@ -251,12 +247,10 @@ namespace storm { } template<> - storm::RationalFunction maximum(std::map const& values) - { + storm::RationalFunction maximum(std::map const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); } - template ValueType maximum(std::map const& values) { assert(!values.empty()); diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index fc4972da2..f219cd9a5 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -102,48 +102,6 @@ namespace storm { return result; } - template - storm::storage::BitVector getTerminalStateCover(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates) { - storm::storage::BitVector terminalStateCandidates(transitionMatrix.getRowGroupCount()); - storm::storage::BitVector terminalStatesWithoutSuccessors(transitionMatrix.getRowCount()); - - std::queue stateQueue; - storm::storage::BitVector statesInQueue(transitionMatrix.getRowGroupCount()); - - for (auto const& initialState : initialStates) { - stateQueue.emplace(initialState); - statesInQueue.set(initialState); - } - - // Perform a BFS. - while (!stateQueue.empty()) { - storm::storage::sparse::state_type currentState = stateQueue.front(); - stateQueue.pop(); - - auto row = transitionMatrix.getRow(currentState); - if (row.empty()) { - terminalStatesWithoutSuccessors.set(currentState); - } else { - bool hasUnvisitedSuccessor = false; - for (auto const& successorEntry : row) { - if (!statesInQueue.get(successorEntry.getColumn())) { - hasUnvisitedSuccessor = true; - stateQueue.emplace(successorEntry.getColumn()); - statesInQueue.set(successorEntry.getColumn()); - } - } - if (!hasUnvisitedSuccessor) { - terminalStateCandidates.set(currentState); - } - } - } - - // Now that we have an overapproximation of the set of states we want to compute, we check whether we - // need to include some of the states that are terminal state candidates or whether the terminal states - // without successors are sufficient. - - } - template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem) { std::vector distances(transitionMatrix.getRowGroupCount()); @@ -292,7 +250,7 @@ namespace storm { } template - storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0) { + storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const&, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0) { storm::dd::Bdd statesWithProbability1 = performProbGreater0(model, transitionMatrix, !psiStates && model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates()); statesWithProbability1 = !statesWithProbability1 && model.getReachableStates(); return statesWithProbability1; @@ -467,7 +425,7 @@ namespace storm { } template - storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps) { + storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps) { size_t numberOfStates = phiStates.size(); // Prepare resulting bit vector. @@ -524,15 +482,15 @@ namespace storm { } template - storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - storm::storage::BitVector statesWithProbability0 = performProbGreater0E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); + storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector statesWithProbability0 = performProbGreater0E(backwardTransitions, phiStates, psiStates); statesWithProbability0.complement(); return statesWithProbability0; } template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - return performProb0A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates); + return performProb0A(backwardTransitions, phiStates, psiStates); } template @@ -605,7 +563,7 @@ namespace storm { std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; - result.first = performProb0A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); + result.first = performProb0A(backwardTransitions, phiStates, psiStates); result.second = performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); return result; } @@ -1225,9 +1183,9 @@ namespace storm { template storm::storage::PartialScheduler computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; - template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); #ifdef STORM_HAVE_CARL @@ -1293,9 +1251,9 @@ namespace storm { - template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; - template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; @@ -1351,9 +1309,9 @@ namespace storm { template storm::storage::PartialScheduler computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; - template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; @@ -1402,9 +1360,9 @@ namespace storm { - template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; - template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index eaf57f034..63b7ead8b 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -291,7 +291,6 @@ namespace storm { * this means that these states have a probability greater 0 of satisfying phi until psi if the * scheduler tries to minimize this probability. * - * @param model The model whose graph structure to search. * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. @@ -300,10 +299,10 @@ namespace storm { * @return A bit vector that represents all states with probability 0. */ template - storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; + storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; template - storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); /*! * Computes the sets of states that have probability 0 of satisfying phi until psi under all diff --git a/src/storm/utility/numerical.h b/src/storm/utility/numerical.h index e8b8dfbd2..bf9a533b4 100644 --- a/src/storm/utility/numerical.h +++ b/src/storm/utility/numerical.h @@ -11,7 +11,7 @@ namespace storm { namespace utility { namespace numerical { template - std::tuple> getFoxGlynnCutoff(ValueType lambda, ValueType underflow, ValueType overflow, ValueType accuracy) { + std::tuple> getFoxGlynnCutoff(ValueType lambda, ValueType overflow, ValueType accuracy) { STORM_LOG_THROW(lambda != storm::utility::zero(), storm::exceptions::InvalidArgumentException, "Error in Fox-Glynn algorithm: lambda must not be zero."); // This code is a modified version of the one in PRISM. According to their implementation, for lambda diff --git a/src/storm/utility/shortestPaths.cpp b/src/storm/utility/shortestPaths.cpp index 7912f15ee..1bd11f8aa 100644 --- a/src/storm/utility/shortestPaths.cpp +++ b/src/storm/utility/shortestPaths.cpp @@ -2,9 +2,11 @@ #include #include -#include "macros.h" -#include "shortestPaths.h" -#include "graph.h" +#include "storm/utility/macros.h" +#include "storm/utility/shortestPaths.h" +#include "storm/utility/graph.h" + +#include "storm/models/sparse/StandardRewardModel.h" // FIXME: I've accidentally used k=0 *twice* now without realizing that k>=1 is required! // Accessing zero should trigger a warning! diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index eeabcbd64..a9357e42f 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -203,21 +203,25 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { #ifdef STORM_HAVE_MSAT -#include "src/abstraction/prism/PrismMenuGameAbstractor.h" +#include "storm/abstraction/MenuGameRefiner.h" +#include "storm/abstraction/prism/PrismMenuGameAbstractor.h" -#include "src/storage/expressions/Expression.h" +#include "storm/storage/expressions/Expression.h" -#include "src/utility/solver.h" +#include "storm/utility/solver.h" TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); + auto smtSolverFactory = std::make_shared(); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, smtSolverFactory); + storm::abstraction::MenuGameRefiner refiner(abstractor, smtSolverFactory->create(manager)); + refiner.refine(initialPredicates); storm::abstraction::MenuGame game = abstractor.abstract(); @@ -252,7 +256,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { EXPECT_TRUE(result.hasPlayer1Strategy()); EXPECT_TRUE(result.hasPlayer2Strategy()); - abstractor.refine({manager.getVariableExpression("s") < manager.integer(2)}); + refiner.refine({manager.getVariableExpression("s") < manager.integer(2)}); game = abstractor.abstract(); // We need to create a new BDD for the target states since the reachable states might have changed. @@ -312,7 +316,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { } TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_unique()); @@ -353,8 +357,11 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5)); initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6)); - storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - + auto smtSolverFactory = std::make_shared(); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, smtSolverFactory); + storm::abstraction::MenuGameRefiner refiner(abstractor, smtSolverFactory->create(manager)); + refiner.refine(initialPredicates); + storm::abstraction::MenuGame game = abstractor.abstract(); // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 1. @@ -413,7 +420,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { } TEST(GraphTest, SymbolicProb01StochasticGameWlan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_unique()); @@ -522,8 +529,11 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) { initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0)); initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1)); - storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, initialPredicates, std::make_shared(), false); - + auto smtSolverFactory = std::make_shared(); + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(program, smtSolverFactory); + storm::abstraction::MenuGameRefiner refiner(abstractor, smtSolverFactory->create(manager)); + refiner.refine(initialPredicates); + storm::abstraction::MenuGame game = abstractor.abstract(); // The target states are those states where col == 2.