sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Started on compiling without Carl 

Former-commit-id: 5e0895d7c5
main
Mavo 9 years ago
parent
c3972e07aa
commit
566cef0f91
68 changed files with 322 additions and 132 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 3
      src/adapters/EigenAdapter.cpp
  2. 6
      src/builder/ExplicitModelBuilder.cpp
  3. 8
      src/cli/cli.cpp
  4. 2
      src/cli/entrypoints.h
  5. 5
      src/generator/Choice.cpp
  6. 7
      src/generator/CompressedState.cpp
  7. 6
      src/generator/JaniNextStateGenerator.cpp
  8. 4
      src/generator/NextStateGenerator.cpp
  9. 13
      src/generator/PrismNextStateGenerator.cpp
  10. 6
      src/generator/StateBehavior.cpp
  11. 5
      src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  12. 53
      src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  13. 5
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  14. 5
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  15. 3
      src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  16. 3
      src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  17. 4
      src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
  18. 3
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  19. 4
      src/modelchecker/results/CheckResult.cpp
  20. 3
      src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
  21. 6
      src/models/sparse/Ctmc.cpp
  22. 6
      src/models/sparse/DeterministicModel.cpp
  23. 4
      src/models/sparse/Dtmc.cpp
  24. 3
      src/models/sparse/MarkovAutomaton.cpp
  25. 6
      src/models/sparse/Mdp.cpp
  26. 9
      src/models/sparse/Model.cpp
  27. 2
      src/models/sparse/Model.h
  28. 6
      src/models/sparse/NondeterministicModel.cpp
  29. 2
      src/models/sparse/StandardRewardModel.cpp
  30. 4
      src/parser/DFTGalileoParser.cpp
  31. 22
      src/solver/EigenLinearEquationSolver.cpp
  32. 4
      src/solver/EigenLinearEquationSolver.h
  33. 7
      src/solver/EliminationLinearEquationSolver.cpp
  34. 11
      src/solver/LinearEquationSolver.cpp
  35. 3
      src/solver/LinearEquationSolver.h
  36. 9
      src/solver/MinMaxLinearEquationSolver.cpp
  37. 3
      src/solver/SolveGoal.cpp
  38. 7
      src/solver/StandardMinMaxLinearEquationSolver.cpp
  39. 3
      src/solver/TerminationCondition.cpp
  40. 4
      src/solver/stateelimination/ConditionalStateEliminator.cpp
  41. 3
      src/solver/stateelimination/DynamicStatePriorityQueue.cpp
  42. 8
      src/solver/stateelimination/EliminatorBase.cpp
  43. 5
      src/solver/stateelimination/EquationSystemEliminator.cpp
  44. 4
      src/solver/stateelimination/LongRunAverageEliminator.cpp
  45. 4
      src/solver/stateelimination/PrioritizedStateEliminator.cpp
  46. 4
      src/solver/stateelimination/StateEliminator.cpp
  47. 2
      src/storage/Distribution.cpp
  48. 5
      src/storage/FlexibleSparseMatrix.cpp
  49. 3
      src/storage/MaximalEndComponentDecomposition.cpp
  50. 2
      src/storage/SparseMatrix.cpp
  51. 8
      src/storage/StronglyConnectedComponentDecomposition.cpp
  52. 2
      src/storage/bisimulation/BisimulationDecomposition.cpp
  53. 2
      src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
  54. 4
      src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
  55. 4
      src/storage/expressions/ExpressionEvaluator.cpp
  56. 4
      src/storage/expressions/ExpressionEvaluator.h
  57. 5
      src/storage/expressions/ExpressionEvaluatorBase.cpp
  58. 5
      src/storage/expressions/ExprtkExpressionEvaluator.cpp
  59. 4
      src/storage/expressions/ToRationalFunctionVisitor.cpp
  60. 4
      src/storage/expressions/ToRationalFunctionVisitor.h
  61. 20
      src/storage/expressions/ToRationalNumberVisitor.cpp
  62. 4
      src/storm-dyftee.cpp
  63. 51
      src/utility/constants.cpp
  64. 15
      src/utility/graph.cpp
  65. 1
      src/utility/parametric.h
  66. 4
      src/utility/prism.cpp
  67. 4
      src/utility/stateelimination.cpp
  68. 4
      src/utility/storm.h

3
src/adapters/EigenAdapter.cpp
View File

@ -21,7 +21,10 @@ namespace storm {
}
template std::unique_ptr<Eigen::SparseMatrix<double>> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix<double> const& matrix);
#ifdef STORM_HAVE_CARL
template std::unique_ptr<Eigen::SparseMatrix<storm::RationalNumber>> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix<storm::RationalNumber> const& matrix);
template std::unique_ptr<Eigen::SparseMatrix<storm::RationalFunction>> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix<storm::RationalFunction> const& matrix);
#endif
}
}

6
src/builder/ExplicitModelBuilder.cpp
View File

@ -412,9 +412,11 @@ namespace storm {
// Explicitly instantiate the class.
template class ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, uint32_t>;
#ifdef STORM_HAVE_CARL
template class ExplicitModelBuilder<RationalNumber, storm::models::sparse::StandardRewardModel<RationalNumber>, uint32_t>;
template class ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<storm::Interval>, uint32_t>;
template class ExplicitModelBuilder<RationalFunction, storm::models::sparse::StandardRewardModel<RationalFunction>, uint32_t>;
template class ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<storm::Interval>, uint32_t>;
#endif
}
}

