From 566cef0f912d8cbc614c2caffabe543f571c60a1 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 26 Jul 2016 13:21:12 +0200 Subject: [PATCH 1/3] Started on compiling without Carl Former-commit-id: 5e0895d7c508c36a5833dd49b324cfc4b81e2609 --- src/adapters/EigenAdapter.cpp | 3 ++ src/builder/ExplicitModelBuilder.cpp | 6 ++- src/cli/cli.cpp | 8 +++ src/cli/entrypoints.h | 2 + src/generator/Choice.cpp | 5 +- src/generator/CompressedState.cpp | 7 ++- src/generator/JaniNextStateGenerator.cpp | 6 ++- src/generator/NextStateGenerator.cpp | 4 +- src/generator/PrismNextStateGenerator.cpp | 13 ++++- src/generator/StateBehavior.cpp | 6 ++- .../csl/SparseCtmcCslModelChecker.cpp | 5 +- .../csl/helper/SparseCtmcCslHelper.cpp | 53 ++++++++++++------- .../prctl/SparseDtmcPrctlModelChecker.cpp | 5 +- .../prctl/SparseMdpPrctlModelChecker.cpp | 5 +- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 3 ++ .../prctl/helper/SparseMdpPrctlHelper.cpp | 3 +- .../SparsePropositionalModelChecker.cpp | 4 +- .../SparseDtmcEliminationModelChecker.cpp | 3 ++ src/modelchecker/results/CheckResult.cpp | 4 +- .../ExplicitQuantitativeCheckResult.cpp | 3 ++ src/models/sparse/Ctmc.cpp | 6 ++- src/models/sparse/DeterministicModel.cpp | 6 ++- src/models/sparse/Dtmc.cpp | 4 +- src/models/sparse/MarkovAutomaton.cpp | 3 +- src/models/sparse/Mdp.cpp | 6 ++- src/models/sparse/Model.cpp | 9 +++- src/models/sparse/Model.h | 2 + src/models/sparse/NondeterministicModel.cpp | 6 ++- src/models/sparse/StandardRewardModel.cpp | 2 + src/parser/DFTGalileoParser.cpp | 4 ++ src/solver/EigenLinearEquationSolver.cpp | 22 ++++---- src/solver/EigenLinearEquationSolver.h | 4 +- .../EliminationLinearEquationSolver.cpp | 7 ++- src/solver/LinearEquationSolver.cpp | 11 ++-- src/solver/LinearEquationSolver.h | 3 +- src/solver/MinMaxLinearEquationSolver.cpp | 9 ++-- src/solver/SolveGoal.cpp | 3 +- .../StandardMinMaxLinearEquationSolver.cpp | 7 ++- src/solver/TerminationCondition.cpp | 3 +- .../ConditionalStateEliminator.cpp | 4 +- .../DynamicStatePriorityQueue.cpp | 3 ++ .../stateelimination/EliminatorBase.cpp | 8 +-- .../EquationSystemEliminator.cpp | 5 +- .../LongRunAverageEliminator.cpp | 4 +- .../PrioritizedStateEliminator.cpp | 4 +- .../stateelimination/StateEliminator.cpp | 4 +- src/storage/Distribution.cpp | 2 + src/storage/FlexibleSparseMatrix.cpp | 5 +- .../MaximalEndComponentDecomposition.cpp | 3 +- src/storage/SparseMatrix.cpp | 2 + ...tronglyConnectedComponentDecomposition.cpp | 8 +-- .../BisimulationDecomposition.cpp | 2 + ...ministicModelBisimulationDecomposition.cpp | 2 + ...ministicModelBisimulationDecomposition.cpp | 4 +- .../expressions/ExpressionEvaluator.cpp | 4 +- src/storage/expressions/ExpressionEvaluator.h | 4 +- .../expressions/ExpressionEvaluatorBase.cpp | 5 +- .../expressions/ExprtkExpressionEvaluator.cpp | 5 +- .../expressions/ToRationalFunctionVisitor.cpp | 4 +- .../expressions/ToRationalFunctionVisitor.h | 4 +- .../expressions/ToRationalNumberVisitor.cpp | 20 +++++-- src/storm-dyftee.cpp | 4 ++ src/utility/constants.cpp | 51 ++++++++++-------- src/utility/graph.cpp | 15 ++---- src/utility/parametric.h | 1 + src/utility/prism.cpp | 4 +- src/utility/stateelimination.cpp | 4 +- src/utility/storm.h | 4 +- 68 files changed, 322 insertions(+), 132 deletions(-) diff --git a/src/adapters/EigenAdapter.cpp b/src/adapters/EigenAdapter.cpp index 350ca8e20..94964964b 100644 --- a/src/adapters/EigenAdapter.cpp +++ b/src/adapters/EigenAdapter.cpp @@ -21,7 +21,10 @@ namespace storm { } template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); + +#ifdef STORM_HAVE_CARL template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); +#endif } } diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp index bb62757a4..5faf386e5 100644 --- a/src/builder/ExplicitModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -412,9 +412,11 @@ namespace storm { // Explicitly instantiate the class. template class ExplicitModelBuilder, uint32_t>; + +#ifdef STORM_HAVE_CARL template class ExplicitModelBuilder, uint32_t>; - - template class ExplicitModelBuilder, uint32_t>; template class ExplicitModelBuilder, uint32_t>; + template class ExplicitModelBuilder, uint32_t>; +#endif } } diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 0c2e80f53..f71f71264 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -228,9 +228,17 @@ namespace storm { } if (storm::settings::getModule().isParametricSet()) { +#ifdef STORM_HAVE_CARL buildAndCheckSymbolicModel(preprocessedProgram, preprocessedFormulas, true); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); +#endif } else if (storm::settings::getModule().isExactSet()) { +#ifdef STORM_HAVE_CARL buildAndCheckSymbolicModel(preprocessedProgram, preprocessedFormulas, true); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); +#endif } else { buildAndCheckSymbolicModel(preprocessedProgram, preprocessedFormulas, true); } diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index c2990b072..ccd48e42b 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -224,6 +224,7 @@ namespace storm { } } +#ifdef STORM_HAVE_CARL template<> void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); @@ -235,6 +236,7 @@ namespace storm { STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); buildAndCheckSymbolicModelWithSparseEngine(program, formulas, onlyInitialStatesRelevant); } +#endif template void buildAndCheckExplicitModel(std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { diff --git a/src/generator/Choice.cpp b/src/generator/Choice.cpp index 7a209ccc4..7f91a4b4d 100644 --- a/src/generator/Choice.cpp +++ b/src/generator/Choice.cpp @@ -100,7 +100,10 @@ namespace storm { } template class Choice; + +#ifdef STORM_HAVE_CARL template class Choice; template class Choice; +#endif } -} \ No newline at end of file +} diff --git a/src/generator/CompressedState.cpp b/src/generator/CompressedState.cpp index 3a229112f..d7707d740 100644 --- a/src/generator/CompressedState.cpp +++ b/src/generator/CompressedState.cpp @@ -30,8 +30,11 @@ namespace storm { } 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); + +#ifdef STORM_HAVE_CARL 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); +#endif } -} \ No newline at end of file +} diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 9e0f10b7f..cfb08fb79 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -492,8 +492,10 @@ namespace storm { } template class JaniNextStateGenerator; + +#ifdef STORM_HAVE_CARL template class JaniNextStateGenerator; template class JaniNextStateGenerator; - +#endif } -} \ No newline at end of file +} diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index 54fb2f280..834a84dac 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -303,8 +303,10 @@ namespace storm { } template class NextStateGenerator; + +#ifdef STORM_HAVE_CARL template class NextStateGenerator; template class NextStateGenerator; - +#endif } } diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 552cd30a9..c0026a98d 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -77,7 +77,11 @@ 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. +#ifdef STORM_HAVE_CARL if (!std::is_same::value && program.hasUndefinedConstants()) { +#else + if (program.hasUndefinedConstants()) { +#endif std::vector> undefinedConstants = program.getUndefinedConstants(); std::stringstream stream; bool printComma = false; @@ -91,9 +95,13 @@ namespace storm { } stream << "."; STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); - } else if (std::is_same::value && !program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) { + } + +#ifdef STORM_HAVE_CARL + 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."); } +#endif } template @@ -561,7 +569,10 @@ namespace storm { } template class PrismNextStateGenerator; + +#ifdef STORM_HAVE_CARL template class PrismNextStateGenerator; template class PrismNextStateGenerator; +#endif } } diff --git a/src/generator/StateBehavior.cpp b/src/generator/StateBehavior.cpp index 28e256c18..4e71c537f 100644 --- a/src/generator/StateBehavior.cpp +++ b/src/generator/StateBehavior.cpp @@ -56,8 +56,10 @@ namespace storm { } template class StateBehavior; + +#ifdef STORM_HAVE_CARL template class StateBehavior; template class StateBehavior; - +#endif } -} \ No newline at end of file +} diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 4d2d8fbea..914b71cc1 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -140,8 +140,11 @@ namespace storm { // Explicitly instantiate the model checker. template class SparseCtmcCslModelChecker>; + +#ifdef STORM_HAVE_CARL template class SparseCtmcCslModelChecker>; template class SparseCtmcCslModelChecker>; - +#endif + } // namespace modelchecker } // namespace storm diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index dab1449de..c51563507 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -688,44 +688,61 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& maybeStates, double uniformizationRate, std::vector const& exitRates); + template std::vector SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, double timeBound, double uniformizationRate, std::vector values, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + +#ifdef STORM_HAVE_CARL + template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); - - template std::vector SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, double timeBound, double uniformizationRate, std::vector values, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + + + + + + +#endif } } } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index bb3a1a701..1b36dd820 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -146,7 +146,10 @@ namespace storm { } template class SparseDtmcPrctlModelChecker>; + +#ifdef STORM_HAVE_CARL template class SparseDtmcPrctlModelChecker>; template class SparseDtmcPrctlModelChecker>; +#endif } -} \ No newline at end of file +} diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 629cf29eb..25804c37a 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -147,6 +147,9 @@ namespace storm { } template class SparseMdpPrctlModelChecker>; + +#ifdef STORM_HAVE_CARL template class SparseMdpPrctlModelChecker>; +#endif } -} \ No newline at end of file +} diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 79a85fdfe..d6b721ade 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -401,8 +401,11 @@ namespace storm { } template class SparseDtmcPrctlHelper; + +#ifdef STORM_HAVE_CARL template class SparseDtmcPrctlHelper; template class SparseDtmcPrctlHelper; +#endif } } } diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 75fbfdfea..c9f7e83c4 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -650,11 +650,12 @@ namespace storm { template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); +#ifdef STORM_HAVE_CARL template class SparseMdpPrctlHelper; template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - +#endif } } } diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp index 5ffc50140..0725cc4a2 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -57,6 +57,7 @@ namespace storm { template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; +#ifdef STORM_HAVE_CARL template class SparsePropositionalModelChecker>>; template class SparsePropositionalModelChecker>; @@ -70,5 +71,6 @@ namespace storm { 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 e6f0bbb2d..fdf541d97 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -986,7 +986,10 @@ 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/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp index 324fdd089..7d8fcd1ac 100644 --- a/src/modelchecker/results/CheckResult.cpp +++ b/src/modelchecker/results/CheckResult.cpp @@ -145,10 +145,12 @@ namespace storm { template HybridQuantitativeCheckResult& CheckResult::asHybridQuantitativeCheckResult(); template HybridQuantitativeCheckResult const& CheckResult::asHybridQuantitativeCheckResult() const; +#ifdef STORM_HAVE_CARL template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; +#endif } -} \ No newline at end of file +} diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 652c094a5..dfe624f2a 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -250,7 +250,10 @@ namespace storm { } template class ExplicitQuantitativeCheckResult; + +#ifdef STORM_HAVE_CARL template class ExplicitQuantitativeCheckResult; template class ExplicitQuantitativeCheckResult; +#endif } } diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp index e48f4590f..26b106c59 100644 --- a/src/models/sparse/Ctmc.cpp +++ b/src/models/sparse/Ctmc.cpp @@ -46,11 +46,13 @@ namespace storm { } template class Ctmc; + +#ifdef STORM_HAVE_CARL template class Ctmc; template class Ctmc>; template class Ctmc; - +#endif } // namespace sparse } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/sparse/DeterministicModel.cpp b/src/models/sparse/DeterministicModel.cpp index c2bd35b16..5962e6500 100644 --- a/src/models/sparse/DeterministicModel.cpp +++ b/src/models/sparse/DeterministicModel.cpp @@ -57,11 +57,13 @@ namespace storm { template class DeterministicModel; template class DeterministicModel; + +#ifdef STORM_HAVE_CARL template class DeterministicModel; template class DeterministicModel>; template class DeterministicModel; - +#endif } // namespace sparse } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp index 7997a1494..ce9f9e5aa 100644 --- a/src/models/sparse/Dtmc.cpp +++ b/src/models/sparse/Dtmc.cpp @@ -69,11 +69,13 @@ namespace storm { template class Dtmc; template class Dtmc; + +#ifdef STORM_HAVE_CARL template class Dtmc; template class Dtmc>; template class Dtmc; - +#endif } // namespace sparse } // namespace models } // namespace storm diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index b09da840e..887d3a13b 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -366,11 +366,12 @@ namespace storm { template class MarkovAutomaton; // template class MarkovAutomaton; +#ifdef STORM_HAVE_CARL template class MarkovAutomaton; template class MarkovAutomaton>; template class MarkovAutomaton; - +#endif } // namespace sparse } // namespace models } // namespace storm diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp index cf436c7e1..8db2670f5 100644 --- a/src/models/sparse/Mdp.cpp +++ b/src/models/sparse/Mdp.cpp @@ -98,11 +98,13 @@ namespace storm { template class Mdp; template class Mdp; + +#ifdef STORM_HAVE_CARL template class Mdp; template class Mdp>; template class Mdp; - +#endif } // namespace sparse } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index 8ea0710dc..d6eefe93a 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -312,7 +312,11 @@ namespace storm { template bool Model::supportsParameters() const { +#ifdef STORM_HAVE_CARL return std::is_same::value; +#else + return false; +#endif } template @@ -346,18 +350,21 @@ namespace storm { return this->rewardModels; } +#ifdef STORM_HAVE_CARL std::set getProbabilityParameters(Model const& model) { return storm::storage::getVariables(model.getTransitionMatrix()); } +#endif template class Model; template class Model; +#ifdef STORM_HAVE_CARL template class Model; template class Model>; template class Model; - +#endif } } } diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index a4422a8be..5936b0fe2 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -357,7 +357,9 @@ namespace storm { boost::optional> choiceLabeling; }; +#ifdef STORM_HAVE_CARL std::set getProbabilityParameters(Model const& model); +#endif } // namespace sparse } // namespace models } // namespace storm diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp index 3a4af6664..f3c4d29d4 100644 --- a/src/models/sparse/NondeterministicModel.cpp +++ b/src/models/sparse/NondeterministicModel.cpp @@ -169,6 +169,8 @@ namespace storm { template class NondeterministicModel; template class NondeterministicModel; + +#ifdef STORM_HAVE_CARL template class NondeterministicModel; template class NondeterministicModel>; @@ -176,7 +178,7 @@ namespace storm { template void NondeterministicModel>::modifyStateRewards(std::string const& modelName, std::map const& modifications); template class NondeterministicModel; - +#endif } } -} \ No newline at end of file +} diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp index 823d3a884..a539cfd15 100644 --- a/src/models/sparse/StandardRewardModel.cpp +++ b/src/models/sparse/StandardRewardModel.cpp @@ -318,6 +318,7 @@ namespace storm { 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; @@ -346,6 +347,7 @@ 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/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index 2cdda4929..5fc2e7c5a 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -71,12 +71,16 @@ namespace storm { toplevelId = stripQuotsFromName(line.substr(toplevelToken.size() + 1)); } else if (boost::starts_with(line, parametricToken)) { +#ifdef STORM_HAVE_CARL STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions."); std::string parameter = stripQuotsFromName(line.substr(parametricToken.size() + 1)); storm::expressions::Variable var = manager->declareRationalVariable(parameter); identifierMapping.emplace(var.getName(), var); parser.setIdentifierMapping(identifierMapping); STORM_LOG_TRACE("Added parameter: " << var.getName()); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); +#endif } else { std::vector tokens; boost::split(tokens, line, boost::is_any_of(" ")); diff --git a/src/solver/EigenLinearEquationSolver.cpp b/src/solver/EigenLinearEquationSolver.cpp index 25c16f1ae..47117b9a3 100644 --- a/src/solver/EigenLinearEquationSolver.cpp +++ b/src/solver/EigenLinearEquationSolver.cpp @@ -94,6 +94,7 @@ namespace storm { return restart; } +#ifdef STORM_HAVE_CARL EigenLinearEquationSolverSettings::EigenLinearEquationSolverSettings() { // Intentionally left empty. } @@ -101,6 +102,7 @@ namespace storm { EigenLinearEquationSolverSettings::EigenLinearEquationSolverSettings() { // Intentionally left empty. } +#endif template EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, EigenLinearEquationSolverSettings const& settings) : eigenA(storm::adapters::EigenAdapter::toEigenSparseMatrix(A)), settings(settings) { @@ -255,8 +257,8 @@ namespace storm { return eigenA->cols(); } - // Specialization form storm::RationalNumber - +#ifdef STORM_HAVE_CARL + // Specialization for storm::RationalNumber template<> void EigenLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b) const { // Map the input vectors to Eigen's format. @@ -268,8 +270,7 @@ namespace storm { solver._solve_impl(eigenB, eigenX); } - // Specialization form storm::RationalFunction - + // Specialization for storm::RationalFunction template<> void EigenLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b) const { // Map the input vectors to Eigen's format. @@ -280,7 +281,8 @@ namespace storm { solver.compute(*eigenA); solver._solve_impl(eigenB, eigenX); } - +#endif + template std::unique_ptr> EigenLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { return std::make_unique>(matrix, settings); @@ -307,16 +309,18 @@ namespace storm { } template class EigenLinearEquationSolverSettings; + template class EigenLinearEquationSolver; + template class EigenLinearEquationSolverFactory; + +#ifdef STORM_HAVE_CARL template class EigenLinearEquationSolverSettings; template class EigenLinearEquationSolverSettings; - template class EigenLinearEquationSolver; template class EigenLinearEquationSolver; template class EigenLinearEquationSolver; - template class EigenLinearEquationSolverFactory; template class EigenLinearEquationSolverFactory; template class EigenLinearEquationSolverFactory; - +#endif } -} \ No newline at end of file +} diff --git a/src/solver/EigenLinearEquationSolver.h b/src/solver/EigenLinearEquationSolver.h index 04c6c9718..688dcae64 100644 --- a/src/solver/EigenLinearEquationSolver.h +++ b/src/solver/EigenLinearEquationSolver.h @@ -40,6 +40,7 @@ namespace storm { uint_fast64_t restart; }; +#ifdef STORM_HAVE_CARL template<> class EigenLinearEquationSolverSettings { public: @@ -51,6 +52,7 @@ namespace storm { public: EigenLinearEquationSolverSettings(); }; +#endif /*! * A class that uses the Eigen library to implement the LinearEquationSolver interface. @@ -96,4 +98,4 @@ namespace storm { EigenLinearEquationSolverSettings settings; }; } -} \ No newline at end of file +} diff --git a/src/solver/EliminationLinearEquationSolver.cpp b/src/solver/EliminationLinearEquationSolver.cpp index 982d2a54b..8cf773c16 100644 --- a/src/solver/EliminationLinearEquationSolver.cpp +++ b/src/solver/EliminationLinearEquationSolver.cpp @@ -173,16 +173,19 @@ namespace storm { } template class EliminationLinearEquationSolverSettings; + template class EliminationLinearEquationSolver; + template class EliminationLinearEquationSolverFactory; + +#ifdef STORM_HAVE_CARL template class EliminationLinearEquationSolverSettings; template class EliminationLinearEquationSolverSettings; - template class EliminationLinearEquationSolver; template class EliminationLinearEquationSolver; template class EliminationLinearEquationSolver; - template class EliminationLinearEquationSolverFactory; template class EliminationLinearEquationSolverFactory; template class EliminationLinearEquationSolverFactory; +#endif } } diff --git a/src/solver/LinearEquationSolver.cpp b/src/solver/LinearEquationSolver.cpp index 81dc4124b..c4d46cd46 100644 --- a/src/solver/LinearEquationSolver.cpp +++ b/src/solver/LinearEquationSolver.cpp @@ -121,6 +121,7 @@ namespace storm { return std::make_unique>(*this); } +#ifdef STORM_HAVE_CARL std::unique_ptr> GeneralLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { return selectSolver(matrix); } @@ -162,18 +163,22 @@ namespace storm { std::unique_ptr> GeneralLinearEquationSolverFactory::clone() const { return std::make_unique>(*this); } +#endif template class LinearEquationSolver; + template class LinearEquationSolverFactory; + template class GeneralLinearEquationSolverFactory; + +#ifdef STORM_HAVE_CARL template class LinearEquationSolver; template class LinearEquationSolver; - template class LinearEquationSolverFactory; template class LinearEquationSolverFactory; template class LinearEquationSolverFactory; - template class GeneralLinearEquationSolverFactory; template class GeneralLinearEquationSolverFactory; template class GeneralLinearEquationSolverFactory; +#endif } -} \ No newline at end of file +} diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index aa243d593..5adac8ea1 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -154,6 +154,7 @@ namespace storm { std::unique_ptr> selectSolver(MatrixType&& matrix) const; }; +#ifdef STORM_HAVE_CARL template<> class GeneralLinearEquationSolverFactory : public LinearEquationSolverFactory { public: @@ -179,7 +180,7 @@ namespace storm { template std::unique_ptr> selectSolver(MatrixType&& matrix) const; }; - +#endif } // namespace solver } // namespace storm diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index a92f19dd9..c82514a37 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -144,6 +144,7 @@ namespace storm { return result; } +#ifdef STORM_HAVE_CARL template<> template std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { @@ -152,15 +153,17 @@ namespace storm { STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration, storm::exceptions::InvalidSettingsException, "For this data type only value iteration and policy iteration are available."); return std::make_unique>(std::forward(matrix), std::make_unique>()); } - +#endif template class MinMaxLinearEquationSolver; template class MinMaxLinearEquationSolver; - template class MinMaxLinearEquationSolver; template class MinMaxLinearEquationSolverFactory; template class GeneralMinMaxLinearEquationSolverFactory; + +#ifdef STORM_HAVE_CARL + template class MinMaxLinearEquationSolver; template class MinMaxLinearEquationSolverFactory; template class GeneralMinMaxLinearEquationSolverFactory; - +#endif } } diff --git a/src/solver/SolveGoal.cpp b/src/solver/SolveGoal.cpp index 2f0cd365c..622a0c8de 100644 --- a/src/solver/SolveGoal.cpp +++ b/src/solver/SolveGoal.cpp @@ -51,8 +51,9 @@ namespace storm { template std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); template std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); +#ifdef STORM_HAVE_CARL template std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); template std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); - +#endif } } diff --git a/src/solver/StandardMinMaxLinearEquationSolver.cpp b/src/solver/StandardMinMaxLinearEquationSolver.cpp index 4e0609e80..1a1f1fcda 100644 --- a/src/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/solver/StandardMinMaxLinearEquationSolver.cpp @@ -370,6 +370,7 @@ namespace storm { } } +#ifdef STORM_HAVE_CARL template<> StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, bool trackScheduler) : MinMaxLinearEquationSolverFactory(trackScheduler) { switch (solverType) { @@ -379,6 +380,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot create the requested solver for this data type."); } } +#endif template std::unique_ptr> StandardMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { @@ -441,11 +443,12 @@ namespace storm { template class NativeMinMaxLinearEquationSolverFactory; template class EliminationMinMaxLinearEquationSolverFactory; +#ifdef STORM_HAVE_CARL template class StandardMinMaxLinearEquationSolverSettings; template class StandardMinMaxLinearEquationSolver; template class StandardMinMaxLinearEquationSolverFactory; template class EigenMinMaxLinearEquationSolverFactory; template class EliminationMinMaxLinearEquationSolverFactory; - +#endif } -} \ No newline at end of file +} diff --git a/src/solver/TerminationCondition.cpp b/src/solver/TerminationCondition.cpp index 0503723bc..b0f155470 100644 --- a/src/solver/TerminationCondition.cpp +++ b/src/solver/TerminationCondition.cpp @@ -40,8 +40,9 @@ namespace storm { template class TerminateIfFilteredSumExceedsThreshold; template class TerminateIfFilteredExtremumExceedsThreshold; +#ifdef STORM_HAVE_CARL template class TerminateIfFilteredSumExceedsThreshold; template class TerminateIfFilteredExtremumExceedsThreshold; - +#endif } } diff --git a/src/solver/stateelimination/ConditionalStateEliminator.cpp b/src/solver/stateelimination/ConditionalStateEliminator.cpp index 0a86894bc..21ffec7ac 100644 --- a/src/solver/stateelimination/ConditionalStateEliminator.cpp +++ b/src/solver/stateelimination/ConditionalStateEliminator.cpp @@ -61,9 +61,11 @@ namespace storm { } template class ConditionalStateEliminator; + +#ifdef STORM_HAVE_CARL template class ConditionalStateEliminator; template class ConditionalStateEliminator; - +#endif } // namespace stateelimination } // namespace storage } // namespace storm diff --git a/src/solver/stateelimination/DynamicStatePriorityQueue.cpp b/src/solver/stateelimination/DynamicStatePriorityQueue.cpp index ec2c4fe3f..a0fede010 100644 --- a/src/solver/stateelimination/DynamicStatePriorityQueue.cpp +++ b/src/solver/stateelimination/DynamicStatePriorityQueue.cpp @@ -62,8 +62,11 @@ namespace storm { } template class DynamicStatePriorityQueue; + +#ifdef STORM_HAVE_CARL template class DynamicStatePriorityQueue; template class DynamicStatePriorityQueue; +#endif } } } diff --git a/src/solver/stateelimination/EliminatorBase.cpp b/src/solver/stateelimination/EliminatorBase.cpp index 43f94f329..4a083d5fc 100644 --- a/src/solver/stateelimination/EliminatorBase.cpp +++ b/src/solver/stateelimination/EliminatorBase.cpp @@ -274,13 +274,15 @@ namespace storm { } template class EliminatorBase; + template class EliminatorBase; + +#ifdef STORM_HAVE_CARL template class EliminatorBase; template class EliminatorBase; - template class EliminatorBase; template class EliminatorBase; template class EliminatorBase; - +#endif } } -} \ No newline at end of file +} diff --git a/src/solver/stateelimination/EquationSystemEliminator.cpp b/src/solver/stateelimination/EquationSystemEliminator.cpp index 2ffe29705..f08f49107 100644 --- a/src/solver/stateelimination/EquationSystemEliminator.cpp +++ b/src/solver/stateelimination/EquationSystemEliminator.cpp @@ -10,8 +10,11 @@ namespace storm { } template class EquationSystemEliminator; + +#ifdef STORM_HAVE_CARL template class EquationSystemEliminator; template class EquationSystemEliminator; +#endif } } -} \ No newline at end of file +} diff --git a/src/solver/stateelimination/LongRunAverageEliminator.cpp b/src/solver/stateelimination/LongRunAverageEliminator.cpp index 758f71a14..982342b5a 100644 --- a/src/solver/stateelimination/LongRunAverageEliminator.cpp +++ b/src/solver/stateelimination/LongRunAverageEliminator.cpp @@ -23,9 +23,11 @@ namespace storm { } template class LongRunAverageEliminator; + +#ifdef STORM_HAVE_CARL template class LongRunAverageEliminator; template class LongRunAverageEliminator; - +#endif } // namespace stateelimination } // namespace storage } // namespace storm diff --git a/src/solver/stateelimination/PrioritizedStateEliminator.cpp b/src/solver/stateelimination/PrioritizedStateEliminator.cpp index 134cb3264..1b8cca6ff 100644 --- a/src/solver/stateelimination/PrioritizedStateEliminator.cpp +++ b/src/solver/stateelimination/PrioritizedStateEliminator.cpp @@ -29,9 +29,11 @@ namespace storm { } template class PrioritizedStateEliminator; + +#ifdef STORM_HAVE_CARL template class PrioritizedStateEliminator; template class PrioritizedStateEliminator; - +#endif } // namespace stateelimination } // namespace storage } // namespace storm diff --git a/src/solver/stateelimination/StateEliminator.cpp b/src/solver/stateelimination/StateEliminator.cpp index 98b1d64b3..c134d9ffa 100644 --- a/src/solver/stateelimination/StateEliminator.cpp +++ b/src/solver/stateelimination/StateEliminator.cpp @@ -28,9 +28,11 @@ namespace storm { } template class StateEliminator; + +#ifdef STORM_HAVE_CARL template class StateEliminator; template class StateEliminator; - +#endif } // namespace stateelimination } // namespace storage } // namespace storm diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp index 7c3b5d99f..78e4a477d 100644 --- a/src/storage/Distribution.cpp +++ b/src/storage/Distribution.cpp @@ -152,10 +152,12 @@ 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/FlexibleSparseMatrix.cpp b/src/storage/FlexibleSparseMatrix.cpp index 563f86633..102d20304 100644 --- a/src/storage/FlexibleSparseMatrix.cpp +++ b/src/storage/FlexibleSparseMatrix.cpp @@ -269,13 +269,14 @@ namespace storm { // Explicitly instantiate the matrix. template class FlexibleSparseMatrix; template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix); + +#ifdef STORM_HAVE_CARL template class FlexibleSparseMatrix; template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix); -#ifdef STORM_HAVE_CARL template class FlexibleSparseMatrix; template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix); #endif } // namespace storage -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index d410b2546..0861513ce 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -193,8 +193,9 @@ namespace storm { template class MaximalEndComponentDecomposition; template MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); +#ifdef STORM_HAVE_CARL template class MaximalEndComponentDecomposition; template MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); - +#endif } } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 95f65ce99..add3debbb 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -1213,10 +1213,12 @@ namespace storm { } } +#ifdef STORM_HAVE_CARL template<> void SparseMatrix::performSuccessiveOverRelaxationStep(Interval omega, std::vector& x, std::vector const& b) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported."); } +#endif template void SparseMatrix::multiplyVectorWithMatrix(std::vector const& vector, std::vector& result) const { diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index e129c8b85..c32184681 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -227,16 +227,17 @@ namespace storm { } // Explicitly instantiate the SCC decomposition. - template class StronglyConnectedComponentDecomposition; + 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 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); +#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); @@ -246,5 +247,6 @@ namespace storm { 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 +} // namespace storm diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index 30fc5a2c9..dbad8c633 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -323,6 +323,7 @@ namespace storm { 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>; @@ -330,5 +331,6 @@ namespace storm { 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 89408e620..3f70fd379 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -652,10 +652,12 @@ 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 a1eea43dc..64a7efe45 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -416,8 +416,10 @@ 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 6d44d680a..cf1493dac 100644 --- a/src/storage/expressions/ExpressionEvaluator.cpp +++ b/src/storage/expressions/ExpressionEvaluator.cpp @@ -30,6 +30,7 @@ namespace storm { this->variableToExpressionMap[variable] = this->getManager().rational(value); } +#ifdef STORM_HAVE_CARL ExpressionEvaluator::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorWithVariableToExpressionMap(manager) { // Intentionally left empty. } @@ -50,5 +51,6 @@ namespace storm { template class ExpressionEvaluatorWithVariableToExpressionMap; template class ExpressionEvaluatorWithVariableToExpressionMap; +#endif } -} \ No newline at end of file +} diff --git a/src/storage/expressions/ExpressionEvaluator.h b/src/storage/expressions/ExpressionEvaluator.h index 2480af12d..e75d1cdf1 100644 --- a/src/storage/expressions/ExpressionEvaluator.h +++ b/src/storage/expressions/ExpressionEvaluator.h @@ -35,6 +35,7 @@ namespace storm { std::unordered_map variableToExpressionMap; }; +#ifdef STORM_HAVE_CARL template<> class ExpressionEvaluator : public ExpressionEvaluatorWithVariableToExpressionMap { public: @@ -58,7 +59,8 @@ namespace storm { // A visitor that can be used to translate expressions to rational functions. mutable ToRationalFunctionVisitor rationalFunctionVisitor; }; +#endif } } -#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATOR_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATOR_H_ */ diff --git a/src/storage/expressions/ExpressionEvaluatorBase.cpp b/src/storage/expressions/ExpressionEvaluatorBase.cpp index d98810886..aeca1b656 100644 --- a/src/storage/expressions/ExpressionEvaluatorBase.cpp +++ b/src/storage/expressions/ExpressionEvaluatorBase.cpp @@ -16,7 +16,10 @@ 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 942c17172..d24bc742c 100755 --- a/src/storage/expressions/ExprtkExpressionEvaluator.cpp +++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -83,7 +83,10 @@ 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 71e052bee..1a3dd0fc3 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp @@ -7,6 +7,8 @@ namespace storm { namespace expressions { + +#ifdef STORM_HAVE_CARL template ToRationalFunctionVisitor::ToRationalFunctionVisitor() : ExpressionVisitor(), cache(new carl::Cache>()) { // Intentionally left empty. @@ -95,6 +97,6 @@ namespace storm { } template class ToRationalFunctionVisitor; - +#endif } } diff --git a/src/storage/expressions/ToRationalFunctionVisitor.h b/src/storage/expressions/ToRationalFunctionVisitor.h index 6bd3a205b..12603f44e 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.h +++ b/src/storage/expressions/ToRationalFunctionVisitor.h @@ -10,6 +10,7 @@ namespace storm { namespace expressions { +#ifdef STORM_HAVE_CARL template class ToRationalFunctionVisitor : public ExpressionVisitor { public: @@ -45,7 +46,8 @@ namespace storm { // The cache that is used in case the underlying type needs a cache. std::shared_ptr>> cache; }; +#endif } } -#endif /* STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ */ diff --git a/src/storage/expressions/ToRationalNumberVisitor.cpp b/src/storage/expressions/ToRationalNumberVisitor.cpp index b17ec335a..785f36950 100644 --- a/src/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storage/expressions/ToRationalNumberVisitor.cpp @@ -2,6 +2,7 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/NotSupportedException.h" namespace storm { namespace expressions { @@ -52,7 +53,7 @@ namespace storm { template boost::any ToRationalNumberVisitor::visit(BinaryRelationExpression const& expression) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template @@ -62,30 +63,39 @@ namespace storm { template boost::any ToRationalNumberVisitor::visit(UnaryBooleanFunctionExpression const& expression) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template boost::any ToRationalNumberVisitor::visit(UnaryNumericalFunctionExpression const& expression) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template boost::any ToRationalNumberVisitor::visit(BooleanLiteralExpression const& expression) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template boost::any ToRationalNumberVisitor::visit(IntegerLiteralExpression const& expression) { +#ifdef STORM_HAVE_CARL return RationalNumberType(carl::rationalize(static_cast(expression.getValue()))); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build."); +#endif } template boost::any ToRationalNumberVisitor::visit(DoubleLiteralExpression const& expression) { +#ifdef STORM_HAVE_CARL return RationalNumberType(carl::rationalize(expression.getValue())); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build."); +#endif } +#ifdef STORM_HAVE_CARL template class ToRationalNumberVisitor; - +#endif } } diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 6b6f74d46..1bad1c994 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -139,7 +139,11 @@ int main(const int argc, const char** argv) { // From this point on we are ready to carry out the actual computations. if (parametric) { +#ifdef STORM_HAVE_CARL analyzeDFT(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC() ); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); +#endif } else { analyzeDFT(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC()); } diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 4821d1b94..eafe4f1bd 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -40,6 +40,7 @@ namespace storm { return true; } +#ifdef STORM_HAVE_CARL template<> bool isOne(storm::RationalNumber const& a) { return carl::isOne(a); @@ -91,18 +92,19 @@ namespace storm { // FIXME: this should be treated more properly. return storm::RationalFunction(-1.0); } +#endif template ValueType pow(ValueType const& value, uint_fast64_t exponent) { return std::pow(value, exponent); } - template - ValueType simplify(ValueType value) { - // In the general case, we don't do anything here, but merely return the value. If something else is - // supposed to happen here, the templated function can be specialized for this particular type. - return value; - } + template + ValueType simplify(ValueType value) { + // In the general case, we don't do anything here, but merely return the value. If something else is + // supposed to happen here, the templated function can be specialized for this particular type. + return value; + } template<> double convertNumber(double const& number){ @@ -114,6 +116,7 @@ namespace storm { return std::fabs(number); } +#ifdef STORM_HAVE_CARL template<> RationalFunction& simplify(RationalFunction& value); @@ -162,6 +165,7 @@ namespace storm { storm::RationalNumber abs(storm::RationalNumber const& number) { return carl::abs(number); } +#endif template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { @@ -186,17 +190,17 @@ namespace storm { template bool isZero(double const& value); template bool isConstant(double const& value); - template double one(); - template double zero(); - template double infinity(); + template double one(); + template double zero(); + template double infinity(); - template double pow(double const& value, uint_fast64_t exponent); + template double pow(double const& value, uint_fast64_t exponent); - template double simplify(double value); + template double simplify(double value); - template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); template double abs(double const& number); @@ -204,17 +208,17 @@ namespace storm { template bool isZero(float const& value); template bool isConstant(float const& value); - template float one(); - template float zero(); - template float infinity(); + template float one(); + template float zero(); + template float infinity(); - template float pow(float const& value, uint_fast64_t exponent); + template float pow(float const& value, uint_fast64_t exponent); - template float simplify(float value); + template float simplify(float value); - template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); template bool isOne(int const& value); template bool isZero(int const& value); @@ -252,6 +256,7 @@ namespace storm { template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); +#ifdef STORM_HAVE_CARL // Instantiations for rational number. template bool isOne(storm::RationalNumber const& value); template bool isZero(storm::RationalNumber const& value); @@ -273,7 +278,7 @@ namespace storm { template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); -#ifdef STORM_HAVE_CARL + // Instantiations for rational function. template bool isOne(RationalFunction const& value); template bool isZero(RationalFunction const& value); template bool isConstant(RationalFunction const& value); diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 8a7e1e185..79b4a32a0 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -22,6 +22,8 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" +#include + namespace storm { namespace utility { namespace graph { @@ -1180,24 +1182,21 @@ namespace storm { template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; // 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 storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); 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::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& rowFilter); @@ -1214,33 +1213,27 @@ namespace storm { 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 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 storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); diff --git a/src/utility/parametric.h b/src/utility/parametric.h index 244e1c141..0805ec34d 100644 --- a/src/utility/parametric.h +++ b/src/utility/parametric.h @@ -10,6 +10,7 @@ #include "src/adapters/CarlAdapter.h" +#include namespace storm { namespace utility { diff --git a/src/utility/prism.cpp b/src/utility/prism.cpp index 947d7e8a2..a34f5e531 100644 --- a/src/utility/prism.cpp +++ b/src/utility/prism.cpp @@ -9,6 +9,8 @@ #include "src/exceptions/InvalidArgumentException.h" +#include + namespace storm { namespace utility { namespace prism { @@ -82,4 +84,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/src/utility/stateelimination.cpp b/src/utility/stateelimination.cpp index 7076c3f15..e70bc6b02 100644 --- a/src/utility/stateelimination.cpp +++ b/src/utility/stateelimination.cpp @@ -202,6 +202,7 @@ namespace storm { template std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse); template std::vector getStateDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward); +#ifdef STORM_HAVE_CARL template uint_fast64_t estimateComplexity(storm::RationalNumber const& value); template std::shared_ptr createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& 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); @@ -215,6 +216,7 @@ 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 std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse); template std::vector getStateDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward); +#endif } } -} \ No newline at end of file +} diff --git a/src/utility/storm.h b/src/utility/storm.h index 49ef4bf04..d6b074832 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -220,6 +220,7 @@ namespace storm { } } +#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."); @@ -229,6 +230,7 @@ namespace storm { 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) { @@ -332,6 +334,7 @@ namespace storm { } +#ifdef STORM_HAVE_CARL template<> inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); @@ -349,7 +352,6 @@ namespace storm { 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; filestream.open(path); From 5b8cf447c7bb073450213be85bb9b1973bfedfb8 Mon Sep 17 00:00:00 2001 From: Mavo Date: Wed, 27 Jul 2016 10:02:08 +0200 Subject: [PATCH 2/3] Small changes in tests to compile without Carl Former-commit-id: 6ec191ce0af195317f83784bf758f4e26db36f13 --- .../modelchecker/EigenDtmcPrctlModelCheckerTest.cpp | 3 ++- test/functional/solver/EigenLinearEquationSolverTest.cpp | 4 +++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp index 8caa788bb..b66c71f09 100644 --- a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp @@ -60,6 +60,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(11.0 / 3.0, quantitativeResult4[0], storm::settings::getModule().getPrecision()); } +#ifdef STORM_HAVE_CARL TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); @@ -159,7 +160,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) { EXPECT_EQ(storm::RationalNumber(11) / storm::RationalNumber(3), quantitativeResult4[0].evaluate(instantiation)); } - +#endif TEST(EigenDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); diff --git a/test/functional/solver/EigenLinearEquationSolverTest.cpp b/test/functional/solver/EigenLinearEquationSolverTest.cpp index 33d073c62..2cd90dc36 100644 --- a/test/functional/solver/EigenLinearEquationSolverTest.cpp +++ b/test/functional/solver/EigenLinearEquationSolverTest.cpp @@ -64,6 +64,7 @@ TEST(EigenLinearEquationSolver, SparseLU) { ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); } +#ifdef STORM_HAVE_CARL TEST(EigenLinearEquationSolver, SparseLU_RationalNumber) { ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder builder); storm::storage::SparseMatrixBuilder builder; @@ -115,6 +116,7 @@ TEST(EigenLinearEquationSolver, SparseLU_RationalFunction) { ASSERT_TRUE(x[1] == storm::RationalFunction(3)); ASSERT_TRUE(x[2] == storm::RationalFunction(-1)); } +#endif TEST(EigenLinearEquationSolver, DGMRES) { ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder builder); @@ -412,4 +414,4 @@ TEST(EigenLinearEquationSolver, MatrixVectorMultiplication) { storm::solver::EigenLinearEquationSolver solver(A); ASSERT_NO_THROW(solver.repeatedMultiply(x, nullptr, 4)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); -} \ No newline at end of file +} From e6abef0615bc2add8e85bd2684220332e9a9f45f Mon Sep 17 00:00:00 2001 From: Mavo Date: Wed, 27 Jul 2016 15:44:58 +0200 Subject: [PATCH 3/3] Pass compiler through to resources Former-commit-id: 250d0e989067744e9da13407755f2066ea48835f --- resources/3rdparty/CMakeLists.txt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index c93b5fa7a..8f158aa6c 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -202,7 +202,7 @@ if(USE_CARL) GIT_TAG master INSTALL_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/carl - CMAKE_ARGS -DCXX=${CMAKE_CXX_COMPILER} -DEXPORT_TO_CMAKE=0 -DUSE_CLN_NUMBERS=1 -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=1 -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl + CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DEXPORT_TO_CMAKE=0 -DUSE_CLN_NUMBERS=1 -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=1 -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl BUILD_IN_SOURCE 0 BUILD_COMMAND make lib_carl INSTALL_COMMAND make install @@ -304,7 +304,7 @@ ExternalProject_Add( DOWNLOAD_COMMAND "" PREFIX "sylvan" SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan - CMAKE_ARGS -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release + CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release BINARY_DIR "${PROJECT_BINARY_DIR}/sylvan" BUILD_IN_SOURCE 0 INSTALL_COMMAND "" @@ -349,7 +349,7 @@ ExternalProject_Add( SOURCE_DIR "${STORM_3RDPARTY_SOURCE_DIR}/gtest-1.7.0" # Force the same output paths for debug and release builds so that # we know in which place the binaries end up when using the Xcode generator - CMAKE_ARGS -Dgtest_force_shared_crt=ON -DCXX=${CMAKE_CXX_COMPILER} -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_DEBUG:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_RELEASE:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 + CMAKE_ARGS -Dgtest_force_shared_crt=ON -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_DEBUG:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_RELEASE:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 # Disable install step INSTALL_COMMAND "" BINARY_DIR "${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0" @@ -549,4 +549,4 @@ if(ENABLE_CUDA) message (STATUS "StoRM - Linking with CUDA") list(APPEND STORM_LINK_LIBRARIES ${STORM_CUDA_LIB_NAME}) include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/") -endif() \ No newline at end of file +endif()