From b2d8cae9ce996109ff5d563cc3c4e4c71c264486 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 7 Sep 2015 14:00:35 +0200
Subject: [PATCH] instantiated (and fixed occurring problems) explicit parsers
with intervals as the reward model value type
Former-commit-id: bf452cd751aaf94e37fb420eea0d2ce44f696fe0
---
src/models/sparse/Ctmc.cpp | 6 ++-
src/models/sparse/DeterministicModel.cpp | 8 ++--
src/models/sparse/DeterministicModel.h | 2 +-
src/models/sparse/Dtmc.cpp | 6 ++-
src/models/sparse/MarkovAutomaton.cpp | 16 +++----
src/models/sparse/MarkovAutomaton.h | 2 +-
src/models/sparse/Mdp.cpp | 42 ++++++++++---------
src/models/sparse/Mdp.h | 4 +-
src/models/sparse/Model.cpp | 2 +
src/models/sparse/NondeterministicModel.cpp | 8 ++--
src/models/sparse/StochasticTwoPlayerGame.cpp | 4 +-
src/parser/AutoParser.cpp | 16 ++++---
src/parser/AutoParser.h | 2 +-
src/parser/DeterministicModelParser.cpp | 6 +++
.../DeterministicSparseTransitionParser.cpp | 9 ++++
src/parser/MarkovAutomatonParser.cpp | 10 ++++-
.../MarkovAutomatonSparseTransitionParser.cpp | 1 -
src/parser/NondeterministicModelParser.cpp | 10 ++++-
...NondeterministicSparseTransitionParser.cpp | 13 +++++-
src/parser/SparseStateRewardParser.cpp | 9 +++-
src/storage/SparseMatrix.cpp | 18 ++++++--
src/storage/SparseMatrix.h | 3 +-
22 files changed, 135 insertions(+), 62 deletions(-)
diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp
index 371d48270..62347c81b 100644
--- a/src/models/sparse/Ctmc.cpp
+++ b/src/models/sparse/Ctmc.cpp
@@ -11,7 +11,7 @@ namespace storm {
Ctmc<ValueType, RewardModelType>::Ctmc(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::models::sparse::StateLabeling const& stateLabeling,
std::unordered_map<std::string, RewardModelType> const& rewardModels,
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());
}
@@ -19,7 +19,7 @@ namespace storm {
Ctmc<ValueType, RewardModelType>::Ctmc(storm::storage::SparseMatrix<ValueType>&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
std::unordered_map<std::string, RewardModelType>&& rewardModels,
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.
exitRates = createExitRateVector(this->getTransitionMatrix());
}
@@ -41,6 +41,8 @@ namespace storm {
template class Ctmc<double>;
#ifdef STORM_HAVE_CARL
+ template class Ctmc<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
template class Ctmc<storm::RationalFunction>;
#endif
diff --git a/src/models/sparse/DeterministicModel.cpp b/src/models/sparse/DeterministicModel.cpp
index d774d5e7f..0fb6de34a 100644
--- a/src/models/sparse/DeterministicModel.cpp
+++ b/src/models/sparse/DeterministicModel.cpp
@@ -12,7 +12,7 @@ namespace storm {
storm::models::sparse::StateLabeling const& stateLabeling,
std::unordered_map<std::string, RewardModelType> const& rewardModels,
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.
}
@@ -22,13 +22,13 @@ namespace storm {
storm::models::sparse::StateLabeling&& stateLabeling,
std::unordered_map<std::string, RewardModelType>&& rewardModels,
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.
}
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 {
- 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.
auto rowIt = this->getTransitionMatrix().begin();
@@ -59,6 +59,8 @@ namespace storm {
template class DeterministicModel<float>;
#ifdef STORM_HAVE_CARL
+ template class DeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
template class DeterministicModel<storm::RationalFunction>;
#endif
diff --git a/src/models/sparse/DeterministicModel.h b/src/models/sparse/DeterministicModel.h
index fb3e367df..cc886c401 100644
--- a/src/models/sparse/DeterministicModel.h
+++ b/src/models/sparse/DeterministicModel.h
@@ -49,7 +49,7 @@ namespace storm {
#ifndef WINDOWS
DeterministicModel(DeterministicModel<ValueType, RewardModelType>&& other) = default;
- DeterministicModel<ValueType>& operator=(DeterministicModel<ValueType, RewardModelType>&& model) = default;
+ DeterministicModel<ValueType, RewardModelType>& operator=(DeterministicModel<ValueType, RewardModelType>&& model) = default;
#endif
virtual void reduceToStateBasedRewards() override;
diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp
index 9cc968136..31c222207 100644
--- a/src/models/sparse/Dtmc.cpp
+++ b/src/models/sparse/Dtmc.cpp
@@ -14,14 +14,14 @@ namespace storm {
storm::models::sparse::StateLabeling const& stateLabeling,
std::unordered_map<std::string, RewardModelType> const& rewardModels,
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.");
}
template <typename ValueType, typename RewardModelType>
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)
- : 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.");
}
@@ -225,6 +225,8 @@ namespace storm {
template class Dtmc<float>;
#ifdef STORM_HAVE_CARL
+ template class Dtmc<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
template class Dtmc<storm::RationalFunction>;
#endif
diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp
index b04c294f7..56a6400d1 100644
--- a/src/models/sparse/MarkovAutomaton.cpp
+++ b/src/models/sparse/MarkovAutomaton.cpp
@@ -15,7 +15,7 @@ namespace storm {
std::vector<ValueType> const& exitRates,
std::unordered_map<std::string, RewardModelType> const& rewardModels,
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();
}
@@ -26,7 +26,7 @@ namespace storm {
std::vector<ValueType> const& exitRates,
std::unordered_map<std::string, RewardModelType>&& rewardModels,
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();
}
@@ -124,7 +124,7 @@ namespace storm {
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 {
- 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.
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
@@ -205,7 +205,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType>
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>
@@ -220,9 +220,11 @@ namespace storm {
template class MarkovAutomaton<double>;
// template class MarkovAutomaton<float>;
-//#ifdef STORM_HAVE_CARL
-// template class MarkovAutomaton<storm::RationalFunction>;
-//#endif
+#ifdef STORM_HAVE_CARL
+ template class MarkovAutomaton<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
+ template class MarkovAutomaton<storm::RationalFunction>;
+#endif
} // namespace sparse
} // namespace models
diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h
index 98d561964..731b845f3 100644
--- a/src/models/sparse/MarkovAutomaton.h
+++ b/src/models/sparse/MarkovAutomaton.h
@@ -12,7 +12,7 @@ namespace storm {
* This class represents a Markov automaton.
*/
template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
- class MarkovAutomaton : public NondeterministicModel<ValueType> {
+ class MarkovAutomaton : public NondeterministicModel<ValueType, RewardModelType> {
public:
/*!
* Constructs a model from the given data.
diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp
index 0ba1e7c28..f6e4b4800 100644
--- a/src/models/sparse/Mdp.cpp
+++ b/src/models/sparse/Mdp.cpp
@@ -9,42 +9,42 @@
namespace storm {
namespace models {
namespace sparse {
-
+
template <typename ValueType, typename RewardModelType>
Mdp<ValueType, RewardModelType>::Mdp(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
storm::models::sparse::StateLabeling const& stateLabeling,
std::unordered_map<std::string, RewardModelType> const& rewardModels,
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.");
}
-
-
+
+
template <typename ValueType, typename RewardModelType>
Mdp<ValueType, RewardModelType>::Mdp(storm::storage::SparseMatrix<ValueType>&& transitionMatrix,
storm::models::sparse::StateLabeling&& stateLabeling,
std::unordered_map<std::string, RewardModelType>&& rewardModels,
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.");
}
-
+
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.");
-
+
std::vector<LabelSet> const& choiceLabeling = this->getChoiceLabeling();
-
+
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true, true);
std::vector<LabelSet> newChoiceLabeling;
-
+
// Check for each choice of each state, whether the choice labels are fully contained in the given label set.
uint_fast64_t currentRow = 0;
for(uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
bool stateHasValidChoice = false;
for (uint_fast64_t choice = this->getTransitionMatrix().getRowGroupIndices()[state]; choice < this->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) {
bool choiceValid = std::includes(enabledChoiceLabels.begin(), enabledChoiceLabels.end(), choiceLabeling[choice].begin(), choiceLabeling[choice].end());
-
+
// If the choice is valid, copy over all its elements.
if (choiceValid) {
if (!stateHasValidChoice) {
@@ -58,7 +58,7 @@ namespace storm {
++currentRow;
}
}
-
+
// If no choice of the current state may be taken, we insert a self-loop to the state instead.
if (!stateHasValidChoice) {
transitionMatrixBuilder.newRowGroup(currentRow);
@@ -67,27 +67,29 @@ namespace storm {
++currentRow;
}
}
-
- Mdp<ValueType> restrictedMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(this->getStateLabeling()),
- std::unordered_map<std::string, RewardModelType>(this->getRewardModels()), boost::optional<std::vector<LabelSet>>(newChoiceLabeling));
-
+
+ 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));
+
return restrictedMdp;
}
-
+
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);
std::unordered_map<std::string, RewardModelType> newRewardModels;
for (auto const& rewardModel : this->getRewardModels()) {
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<float>;
#ifdef STORM_HAVE_CARL
+ template class Mdp<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
template class Mdp<storm::RationalFunction>;
#endif
diff --git a/src/models/sparse/Mdp.h b/src/models/sparse/Mdp.h
index 6354551f9..9bc29bbc9 100644
--- a/src/models/sparse/Mdp.h
+++ b/src/models/sparse/Mdp.h
@@ -57,7 +57,7 @@ namespace storm {
* and which ones need to be ignored.
* @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.
@@ -65,7 +65,7 @@ namespace storm {
* @param enabledActions A BitVector of lenght numberOfChoices(), which is one iff the action should be kept.
* @return A subMDP.
*/
- Mdp<ValueType> restrictActions(storm::storage::BitVector const& enabledActions) const;
+ Mdp<ValueType, RewardModelType> restrictActions(storm::storage::BitVector const& enabledActions) const;
};
} // namespace sparse
diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp
index 8ed43e87a..cf22ecf6c 100644
--- a/src/models/sparse/Model.cpp
+++ b/src/models/sparse/Model.cpp
@@ -300,6 +300,8 @@ namespace storm {
template class Model<float>;
#ifdef STORM_HAVE_CARL
+ template class Model<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
template class Model<storm::RationalFunction>;
#endif
diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp
index c5e3e9ecf..9cfbe75f9 100644
--- a/src/models/sparse/NondeterministicModel.cpp
+++ b/src/models/sparse/NondeterministicModel.cpp
@@ -16,7 +16,7 @@ namespace storm {
storm::models::sparse::StateLabeling const& stateLabeling,
std::unordered_map<std::string, RewardModelType> const& rewardModels,
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.
}
@@ -26,7 +26,7 @@ namespace storm {
storm::models::sparse::StateLabeling&& stateLabeling,
std::unordered_map<std::string, RewardModelType>&& rewardModels,
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)) {
// Intentionally left empty.
}
@@ -79,7 +79,7 @@ namespace storm {
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 {
- 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.
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
@@ -151,6 +151,8 @@ namespace storm {
template class NondeterministicModel<float>;
#ifdef STORM_HAVE_CARL
+ template class NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+
template class NondeterministicModel<storm::RationalFunction>;
#endif
diff --git a/src/models/sparse/StochasticTwoPlayerGame.cpp b/src/models/sparse/StochasticTwoPlayerGame.cpp
index ecbb204c5..fbe79af36 100644
--- a/src/models/sparse/StochasticTwoPlayerGame.cpp
+++ b/src/models/sparse/StochasticTwoPlayerGame.cpp
@@ -34,9 +34,9 @@ namespace storm {
template class StochasticTwoPlayerGame<double>;
// template class StochasticTwoPlayerGame<float>;
-//#ifdef STORM_HAVE_CARL
+#ifdef STORM_HAVE_CARL
// template class StochasticTwoPlayerGame<storm::RationalFunction>;
-//#endif
+#endif
} // namespace sparse
} // namespace models
diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp
index ca01c758f..2ec30fb64 100644
--- a/src/parser/AutoParser.cpp
+++ b/src/parser/AutoParser.cpp
@@ -10,6 +10,8 @@
#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
+#include "src/adapters/CarlAdapter.h"
+
#include "src/utility/cstring.h"
#include "src/utility/OsDetection.h"
@@ -19,7 +21,7 @@ namespace storm {
using namespace storm::utility::cstring;
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& stateRewardFilename,
std::string const& transitionRewardFilename,
@@ -33,22 +35,22 @@ namespace storm {
switch (type) {
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;
}
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;
}
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;
}
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;
}
default:
@@ -94,6 +96,10 @@ namespace storm {
// Explicitly instantiate the parser.
template class AutoParser<double, double>;
+
+#ifdef STORM_HAVE_CARL
+ template class AutoParser<double, storm::Interval>;
+#endif
} // namespace parser
} // namespace storm
diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h
index fd144b24e..525795e9d 100644
--- a/src/parser/AutoParser.h
+++ b/src/parser/AutoParser.h
@@ -47,7 +47,7 @@ namespace storm {
* is meaningful, this file will not be parsed.
* @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& stateRewardFilename = "",
std::string const& transitionRewardFilename = "",
diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp
index 34bec0855..18f14428a 100644
--- a/src/parser/DeterministicModelParser.cpp
+++ b/src/parser/DeterministicModelParser.cpp
@@ -9,6 +9,8 @@
#include "src/parser/AtomicPropositionLabelingParser.h"
#include "src/parser/SparseStateRewardParser.h"
+#include "src/adapters/CarlAdapter.h"
+
namespace storm {
namespace parser {
@@ -62,6 +64,10 @@ namespace storm {
}
template class DeterministicModelParser<double, double>;
+
+#ifdef STORM_HAVE_CARL
+ template class DeterministicModelParser<double, storm::Interval>;
+#endif
} /* namespace parser */
} /* namespace storm */
diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp
index bb91355d4..94b82a4c7 100644
--- a/src/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/parser/DeterministicSparseTransitionParser.cpp
@@ -16,6 +16,8 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
+#include "src/adapters/CarlAdapter.h"
+
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
@@ -297,5 +299,12 @@ namespace storm {
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>::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 storm
diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp
index 683b4142c..6a68abda8 100644
--- a/src/parser/MarkovAutomatonParser.cpp
+++ b/src/parser/MarkovAutomatonParser.cpp
@@ -6,6 +6,8 @@
#include "src/exceptions/WrongFormatException.h"
+#include "src/adapters/CarlAdapter.h"
+
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
@@ -31,7 +33,7 @@ namespace storm {
stateRewards.reset(storm::parser::SparseStateRewardParser<RewardValueType>::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename));
}
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.
if (transitionRewardFilename != "") {
@@ -46,6 +48,10 @@ namespace storm {
}
template class MarkovAutomatonParser<double, double>;
-
+
+#ifdef STORM_HAVE_CARL
+ template class MarkovAutomatonParser<double, storm::Interval>;
+#endif
+
} // namespace parser
} // namespace storm
diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp
index 539a67739..6bc214cab 100644
--- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp
+++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp
@@ -8,7 +8,6 @@
#include "src/utility/cstring.h"
#include "src/utility/macros.h"
-
namespace storm {
namespace parser {
diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp
index 743d6e9b2..220451c33 100644
--- a/src/parser/NondeterministicModelParser.cpp
+++ b/src/parser/NondeterministicModelParser.cpp
@@ -10,6 +10,8 @@
#include "src/parser/SparseStateRewardParser.h"
#include "src/parser/SparseChoiceLabelingParser.h"
+#include "src/adapters/CarlAdapter.h"
+
namespace storm {
namespace parser {
@@ -31,7 +33,7 @@ namespace storm {
}
// 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()) {
transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser<RewardValueType>::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions));
}
@@ -61,6 +63,10 @@ namespace storm {
}
template class NondeterministicModelParser<double, double>;
-
+
+#ifdef STORM_HAVE_CARL
+ template class NondeterministicModelParser<double, storm::Interval>;
+#endif
+
} /* namespace parser */
} /* namespace storm */
diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp
index 646fc0352..3136bc36f 100644
--- a/src/parser/NondeterministicSparseTransitionParser.cpp
+++ b/src/parser/NondeterministicSparseTransitionParser.cpp
@@ -13,6 +13,8 @@
#include "src/utility/cstring.h"
+#include "src/adapters/CarlAdapter.h"
+
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
@@ -189,7 +191,7 @@ namespace storm {
// Finally, build the actual matrix, test and return it.
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)) {
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.";
@@ -336,6 +338,13 @@ namespace storm {
template class NondeterministicSparseTransitionParser<double>;
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);
-
+
+#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 storm
diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp
index d2424740d..b60856eb8 100644
--- a/src/parser/SparseStateRewardParser.cpp
+++ b/src/parser/SparseStateRewardParser.cpp
@@ -6,6 +6,9 @@
#include "src/exceptions/FileIoException.h"
#include "src/utility/cstring.h"
#include "src/parser/MappedFile.h"
+
+#include "src/adapters/CarlAdapter.h"
+
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
@@ -27,7 +30,7 @@ namespace storm {
char const* buf = file.getData();
// Create state reward vector with given state count.
- std::vector<double> stateRewards(stateCount);
+ std::vector<ValueType> stateRewards(stateCount);
// Now parse state reward assignments.
uint_fast64_t state = 0;
@@ -71,5 +74,9 @@ namespace storm {
template class SparseStateRewardParser<double>;
+#ifdef STORM_HAVE_CARL
+ template class SparseStateRewardParser<storm::Interval>;
+#endif
+
} // namespace parser
} // namespace storm
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index 20b7cd7f5..4648950b3 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -1081,7 +1081,8 @@ namespace storm {
}
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.
if (this->getRowCount() != matrix.getRowCount()) return false;
if (this->getColumnCount() != matrix.getColumnCount()) return false;
@@ -1089,7 +1090,9 @@ namespace storm {
// Check the subset property for all rows individually.
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.
while (it2 != ite2 && it2->getColumn() < it1->getColumn()) {
++it2;
@@ -1165,14 +1168,16 @@ namespace storm {
template class SparseMatrix<double>;
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;
-
- // float
+ template bool SparseMatrix<double>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
+
+ // float
template class MatrixEntry<typename SparseMatrix<float>::index_type, float>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, float> const& entry);
template class SparseMatrixBuilder<float>;
template class SparseMatrix<float>;
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 bool SparseMatrix<float>::isSubmatrixOf(SparseMatrix<float> const& matrix) const;
// int
template class MatrixEntry<typename SparseMatrix<int>::index_type, int>;
@@ -1180,6 +1185,7 @@ namespace storm {
template class SparseMatrixBuilder<int>;
template class SparseMatrix<int>;
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
// 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<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 bool SparseMatrix<storm::RationalFunction>::isSubmatrixOf(SparseMatrix<storm::RationalFunction> const& matrix) const;
// Intervals
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 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 bool SparseMatrix<storm::Interval>::isSubmatrixOf(SparseMatrix<storm::Interval> const& matrix) const;
+
+ template bool SparseMatrix<storm::Interval>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
#endif
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 03de1bd6b..1b5bef847 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -753,7 +753,8 @@ namespace storm {
* @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.
*/
- bool isSubmatrixOf(SparseMatrix<value_type> const& matrix) const;
+ template<typename OtherValueType>
+ bool isSubmatrixOf(SparseMatrix<OtherValueType> const& matrix) const;
template<typename TPrime>
friend std::ostream& operator<<(std::ostream& out, SparseMatrix<TPrime> const& matrix);