8
src/cli/cli.cpp
View File

@ -228,9 +228,17 @@ namespace storm {
}
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
#ifdef STORM_HAVE_CARL
buildAndCheckSymbolicModel<storm::RationalFunction>(preprocessedProgram, preprocessedFormulas, true);
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build.");
#endif
} else if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
#ifdef STORM_HAVE_CARL
buildAndCheckSymbolicModel<storm::RationalNumber>(preprocessedProgram, preprocessedFormulas, true);
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build.");
#endif
} else {
buildAndCheckSymbolicModel<double>(preprocessedProgram, preprocessedFormulas, true);
}

2
src/cli/entrypoints.h
View File

@ -224,6 +224,7 @@ namespace storm {
}
}
#ifdef STORM_HAVE_CARL
template<>
void buildAndCheckSymbolicModel<storm::RationalNumber>(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().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<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one.");
buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(program, formulas, onlyInitialStatesRelevant);
}
#endif
template<typename ValueType>
void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {

5
src/generator/Choice.cpp
View File

@ -100,7 +100,10 @@ namespace storm {
}
template class Choice<double>;
#ifdef STORM_HAVE_CARL
template class Choice<storm::RationalNumber>;
template class Choice<storm::RationalFunction>;
#endif
}
}
}

7
src/generator/CompressedState.cpp
View File

@ -30,8 +30,11 @@ namespace storm {
}
template void unpackStateIntoEvaluator<double>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<double>& evaluator);
storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
#ifdef STORM_HAVE_CARL
template void unpackStateIntoEvaluator<storm::RationalNumber>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalNumber>& evaluator);
template void unpackStateIntoEvaluator<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalFunction>& evaluator);
storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
#endif
}
}
}

6
src/generator/JaniNextStateGenerator.cpp
View File

@ -492,8 +492,10 @@ namespace storm {
}
template class JaniNextStateGenerator<double>;
#ifdef STORM_HAVE_CARL
template class JaniNextStateGenerator<storm::RationalNumber>;
template class JaniNextStateGenerator<storm::RationalFunction>;
#endif
}
}
}

4
src/generator/NextStateGenerator.cpp
View File

@ -303,8 +303,10 @@ namespace storm {
}
template class NextStateGenerator<double>;
#ifdef STORM_HAVE_CARL
template class NextStateGenerator<storm::RationalNumber>;
template class NextStateGenerator<storm::RationalFunction>;
#endif
}
}

13
src/generator/PrismNextStateGenerator.cpp
View File

@ -77,7 +77,11 @@ namespace storm {
template<typename ValueType, typename StateType>
void PrismNextStateGenerator<ValueType, StateType>::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<ValueType, storm::RationalFunction>::value && program.hasUndefinedConstants()) {
#else
if (program.hasUndefinedConstants()) {
#endif
std::vector<std::reference_wrapper<storm::prism::Constant const>> 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<ValueType, storm::RationalFunction>::value && !program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
}
#ifdef STORM_HAVE_CARL
else if (std::is_same<ValueType, storm::RationalFunction>::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<typename ValueType, typename StateType>
@ -561,7 +569,10 @@ namespace storm {
}
template class PrismNextStateGenerator<double>;
#ifdef STORM_HAVE_CARL
template class PrismNextStateGenerator<storm::RationalNumber>;
template class PrismNextStateGenerator<storm::RationalFunction>;
#endif
}
}

6
src/generator/StateBehavior.cpp
View File

@ -56,8 +56,10 @@ namespace storm {
}
template class StateBehavior<double>;
#ifdef STORM_HAVE_CARL
template class StateBehavior<storm::RationalNumber>;
template class StateBehavior<storm::RationalFunction>;
#endif
}
}
}

5
src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
View File

@ -140,8 +140,11 @@ namespace storm {
// Explicitly instantiate the model checker.
template class SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>>;
#ifdef STORM_HAVE_CARL
template class SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<storm::RationalNumber>>;
template class SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>>;
#endif
} // namespace modelchecker
} // namespace storm

53
src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
View File

@ -688,44 +688,61 @@ namespace storm {
template std::vector<double> SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<double> const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<double> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<double> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template storm::storage::SparseMatrix<double> SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::BitVector const& maybeStates, double uniformizationRate, std::vector<double> const& exitRates);
template std::vector<double> SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix<double> const& uniformizedMatrix, std::vector<double> const* addVector, double timeBound, double uniformizationRate, std::vector<double> values, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
#ifdef STORM_HAVE_CARL
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template storm::storage::SparseMatrix<double> SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRates);
template storm::storage::SparseMatrix<storm::RationalNumber> SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRates);
template storm::storage::SparseMatrix<storm::RationalFunction> SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRates);
template std::vector<double> SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix<double> const& uniformizedMatrix, std::vector<double> const* addVector, double timeBound, double uniformizationRate, std::vector<double> values, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
#endif
}
}
}

5
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -146,7 +146,10 @@ namespace storm {
}
template class SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>>;
#ifdef STORM_HAVE_CARL
template class SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>>;
template class SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>;
#endif
}
}
}

5
src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
View File

@ -147,6 +147,9 @@ namespace storm {
}
template class SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>>;
#ifdef STORM_HAVE_CARL
template class SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
#endif
}
}
}

3
src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
View File

