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

instantiated (and fixed occurring problems) explicit parsers with intervals as the reward model value type 

Former-commit-id: bf452cd751
main
dehnert 10 years ago
parent
bc3f6b8d80
commit
b2d8cae9ce
22 changed files with 135 additions and 62 deletions
Unified View
  1. 6
      src/models/sparse/Ctmc.cpp
  2. 8
      src/models/sparse/DeterministicModel.cpp
  3. 2
      src/models/sparse/DeterministicModel.h
  4. 6
      src/models/sparse/Dtmc.cpp
  5. 16
      src/models/sparse/MarkovAutomaton.cpp
  6. 2
      src/models/sparse/MarkovAutomaton.h
  7. 14
      src/models/sparse/Mdp.cpp
  8. 4
      src/models/sparse/Mdp.h
  9. 2
      src/models/sparse/Model.cpp
  10. 8
      src/models/sparse/NondeterministicModel.cpp
  11. 4
      src/models/sparse/StochasticTwoPlayerGame.cpp
  12. 16
      src/parser/AutoParser.cpp
  13. 2
      src/parser/AutoParser.h
  14. 6
      src/parser/DeterministicModelParser.cpp
  15. 9
      src/parser/DeterministicSparseTransitionParser.cpp
  16. 8
      src/parser/MarkovAutomatonParser.cpp
  17. 1
      src/parser/MarkovAutomatonSparseTransitionParser.cpp
  18. 8
      src/parser/NondeterministicModelParser.cpp
  19. 11
      src/parser/NondeterministicSparseTransitionParser.cpp
  20. 9
      src/parser/SparseStateRewardParser.cpp
  21. 14
      src/storage/SparseMatrix.cpp
  22. 3
      src/storage/SparseMatrix.h

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

