From f3fa90cc37c6fac5b8f2397a04591269b95ef005 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 21 Jun 2016 17:02:15 +0200 Subject: [PATCH] more work towards exact solving Former-commit-id: 38edbcf2ca25e0eeeeb880ca2ded6cd920eada6e --- src/adapters/CarlAdapter.h | 6 +- src/builder/ExplicitModelBuilder.cpp | 5 +- src/cli/entrypoints.h | 26 ++- src/generator/Choice.cpp | 1 + src/generator/CompressedState.cpp | 1 + src/generator/JaniNextStateGenerator.cpp | 1 + src/generator/NextStateGenerator.cpp | 6 + src/generator/NextStateGenerator.h | 6 + src/generator/PrismNextStateGenerator.cpp | 29 +++- src/generator/PrismNextStateGenerator.h | 2 + src/generator/StateBehavior.cpp | 1 + .../csl/SparseCtmcCslModelChecker.cpp | 2 + .../csl/helper/SparseCtmcCslHelper.cpp | 5 +- .../prctl/SparseDtmcPrctlModelChecker.cpp | 1 + .../prctl/helper/SparseDtmcPrctlHelper.cpp | 5 +- .../SparsePropositionalModelChecker.cpp | 8 +- .../SparseDtmcEliminationModelChecker.cpp | 4 +- .../ExplicitQuantitativeCheckResult.cpp | 20 +-- src/models/sparse/Ctmc.cpp | 4 +- src/models/sparse/DeterministicModel.cpp | 4 +- src/models/sparse/Dtmc.cpp | 158 +----------------- src/models/sparse/Dtmc.h | 7 - src/models/sparse/MarkovAutomaton.cpp | 4 +- src/models/sparse/Mdp.cpp | 4 +- src/models/sparse/Model.cpp | 7 +- src/models/sparse/NondeterministicModel.cpp | 3 +- src/models/sparse/StandardRewardModel.cpp | 11 +- .../ConditionalStateEliminator.cpp | 4 +- .../DynamicStatePriorityQueue.cpp | 4 +- .../LongRunAverageEliminator.cpp | 4 +- .../PrioritizedStateEliminator.cpp | 3 - .../stateelimination/StateEliminator.cpp | 3 - src/storage/Distribution.cpp | 7 +- ...tronglyConnectedComponentDecomposition.cpp | 7 +- .../BisimulationDecomposition.cpp | 8 +- ...ministicModelBisimulationDecomposition.cpp | 7 +- ...ministicModelBisimulationDecomposition.cpp | 4 +- .../expressions/ExpressionEvaluator.cpp | 38 +++-- src/storage/expressions/ExpressionEvaluator.h | 36 +++- .../expressions/ExpressionEvaluatorBase.cpp | 3 +- .../expressions/ExprtkExpressionEvaluator.cpp | 3 +- .../expressions/ToRationalFunctionVisitor.cpp | 4 - .../expressions/ToRationalFunctionVisitor.h | 2 - .../expressions/ToRationalNumberVisitor.cpp | 91 ++++++++++ .../expressions/ToRationalNumberVisitor.h | 31 ++++ src/utility/constants.cpp | 22 ++- src/utility/graph.cpp | 58 ++++++- src/utility/solver.cpp | 15 +- src/utility/solver.h | 14 +- src/utility/stateelimination.cpp | 7 +- src/utility/storm.h | 72 ++++++-- .../EigenDtmcPrctlModelCheckerTest.cpp | 8 +- 52 files changed, 477 insertions(+), 309 deletions(-) create mode 100644 src/storage/expressions/ToRationalNumberVisitor.cpp create mode 100644 src/storage/expressions/ToRationalNumberVisitor.h diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h index 5b7225a15..fb0a45749 100644 --- a/src/adapters/CarlAdapter.h +++ b/src/adapters/CarlAdapter.h @@ -30,8 +30,8 @@ namespace carl { return h(p); } - template - inline size_t hash_value(carl::RationalFunction const& f) { + template + inline size_t hash_value(carl::RationalFunction const& f) { std::hash h; return h(f.nominator()) ^ h(f.denominator()); } @@ -62,7 +62,7 @@ namespace storm { typedef carl::FactorizedPolynomial Polynomial; typedef carl::Relation CompareRelation; - typedef carl::RationalFunction RationalFunction; + typedef carl::RationalFunction RationalFunction; typedef carl::Interval Interval; template using ArithConstraint = carl::SimpleConstraint; } diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp index 352694187..f5cb33aca 100644 --- a/src/builder/ExplicitModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -134,7 +134,7 @@ namespace storm { result = std::shared_ptr>(new storm::models::sparse::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); break; default: - STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model from probabilistic program: cannot handle this model type."); + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model: cannot handle this model type."); break; } @@ -352,10 +352,9 @@ namespace storm { // Explicitly instantiate the class. template class ExplicitModelBuilder, uint32_t>; + template class ExplicitModelBuilder, uint32_t>; -#ifdef STORM_HAVE_CARL template class ExplicitModelBuilder, uint32_t>; template class ExplicitModelBuilder, uint32_t>; -#endif } } diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 41dfd2ab1..84b7fb753 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -146,7 +146,7 @@ namespace storm { } #define BRANCH_ON_SPARSE_MODELTYPE(result, model, value_type, function, ...) \ - STORM_LOG_ASSERT(model->isSparseModel(), "Unknown model type."); \ + STORM_LOG_ASSERT(model->isSparseModel(), "Illegal model type."); \ if (model->isOfType(storm::models::ModelType::Dtmc)) { \ result = function>(model->template as>(), __VA_ARGS__); \ } else if (model->isOfType(storm::models::ModelType::Ctmc)) { \ @@ -178,19 +178,21 @@ namespace storm { template void buildAndCheckSymbolicModelWithSparseEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { // Start by building the model. - auto model = buildSparseModel(program, formulas); + std::shared_ptr model = buildSparseModel(program, formulas); // Print some information about the model. model->printModelInformationToStream(std::cout); - + // Preprocess the model. BRANCH_ON_SPARSE_MODELTYPE(model, model, ValueType, preprocessModel, formulas); + std::shared_ptr> sparseModel = model->template as>(); + // Finally, treat the formulas. if (storm::settings::getModule().isCounterexampleSet()) { - generateCounterexamples(program, formulas); + generateCounterexamples(program, sparseModel, formulas); } else { - verifySparseModel(model, formulas, onlyInitialStatesRelevant); + verifySparseModel(sparseModel, formulas, onlyInitialStatesRelevant); } } @@ -221,7 +223,19 @@ namespace storm { } } } - + + template<> + void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); + buildAndCheckSymbolicModelWithSparseEngine(program, formulas, onlyInitialStatesRelevant); + } + + template<> + void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); + buildAndCheckSymbolicModelWithSparseEngine(program, formulas, onlyInitialStatesRelevant); + } + template void buildAndCheckExplicitModel(std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { storm::settings::modules::IOSettings const& settings = storm::settings::getModule(); diff --git a/src/generator/Choice.cpp b/src/generator/Choice.cpp index 9202f2c5e..7a209ccc4 100644 --- a/src/generator/Choice.cpp +++ b/src/generator/Choice.cpp @@ -100,6 +100,7 @@ namespace storm { } template class Choice; + template class Choice; template class Choice; } } \ No newline at end of file diff --git a/src/generator/CompressedState.cpp b/src/generator/CompressedState.cpp index 03ba3d4c7..3a229112f 100644 --- a/src/generator/CompressedState.cpp +++ b/src/generator/CompressedState.cpp @@ -30,6 +30,7 @@ namespace storm { } template void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); + template void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); template void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager); } diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 7202ebcc7..9e0f10b7f 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -492,6 +492,7 @@ namespace storm { } template class JaniNextStateGenerator; + template class JaniNextStateGenerator; template class JaniNextStateGenerator; } diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index 00b8d794c..a99f0dcea 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -216,6 +216,11 @@ namespace storm { // Intentionally left empty. } + template + NextStateGenerator::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(), evaluator(expressionManager), state(nullptr) { + // Intentionally left empty. + } + template NextStateGeneratorOptions const& NextStateGenerator::getOptions() const { return options; @@ -297,6 +302,7 @@ namespace storm { } template class NextStateGenerator; + template class NextStateGenerator; template class NextStateGenerator; } diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index 2e6214c70..30a4157cd 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -162,6 +162,12 @@ namespace storm { NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options); + /*! + * Creates a new next state generator. This version of the constructor default-constructs the variable information. + * Hence, the subclass is responsible for suitably initializing it in its constructor. + */ + NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options); + uint64_t getStateSize() const; virtual ModelType getModelType() const = 0; virtual bool isDeterministicModel() const = 0; diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 77b547969..5de59feb0 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -22,9 +22,13 @@ namespace storm { } template - PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(program.getManager(), VariableInformation(program), options), program(program), rewardModels() { + PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(program.getManager(), options), program(program), rewardModels() { STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); + // Only after checking validity of the program, we initialize the variable information. + this->checkValid(program); + this->variableInformation = VariableInformation(program); + if (this->options.isBuildAllRewardModelsSet()) { for (auto const& rewardModel : this->program.getRewardModels()) { rewardModels.push_back(rewardModel); @@ -70,6 +74,28 @@ namespace storm { } } + template + void PrismNextStateGenerator::checkValid(storm::prism::Program const& program) { + // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message. + if (!std::is_same::value && program.hasUndefinedConstants()) { + std::vector> undefinedConstants = program.getUndefinedConstants(); + std::stringstream stream; + bool printComma = false; + for (auto const& constant : undefinedConstants) { + if (printComma) { + stream << ", "; + } else { + printComma = true; + } + stream << constant.get().getName() << " (" << constant.get().getType() << ")"; + } + stream << "."; + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); + } else if (std::is_same::value && !program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted."); + } + } + template ModelType PrismNextStateGenerator::getModelType() const { switch (program.getModelType()) { @@ -535,6 +561,7 @@ namespace storm { } template class PrismNextStateGenerator; + template class PrismNextStateGenerator; template class PrismNextStateGenerator; } } \ No newline at end of file diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h index 652903c98..d2004b9d3 100644 --- a/src/generator/PrismNextStateGenerator.h +++ b/src/generator/PrismNextStateGenerator.h @@ -27,6 +27,8 @@ namespace storm { virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) override; + static void checkValid(storm::prism::Program const& program); + private: /*! * A delegate constructor that is used to preprocess the program before the constructor of the superclass is diff --git a/src/generator/StateBehavior.cpp b/src/generator/StateBehavior.cpp index 6ae1f6de0..28e256c18 100644 --- a/src/generator/StateBehavior.cpp +++ b/src/generator/StateBehavior.cpp @@ -56,6 +56,7 @@ namespace storm { } template class StateBehavior; + template class StateBehavior; template class StateBehavior; } diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 8356620c1..bf70ca586 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -15,6 +15,8 @@ #include "src/logic/FragmentSpecification.h" +#include "src/adapters/CarlAdapter.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/NotImplementedException.h" diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index c9ee33622..12bb227b9 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -701,12 +701,13 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + -#ifdef STORM_HAVE_CARL template std::vector SparseCtmcCslHelper::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); template std::vector SparseCtmcCslHelper::computeReachabilityTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative); template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); -#endif } } } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index bf8ea19ff..ee9195b6e 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -146,6 +146,7 @@ namespace storm { } template class SparseDtmcPrctlModelChecker>; + template class SparseDtmcPrctlModelChecker>; template class SparseDtmcPrctlModelChecker>; } } \ No newline at end of file diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 22d80d46a..857da9a6f 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -67,7 +67,7 @@ namespace storm { // Check whether we need to compute exact probabilities for some states. if (qualitative) { // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1. - storm::utility::vector::setVectorValues(result, maybeStates, ValueType(0.5)); + storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::convertNumber(0.5)); } else { if (!maybeStates.empty()) { // In this case we have have to compute the probabilities. @@ -82,7 +82,7 @@ namespace storm { // Initialize the x vector with 0.5 for each element. This is the initial guess for // the iterative solvers. It should be safe as for all 'maybe' states we know that the // probability is strictly larger than 0. - std::vector x(maybeStates.getNumberOfSetBits(), ValueType(0.5)); + std::vector x(maybeStates.getNumberOfSetBits(), storm::utility::convertNumber(0.5)); // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. @@ -401,6 +401,7 @@ namespace storm { } template class SparseDtmcPrctlHelper; + template class SparseDtmcPrctlHelper; template class SparseDtmcPrctlHelper; } } diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp index aa947c8cb..5ffc50140 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -57,14 +57,18 @@ namespace storm { template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; -#ifdef STORM_HAVE_CARL template class SparsePropositionalModelChecker>>; + template class SparsePropositionalModelChecker>; + template class SparsePropositionalModelChecker>; + template class SparsePropositionalModelChecker>; + template class SparsePropositionalModelChecker>; + template class SparsePropositionalModelChecker>; + template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; -#endif } } \ No newline at end of file diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 02cf81343..662881ed0 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -1032,9 +1032,7 @@ namespace storm { } template class SparseDtmcEliminationModelChecker>; - -#ifdef STORM_HAVE_CARL + template class SparseDtmcEliminationModelChecker>; template class SparseDtmcEliminationModelChecker>; -#endif } // namespace modelchecker } // namespace storm diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 08ca016fd..218af9179 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -133,28 +133,28 @@ namespace storm { switch (comparisonType) { case logic::ComparisonType::Less: for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { - if (valuesAsVector[index] < bound) { + if (valuesAsVector[index] < storm::utility::convertNumber(bound)) { result.set(index); } } break; case logic::ComparisonType::LessEqual: for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { - if (valuesAsVector[index] <= bound) { + if (valuesAsVector[index] <= storm::utility::convertNumber(bound)) { result.set(index); } } break; case logic::ComparisonType::Greater: for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { - if (valuesAsVector[index] > bound) { + if (valuesAsVector[index] > storm::utility::convertNumber(bound)) { result.set(index); } } break; case logic::ComparisonType::GreaterEqual: for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { - if (valuesAsVector[index] >= bound) { + if (valuesAsVector[index] >= storm::utility::convertNumber(bound)) { result.set(index); } } @@ -167,22 +167,22 @@ namespace storm { switch (comparisonType) { case logic::ComparisonType::Less: for (auto const& element : valuesAsMap) { - result[element.first] = element.second < bound; + result[element.first] = element.second < storm::utility::convertNumber(bound); } break; case logic::ComparisonType::LessEqual: for (auto const& element : valuesAsMap) { - result[element.first] = element.second <= bound; + result[element.first] = element.second <= storm::utility::convertNumber(bound); } break; case logic::ComparisonType::Greater: for (auto const& element : valuesAsMap) { - result[element.first] = element.second > bound; + result[element.first] = element.second > storm::utility::convertNumber(bound); } break; case logic::ComparisonType::GreaterEqual: for (auto const& element : valuesAsMap) { - result[element.first] = element.second >= bound; + result[element.first] = element.second >= storm::utility::convertNumber(bound); } break; } @@ -248,9 +248,7 @@ namespace storm { } template class ExplicitQuantitativeCheckResult; - -#ifdef STORM_HAVE_CARL + template class ExplicitQuantitativeCheckResult; template class ExplicitQuantitativeCheckResult; -#endif } } \ No newline at end of file diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp index 1d07c48a9..e48f4590f 100644 --- a/src/models/sparse/Ctmc.cpp +++ b/src/models/sparse/Ctmc.cpp @@ -46,12 +46,10 @@ namespace storm { } template class Ctmc; + template class Ctmc; -#ifdef STORM_HAVE_CARL template class Ctmc>; - template class Ctmc; -#endif } // namespace sparse } // namespace models diff --git a/src/models/sparse/DeterministicModel.cpp b/src/models/sparse/DeterministicModel.cpp index 0fb6de34a..c2bd35b16 100644 --- a/src/models/sparse/DeterministicModel.cpp +++ b/src/models/sparse/DeterministicModel.cpp @@ -57,12 +57,10 @@ namespace storm { template class DeterministicModel; template class DeterministicModel; + template class DeterministicModel; -#ifdef STORM_HAVE_CARL template class DeterministicModel>; - template class DeterministicModel; -#endif } // namespace sparse } // namespace models diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp index cbfeed391..7997a1494 100644 --- a/src/models/sparse/Dtmc.cpp +++ b/src/models/sparse/Dtmc.cpp @@ -25,160 +25,6 @@ namespace storm { STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); } - template - Dtmc Dtmc::getSubDtmc(storm::storage::BitVector const& states) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This function is not yet implemented."); - // FIXME: repair this - // - // - // // Is there any state in the subsystem? - // if(subSysStates.getNumberOfSetBits() == 0) { - // STORM_LOG_ERROR("No states in subsystem!"); - // return storm::models::Dtmc(storm::storage::SparseMatrix(), - // storm::models::sparse::StateLabeling(this->getStateLabeling(), subSysStates), - // boost::optional>(), - // boost::optional>(), - // boost::optional>()); - // } - // - // // Does the vector have the right size? - // if(subSysStates.size() != this->getNumberOfStates()) { - // STORM_LOG_INFO("BitVector has wrong size. Resizing it..."); - // subSysStates.resize(this->getNumberOfStates()); - // } - // - // // Test if it is a proper subsystem of this Dtmc, i.e. if there is at least one state to be left out. - // if(subSysStates.getNumberOfSetBits() == subSysStates.size()) { - // STORM_LOG_INFO("All states are kept. This is no proper subsystem."); - // return storm::models::Dtmc(*this); - // } - // - // // 1. Get all necessary information from the old transition matrix - // storm::storage::SparseMatrix const & origMat = this->getTransitionMatrix(); - // - // // Iterate over all rows. Count the number of all transitions from the old system to be - // // transfered to the new one. Also build a mapping from the state number of the old system - // // to the state number of the new system. - // uint_fast64_t subSysTransitionCount = 0; - // uint_fast64_t newRow = 0; - // std::vector stateMapping; - // for(uint_fast64_t row = 0; row < origMat.getRowCount(); ++row) { - // if(subSysStates.get(row)){ - // for(auto const& entry : origMat.getRow(row)) { - // if(subSysStates.get(entry.getColumn())) { - // subSysTransitionCount++; - // } - // } - // stateMapping.push_back(newRow); - // newRow++; - // } else { - // stateMapping.push_back((uint_fast64_t) -1); - // } - // } - // - // // 2. Construct transition matrix - // - // // Take all states indicated by the vector as well as one additional state s_b as target of - // // all transitions that target a state that is not kept. - // uint_fast64_t const newStateCount = subSysStates.getNumberOfSetBits() + 1; - // - // // The number of transitions of the new Dtmc is the number of transitions transfered - // // from the old one plus one transition for each state to s_b. - // storm::storage::SparseMatrixBuilder newMatBuilder(newStateCount,newStateCount,subSysTransitionCount + newStateCount); - // - // // Now fill the matrix. - // newRow = 0; - // T rest = storm::utility::zero(); - // for(uint_fast64_t row = 0; row < origMat.getRowCount(); ++row) { - // if(subSysStates.get(row)){ - // // Transfer transitions - // for(auto& entry : origMat.getRow(row)) { - // if(subSysStates.get(entry.getColumn())) { - // newMatBuilder.addNextValue(newRow, stateMapping[entry.getColumn()], entry.getValue()); - // } else { - // rest += entry.getValue(); - // } - // } - // - // // Insert the transition taking care of the remaining outgoing probability. - // newMatBuilder.addNextValue(newRow, newStateCount - 1, rest); - // rest = storm::utility::zero(); - // - // newRow++; - // } - // } - // - // // Insert last transition: self loop on s_b - // newMatBuilder.addNextValue(newStateCount - 1, newStateCount - 1, storm::utility::one()); - // - // // 3. Take care of the labeling. - // storm::models::sparse::StateLabeling newLabeling = storm::models::sparse::StateLabeling(this->getStateLabeling(), subSysStates); - // newLabeling.addState(); - // if(!newLabeling.containsLabel("s_b")) { - // newLabeling.addLabel("s_b"); - // } - // newLabeling.addLabelToState("s_b", newStateCount - 1); - // - // // 4. Handle the optionals - // - // boost::optional> newStateRewards; - // if(this->hasStateRewards()) { - // - // // Get the rewards and move the needed values to the front. - // std::vector newRewards(this->getStateRewardVector()); - // storm::utility::vector::selectVectorValues(newRewards, subSysStates, newRewards); - // - // // Throw away all values after the last state and set the reward for s_b to 0. - // newRewards.resize(newStateCount); - // newRewards[newStateCount - 1] = (T) 0; - // - // newStateRewards = newRewards; - // } - // - // boost::optional> newTransitionRewards; - // if(this->hasTransitionRewards()) { - // - // storm::storage::SparseMatrixBuilder newTransRewardsBuilder(newStateCount, subSysTransitionCount + newStateCount); - // - // // Copy the rewards for the kept states - // newRow = 0; - // for(uint_fast64_t row = 0; row < this->getTransitionRewardMatrix().getRowCount(); ++row) { - // if(subSysStates.get(row)){ - // // Transfer transition rewards - // for(auto& entry : this->getTransitionRewardMatrix().getRow(row)) { - // if(subSysStates.get(entry.getColumn())) { - // newTransRewardsBuilder.addNextValue(newRow, stateMapping[entry.getColumn()], entry.getValue()); - // } - // } - // - // // Insert the reward (e.g. 0) for the transition taking care of the remaining outgoing probability. - // newTransRewardsBuilder.addNextValue(newRow, newStateCount - 1, storm::utility::zero()); - // - // newRow++; - // } - // } - // - // newTransitionRewards = newTransRewardsBuilder.build(); - // } - // - // boost::optional> newChoiceLabels; - // if(this->hasChoiceLabeling()) { - // - // // Get the choice label sets and move the needed values to the front. - // std::vector newChoice(this->getChoiceLabeling()); - // storm::utility::vector::selectVectorValues(newChoice, subSysStates, this->getChoiceLabeling()); - // - // // Throw away all values after the last state and set the choice label set for s_b as empty. - // newChoice.resize(newStateCount); - // newChoice[newStateCount - 1] = LabelSet(); - // - // newChoiceLabels = newChoice; - // } - // - // // 5. Make Dtmc from its parts and return it - // return storm::models::Dtmc(newMatBuilder.build(), newLabeling, newStateRewards, std::move(newTransitionRewards), newChoiceLabels); - } - #ifdef STORM_HAVE_CARL template Dtmc::ConstraintCollector::ConstraintCollector(Dtmc const& dtmc) { @@ -223,12 +69,10 @@ namespace storm { template class Dtmc; template class Dtmc; + template class Dtmc; -#ifdef STORM_HAVE_CARL template class Dtmc>; - template class Dtmc; -#endif } // namespace sparse } // namespace models diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h index bf1b5c3e4..5e6846b76 100644 --- a/src/models/sparse/Dtmc.h +++ b/src/models/sparse/Dtmc.h @@ -49,13 +49,6 @@ namespace storm { Dtmc& operator=(Dtmc&& dtmc) = default; #endif - /*! - * Retrieves the sub-DTMC that only contains the given set of states. - * - * @param states The states of the sub-DTMC. - * @return The resulting sub-DTMC. - */ - Dtmc getSubDtmc(storm::storage::BitVector const& states) const; #ifdef STORM_HAVE_CARL class ConstraintCollector { diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index b9739203f..81f3bc5c9 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -322,12 +322,10 @@ namespace storm { template class MarkovAutomaton; // template class MarkovAutomaton; + template class MarkovAutomaton; -#ifdef STORM_HAVE_CARL template class MarkovAutomaton>; - template class MarkovAutomaton; -#endif } // namespace sparse } // namespace models diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp index 4a4b37d60..cf436c7e1 100644 --- a/src/models/sparse/Mdp.cpp +++ b/src/models/sparse/Mdp.cpp @@ -98,12 +98,10 @@ namespace storm { template class Mdp; template class Mdp; + template class Mdp; -#ifdef STORM_HAVE_CARL template class Mdp>; - template class Mdp; -#endif } // namespace sparse } // namespace models diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index 265f0d8b0..83d0c8aa2 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -354,12 +354,11 @@ namespace storm { template class Model; template class Model; - -#ifdef STORM_HAVE_CARL - template class Model>; + template class Model; + + template class Model>; template class Model; -#endif } } diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp index 29662f6cf..3a4af6664 100644 --- a/src/models/sparse/NondeterministicModel.cpp +++ b/src/models/sparse/NondeterministicModel.cpp @@ -169,14 +169,13 @@ namespace storm { template class NondeterministicModel; template class NondeterministicModel; + template class NondeterministicModel; -#ifdef STORM_HAVE_CARL template class NondeterministicModel>; template void NondeterministicModel>::modifyStateActionRewards(std::string const& modelName, std::map const& modifications); template void NondeterministicModel>::modifyStateRewards(std::string const& modelName, std::map const& modifications); template class NondeterministicModel; -#endif } } diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp index 88b88915e..3bd624d3d 100644 --- a/src/models/sparse/StandardRewardModel.cpp +++ b/src/models/sparse/StandardRewardModel.cpp @@ -303,8 +303,16 @@ namespace storm { template void StandardRewardModel::setStateReward(uint_fast64_t state, float const & newValue); template class StandardRewardModel; template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); + + template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); + template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue); + template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue); + template class StandardRewardModel; + template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); -#ifdef STORM_HAVE_CARL template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; @@ -324,7 +332,6 @@ namespace storm { template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template class StandardRewardModel; template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); -#endif } } diff --git a/src/solver/stateelimination/ConditionalStateEliminator.cpp b/src/solver/stateelimination/ConditionalStateEliminator.cpp index f15b3342b..0a86894bc 100644 --- a/src/solver/stateelimination/ConditionalStateEliminator.cpp +++ b/src/solver/stateelimination/ConditionalStateEliminator.cpp @@ -61,10 +61,8 @@ namespace storm { } template class ConditionalStateEliminator; - -#ifdef STORM_HAVE_CARL + template class ConditionalStateEliminator; template class ConditionalStateEliminator; -#endif } // namespace stateelimination } // namespace storage diff --git a/src/solver/stateelimination/DynamicStatePriorityQueue.cpp b/src/solver/stateelimination/DynamicStatePriorityQueue.cpp index 8c4d0a83d..afff0b7a3 100644 --- a/src/solver/stateelimination/DynamicStatePriorityQueue.cpp +++ b/src/solver/stateelimination/DynamicStatePriorityQueue.cpp @@ -66,10 +66,8 @@ namespace storm { } template class DynamicStatePriorityQueue; - -#ifdef STORM_HAVE_CARL + template class DynamicStatePriorityQueue; template class DynamicStatePriorityQueue; -#endif } } } diff --git a/src/solver/stateelimination/LongRunAverageEliminator.cpp b/src/solver/stateelimination/LongRunAverageEliminator.cpp index c06fed5bb..758f71a14 100644 --- a/src/solver/stateelimination/LongRunAverageEliminator.cpp +++ b/src/solver/stateelimination/LongRunAverageEliminator.cpp @@ -23,10 +23,8 @@ namespace storm { } template class LongRunAverageEliminator; - -#ifdef STORM_HAVE_CARL + template class LongRunAverageEliminator; template class LongRunAverageEliminator; -#endif } // namespace stateelimination } // namespace storage diff --git a/src/solver/stateelimination/PrioritizedStateEliminator.cpp b/src/solver/stateelimination/PrioritizedStateEliminator.cpp index 5fa1cfc8a..134cb3264 100644 --- a/src/solver/stateelimination/PrioritizedStateEliminator.cpp +++ b/src/solver/stateelimination/PrioritizedStateEliminator.cpp @@ -30,10 +30,7 @@ namespace storm { template class PrioritizedStateEliminator; template class PrioritizedStateEliminator; - -#ifdef STORM_HAVE_CARL template class PrioritizedStateEliminator; -#endif } // namespace stateelimination } // namespace storage diff --git a/src/solver/stateelimination/StateEliminator.cpp b/src/solver/stateelimination/StateEliminator.cpp index ef4bb355e..41d3ef2d9 100644 --- a/src/solver/stateelimination/StateEliminator.cpp +++ b/src/solver/stateelimination/StateEliminator.cpp @@ -265,10 +265,7 @@ namespace storm { template class StateEliminator; template class StateEliminator; - -#ifdef STORM_HAVE_CARL template class StateEliminator; -#endif } // namespace stateelimination } // namespace storage diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp index 5843e964b..7c3b5d99f 100644 --- a/src/storage/Distribution.cpp +++ b/src/storage/Distribution.cpp @@ -151,10 +151,11 @@ namespace storm { template class Distribution; template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); - -#ifdef STORM_HAVE_CARL + + template class Distribution; + template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); + template class Distribution; template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); -#endif } } diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index fe2c60e4e..e129c8b85 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -237,11 +237,14 @@ namespace storm { template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); -#ifdef STORM_HAVE_CARL + template class StronglyConnectedComponentDecomposition; + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); + template class StronglyConnectedComponentDecomposition; template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); -#endif } // namespace storage } // namespace storm \ No newline at end of file diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index 4b31551f9..751708e24 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -322,11 +322,13 @@ namespace storm { template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; - -#ifdef STORM_HAVE_CARL + + template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; + template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; + template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; + template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; -#endif } } diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index e968c98cd..89408e620 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -651,10 +651,11 @@ namespace storm { template class DeterministicModelBisimulationDecomposition>; template class DeterministicModelBisimulationDecomposition>; - -#ifdef STORM_HAVE_CARL + + template class DeterministicModelBisimulationDecomposition>; + template class DeterministicModelBisimulationDecomposition>; + template class DeterministicModelBisimulationDecomposition>; template class DeterministicModelBisimulationDecomposition>; -#endif } } diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index 2e7d54113..c117b0628 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -416,10 +416,8 @@ namespace storm { } template class NondeterministicModelBisimulationDecomposition>; - -#ifdef STORM_HAVE_CARL + template class NondeterministicModelBisimulationDecomposition>; template class NondeterministicModelBisimulationDecomposition>; -#endif } } diff --git a/src/storage/expressions/ExpressionEvaluator.cpp b/src/storage/expressions/ExpressionEvaluator.cpp index 46ef54c24..6d44d680a 100644 --- a/src/storage/expressions/ExpressionEvaluator.cpp +++ b/src/storage/expressions/ExpressionEvaluator.cpp @@ -7,30 +7,48 @@ namespace storm { // Intentionally left empty. } -#ifdef STORM_HAVE_CARL - ExpressionEvaluator::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase(manager) { + template + ExpressionEvaluatorWithVariableToExpressionMap::ExpressionEvaluatorWithVariableToExpressionMap(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase(manager) { // Intentionally left empty. } - void ExpressionEvaluator::setBooleanValue(storm::expressions::Variable const& variable, bool value) { - ExprtkExpressionEvaluatorBase::setBooleanValue(variable, value); + template + void ExpressionEvaluatorWithVariableToExpressionMap::setBooleanValue(storm::expressions::Variable const& variable, bool value) { + ExprtkExpressionEvaluatorBase::setBooleanValue(variable, value); this->variableToExpressionMap[variable] = this->getManager().boolean(value); } - void ExpressionEvaluator::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) { - ExprtkExpressionEvaluatorBase::setIntegerValue(variable, value); + template + void ExpressionEvaluatorWithVariableToExpressionMap::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) { + ExprtkExpressionEvaluatorBase::setIntegerValue(variable, value); this->variableToExpressionMap[variable] = this->getManager().integer(value); } - void ExpressionEvaluator::setRationalValue(storm::expressions::Variable const& variable, double value) { - ExprtkExpressionEvaluatorBase::setRationalValue(variable, value); + template + void ExpressionEvaluatorWithVariableToExpressionMap::setRationalValue(storm::expressions::Variable const& variable, double value) { + ExprtkExpressionEvaluatorBase::setRationalValue(variable, value); this->variableToExpressionMap[variable] = this->getManager().rational(value); } + + ExpressionEvaluator::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorWithVariableToExpressionMap(manager) { + // Intentionally left empty. + } + + RationalNumber ExpressionEvaluator::asRational(Expression const& expression) const { + Expression substitutedExpression = expression.substitute(this->variableToExpressionMap); + return this->rationalNumberVisitor.toRationalNumber(substitutedExpression); + } + + ExpressionEvaluator::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorWithVariableToExpressionMap(manager) { + // Intentionally left empty. + } RationalFunction ExpressionEvaluator::asRational(Expression const& expression) const { - Expression substitutedExpression = expression.substitute(variableToExpressionMap); + Expression substitutedExpression = expression.substitute(this->variableToExpressionMap); return this->rationalFunctionVisitor.toRationalFunction(substitutedExpression); } -#endif + + template class ExpressionEvaluatorWithVariableToExpressionMap; + template class ExpressionEvaluatorWithVariableToExpressionMap; } } \ No newline at end of file diff --git a/src/storage/expressions/ExpressionEvaluator.h b/src/storage/expressions/ExpressionEvaluator.h index d9fa1653b..2480af12d 100644 --- a/src/storage/expressions/ExpressionEvaluator.h +++ b/src/storage/expressions/ExpressionEvaluator.h @@ -8,6 +8,7 @@ #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/ExprtkExpressionEvaluator.h" #include "src/storage/expressions/ToRationalFunctionVisitor.h" +#include "src/storage/expressions/ToRationalNumberVisitor.h" namespace storm { namespace expressions { @@ -20,26 +21,43 @@ namespace storm { ExpressionEvaluator(storm::expressions::ExpressionManager const& manager); }; -#ifdef STORM_HAVE_CARL - template<> - class ExpressionEvaluator : public ExprtkExpressionEvaluatorBase { + template + class ExpressionEvaluatorWithVariableToExpressionMap : public ExprtkExpressionEvaluatorBase { public: - ExpressionEvaluator(storm::expressions::ExpressionManager const& manager); - + ExpressionEvaluatorWithVariableToExpressionMap(storm::expressions::ExpressionManager const& manager); + void setBooleanValue(storm::expressions::Variable const& variable, bool value) override; void setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) override; void setRationalValue(storm::expressions::Variable const& variable, double value) override; + + protected: + // A mapping of variables to their expressions. + std::unordered_map variableToExpressionMap; + }; + + template<> + class ExpressionEvaluator : public ExpressionEvaluatorWithVariableToExpressionMap { + public: + ExpressionEvaluator(storm::expressions::ExpressionManager const& manager); - RationalFunction asRational(Expression const& expression) const override; + RationalNumber asRational(Expression const& expression) const override; private: - // A mapping of variables to their expressions. - std::unordered_map variableToExpressionMap; + // A visitor that can be used to translate expressions to rational numbers. + mutable ToRationalNumberVisitor rationalNumberVisitor; + }; + + template<> + class ExpressionEvaluator : public ExpressionEvaluatorWithVariableToExpressionMap { + public: + ExpressionEvaluator(storm::expressions::ExpressionManager const& manager); + RationalFunction asRational(Expression const& expression) const override; + + private: // A visitor that can be used to translate expressions to rational functions. mutable ToRationalFunctionVisitor rationalFunctionVisitor; }; -#endif } } diff --git a/src/storage/expressions/ExpressionEvaluatorBase.cpp b/src/storage/expressions/ExpressionEvaluatorBase.cpp index e707a48ca..d98810886 100644 --- a/src/storage/expressions/ExpressionEvaluatorBase.cpp +++ b/src/storage/expressions/ExpressionEvaluatorBase.cpp @@ -16,8 +16,7 @@ namespace storm { } template class ExpressionEvaluatorBase; -#ifdef STORM_HAVE_CARL + template class ExpressionEvaluatorBase; template class ExpressionEvaluatorBase; -#endif } } \ No newline at end of file diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storage/expressions/ExprtkExpressionEvaluator.cpp index 1d225ec12..942c17172 100755 --- a/src/storage/expressions/ExprtkExpressionEvaluator.cpp +++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -83,8 +83,7 @@ namespace storm { } template class ExprtkExpressionEvaluatorBase; -#ifdef STORM_HAVE_CARL + template class ExprtkExpressionEvaluatorBase; template class ExprtkExpressionEvaluatorBase; -#endif } } \ No newline at end of file diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp index b42f23aa4..71e052bee 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp @@ -5,8 +5,6 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" -#ifdef STORM_HAVE_CARL - namespace storm { namespace expressions { template @@ -100,5 +98,3 @@ namespace storm { } } - -#endif diff --git a/src/storage/expressions/ToRationalFunctionVisitor.h b/src/storage/expressions/ToRationalFunctionVisitor.h index 4ad74acc9..6bd3a205b 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.h +++ b/src/storage/expressions/ToRationalFunctionVisitor.h @@ -7,7 +7,6 @@ #include "src/storage/expressions/ExpressionVisitor.h" #include "src/storage/expressions/Variable.h" -#ifdef STORM_HAVE_CARL namespace storm { namespace expressions { @@ -48,6 +47,5 @@ namespace storm { }; } } -#endif #endif /* STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/ToRationalNumberVisitor.cpp b/src/storage/expressions/ToRationalNumberVisitor.cpp new file mode 100644 index 000000000..b17ec335a --- /dev/null +++ b/src/storage/expressions/ToRationalNumberVisitor.cpp @@ -0,0 +1,91 @@ +#include "src/storage/expressions/ToRationalNumberVisitor.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace expressions { + template + ToRationalNumberVisitor::ToRationalNumberVisitor() : ExpressionVisitor() { + // Intentionally left empty. + } + + template + RationalNumberType ToRationalNumberVisitor::toRationalNumber(Expression const& expression) { + return boost::any_cast(expression.accept(*this)); + } + + template + boost::any ToRationalNumberVisitor::visit(IfThenElseExpression const& expression) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); + } + + template + boost::any ToRationalNumberVisitor::visit(BinaryBooleanFunctionExpression const& expression) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); + } + + template + boost::any ToRationalNumberVisitor::visit(BinaryNumericalFunctionExpression const& expression) { + RationalNumberType firstOperandAsRationalFunction = boost::any_cast(expression.getFirstOperand()->accept(*this)); + RationalNumberType secondOperandAsRationalFunction = boost::any_cast(expression.getSecondOperand()->accept(*this)); + switch(expression.getOperatorType()) { + case BinaryNumericalFunctionExpression::OperatorType::Plus: + return firstOperandAsRationalFunction + secondOperandAsRationalFunction; + break; + case BinaryNumericalFunctionExpression::OperatorType::Minus: + return firstOperandAsRationalFunction - secondOperandAsRationalFunction; + break; + case BinaryNumericalFunctionExpression::OperatorType::Times: + return firstOperandAsRationalFunction * secondOperandAsRationalFunction; + break; + case BinaryNumericalFunctionExpression::OperatorType::Divide: + return firstOperandAsRationalFunction / secondOperandAsRationalFunction; + break; + default: + STORM_LOG_ASSERT(false, "Illegal operator type."); + } + + // Return a dummy. This point must, however, never be reached. + return boost::any(); + } + + template + boost::any ToRationalNumberVisitor::visit(BinaryRelationExpression const& expression) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + } + + template + boost::any ToRationalNumberVisitor::visit(VariableExpression const& expression) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot transform expressions containing variables to a rational number."); + } + + template + boost::any ToRationalNumberVisitor::visit(UnaryBooleanFunctionExpression const& expression) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + } + + template + boost::any ToRationalNumberVisitor::visit(UnaryNumericalFunctionExpression const& expression) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + } + + template + boost::any ToRationalNumberVisitor::visit(BooleanLiteralExpression const& expression) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + } + + template + boost::any ToRationalNumberVisitor::visit(IntegerLiteralExpression const& expression) { + return RationalNumberType(carl::rationalize(static_cast(expression.getValue()))); + } + + template + boost::any ToRationalNumberVisitor::visit(DoubleLiteralExpression const& expression) { + return RationalNumberType(carl::rationalize(expression.getValue())); + } + + template class ToRationalNumberVisitor; + + } +} diff --git a/src/storage/expressions/ToRationalNumberVisitor.h b/src/storage/expressions/ToRationalNumberVisitor.h new file mode 100644 index 000000000..2254931f6 --- /dev/null +++ b/src/storage/expressions/ToRationalNumberVisitor.h @@ -0,0 +1,31 @@ +#pragma once + +#include "src/adapters/CarlAdapter.h" +#include "src/storage/expressions/Expression.h" +#include "src/storage/expressions/Expressions.h" +#include "src/storage/expressions/ExpressionVisitor.h" +#include "src/storage/expressions/Variable.h" + +namespace storm { + namespace expressions { + + template + class ToRationalNumberVisitor : public ExpressionVisitor { + public: + ToRationalNumberVisitor(); + + RationalNumberType toRationalNumber(Expression const& expression); + + virtual boost::any visit(IfThenElseExpression const& expression) override; + virtual boost::any visit(BinaryBooleanFunctionExpression const& expression) override; + virtual boost::any visit(BinaryNumericalFunctionExpression const& expression) override; + virtual boost::any visit(BinaryRelationExpression const& expression) override; + virtual boost::any visit(VariableExpression const& expression) override; + virtual boost::any visit(UnaryBooleanFunctionExpression const& expression) override; + virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; + virtual boost::any visit(BooleanLiteralExpression const& expression) override; + virtual boost::any visit(IntegerLiteralExpression const& expression) override; + virtual boost::any visit(DoubleLiteralExpression const& expression) override; + }; + } +} diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index b2b182247..dfe0101ad 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -40,8 +40,12 @@ namespace storm { return true; } + template<> + storm::RationalNumber infinity() { + // FIXME: this should be treated more properly. + return storm::RationalNumber(-1); + } -#ifdef STORM_HAVE_CARL template<> bool isOne(storm::RationalFunction const& a) { return a.isOne(); @@ -88,8 +92,6 @@ namespace storm { return carl::isZero(a); } -#endif - template ValueType pow(ValueType const& value, uint_fast64_t exponent) { return std::pow(value, exponent); @@ -102,7 +104,11 @@ namespace storm { return value; } -#ifdef STORM_HAVE_CARL + template<> + double convertNumber(double const& number){ + return number; + } + template<> RationalFunction& simplify(RationalFunction& value); @@ -142,7 +148,10 @@ namespace storm { return carl::rationalize(number); } -#endif + template<> + RationalFunction convertNumber(double const& number){ + return RationalFunction(carl::rationalize(number)); + } template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { @@ -238,7 +247,8 @@ namespace storm { template storm::RationalNumber one(); template storm::RationalNumber zero(); - + template storm::RationalNumber infinity(); + template double convertNumber(storm::RationalNumber const& number); template storm::RationalNumber convertNumber(double const& number); diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index b188872cf..05541ae01 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -1116,8 +1116,62 @@ namespace storm { template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; -#ifdef STORM_HAVE_CARL + // Instantiations for storm::RationalNumber. + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); + + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); + + + template storm::storage::BitVector performProbGreater0(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 performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0); + + + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template std::pair performProb01(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 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::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + template storm::storage::BitVector performProb1E(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 performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + template 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) ; + + + template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + + template storm::storage::BitVector performProbGreater0A(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 performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template storm::storage::BitVector performProb0E(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 performProb1A( 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 std::pair performProb01Min(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 std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + + + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); + // End of instantiations for storm::RationalNumber. + +#ifdef STORM_HAVE_CARL template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); @@ -1169,7 +1223,7 @@ namespace storm { template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); #endif diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 92f2b8e94..43fadb20b 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -57,9 +57,21 @@ namespace storm { default: return std::make_unique>(matrix); } } + + std::unique_ptr> LinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { + storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); + switch (equationSolver) { + case storm::solver::EquationSolverType::Elimination: return std::make_unique>(matrix); + default: return std::make_unique>(matrix); + } + } std::unique_ptr> LinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::make_unique>(matrix); + storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); + switch (equationSolver) { + case storm::solver::EquationSolverType::Elimination: return std::make_unique>(matrix); + default: return std::make_unique>(matrix); + } } template @@ -216,6 +228,7 @@ namespace storm { template class MinMaxLinearEquationSolverFactory; template class GameSolverFactory; + template class LinearEquationSolverFactory; template class EigenLinearEquationSolverFactory; } } diff --git a/src/utility/solver.h b/src/utility/solver.h index 201cfccb1..4791737a8 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -88,7 +88,19 @@ namespace storm { */ virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const; }; - + + template<> + class LinearEquationSolverFactory { + public: + /*! + * Creates a new linear equation solver instance with the given matrix. + * + * @param matrix The matrix that defines the equation system. + * @return A pointer to the newly created solver. + */ + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const; + }; + template<> class LinearEquationSolverFactory { public: diff --git a/src/utility/stateelimination.cpp b/src/utility/stateelimination.cpp index bfb967da2..c2882dcde 100644 --- a/src/utility/stateelimination.cpp +++ b/src/utility/stateelimination.cpp @@ -153,13 +153,14 @@ namespace storm { template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); template uint_fast64_t estimateComplexity(storm::RationalNumber const& value); - -#ifdef STORM_HAVE_CARL + template std::shared_ptr createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); + template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + template uint_fast64_t estimateComplexity(storm::RationalFunction const& value); template std::shared_ptr createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); -#endif } } } \ No newline at end of file diff --git a/src/utility/storm.h b/src/utility/storm.h index 8f0f5b79f..d590aa033 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -198,14 +198,6 @@ namespace storm { return model; } - - template - void generateCounterexamples(storm::prism::Program const& program, std::shared_ptr> model, std::vector> const& formulas) { - for (auto const& formula : formulas) { - generateCounterexample(program, model, formula); - } - } - template void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { if (storm::settings::getModule().isMinimalCommandSetGenerationSet()) { @@ -227,13 +219,23 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No suitable counterexample representation selected."); } } - -#ifdef STORM_HAVE_CARL + + template<> + inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); + } + template<> inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); } -#endif + + template + void generateCounterexamples(storm::prism::Program const& program, std::shared_ptr> model, std::vector> const& formulas) { + for (auto const& formula : formulas) { + generateCounterexample(program, model, formula); + } + } template std::unique_ptr verifyModel(std::shared_ptr model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { @@ -310,7 +312,32 @@ namespace storm { return result; } - + + template<> + inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } else { + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The exact engine currently does not support this property on DTMCs."); + } + } + } else { + STORM_LOG_ASSERT(false, "Illegal model type."); + } + return result; + } + #ifdef STORM_HAVE_CARL inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { std::ofstream filestream; @@ -330,15 +357,26 @@ namespace storm { template<> inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); + if (storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Elimination) { + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support this property on DTMCs."); + } } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support this property on DTMCs."); + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support this property on DTMCs."); + } } } else if (model->getType() == storm::models::ModelType::Mdp) { std::shared_ptr> mdp = model->template as>(); diff --git a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp index f8b262e2d..8462fa8e6 100644 --- a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp @@ -14,7 +14,7 @@ #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" #include "src/parser/PrismParser.h" -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/ExplicitModelBuilder.h" TEST(EigenDtmcPrctlModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); @@ -63,7 +63,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) { TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) { // FIXME: this should use rational numbers not functions. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -109,7 +109,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) { TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) { // FIXME: this should use rational numbers not functions. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/parametric_die.pm"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -378,7 +378,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, LRA) { TEST(EigenDtmcPrctlModelCheckerTest, Conditional) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/test_conditional.pm"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); ASSERT_EQ(4ul, model->getNumberOfStates()); ASSERT_EQ(5ul, model->getNumberOfTransitions());