@ -401,8 +401,11 @@ namespace storm {
}
template class SparseDtmcPrctlHelper<double>;
#ifdef STORM_HAVE_CARL
template class SparseDtmcPrctlHelper<storm::RationalNumber>;
template class SparseDtmcPrctlHelper<storm::RationalFunction>;
#endif
}
}
}

3
src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -650,11 +650,12 @@ namespace storm {
template std::vector<double> SparseMdpPrctlHelper<double>::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::models::sparse::StandardRewardModel<double> const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
template std::vector<double> SparseMdpPrctlHelper<double>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
#ifdef STORM_HAVE_CARL
template class SparseMdpPrctlHelper<storm::RationalNumber>;
template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
#endif
}
}
}

4
src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
View File

@ -57,6 +57,7 @@ namespace storm {
template class SparsePropositionalModelChecker<storm::models::sparse::Mdp<double>>;
template class SparsePropositionalModelChecker<storm::models::sparse::MarkovAutomaton<double>>;
#ifdef STORM_HAVE_CARL
template class SparsePropositionalModelChecker<storm::models::sparse::Mdp<double, storm::models::sparse::StandardRewardModel<storm::Interval>>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalNumber>>;
@ -70,5 +71,6 @@ namespace storm {
template class SparsePropositionalModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>>;
template class SparsePropositionalModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>;
#endif
}
}
}

3
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
View File

@ -986,7 +986,10 @@ namespace storm {
}
template class SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>>;
#ifdef STORM_HAVE_CARL
template class SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>>;
template class SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>;
#endif
} // namespace modelchecker
} // namespace storm

4
src/modelchecker/results/CheckResult.cpp
View File

@ -145,10 +145,12 @@ namespace storm {
template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asHybridQuantitativeCheckResult();
template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asHybridQuantitativeCheckResult() const;
#ifdef STORM_HAVE_CARL
template ExplicitQuantitativeCheckResult<storm::RationalNumber>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<storm::RationalNumber> const& CheckResult::asExplicitQuantitativeCheckResult() const;
template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asExplicitQuantitativeCheckResult() const;
#endif
}
}
}

3
src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
View File

@ -250,7 +250,10 @@ namespace storm {
}
template class ExplicitQuantitativeCheckResult<double>;
#ifdef STORM_HAVE_CARL
template class ExplicitQuantitativeCheckResult<storm::RationalNumber>;
template class ExplicitQuantitativeCheckResult<storm::RationalFunction>;
#endif
}
}

6
src/models/sparse/Ctmc.cpp
View File

@ -46,11 +46,13 @@ namespace storm {
}
template class Ctmc<double>;
#ifdef STORM_HAVE_CARL
template class Ctmc<storm::RationalNumber>;
template class Ctmc<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class Ctmc<storm::RationalFunction>;
#endif
} // namespace sparse
} // namespace models
} // namespace storm
} // namespace storm

6
src/models/sparse/DeterministicModel.cpp
View File

@ -57,11 +57,13 @@ namespace storm {
template class DeterministicModel<double>;
template class DeterministicModel<float>;
#ifdef STORM_HAVE_CARL
template class DeterministicModel<storm::RationalNumber>;
template class DeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class DeterministicModel<storm::RationalFunction>;
#endif
} // namespace sparse
} // namespace models
} // namespace storm
} // namespace storm

4
src/models/sparse/Dtmc.cpp
View File

@ -69,11 +69,13 @@ namespace storm {
template class Dtmc<double>;
template class Dtmc<float>;
#ifdef STORM_HAVE_CARL
template class Dtmc<storm::RationalNumber>;
template class Dtmc<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class Dtmc<storm::RationalFunction>;
#endif
} // namespace sparse
} // namespace models
} // namespace storm

3
src/models/sparse/MarkovAutomaton.cpp
View File

@ -366,11 +366,12 @@ namespace storm {
template class MarkovAutomaton<double>;
// template class MarkovAutomaton<float>;
#ifdef STORM_HAVE_CARL
template class MarkovAutomaton<storm::RationalNumber>;
template class MarkovAutomaton<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class MarkovAutomaton<storm::RationalFunction>;
#endif
} // namespace sparse
} // namespace models
} // namespace storm

6
src/models/sparse/Mdp.cpp
View File

@ -98,11 +98,13 @@ namespace storm {
template class Mdp<double>;
template class Mdp<float>;
#ifdef STORM_HAVE_CARL
template class Mdp<storm::RationalNumber>;
template class Mdp<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class Mdp<storm::RationalFunction>;
#endif
} // namespace sparse
} // namespace models
} // namespace storm
} // namespace storm

9
src/models/sparse/Model.cpp
View File

@ -312,7 +312,11 @@ namespace storm {
template<typename ValueType, typename RewardModelType>
bool Model<ValueType, RewardModelType>::supportsParameters() const {
#ifdef STORM_HAVE_CARL
return std::is_same<ValueType, storm::RationalFunction>::value;
#else
return false;
#endif
}
template<typename ValueType, typename RewardModelType>
@ -346,18 +350,21 @@ namespace storm {
return this->rewardModels;
}
#ifdef STORM_HAVE_CARL
std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model) {
return storm::storage::getVariables(model.getTransitionMatrix());
}
#endif
template class Model<double>;
template class Model<float>;
#ifdef STORM_HAVE_CARL
template class Model<storm::RationalNumber>;
template class Model<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class Model<storm::RationalFunction>;
#endif
}
}
}