@ -11,7 +11,7 @@ namespace storm {
Ctmc<ValueType, RewardModelType>::Ctmc(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::models::sparse::StateLabeling const& stateLabeling, Ctmc<ValueType, RewardModelType>::Ctmc(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::models::sparse::StateLabeling const& stateLabeling,
std::unordered_map<std::string, RewardModelType> const& rewardModels, std::unordered_map<std::string, RewardModelType> const& rewardModels,
boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling) boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
: DeterministicModel<ValueType>(storm::models::ModelType::Ctmc, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { : DeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Ctmc, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
exitRates = createExitRateVector(this->getTransitionMatrix()); exitRates = createExitRateVector(this->getTransitionMatrix());
} }
@ -19,7 +19,7 @@ namespace storm {
Ctmc<ValueType, RewardModelType>::Ctmc(storm::storage::SparseMatrix<ValueType>&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling, Ctmc<ValueType, RewardModelType>::Ctmc(storm::storage::SparseMatrix<ValueType>&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
std::unordered_map<std::string, RewardModelType>&& rewardModels, std::unordered_map<std::string, RewardModelType>&& rewardModels,
boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling) boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
: DeterministicModel<ValueType>(storm::models::ModelType::Ctmc, std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { : DeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Ctmc, std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
// It is important to refer to the transition matrix here, because the given rate matrix has been move elsewhere. // It is important to refer to the transition matrix here, because the given rate matrix has been move elsewhere.
exitRates = createExitRateVector(this->getTransitionMatrix()); exitRates = createExitRateVector(this->getTransitionMatrix());
} }
@ -41,6 +41,8 @@ namespace storm {
template class Ctmc<double>; template class Ctmc<double>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class Ctmc<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class Ctmc<storm::RationalFunction>; template class Ctmc<storm::RationalFunction>;
#endif #endif

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

@ -12,7 +12,7 @@ namespace storm {
storm::models::sparse::StateLabeling const& stateLabeling, storm::models::sparse::StateLabeling const& stateLabeling,
std::unordered_map<std::string, RewardModelType> const& rewardModels, std::unordered_map<std::string, RewardModelType> const& rewardModels,
boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling) boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
: Model<ValueType>(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { : Model<ValueType, RewardModelType>(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -22,13 +22,13 @@ namespace storm {
storm::models::sparse::StateLabeling&& stateLabeling, storm::models::sparse::StateLabeling&& stateLabeling,
std::unordered_map<std::string, RewardModelType>&& rewardModels, std::unordered_map<std::string, RewardModelType>&& rewardModels,
boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling) boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
: Model<ValueType>(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { : Model<ValueType, RewardModelType>(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
// Intentionally left empty. // Intentionally left empty.
} }
template <typename ValueType, typename RewardModelType> template <typename ValueType, typename RewardModelType>
void DeterministicModel<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector<ValueType> const* firstValue, std::vector<ValueType> const* secondValue, std::vector<uint_fast64_t> const* stateColoring, std::vector<std::string> const* colors, std::vector<uint_fast64_t>* scheduler, bool finalizeOutput) const { void DeterministicModel<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector<ValueType> const* firstValue, std::vector<ValueType> const* secondValue, std::vector<uint_fast64_t> const* stateColoring, std::vector<std::string> const* colors, std::vector<uint_fast64_t>* scheduler, bool finalizeOutput) const {
Model<ValueType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); Model<ValueType, RewardModelType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
// Simply iterate over all transitions and draw the arrows with probability information attached. // Simply iterate over all transitions and draw the arrows with probability information attached.
auto rowIt = this->getTransitionMatrix().begin(); auto rowIt = this->getTransitionMatrix().begin();
@ -59,6 +59,8 @@ namespace storm {
template class DeterministicModel<float>; template class DeterministicModel<float>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class DeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class DeterministicModel<storm::RationalFunction>; template class DeterministicModel<storm::RationalFunction>;
#endif #endif

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

@ -49,7 +49,7 @@ namespace storm {
#ifndef WINDOWS #ifndef WINDOWS
DeterministicModel(DeterministicModel<ValueType, RewardModelType>&& other) = default; DeterministicModel(DeterministicModel<ValueType, RewardModelType>&& other) = default;
DeterministicModel<ValueType>& operator=(DeterministicModel<ValueType, RewardModelType>&& model) = default; DeterministicModel<ValueType, RewardModelType>& operator=(DeterministicModel<ValueType, RewardModelType>&& model) = default;
#endif #endif
virtual void reduceToStateBasedRewards() override; virtual void reduceToStateBasedRewards() override;

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

@ -14,14 +14,14 @@ namespace storm {
storm::models::sparse::StateLabeling const& stateLabeling, storm::models::sparse::StateLabeling const& stateLabeling,
std::unordered_map<std::string, RewardModelType> const& rewardModels, std::unordered_map<std::string, RewardModelType> const& rewardModels,
boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling) boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
: DeterministicModel<ValueType>(storm::models::ModelType::Dtmc, probabilityMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { : DeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Dtmc, probabilityMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
} }
template <typename ValueType, typename RewardModelType> template <typename ValueType, typename RewardModelType>
Dtmc<ValueType, RewardModelType>::Dtmc(storm::storage::SparseMatrix<ValueType>&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling, Dtmc<ValueType, RewardModelType>::Dtmc(storm::storage::SparseMatrix<ValueType>&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
std::unordered_map<std::string, RewardModelType>&& rewardModels, boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling) std::unordered_map<std::string, RewardModelType>&& rewardModels, boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
: DeterministicModel<ValueType>(storm::models::ModelType::Dtmc, std::move(probabilityMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { : DeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Dtmc, std::move(probabilityMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
} }
@ -225,6 +225,8 @@ namespace storm {
template class Dtmc<float>; template class Dtmc<float>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class Dtmc<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class Dtmc<storm::RationalFunction>; template class Dtmc<storm::RationalFunction>;
#endif #endif

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

@ -15,7 +15,7 @@ namespace storm {
std::vector<ValueType> const& exitRates, std::vector<ValueType> const& exitRates,
std::unordered_map<std::string, RewardModelType> const& rewardModels, std::unordered_map<std::string, RewardModelType> const& rewardModels,
boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling) boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
: NondeterministicModel<ValueType>(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) { : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) {
this->turnRatesToProbabilities(); this->turnRatesToProbabilities();
} }
@ -26,7 +26,7 @@ namespace storm {
std::vector<ValueType> const& exitRates, std::vector<ValueType> const& exitRates,
std::unordered_map<std::string, RewardModelType>&& rewardModels, std::unordered_map<std::string, RewardModelType>&& rewardModels,
boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling) boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
: NondeterministicModel<ValueType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) { : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) {
this->turnRatesToProbabilities(); this->turnRatesToProbabilities();
} }
@ -124,7 +124,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType> template <typename ValueType, typename RewardModelType>
void MarkovAutomaton<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector<ValueType> const* firstValue, std::vector<ValueType> const* secondValue, std::vector<uint_fast64_t> const* stateColoring, std::vector<std::string> const* colors, std::vector<uint_fast64_t>* scheduler, bool finalizeOutput) const { void MarkovAutomaton<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector<ValueType> const* firstValue, std::vector<ValueType> const* secondValue, std::vector<uint_fast64_t> const* stateColoring, std::vector<std::string> const* colors, std::vector<uint_fast64_t>* scheduler, bool finalizeOutput) const {
NondeterministicModel<ValueType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); NondeterministicModel<ValueType, RewardModelType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
// Write the probability distributions for all the states. // Write the probability distributions for all the states.
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
@ -205,7 +205,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType> template <typename ValueType, typename RewardModelType>
std::size_t MarkovAutomaton<ValueType, RewardModelType>::getSizeInBytes() const { std::size_t MarkovAutomaton<ValueType, RewardModelType>::getSizeInBytes() const {
return NondeterministicModel<ValueType>::getSizeInBytes() + markovianStates.getSizeInBytes() + exitRates.size() * sizeof(ValueType); return NondeterministicModel<ValueType, RewardModelType>::getSizeInBytes() + markovianStates.getSizeInBytes() + exitRates.size() * sizeof(ValueType);
} }
template <typename ValueType, typename RewardModelType> template <typename ValueType, typename RewardModelType>
@ -220,9 +220,11 @@ namespace storm {
template class MarkovAutomaton<double>; template class MarkovAutomaton<double>;
// template class MarkovAutomaton<float>; // template class MarkovAutomaton<float>;
//#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
// template class MarkovAutomaton<storm::RationalFunction>; template class MarkovAutomaton<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
//#endif template class MarkovAutomaton<storm::RationalFunction>;
#endif
} // namespace sparse } // namespace sparse
} // namespace models } // namespace models

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

@ -12,7 +12,7 @@ namespace storm {
* This class represents a Markov automaton. * This class represents a Markov automaton.
*/ */
template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>> template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
class MarkovAutomaton : public NondeterministicModel<ValueType> { class MarkovAutomaton : public NondeterministicModel<ValueType, RewardModelType> {
public: public:
/*! /*!
* Constructs a model from the given data. * Constructs a model from the given data.

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

@ -15,7 +15,7 @@ namespace storm {
storm::models::sparse::StateLabeling const& stateLabeling, storm::models::sparse::StateLabeling const& stateLabeling,
std::unordered_map<std::string, RewardModelType> const& rewardModels, std::unordered_map<std::string, RewardModelType> const& rewardModels,
boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling) boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
: NondeterministicModel<ValueType>(storm::models::ModelType::Mdp, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Mdp, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
STORM_LOG_THROW(transitionMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); STORM_LOG_THROW(transitionMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
} }
@ -25,12 +25,12 @@ namespace storm {
storm::models::sparse::StateLabeling&& stateLabeling, storm::models::sparse::StateLabeling&& stateLabeling,
std::unordered_map<std::string, RewardModelType>&& rewardModels, std::unordered_map<std::string, RewardModelType>&& rewardModels,
boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling) boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
: NondeterministicModel<ValueType>(storm::models::ModelType::Mdp, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Mdp, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) {
STORM_LOG_THROW(transitionMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); STORM_LOG_THROW(transitionMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
} }
template <typename ValueType, typename RewardModelType> template <typename ValueType, typename RewardModelType>
Mdp<ValueType> Mdp<ValueType, RewardModelType>::restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const { Mdp<ValueType, RewardModelType> Mdp<ValueType, RewardModelType>::restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const {
STORM_LOG_THROW(this->hasChoiceLabeling(), storm::exceptions::InvalidArgumentException, "Restriction to label set is impossible for unlabeled model."); STORM_LOG_THROW(this->hasChoiceLabeling(), storm::exceptions::InvalidArgumentException, "Restriction to label set is impossible for unlabeled model.");
std::vector<LabelSet> const& choiceLabeling = this->getChoiceLabeling(); std::vector<LabelSet> const& choiceLabeling = this->getChoiceLabeling();
@ -68,26 +68,28 @@ namespace storm {
} }
} }
Mdp<ValueType> restrictedMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(this->getStateLabeling()), Mdp<ValueType, RewardModelType> restrictedMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(this->getStateLabeling()),
std::unordered_map<std::string, RewardModelType>(this->getRewardModels()), boost::optional<std::vector<LabelSet>>(newChoiceLabeling)); std::unordered_map<std::string, RewardModelType>(this->getRewardModels()), boost::optional<std::vector<LabelSet>>(newChoiceLabeling));
return restrictedMdp; return restrictedMdp;
} }
template <typename ValueType, typename RewardModelType> template <typename ValueType, typename RewardModelType>
Mdp<ValueType> Mdp<ValueType, RewardModelType>::restrictActions(storm::storage::BitVector const& enabledActions) const { Mdp<ValueType, RewardModelType> Mdp<ValueType, RewardModelType>::restrictActions(storm::storage::BitVector const& enabledActions) const {
storm::storage::SparseMatrix<ValueType> restrictedTransitions = this->getTransitionMatrix().restrictRows(enabledActions); storm::storage::SparseMatrix<ValueType> restrictedTransitions = this->getTransitionMatrix().restrictRows(enabledActions);
std::unordered_map<std::string, RewardModelType> newRewardModels; std::unordered_map<std::string, RewardModelType> newRewardModels;
for (auto const& rewardModel : this->getRewardModels()) { for (auto const& rewardModel : this->getRewardModels()) {
newRewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledActions)); newRewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledActions));
} }
return Mdp<ValueType>(restrictedTransitions, this->getStateLabeling(), newRewardModels, this->getOptionalChoiceLabeling()); return Mdp<ValueType, RewardModelType>(restrictedTransitions, this->getStateLabeling(), newRewardModels, this->getOptionalChoiceLabeling());
} }
template class Mdp<double>; template class Mdp<double>;
template class Mdp<float>; template class Mdp<float>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class Mdp<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class Mdp<storm::RationalFunction>; template class Mdp<storm::RationalFunction>;
#endif #endif

4
src/models/sparse/Mdp.h
View File

@ -57,7 +57,7 @@ namespace storm {
* and which ones need to be ignored. * and which ones need to be ignored.
* @return A restricted version of the current MDP that only uses choice labels from the given set. * @return A restricted version of the current MDP that only uses choice labels from the given set.
*/ */
Mdp<ValueType> restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const; Mdp<ValueType, RewardModelType> restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const;
/*! /*!
* Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones given by the bitvector. * Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones given by the bitvector.
@ -65,7 +65,7 @@ namespace storm {
* @param enabledActions A BitVector of lenght numberOfChoices(), which is one iff the action should be kept. * @param enabledActions A BitVector of lenght numberOfChoices(), which is one iff the action should be kept.
* @return A subMDP. * @return A subMDP.
*/ */
Mdp<ValueType> restrictActions(storm::storage::BitVector const& enabledActions) const; Mdp<ValueType, RewardModelType> restrictActions(storm::storage::BitVector const& enabledActions) const;
}; };
} // namespace sparse } // namespace sparse

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

@ -300,6 +300,8 @@ namespace storm {
template class Model<float>; template class Model<float>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class Model<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class Model<storm::RationalFunction>; template class Model<storm::RationalFunction>;
#endif #endif

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

@ -16,7 +16,7 @@ namespace storm {
storm::models::sparse::StateLabeling const& stateLabeling, storm::models::sparse::StateLabeling const& stateLabeling,
std::unordered_map<std::string, RewardModelType> const& rewardModels, std::unordered_map<std::string, RewardModelType> const& rewardModels,
boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling) boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
: Model<ValueType>(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { : Model<ValueType, RewardModelType>(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -26,7 +26,7 @@ namespace storm {
storm::models::sparse::StateLabeling&& stateLabeling, storm::models::sparse::StateLabeling&& stateLabeling,
std::unordered_map<std::string, RewardModelType>&& rewardModels, std::unordered_map<std::string, RewardModelType>&& rewardModels,
boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling) boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
: Model<ValueType>(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), : Model<ValueType, RewardModelType>(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels),
std::move(optionalChoiceLabeling)) { std::move(optionalChoiceLabeling)) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -79,7 +79,7 @@ namespace storm {
template<typename ValueType, typename RewardModelType> template<typename ValueType, typename RewardModelType>
void NondeterministicModel<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector<ValueType> const* firstValue, std::vector<ValueType> const* secondValue, std::vector<uint_fast64_t> const* stateColoring, std::vector<std::string> const* colors, std::vector<uint_fast64_t>* scheduler, bool finalizeOutput) const { void NondeterministicModel<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector<ValueType> const* firstValue, std::vector<ValueType> const* secondValue, std::vector<uint_fast64_t> const* stateColoring, std::vector<std::string> const* colors, std::vector<uint_fast64_t>* scheduler, bool finalizeOutput) const {
Model<ValueType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); Model<ValueType, RewardModelType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
// Write the probability distributions for all the states. // Write the probability distributions for all the states.
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
@ -151,6 +151,8 @@ namespace storm {
template class NondeterministicModel<float>; template class NondeterministicModel<float>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class NondeterministicModel<storm::RationalFunction>; template class NondeterministicModel<storm::RationalFunction>;
#endif #endif

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

@ -34,9 +34,9 @@ namespace storm {
template class StochasticTwoPlayerGame<double>; template class StochasticTwoPlayerGame<double>;
// template class StochasticTwoPlayerGame<float>; // template class StochasticTwoPlayerGame<float>;
//#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
// template class StochasticTwoPlayerGame<storm::RationalFunction>; // template class StochasticTwoPlayerGame<storm::RationalFunction>;
//#endif #endif
} // namespace sparse } // namespace sparse
} // namespace models } // namespace models

16
src/parser/AutoParser.cpp
View File

@ -10,6 +10,8 @@
#include "src/utility/macros.h" #include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
#include "src/adapters/CarlAdapter.h"
#include "src/utility/cstring.h" #include "src/utility/cstring.h"
#include "src/utility/OsDetection.h" #include "src/utility/OsDetection.h"
@ -19,7 +21,7 @@ namespace storm {
using namespace storm::utility::cstring; using namespace storm::utility::cstring;
template<typename ValueType, typename RewardValueType> template<typename ValueType, typename RewardValueType>
std::shared_ptr<storm::models::sparse::Model<double>> AutoParser<ValueType, RewardValueType>::parseModel(std::string const& transitionsFilename, std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>> AutoParser<ValueType, RewardValueType>::parseModel(std::string const& transitionsFilename,
std::string const& labelingFilename, std::string const& labelingFilename,
std::string const& stateRewardFilename, std::string const& stateRewardFilename,
std::string const& transitionRewardFilename, std::string const& transitionRewardFilename,
@ -33,22 +35,22 @@ namespace storm {
switch (type) { switch (type) {
case storm::models::ModelType::Dtmc: case storm::models::ModelType::Dtmc:
{ {
model.reset(new storm::models::sparse::Dtmc<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(DeterministicModelParser<ValueType, RewardValueType>::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); model = std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>>(new storm::models::sparse::Dtmc<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(DeterministicModelParser<ValueType, RewardValueType>::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
break; break;
} }
case storm::models::ModelType::Ctmc: case storm::models::ModelType::Ctmc:
{ {
model.reset(new storm::models::sparse::Ctmc<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(DeterministicModelParser<ValueType, RewardValueType>::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); model = std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>>(new storm::models::sparse::Ctmc<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(DeterministicModelParser<ValueType, RewardValueType>::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
break; break;
} }
case storm::models::ModelType::Mdp: case storm::models::ModelType::Mdp:
{ {
model.reset(new storm::models::sparse::Mdp<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(NondeterministicModelParser<ValueType, RewardValueType>::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename)))); model = std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>>(new storm::models::sparse::Mdp<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(NondeterministicModelParser<ValueType, RewardValueType>::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename))));
break; break;
} }
case storm::models::ModelType::MarkovAutomaton: case storm::models::ModelType::MarkovAutomaton:
{ {
model.reset(new storm::models::sparse::MarkovAutomaton<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(storm::parser::MarkovAutomatonParser<ValueType, RewardValueType>::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))); model = std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>>(new storm::models::sparse::MarkovAutomaton<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>(std::move(storm::parser::MarkovAutomatonParser<ValueType, RewardValueType>::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
break; break;
} }
default: default:
@ -95,5 +97,9 @@ namespace storm {
// Explicitly instantiate the parser. // Explicitly instantiate the parser.
template class AutoParser<double, double>; template class AutoParser<double, double>;
#ifdef STORM_HAVE_CARL
template class AutoParser<double, storm::Interval>;
#endif
} // namespace parser } // namespace parser
} // namespace storm } // namespace storm

2
src/parser/AutoParser.h
View File

@ -47,7 +47,7 @@ namespace storm {
* is meaningful, this file will not be parsed. * is meaningful, this file will not be parsed.
* @return A shared_ptr containing the resulting model. * @return A shared_ptr containing the resulting model.
*/ */
static std::shared_ptr<storm::models::sparse::Model<double>> parseModel(std::string const& transitionsFilename, static std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>> parseModel(std::string const& transitionsFilename,
std::string const& labelingFilename, std::string const& labelingFilename,
std::string const& stateRewardFilename = "", std::string const& stateRewardFilename = "",
std::string const& transitionRewardFilename = "", std::string const& transitionRewardFilename = "",

6
src/parser/DeterministicModelParser.cpp
View File

@ -9,6 +9,8 @@
#include "src/parser/AtomicPropositionLabelingParser.h" #include "src/parser/AtomicPropositionLabelingParser.h"
#include "src/parser/SparseStateRewardParser.h" #include "src/parser/SparseStateRewardParser.h"
#include "src/adapters/CarlAdapter.h"
namespace storm { namespace storm {
namespace parser { namespace parser {
@ -63,5 +65,9 @@ namespace storm {
template class DeterministicModelParser<double, double>; template class DeterministicModelParser<double, double>;
#ifdef STORM_HAVE_CARL
template class DeterministicModelParser<double, storm::Interval>;
#endif
} /* namespace parser */ } /* namespace parser */
} /* namespace storm */ } /* namespace storm */

9
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -16,6 +16,8 @@
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GeneralSettings.h"
#include "src/adapters/CarlAdapter.h"
#include "log4cplus/logger.h" #include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h" #include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger; extern log4cplus::Logger logger;
@ -297,5 +299,12 @@ namespace storm {
template class DeterministicSparseTransitionParser<double>; template class DeterministicSparseTransitionParser<double>;
template storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser<double>::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const& transitionMatrix); template storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser<double>::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const& transitionMatrix);
template storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser<double>::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const& transitionMatrix); template storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser<double>::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const& transitionMatrix);
#ifdef STORM_HAVE_CARL
template class DeterministicSparseTransitionParser<storm::Interval>;
template storm::storage::SparseMatrix<storm::Interval> DeterministicSparseTransitionParser<storm::Interval>::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const& transitionMatrix);
template storm::storage::SparseMatrix<storm::Interval> DeterministicSparseTransitionParser<storm::Interval>::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const& transitionMatrix);
#endif
} // namespace parser } // namespace parser
} // namespace storm } // namespace storm

8
src/parser/MarkovAutomatonParser.cpp
View File

@ -6,6 +6,8 @@
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
#include "src/adapters/CarlAdapter.h"
#include "log4cplus/logger.h" #include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h" #include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger; extern log4cplus::Logger logger;
@ -31,7 +33,7 @@ namespace storm {
stateRewards.reset(storm::parser::SparseStateRewardParser<RewardValueType>::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename)); stateRewards.reset(storm::parser::SparseStateRewardParser<RewardValueType>::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename));
} }
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<RewardValueType>> rewardModels; std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<RewardValueType>> rewardModels;
rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel<RewardValueType>(stateRewards, boost::optional<std::vector<double>>(), boost::optional<storm::storage::SparseMatrix<double>>()))); rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel<RewardValueType>(stateRewards, boost::optional<std::vector<RewardValueType>>(), boost::optional<storm::storage::SparseMatrix<RewardValueType>>())));
// Since Markov Automata do not support transition rewards no path should be given here. // Since Markov Automata do not support transition rewards no path should be given here.
if (transitionRewardFilename != "") { if (transitionRewardFilename != "") {
@ -47,5 +49,9 @@ namespace storm {
template class MarkovAutomatonParser<double, double>; template class MarkovAutomatonParser<double, double>;
#ifdef STORM_HAVE_CARL
template class MarkovAutomatonParser<double, storm::Interval>;
#endif
} // namespace parser } // namespace parser
} // namespace storm } // namespace storm

1
src/parser/MarkovAutomatonSparseTransitionParser.cpp
View File

@ -8,7 +8,6 @@
#include "src/utility/cstring.h" #include "src/utility/cstring.h"
#include "src/utility/macros.h" #include "src/utility/macros.h"
namespace storm { namespace storm {
namespace parser { namespace parser {

8
src/parser/NondeterministicModelParser.cpp
View File

@ -10,6 +10,8 @@
#include "src/parser/SparseStateRewardParser.h" #include "src/parser/SparseStateRewardParser.h"
#include "src/parser/SparseChoiceLabelingParser.h" #include "src/parser/SparseChoiceLabelingParser.h"
#include "src/adapters/CarlAdapter.h"
namespace storm { namespace storm {
namespace parser { namespace parser {
@ -31,7 +33,7 @@ namespace storm {
} }
// Only parse transition rewards if a file is given. // Only parse transition rewards if a file is given.
boost::optional<storm::storage::SparseMatrix<double>> transitionRewards; boost::optional<storm::storage::SparseMatrix<RewardValueType>> transitionRewards;
if (!transitionRewardFilename.empty()) { if (!transitionRewardFilename.empty()) {
transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser<RewardValueType>::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions)); transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser<RewardValueType>::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions));
} }
@ -62,5 +64,9 @@ namespace storm {
template class NondeterministicModelParser<double, double>; template class NondeterministicModelParser<double, double>;
#ifdef STORM_HAVE_CARL
template class NondeterministicModelParser<double, storm::Interval>;
#endif
} /* namespace parser */ } /* namespace parser */
} /* namespace storm */ } /* namespace storm */

11
src/parser/NondeterministicSparseTransitionParser.cpp
View File

@ -13,6 +13,8 @@
#include "src/utility/cstring.h" #include "src/utility/cstring.h"
#include "src/adapters/CarlAdapter.h"
#include "log4cplus/logger.h" #include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h" #include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger; extern log4cplus::Logger logger;
@ -189,7 +191,7 @@ namespace storm {
// Finally, build the actual matrix, test and return it. // Finally, build the actual matrix, test and return it.
storm::storage::SparseMatrix<ValueType> resultMatrix = matrixBuilder.build(); storm::storage::SparseMatrix<ValueType> resultMatrix = matrixBuilder.build();
// Since we cannot do the testing if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards. // Since we cannot check if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards.
if (isRewardFile && !resultMatrix.isSubmatrixOf(modelInformation)) { if (isRewardFile && !resultMatrix.isSubmatrixOf(modelInformation)) {
LOG4CPLUS_ERROR(logger, "There are rewards for non existent transitions given in the reward file."); LOG4CPLUS_ERROR(logger, "There are rewards for non existent transitions given in the reward file.");
throw storm::exceptions::WrongFormatException() << "There are rewards for non existent transitions given in the reward file."; throw storm::exceptions::WrongFormatException() << "There are rewards for non existent transitions given in the reward file.";
@ -337,5 +339,12 @@ namespace storm {
template storm::storage::SparseMatrix<double> NondeterministicSparseTransitionParser<double>::parseNondeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const& modelInformation); template storm::storage::SparseMatrix<double> NondeterministicSparseTransitionParser<double>::parseNondeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const& modelInformation);
template storm::storage::SparseMatrix<double> NondeterministicSparseTransitionParser<double>::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const& modelInformation); template storm::storage::SparseMatrix<double> NondeterministicSparseTransitionParser<double>::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const& modelInformation);
#ifdef STORM_HAVE_CARL
template class NondeterministicSparseTransitionParser<storm::Interval>;
template storm::storage::SparseMatrix<storm::Interval> NondeterministicSparseTransitionParser<storm::Interval>::parseNondeterministicTransitionRewards<double>(std::string const& filename, storm::storage::SparseMatrix<double> const& modelInformation);
template storm::storage::SparseMatrix<storm::Interval> NondeterministicSparseTransitionParser<storm::Interval>::parse<double>(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const& modelInformation);
#endif
} // namespace parser } // namespace parser
} // namespace storm } // namespace storm

9
src/parser/SparseStateRewardParser.cpp
View File

@ -6,6 +6,9 @@
#include "src/exceptions/FileIoException.h" #include "src/exceptions/FileIoException.h"
#include "src/utility/cstring.h" #include "src/utility/cstring.h"
#include "src/parser/MappedFile.h" #include "src/parser/MappedFile.h"
#include "src/adapters/CarlAdapter.h"
#include "log4cplus/logger.h" #include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h" #include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger; extern log4cplus::Logger logger;
@ -27,7 +30,7 @@ namespace storm {
char const* buf = file.getData(); char const* buf = file.getData();
// Create state reward vector with given state count. // Create state reward vector with given state count.
std::vector<double> stateRewards(stateCount); std::vector<ValueType> stateRewards(stateCount);
// Now parse state reward assignments. // Now parse state reward assignments.
uint_fast64_t state = 0; uint_fast64_t state = 0;
@ -71,5 +74,9 @@ namespace storm {
template class SparseStateRewardParser<double>; template class SparseStateRewardParser<double>;
#ifdef STORM_HAVE_CARL
template class SparseStateRewardParser<storm::Interval>;
#endif
} // namespace parser } // namespace parser
} // namespace storm } // namespace storm

14
src/storage/SparseMatrix.cpp
View File

@ -1081,7 +1081,8 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
bool SparseMatrix<ValueType>::isSubmatrixOf(SparseMatrix<ValueType> const& matrix) const { template<typename OtherValueType>
bool SparseMatrix<ValueType>::isSubmatrixOf(SparseMatrix<OtherValueType> const& matrix) const {
// Check for matching sizes. // Check for matching sizes.
if (this->getRowCount() != matrix.getRowCount()) return false; if (this->getRowCount() != matrix.getRowCount()) return false;
if (this->getColumnCount() != matrix.getColumnCount()) return false; if (this->getColumnCount() != matrix.getColumnCount()) return false;
@ -1089,7 +1090,9 @@ namespace storm {
// Check the subset property for all rows individually. // Check the subset property for all rows individually.
for (index_type row = 0; row < this->getRowCount(); ++row) { for (index_type row = 0; row < this->getRowCount(); ++row) {
for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = matrix.begin(row), ite2 = matrix.end(row); it1 != ite1; ++it1) { auto it2 = matrix.begin(row);
auto ite2 = matrix.end(row);
for (const_iterator it1 = this->begin(row), ite1 = this->end(row); it1 != ite1; ++it1) {
// Skip over all entries of the other matrix that are before the current entry in the current matrix. // Skip over all entries of the other matrix that are before the current entry in the current matrix.
while (it2 != ite2 && it2->getColumn() < it1->getColumn()) { while (it2 != ite2 && it2->getColumn() < it1->getColumn()) {
++it2; ++it2;
@ -1165,6 +1168,7 @@ namespace storm {
template class SparseMatrix<double>; template class SparseMatrix<double>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix); template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
template std::vector<double> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<double> const& otherMatrix) const; template std::vector<double> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<double> const& otherMatrix) const;
template bool SparseMatrix<double>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
// float // float
template class MatrixEntry<typename SparseMatrix<float>::index_type, float>; template class MatrixEntry<typename SparseMatrix<float>::index_type, float>;
@ -1173,6 +1177,7 @@ namespace storm {
template class SparseMatrix<float>; template class SparseMatrix<float>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<float> const& matrix); template std::ostream& operator<<(std::ostream& out, SparseMatrix<float> const& matrix);
template std::vector<float> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<float> const& otherMatrix) const; template std::vector<float> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<float> const& otherMatrix) const;
template bool SparseMatrix<float>::isSubmatrixOf(SparseMatrix<float> const& matrix) const;
// int // int
template class MatrixEntry<typename SparseMatrix<int>::index_type, int>; template class MatrixEntry<typename SparseMatrix<int>::index_type, int>;
@ -1180,6 +1185,7 @@ namespace storm {
template class SparseMatrixBuilder<int>; template class SparseMatrixBuilder<int>;
template class SparseMatrix<int>; template class SparseMatrix<int>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix); template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);
template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<int> const& matrix) const;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
// Rat Function // Rat Function
@ -1192,6 +1198,7 @@ namespace storm {
template std::vector<storm::RationalFunction> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const; template std::vector<storm::RationalFunction> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
template std::vector<storm::RationalFunction> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const; template std::vector<storm::RationalFunction> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
template std::vector<storm::RationalFunction> SparseMatrix<int>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const; template std::vector<storm::RationalFunction> SparseMatrix<int>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
template bool SparseMatrix<storm::RationalFunction>::isSubmatrixOf(SparseMatrix<storm::RationalFunction> const& matrix) const;
// Intervals // Intervals
template std::vector<storm::Interval> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const; template std::vector<storm::Interval> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
@ -1201,6 +1208,9 @@ namespace storm {
template class SparseMatrix<Interval>; template class SparseMatrix<Interval>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<Interval> const& matrix); template std::ostream& operator<<(std::ostream& out, SparseMatrix<Interval> const& matrix);
template std::vector<storm::Interval> SparseMatrix<Interval>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const; template std::vector<storm::Interval> SparseMatrix<Interval>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
template bool SparseMatrix<storm::Interval>::isSubmatrixOf(SparseMatrix<storm::Interval> const& matrix) const;
template bool SparseMatrix<storm::Interval>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
#endif #endif

3
src/storage/SparseMatrix.h
View File

@ -753,7 +753,8 @@ namespace storm {
* @param matrix The matrix that possibly is a supermatrix of the current matrix. * @param matrix The matrix that possibly is a supermatrix of the current matrix.
* @return True iff the current matrix is a submatrix of the given matrix. * @return True iff the current matrix is a submatrix of the given matrix.
*/ */
bool isSubmatrixOf(SparseMatrix<value_type> const& matrix) const; template<typename OtherValueType>
bool isSubmatrixOf(SparseMatrix<OtherValueType> const& matrix) const;
template<typename TPrime> template<typename TPrime>
friend std::ostream& operator<<(std::ostream& out, SparseMatrix<TPrime> const& matrix); friend std::ostream& operator<<(std::ostream& out, SparseMatrix<TPrime> const& matrix);

Write Preview
|||||||
100:0
Loading…
Cancel
Save