diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 2af7fed58..a397b0de0 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -32,12 +32,9 @@ namespace storm { template class DdPrismModelBuilder::GenerationInformation { public: - GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared>())), columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() { + GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared>())), columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() { // Initializes variables and identity DDs. createMetaVariablesAndIdentities(); - - rowExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToRowMetaVariableMap)); - columnExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToColumnMetaVariableMap)); } // The program that is currently translated. @@ -49,12 +46,12 @@ namespace storm { // The meta variables for the row encoding. std::set rowMetaVariables; std::shared_ptr> variableToRowMetaVariableMap; - std::shared_ptr> rowExpressionAdapter; + std::shared_ptr> rowExpressionAdapter; // The meta variables for the column encoding. std::set columnMetaVariables; std::shared_ptr> variableToColumnMetaVariableMap; - std::shared_ptr> columnExpressionAdapter; + std::shared_ptr> columnExpressionAdapter; // All pairs of row/column meta variables. std::vector> rowColumnMetaVariablePairs; @@ -794,7 +791,7 @@ namespace storm { } } - result.setValue(metaVariableNameToValueMap, 1); + result.setValue(metaVariableNameToValueMap, ValueType(1)); return result; } @@ -835,7 +832,7 @@ namespace storm { for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { // Determine the set of states with exactly currentChoices choices. - equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(static_cast(currentChoices))); + equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(ValueType(currentChoices))); // If there is no such state, continue with the next possible number of choices. if (equalsNumberOfChoicesDd.isZero()) { @@ -1110,7 +1107,7 @@ namespace storm { } template - storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd) { + storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd) { // Start by creating the state reward vector. boost::optional> stateRewards; @@ -1222,7 +1219,7 @@ namespace storm { } } - return storm::models::symbolic::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards); + return storm::models::symbolic::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards); } template @@ -1394,7 +1391,7 @@ namespace storm { selectedRewardModels.push_back(preparedProgram->getRewardModel(0)); } - std::unordered_map> rewardModels; + std::unordered_map> rewardModels; for (auto const& rewardModel : selectedRewardModels) { rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, transitionMatrix, reachableStatesAdd, stateActionDd)); } @@ -1406,11 +1403,11 @@ namespace storm { } if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { - return std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); } else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) { - return std::shared_ptr>(new storm::models::symbolic::Ctmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Ctmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels)); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); } diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 0cb8cc6fd..6db0c4639 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -238,7 +238,7 @@ namespace storm { static storm::dd::Add createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); - static storm::models::symbolic::StandardRewardModel createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd); + static storm::models::symbolic::StandardRewardModel createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd); static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo); diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp index c8fd2aa8f..823d3a884 100644 --- a/src/models/sparse/StandardRewardModel.cpp +++ b/src/models/sparse/StandardRewardModel.cpp @@ -248,7 +248,13 @@ namespace storm { if(hasStateRewards() && !std::all_of(getStateRewardVector().begin(), getStateRewardVector().end(), storm::utility::isZero)) { return false; } - return !(static_cast(this->optionalStateRewardVector) || static_cast(this->optionalStateActionRewardVector) || static_cast(this->optionalTransitionRewardMatrix)); + if(hasStateActionRewards() && !std::all_of(getStateActionRewardVector().begin(), getStateActionRewardVector().end(), storm::utility::isZero)) { + return false; + } + if(hasTransitionRewards() && !std::all_of(getTransitionRewardMatrix().begin(), getTransitionRewardMatrix().end(), [](storm::storage::MatrixEntry entry){ return storm::utility::isZero(entry.getValue()); })) { + return false; + } + return true; } diff --git a/src/models/symbolic/Ctmc.cpp b/src/models/symbolic/Ctmc.cpp index 2f1e65aec..1c612d090 100644 --- a/src/models/symbolic/Ctmc.cpp +++ b/src/models/symbolic/Ctmc.cpp @@ -23,7 +23,7 @@ namespace storm { std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { + : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { exitRates = this->getTransitionMatrix().sumAbstract(this->getColumnVariables()); } diff --git a/src/models/symbolic/DeterministicModel.cpp b/src/models/symbolic/DeterministicModel.cpp index 66f97bc87..6824357d6 100644 --- a/src/models/symbolic/DeterministicModel.cpp +++ b/src/models/symbolic/DeterministicModel.cpp @@ -24,7 +24,7 @@ namespace storm { std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { + : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { // Intentionally left empty. } @@ -34,4 +34,4 @@ namespace storm { } // namespace symbolic } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/symbolic/Dtmc.cpp b/src/models/symbolic/Dtmc.cpp index a9483862f..6f63ff394 100644 --- a/src/models/symbolic/Dtmc.cpp +++ b/src/models/symbolic/Dtmc.cpp @@ -33,4 +33,4 @@ namespace storm { } // namespace symbolic } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/symbolic/Mdp.cpp b/src/models/symbolic/Mdp.cpp index 70017195a..f438e6f1d 100644 --- a/src/models/symbolic/Mdp.cpp +++ b/src/models/symbolic/Mdp.cpp @@ -34,4 +34,4 @@ namespace storm { } // namespace symbolic } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 25bc5404b..16339c0d1 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -249,4 +249,4 @@ namespace storm { } // namespace symbolic } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/symbolic/StandardRewardModel.cpp b/src/models/symbolic/StandardRewardModel.cpp index 4ec405405..1342abb3d 100644 --- a/src/models/symbolic/StandardRewardModel.cpp +++ b/src/models/symbolic/StandardRewardModel.cpp @@ -155,4 +155,4 @@ namespace storm { template class StandardRewardModel; } } -} \ No newline at end of file +} diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 81705d431..d7676c973 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -256,7 +256,7 @@ namespace storm { void BitVector::enlargeLiberally(uint_fast64_t minimumLength, bool init) { if(minimumLength > this->size()) { uint_fast64_t newLength = this->bucketCount(); - newLength = std::max(newLength, 1ull) << 6; + newLength = std::max(newLength, static_cast(1u)) << 6; while(newLength < minimumLength) { newLength = newLength << 1; } diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index c117b0628..a1eea43dc 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -74,7 +74,7 @@ namespace storm { } } - for (auto state = 0; state < this->model.getNumberOfStates(); ++state) { + for (decltype(this->model.getNumberOfStates()) state = 0; state < this->model.getNumberOfStates(); ++state) { updateOrderedQuotientDistributions(state); } } @@ -248,7 +248,7 @@ namespace storm { template bool NondeterministicModelBisimulationDecomposition::checkQuotientDistributions() const { std::vector nondeterministicChoiceIndices = this->model.getTransitionMatrix().getRowGroupIndices(); - for (auto state = 0; state < this->model.getNumberOfStates(); ++state) { + for (decltype(this->model.getNumberOfStates()) state = 0; state < this->model.getNumberOfStates(); ++state) { for (auto choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { storm::storage::Distribution distribution; for (auto const& element : this->model.getTransitionMatrix().getRow(choice)) { diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index bcff0e3da..a6cb3daac 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -767,4 +767,4 @@ namespace storm { template class Add; template class Add; } -} \ No newline at end of file +} diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 0925b4f58..393e8d262 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -596,4 +596,4 @@ namespace storm { template class InternalAdd; template class InternalAdd; } -} \ No newline at end of file +} diff --git a/src/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storage/dd/cudd/InternalCuddDdManager.cpp index 9f33c803d..5fc5ebcd0 100644 --- a/src/storage/dd/cudd/InternalCuddDdManager.cpp +++ b/src/storage/dd/cudd/InternalCuddDdManager.cpp @@ -106,4 +106,4 @@ namespace storm { template InternalAdd InternalDdManager::getConstant(double const& value) const; template InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; } -} \ No newline at end of file +} diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index 840f5b77b..019ebe6e1 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -79,7 +79,7 @@ namespace storm { template unsigned DFTBuilder::computeRank(DFTElementPointer const& elem) { - if(elem->rank() == -1) { + if(elem->rank() == static_castrank())>(-1)) { if(elem->nrChildren() == 0 || elem->isDependency()) { elem->setRank(0); } else { diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 18d0f24bd..df5f4dde6 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -10,6 +10,7 @@ #include "src/parser/AutoParser.h" #include "src/parser/FormulaParser.h" #include "src/models/sparse/StandardRewardModel.h" +#include "src/solver/GmmxxLinearEquationSolver.h" TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); @@ -21,7 +22,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolverFactory())); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -59,7 +60,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolverFactory())); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 3126b4f71..3ae471fa3 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -8,7 +8,7 @@ #include "src/utility/solver.h" #include "src/parser/AutoParser.h" #include "src/models/sparse/StandardRewardModel.h" - +#include "src/solver/MinMaxLinearEquationSolver.h" #include "src/parser/FormulaParser.h" TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { @@ -24,7 +24,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -82,7 +82,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); diff --git a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index 95a112a56..ea1d839f0 100644 --- a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -10,6 +10,7 @@ #include "src/parser/AutoParser.h" #include "src/parser/FormulaParser.h" #include "src/models/sparse/StandardRewardModel.h" +#include "src/solver/NativeLinearEquationSolver.h" TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); @@ -21,7 +22,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::NativeLinearEquationSolverFactory())); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -59,7 +60,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::NativeLinearEquationSolverFactory())); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 7ee778b83..0b62a805a 100644 --- a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -25,7 +25,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -83,7 +83,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); diff --git a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 987670e8c..67809f12c 100644 --- a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -20,7 +20,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLea ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -67,7 +67,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");