2
src/models/sparse/Model.h
View File

@ -357,7 +357,9 @@ namespace storm {
boost::optional<std::vector<LabelSet>> choiceLabeling;
};
#ifdef STORM_HAVE_CARL
std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model);
#endif
} // namespace sparse
} // namespace models
} // namespace storm

6
src/models/sparse/NondeterministicModel.cpp
View File

@ -169,6 +169,8 @@ namespace storm {
template class NondeterministicModel<double>;
template class NondeterministicModel<float>;
#ifdef STORM_HAVE_CARL
template class NondeterministicModel<storm::RationalNumber>;
template class NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
@ -176,7 +178,7 @@ namespace storm {
template void NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>>::modifyStateRewards(std::string const& modelName, std::map<uint_fast64_t, double> const& modifications);
template class NondeterministicModel<storm::RationalFunction>;
#endif
}
}
}
}

2
src/models/sparse/StandardRewardModel.cpp
View File

@ -318,6 +318,7 @@ namespace storm {
template class StandardRewardModel<float>;
template std::ostream& operator<<<float>(std::ostream& out, StandardRewardModel<float> const& rewardModel);
#ifdef STORM_HAVE_CARL
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& weights) const;
@ -346,6 +347,7 @@ namespace storm {
template void StandardRewardModel<storm::Interval>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards);
template class StandardRewardModel<storm::Interval>;
template std::ostream& operator<<<storm::Interval>(std::ostream& out, StandardRewardModel<storm::Interval> const& rewardModel);
#endif
}
}

4
src/parser/DFTGalileoParser.cpp
View File

@ -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<ValueType, storm::RationalFunction>::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<std::string> tokens;
boost::split(tokens, line, boost::is_any_of(" "));

22
src/solver/EigenLinearEquationSolver.cpp
View File

@ -94,6 +94,7 @@ namespace storm {
return restart;
}
#ifdef STORM_HAVE_CARL
EigenLinearEquationSolverSettings<storm::RationalNumber>::EigenLinearEquationSolverSettings() {
// Intentionally left empty.
}
@ -101,6 +102,7 @@ namespace storm {
EigenLinearEquationSolverSettings<storm::RationalFunction>::EigenLinearEquationSolverSettings() {
// Intentionally left empty.
}
#endif
template<typename ValueType>
EigenLinearEquationSolver<ValueType>::EigenLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, EigenLinearEquationSolverSettings<ValueType> const& settings) : eigenA(storm::adapters::EigenAdapter::toEigenSparseMatrix<ValueType>(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<storm::RationalNumber>::solveEquations(std::vector<storm::RationalNumber>& x, std::vector<storm::RationalNumber> 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<storm::RationalFunction>::solveEquations(std::vector<storm::RationalFunction>& x, std::vector<storm::RationalFunction> 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<typename ValueType>
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> EigenLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
return std::make_unique<storm::solver::EigenLinearEquationSolver<ValueType>>(matrix, settings);
@ -307,16 +309,18 @@ namespace storm {
}
template class EigenLinearEquationSolverSettings<double>;
template class EigenLinearEquationSolver<double>;
template class EigenLinearEquationSolverFactory<double>;
#ifdef STORM_HAVE_CARL
template class EigenLinearEquationSolverSettings<storm::RationalNumber>;
template class EigenLinearEquationSolverSettings<storm::RationalFunction>;
template class EigenLinearEquationSolver<double>;
template class EigenLinearEquationSolver<storm::RationalNumber>;
template class EigenLinearEquationSolver<storm::RationalFunction>;
template class EigenLinearEquationSolverFactory<double>;
template class EigenLinearEquationSolverFactory<storm::RationalNumber>;
template class EigenLinearEquationSolverFactory<storm::RationalFunction>;
#endif
}
}
}

4
src/solver/EigenLinearEquationSolver.h
View File

@ -40,6 +40,7 @@ namespace storm {
uint_fast64_t restart;
};
#ifdef STORM_HAVE_CARL
template<>
class EigenLinearEquationSolverSettings<storm::RationalNumber> {
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<ValueType> settings;
};
}
}
}

7
src/solver/EliminationLinearEquationSolver.cpp
View File

@ -173,16 +173,19 @@ namespace storm {
}
template class EliminationLinearEquationSolverSettings<double>;
template class EliminationLinearEquationSolver<double>;
template class EliminationLinearEquationSolverFactory<double>;
#ifdef STORM_HAVE_CARL
template class EliminationLinearEquationSolverSettings<storm::RationalNumber>;
template class EliminationLinearEquationSolverSettings<storm::RationalFunction>;
template class EliminationLinearEquationSolver<double>;
template class EliminationLinearEquationSolver<storm::RationalNumber>;
template class EliminationLinearEquationSolver<storm::RationalFunction>;
template class EliminationLinearEquationSolverFactory<double>;
template class EliminationLinearEquationSolverFactory<storm::RationalNumber>;
template class EliminationLinearEquationSolverFactory<storm::RationalFunction>;
#endif
}
}

11
src/solver/LinearEquationSolver.cpp
View File

@ -121,6 +121,7 @@ namespace storm {
return std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>(*this);
}
#ifdef STORM_HAVE_CARL
std::unique_ptr<LinearEquationSolver<storm::RationalNumber>> GeneralLinearEquationSolverFactory<storm::RationalNumber>::create(storm::storage::SparseMatrix<storm::RationalNumber> const& matrix) const {
return selectSolver(matrix);
}
@ -162,18 +163,22 @@ namespace storm {
std::unique_ptr<LinearEquationSolverFactory<storm::RationalFunction>> GeneralLinearEquationSolverFactory<storm::RationalFunction>::clone() const {
return std::make_unique<GeneralLinearEquationSolverFactory<storm::RationalFunction>>(*this);
}
#endif
template class LinearEquationSolver<double>;
template class LinearEquationSolverFactory<double>;
template class GeneralLinearEquationSolverFactory<double>;
#ifdef STORM_HAVE_CARL
template class LinearEquationSolver<storm::RationalNumber>;
template class LinearEquationSolver<storm::RationalFunction>;
template class LinearEquationSolverFactory<double>;
template class LinearEquationSolverFactory<storm::RationalNumber>;
template class LinearEquationSolverFactory<storm::RationalFunction>;
template class GeneralLinearEquationSolverFactory<double>;
template class GeneralLinearEquationSolverFactory<storm::RationalNumber>;
template class GeneralLinearEquationSolverFactory<storm::RationalFunction>;
#endif
}
}
}

3
src/solver/LinearEquationSolver.h
View File

@ -154,6 +154,7 @@ namespace storm {
std::unique_ptr<LinearEquationSolver<ValueType>> selectSolver(MatrixType&& matrix) const;
};
#ifdef STORM_HAVE_CARL
template<>
class GeneralLinearEquationSolverFactory<storm::RationalNumber> : public LinearEquationSolverFactory<storm::RationalNumber> {
public:
@ -179,7 +180,7 @@ namespace storm {
template<typename MatrixType>
std::unique_ptr<LinearEquationSolver<storm::RationalFunction>> selectSolver(MatrixType&& matrix) const;
};
#endif
} // namespace solver
} // namespace storm

9
src/solver/MinMaxLinearEquationSolver.cpp
View File

@ -144,6 +144,7 @@ namespace storm {
return result;
}
#ifdef STORM_HAVE_CARL
template<>
template<typename MatrixType>
std::unique_ptr<MinMaxLinearEquationSolver<storm::RationalNumber>> GeneralMinMaxLinearEquationSolverFactory<storm::RationalNumber>::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<StandardMinMaxLinearEquationSolver<storm::RationalNumber>>(std::forward<MatrixType>(matrix), std::make_unique<GeneralLinearEquationSolverFactory<storm::RationalNumber>>());
}
#endif
template class MinMaxLinearEquationSolver<float>;
template class MinMaxLinearEquationSolver<double>;
template class MinMaxLinearEquationSolver<storm::RationalNumber>;
template class MinMaxLinearEquationSolverFactory<double>;
template class GeneralMinMaxLinearEquationSolverFactory<double>;
#ifdef STORM_HAVE_CARL
template class MinMaxLinearEquationSolver<storm::RationalNumber>;
template class MinMaxLinearEquationSolverFactory<storm::RationalNumber>;
template class GeneralMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
#endif
}
}

3
src/solver/SolveGoal.cpp
View File

@ -51,8 +51,9 @@ namespace storm {
template std::unique_ptr<storm::solver::LinearEquationSolver<double>> configureLinearEquationSolver(BoundedGoal<double> const& goal, storm::solver::LinearEquationSolverFactory<double> const& factory, storm::storage::SparseMatrix<double> const& matrix);
template std::unique_ptr<storm::solver::LinearEquationSolver<double>> configureLinearEquationSolver(SolveGoal const& goal, storm::solver::LinearEquationSolverFactory<double> const& factory, storm::storage::SparseMatrix<double> const& matrix);
#ifdef STORM_HAVE_CARL
template std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<storm::RationalNumber>> configureMinMaxLinearEquationSolver(BoundedGoal<storm::RationalNumber> const& goal, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& factory, storm::storage::SparseMatrix<storm::RationalNumber> const& matrix);
template std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<storm::RationalNumber>> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& factory, storm::storage::SparseMatrix<storm::RationalNumber> const& matrix);
#endif
}
}

7
src/solver/StandardMinMaxLinearEquationSolver.cpp
View File

@ -370,6 +370,7 @@ namespace storm {
}
}
#ifdef STORM_HAVE_CARL
template<>
StandardMinMaxLinearEquationSolverFactory<storm::RationalNumber>::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, bool trackScheduler) : MinMaxLinearEquationSolverFactory<storm::RationalNumber>(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<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> StandardMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
@ -441,11 +443,12 @@ namespace storm {
template class NativeMinMaxLinearEquationSolverFactory<double>;
template class EliminationMinMaxLinearEquationSolverFactory<double>;
#ifdef STORM_HAVE_CARL
template class StandardMinMaxLinearEquationSolverSettings<storm::RationalNumber>;
template class StandardMinMaxLinearEquationSolver<storm::RationalNumber>;
template class StandardMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
template class EigenMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
template class EliminationMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
#endif
}
}
}

3
src/solver/TerminationCondition.cpp
View File

@ -40,8 +40,9 @@ namespace storm {
template class TerminateIfFilteredSumExceedsThreshold<double>;
template class TerminateIfFilteredExtremumExceedsThreshold<double>;
#ifdef STORM_HAVE_CARL
template class TerminateIfFilteredSumExceedsThreshold<storm::RationalNumber>;
template class TerminateIfFilteredExtremumExceedsThreshold<storm::RationalNumber>;
#endif
}
}

4
src/solver/stateelimination/ConditionalStateEliminator.cpp
View File

@ -61,9 +61,11 @@ namespace storm {
}
template class ConditionalStateEliminator<double>;
#ifdef STORM_HAVE_CARL
template class ConditionalStateEliminator<storm::RationalNumber>;
template class ConditionalStateEliminator<storm::RationalFunction>;
#endif
} // namespace stateelimination
} // namespace storage
} // namespace storm

3
src/solver/stateelimination/DynamicStatePriorityQueue.cpp
View File

@ -62,8 +62,11 @@ namespace storm {
}
template class DynamicStatePriorityQueue<double>;
#ifdef STORM_HAVE_CARL
template class DynamicStatePriorityQueue<storm::RationalNumber>;
template class DynamicStatePriorityQueue<storm::RationalFunction>;
#endif
}
}
}

8
src/solver/stateelimination/EliminatorBase.cpp
View File

@ -274,13 +274,15 @@ namespace storm {
}
template class EliminatorBase<double, ScalingMode::Divide>;
template class EliminatorBase<double, ScalingMode::DivideOneMinus>;
#ifdef STORM_HAVE_CARL
template class EliminatorBase<storm::RationalNumber, ScalingMode::Divide>;
template class EliminatorBase<storm::RationalFunction, ScalingMode::Divide>;
template class EliminatorBase<double, ScalingMode::DivideOneMinus>;
template class EliminatorBase<storm::RationalNumber, ScalingMode::DivideOneMinus>;
template class EliminatorBase<storm::RationalFunction, ScalingMode::DivideOneMinus>;
#endif
}
}
}
}

5
src/solver/stateelimination/EquationSystemEliminator.cpp
View File

@ -10,8 +10,11 @@ namespace storm {
}
template class EquationSystemEliminator<double>;
#ifdef STORM_HAVE_CARL
template class EquationSystemEliminator<storm::RationalNumber>;
template class EquationSystemEliminator<storm::RationalFunction>;
#endif
}
}
}
}

4
src/solver/stateelimination/LongRunAverageEliminator.cpp
View File

@ -23,9 +23,11 @@ namespace storm {
}
template class LongRunAverageEliminator<double>;
#ifdef STORM_HAVE_CARL
template class LongRunAverageEliminator<storm::RationalNumber>;
template class LongRunAverageEliminator<storm::RationalFunction>;
#endif
} // namespace stateelimination
} // namespace storage
} // namespace storm

4
src/solver/stateelimination/PrioritizedStateEliminator.cpp
View File

@ -29,9 +29,11 @@ namespace storm {
}
template class PrioritizedStateEliminator<double>;
#ifdef STORM_HAVE_CARL
template class PrioritizedStateEliminator<storm::RationalNumber>;
template class PrioritizedStateEliminator<storm::RationalFunction>;
#endif
} // namespace stateelimination
} // namespace storage
} // namespace storm

4
src/solver/stateelimination/StateEliminator.cpp
View File

@ -28,9 +28,11 @@ namespace storm {
}
template class StateEliminator<double>;
#ifdef STORM_HAVE_CARL
template class StateEliminator<storm::RationalNumber>;
template class StateEliminator<storm::RationalFunction>;
#endif
} // namespace stateelimination
} // namespace storage
} // namespace storm

2
src/storage/Distribution.cpp
View File

@ -152,10 +152,12 @@ namespace storm {
template class Distribution<double>;
template std::ostream& operator<<(std::ostream& out, Distribution<double> const& distribution);
#ifdef STORM_HAVE_CARL
template class Distribution<storm::RationalNumber>;
template std::ostream& operator<<(std::ostream& out, Distribution<storm::RationalNumber> const& distribution);
template class Distribution<storm::RationalFunction>;
template std::ostream& operator<<(std::ostream& out, Distribution<storm::RationalFunction> const& distribution);
#endif
}
}

5
src/storage/FlexibleSparseMatrix.cpp
View File

@ -269,13 +269,14 @@ namespace storm {
// Explicitly instantiate the matrix.
template class FlexibleSparseMatrix<double>;
template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix<double> const& matrix);
#ifdef STORM_HAVE_CARL
template class FlexibleSparseMatrix<storm::RationalNumber>;
template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix<storm::RationalNumber> const& matrix);
#ifdef STORM_HAVE_CARL
template class FlexibleSparseMatrix<storm::RationalFunction>;
template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix<storm::RationalFunction> const& matrix);
#endif
} // namespace storage
} // namespace storm
} // namespace storm

3
src/storage/MaximalEndComponentDecomposition.cpp
View File

@ -193,8 +193,9 @@ namespace storm {
template class MaximalEndComponentDecomposition<double>;
template MaximalEndComponentDecomposition<double>::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<double> const& model);
#ifdef STORM_HAVE_CARL
template class MaximalEndComponentDecomposition<storm::RationalNumber>;
template MaximalEndComponentDecomposition<storm::RationalNumber>::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model);
#endif
}
}

2
src/storage/SparseMatrix.cpp
View File

@ -1213,10 +1213,12 @@ namespace storm {
}
}
#ifdef STORM_HAVE_CARL
template<>
void SparseMatrix<Interval>::performSuccessiveOverRelaxationStep(Interval omega, std::vector<Interval>& x, std::vector<Interval> const& b) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported.");
}
#endif
template<typename ValueType>
void SparseMatrix<ValueType>::multiplyVectorWithMatrix(std::vector<value_type> const& vector, std::vector<value_type>& result) const {

8
src/storage/StronglyConnectedComponentDecomposition.cpp
View File

@ -227,16 +227,17 @@ namespace storm {
}
// Explicitly instantiate the SCC decomposition.
template class StronglyConnectedComponentDecomposition<double>;
template class StronglyConnectedComponentDecomposition<double>;
template StronglyConnectedComponentDecomposition<double>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<double> const& model, bool dropNaiveSccs, bool onlyBottomSccs);
template StronglyConnectedComponentDecomposition<double>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<double> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs);
template StronglyConnectedComponentDecomposition<double>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<double> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs);
template class StronglyConnectedComponentDecomposition<float>;
template class StronglyConnectedComponentDecomposition<float>;
template StronglyConnectedComponentDecomposition<float>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<float> const& model, bool dropNaiveSccs, bool onlyBottomSccs);
template StronglyConnectedComponentDecomposition<float>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<float> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs);
template StronglyConnectedComponentDecomposition<float>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<float> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs);
#ifdef STORM_HAVE_CARL
template class StronglyConnectedComponentDecomposition<storm::RationalNumber>;
template StronglyConnectedComponentDecomposition<storm::RationalNumber>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<storm::RationalNumber> const& model, bool dropNaiveSccs, bool onlyBottomSccs);
template StronglyConnectedComponentDecomposition<storm::RationalNumber>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<storm::RationalNumber> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs);
@ -246,5 +247,6 @@ namespace storm {
template StronglyConnectedComponentDecomposition<storm::RationalFunction>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<storm::RationalFunction> const& model, bool dropNaiveSccs, bool onlyBottomSccs);
template StronglyConnectedComponentDecomposition<storm::RationalFunction>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<storm::RationalFunction> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs);
template StronglyConnectedComponentDecomposition<storm::RationalFunction>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<storm::RationalFunction> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs);
#endif
} // namespace storage
} // namespace storm
} // namespace storm

2
src/storage/bisimulation/BisimulationDecomposition.cpp
View File

@ -323,6 +323,7 @@ namespace storm {
template class BisimulationDecomposition<storm::models::sparse::Ctmc<double>, bisimulation::DeterministicBlockData>;
template class BisimulationDecomposition<storm::models::sparse::Mdp<double>, bisimulation::DeterministicBlockData>;
#ifdef STORM_HAVE_CARL
template class BisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalNumber>, bisimulation::DeterministicBlockData>;
template class BisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalNumber>, bisimulation::DeterministicBlockData>;
template class BisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalNumber>, bisimulation::DeterministicBlockData>;
@ -330,5 +331,6 @@ namespace storm {
template class BisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
template class BisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
template class BisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
#endif
}
}

2
src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
View File

@ -652,10 +652,12 @@ namespace storm {
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>;
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>>;
#ifdef STORM_HAVE_CARL
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalNumber>>;
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalNumber>>;
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>>;
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>>;
#endif
}
}

4
src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
View File

@ -416,8 +416,10 @@ namespace storm {
}
template class NondeterministicModelBisimulationDecomposition<storm::models::sparse::Mdp<double>>;
#ifdef STORM_HAVE_CARL
template class NondeterministicModelBisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalNumber>>;
template class NondeterministicModelBisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalFunction>>;
#endif
}
}

4
src/storage/expressions/ExpressionEvaluator.cpp
View File

@ -30,6 +30,7 @@ namespace storm {
this->variableToExpressionMap[variable] = this->getManager().rational(value);
}
#ifdef STORM_HAVE_CARL
ExpressionEvaluator<RationalNumber>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorWithVariableToExpressionMap<RationalNumber>(manager) {
// Intentionally left empty.
}
@ -50,5 +51,6 @@ namespace storm {
template class ExpressionEvaluatorWithVariableToExpressionMap<RationalNumber>;
template class ExpressionEvaluatorWithVariableToExpressionMap<RationalFunction>;
#endif
}
}
}

4
src/storage/expressions/ExpressionEvaluator.h
View File

@ -35,6 +35,7 @@ namespace storm {
std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> variableToExpressionMap;
};
#ifdef STORM_HAVE_CARL
template<>
class ExpressionEvaluator<RationalNumber> : public ExpressionEvaluatorWithVariableToExpressionMap<RationalNumber> {
public:
@ -58,7 +59,8 @@ namespace storm {
// A visitor that can be used to translate expressions to rational functions.
mutable ToRationalFunctionVisitor<RationalFunction> rationalFunctionVisitor;
};
#endif
}
}
#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATOR_H_ */
#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATOR_H_ */

5
src/storage/expressions/ExpressionEvaluatorBase.cpp
View File

@ -16,7 +16,10 @@ namespace storm {
}
template class ExpressionEvaluatorBase<double>;
#ifdef STORM_HAVE_CARL
template class ExpressionEvaluatorBase<storm::RationalNumber>;
template class ExpressionEvaluatorBase<storm::RationalFunction>;
#endif
}
}
}

5
src/storage/expressions/ExprtkExpressionEvaluator.cpp
View File

@ -83,7 +83,10 @@ namespace storm {
}
template class ExprtkExpressionEvaluatorBase<double>;
#ifdef STORM_HAVE_CARL
template class ExprtkExpressionEvaluatorBase<RationalNumber>;
template class ExprtkExpressionEvaluatorBase<RationalFunction>;
#endif
}
}
}

4
src/storage/expressions/ToRationalFunctionVisitor.cpp
View File

@ -7,6 +7,8 @@
namespace storm {
namespace expressions {
#ifdef STORM_HAVE_CARL
template<typename RationalFunctionType>
ToRationalFunctionVisitor<RationalFunctionType>::ToRationalFunctionVisitor() : ExpressionVisitor(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>()) {
// Intentionally left empty.
@ -95,6 +97,6 @@ namespace storm {
}
template class ToRationalFunctionVisitor<storm::RationalFunction>;
#endif
}
}

4
src/storage/expressions/ToRationalFunctionVisitor.h
View File

@ -10,6 +10,7 @@
namespace storm {
namespace expressions {
#ifdef STORM_HAVE_CARL
template<typename RationalFunctionType>
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<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
};
#endif
}
}
#endif /* STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ */
#endif /* STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ */

20
src/storage/expressions/ToRationalNumberVisitor.cpp
View File

@ -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<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::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<typename RationalNumberType>
@ -62,30 +63,39 @@ namespace storm {
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::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<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::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<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::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<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IntegerLiteralExpression const& expression) {
#ifdef STORM_HAVE_CARL
return RationalNumberType(carl::rationalize<storm::RationalNumber>(static_cast<size_t>(expression.getValue())));
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build.");
#endif
}
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(DoubleLiteralExpression const& expression) {
#ifdef STORM_HAVE_CARL
return RationalNumberType(carl::rationalize<storm::RationalNumber>(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<storm::RationalNumber>;
#endif
}
}

4
src/storm-dyftee.cpp
View File

@ -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<storm::RationalFunction>(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<double>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC());
}

51
src/utility/constants.cpp
View File

@ -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<typename ValueType>
ValueType pow(ValueType const& value, uint_fast64_t exponent) {
return std::pow(value, exponent);
}
template<typename ValueType>
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<typename ValueType>
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<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType> simplify(storm::storage::MatrixEntry<IndexType, ValueType> 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<storm::storage::sparse::state_type, double> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& 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<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry);
template bool isOne(int const& value);
template bool isZero(int const& value);
@ -252,6 +256,7 @@ namespace storm {
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& 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<storm::storage::sparse::state_type, storm::RationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& 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);

15
src/utility/graph.cpp
View File

@ -22,6 +22,8 @@
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
#include <queue>
namespace storm {
namespace utility {
namespace graph {
@ -1180,24 +1182,21 @@ namespace storm {
template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<float> const& matrix) ;
// Instantiations for storm::RationalNumber.
#ifdef STORM_HAVE_CARL
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalNumber> 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<storm::RationalNumber> const& transitionMatrix);
template std::vector<uint_fast64_t> getDistances(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<storm::RationalNumber> 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<storm::RationalNumber> 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<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::sparse::DeterministicModel<storm::RationalNumber> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<storm::storage::BitVector> const& rowFilter);
@ -1214,33 +1213,27 @@ namespace storm {
template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> 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<storm::RationalNumber> const& model, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<storm::RationalNumber> const& matrix);
// End of instantiations for storm::RationalNumber.
#ifdef STORM_HAVE_CARL
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalFunction> 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<storm::RationalFunction> const& transitionMatrix);

1
src/utility/parametric.h
View File

@ -10,6 +10,7 @@
#include "src/adapters/CarlAdapter.h"
#include <map>
namespace storm {
namespace utility {

4
src/utility/prism.cpp
View File

@ -9,6 +9,8 @@
#include "src/exceptions/InvalidArgumentException.h"
#include <boost/algorithm/string.hpp>
namespace storm {
namespace utility {
namespace prism {
@ -82,4 +84,4 @@ namespace storm {
}
}
}
}

4
src/utility/stateelimination.cpp
View File

@ -202,6 +202,7 @@ namespace storm {
template std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<double> const& oneStepProbabilities, bool forward, bool reverse);
template std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<double> const& oneStepProbabilities, bool forward);
#ifdef STORM_HAVE_CARL
template uint_fast64_t estimateComplexity(storm::RationalNumber const& value);
template std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& oneStepProbabilities, storm::storage::BitVector const& states);
template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& oneStepProbabilities);
@ -215,6 +216,7 @@ namespace storm {
template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& oneStepProbabilities);
template std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<storm::RationalFunction> const& oneStepProbabilities, bool forward, bool reverse);
template std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<storm::RationalFunction> const& oneStepProbabilities, bool forward);
#endif
}
}
}
}

4
src/utility/storm.h
View File

@ -220,6 +220,7 @@ namespace storm {
}
}
#ifdef STORM_HAVE_CARL
template<>
inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model, std::shared_ptr<storm::logic::Formula const> 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<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
}
#endif
template<typename ValueType>
void generateCounterexamples(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
@ -332,6 +334,7 @@ namespace storm {
}
#ifdef STORM_HAVE_CARL
template<>
inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant) {
storm::modelchecker::CheckTask<storm::logic::Formula> 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<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) {
std::ofstream filestream;
filestream.open(path);

Write Preview
Loading…
Cancel
Save