diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 4b562a467..2807e2f51 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -336,17 +336,19 @@ namespace storm {
}
template <storm::dd::DdType Type>
- typename DdPrismModelBuilder<Type>::ActionDecisionDiagram DdPrismModelBuilder<Type>::createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, boost::optional<uint_fast64_t> synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset) {
+ typename DdPrismModelBuilder<Type>::ActionDecisionDiagram DdPrismModelBuilder<Type>::createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, uint_fast64_t synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset) {
std::vector<ActionDecisionDiagram> commandDds;
for (storm::prism::Command const& command : module.getCommands()) {
// Determine whether the command is relevant for the selected action.
- bool relevant = (!synchronizationActionIndex && !command.isLabeled()) || (synchronizationActionIndex && command.isLabeled() && command.getActionIndex() == synchronizationActionIndex.get());
+ bool relevant = (synchronizationActionIndex == 0 && !command.isLabeled()) || (synchronizationActionIndex && command.isLabeled() && command.getActionIndex() == synchronizationActionIndex);
if (!relevant) {
continue;
}
+ STORM_LOG_TRACE("Translating command " << command);
+
// At this point, the command is known to be relevant for the action.
commandDds.push_back(createCommandDecisionDiagram(generationInfo, module, command));
}
@@ -551,12 +553,12 @@ namespace storm {
template <storm::dd::DdType Type>
typename DdPrismModelBuilder<Type>::ModuleDecisionDiagram DdPrismModelBuilder<Type>::createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap) {
// Start by creating the action DD for the independent action.
- ActionDecisionDiagram independentActionDd = createActionDecisionDiagram(generationInfo, module, boost::optional<uint_fast64_t>(), 0);
+ ActionDecisionDiagram independentActionDd = createActionDecisionDiagram(generationInfo, module, 0, 0);
uint_fast64_t numberOfUsedNondeterminismVariables = independentActionDd.numberOfUsedNondeterminismVariables;
// Create module DD for all synchronizing actions of the module.
std::map<uint_fast64_t, ActionDecisionDiagram> actionIndexToDdMap;
- for (auto const& actionIndex : module.getActionIndices()) {
+ for (auto const& actionIndex : module.getSynchronizingActionIndices()) {
STORM_LOG_TRACE("Creating DD for action '" << actionIndex << "'.");
ActionDecisionDiagram tmp = createActionDecisionDiagram(generationInfo, module, actionIndex, synchronizingActionToOffsetMap.at(actionIndex));
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, tmp.numberOfUsedNondeterminismVariables);
@@ -567,12 +569,18 @@ namespace storm {
}
template <storm::dd::DdType Type>
- storm::dd::Add<Type> DdPrismModelBuilder<Type>::getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, boost::optional<uint_fast64_t> const& synchronizationAction) {
+ storm::dd::Add<Type> DdPrismModelBuilder<Type>::getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, uint_fast64_t actionIndex) {
storm::dd::Add<Type> synchronization = generationInfo.manager->getAddOne();
- for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) {
- if (synchronizationAction && synchronizationAction.get() == i) {
- synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1).toAdd();
- } else {
+ if (actionIndex != 0) {
+ for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) {
+ if ((actionIndex - 1) == i) {
+ synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1).toAdd();
+ } else {
+ synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0).toAdd();
+ }
+ }
+ } else {
+ for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) {
synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0).toAdd();
}
}
@@ -670,7 +678,7 @@ namespace storm {
}
// Combine synchronizing actions.
- for (auto const& actionIndex : currentModule.getActionIndices()) {
+ for (auto const& actionIndex : currentModule.getSynchronizingActionIndices()) {
if (system.hasSynchronizingAction(actionIndex)) {
system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineSynchronizingActions(generationInfo, system.synchronizingActionToDecisionDiagramMap[actionIndex], nextModule.synchronizingActionToDecisionDiagramMap[actionIndex]);
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables);
diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h
index 0c307983d..a6d45c3fc 100644
--- a/src/builder/DdPrismModelBuilder.h
+++ b/src/builder/DdPrismModelBuilder.h
@@ -173,7 +173,7 @@ namespace storm {
static ActionDecisionDiagram createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command);
- static ActionDecisionDiagram createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, boost::optional<uint_fast64_t> synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset);
+ static ActionDecisionDiagram createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, uint_fast64_t synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset);
static ActionDecisionDiagram combineCommandsToActionDTMC(GenerationInformation& generationInfo, std::vector<ActionDecisionDiagram> const& commandDds);
@@ -185,7 +185,7 @@ namespace storm {
static ModuleDecisionDiagram createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap);
- static storm::dd::Add<Type> getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, boost::optional<uint_fast64_t> const& synchronizationAction = boost::optional<uint_fast64_t>());
+ static storm::dd::Add<Type> getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, uint_fast64_t actionIndex = 0);
static storm::dd::Add<Type> createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module);
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index 65a10a438..18c58a69a 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -499,7 +499,6 @@ namespace storm {
}
// Check that the resulting distribution is in fact a distribution.
- std::cout << probabilitySum << " vs " << comparator.isOne(probabilitySum) << " // " << (probabilitySum - 1) << std::endl;
STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
// Dispose of the temporary maps.
@@ -535,7 +534,6 @@ namespace storm {
}
// A comparator that can be used to check whether we actually have distributions.
- std::cout << "creating comparator.. " << std::endl;
storm::utility::ConstantsComparator<ValueType> comparator;
// Initialize a queue and insert the initial state.
@@ -650,7 +648,17 @@ namespace storm {
if (deterministicModel) {
Choice<ValueType> globalChoice;
- std::unordered_map<IndexType, ValueType> stateToRewardMap;
+ // We need to prepare the entries of those vectors that are going to be used.
+ auto builderIt = rewardModelBuilders.begin();
+ for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
+ if (rewardModelIt->get().hasStateRewards()) {
+ builderIt->stateRewardVector.push_back(storm::utility::zero<ValueType>());
+ }
+
+ if (rewardModelIt->get().hasStateActionRewards()) {
+ builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
+ }
+ }
// Combine all the choices and scale them with the total number of choices of the current state.
for (auto const& choice : allUnlabeledChoices) {
@@ -661,7 +669,6 @@ namespace storm {
auto builderIt = rewardModelBuilders.begin();
for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
if (rewardModelIt->get().hasStateRewards()) {
- builderIt->stateRewardVector.push_back(storm::utility::zero<ValueType>());
for (auto const& stateReward : rewardModelIt->get().getStateRewards()) {
if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
@@ -670,7 +677,6 @@ namespace storm {
}
if (rewardModelIt->get().hasStateActionRewards()) {
- builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
if (!stateActionReward.isLabeled()) {
if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp
index e469e110f..fb0538605 100644
--- a/src/models/symbolic/Model.cpp
+++ b/src/models/symbolic/Model.cpp
@@ -1,5 +1,7 @@
#include "src/models/symbolic/Model.h"
+#include <boost/algorithm/string/join.hpp>
+
#include "src/exceptions/IllegalArgumentException.h"
#include "src/adapters/AddExpressionAdapter.h"
@@ -164,11 +166,47 @@ namespace storm {
template<storm::dd::DdType Type>
void Model<Type>::printModelInformationToStream(std::ostream& out) const {
+ this->printModelInformationHeaderToStream(out);
+ this->printModelInformationFooterToStream(out);
+ }
+
+ template<storm::dd::DdType Type>
+ void Model<Type>::printModelInformationHeaderToStream(std::ostream& out) const {
out << "-------------------------------------------------------------- " << std::endl;
out << "Model type: \t" << this->getType() << " (symbolic)" << std::endl;
out << "States: \t" << this->getNumberOfStates() << " (" << reachableStates.getNodeCount() << " nodes)" << std::endl;
out << "Transitions: \t" << this->getNumberOfTransitions() << " (" << transitionMatrix.getNodeCount() << " nodes)" << std::endl;
-
+ }
+
+ template<storm::dd::DdType Type>
+ void Model<Type>::printModelInformationFooterToStream(std::ostream& out) const {
+ this->printRewardModelsInformationToStream(out);
+ this->printDdVariableInformationToStream(out);
+ out << std::endl;
+ out << "Labels: \t" << this->labelToExpressionMap.size() << std::endl;
+ for (auto const& label : labelToExpressionMap) {
+ out << " * " << label.first << std::endl;
+ }
+ out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl;
+ out << "-------------------------------------------------------------- " << std::endl;
+ }
+
+ template<storm::dd::DdType Type>
+ void Model<Type>::printRewardModelsInformationToStream(std::ostream& out) const {
+ if (this->rewardModels.size()) {
+ std::vector<std::string> rewardModelNames;
+ std::for_each(this->rewardModels.cbegin(), this->rewardModels.cend(),
+ [&rewardModelNames] (typename std::pair<std::string, RewardModelType> const& nameRewardModelPair) {
+ if (nameRewardModelPair.first.empty()) { rewardModelNames.push_back("(default)"); } else { rewardModelNames.push_back(nameRewardModelPair.first); }
+ });
+ out << "Reward Models: " << boost::join(rewardModelNames, ", ") << std::endl;
+ } else {
+ out << "Reward Models: none" << std::endl;
+ }
+ }
+
+ template<storm::dd::DdType Type>
+ void Model<Type>::printDdVariableInformationToStream(std::ostream& out) const {
uint_fast64_t rowVariableCount = 0;
for (auto const& metaVariable : this->rowVariables) {
rowVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
@@ -178,13 +216,7 @@ namespace storm {
columnVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
}
- out << "Variables: \t" << "rows: " << this->rowVariables.size() << " meta variables (" << rowVariableCount << " DD variables)" << ", columns: " << this->columnVariables.size() << " meta variables (" << columnVariableCount << " DD variables)" << std::endl;
- out << "Labels: \t" << this->labelToExpressionMap.size() << std::endl;
- for (auto const& label : labelToExpressionMap) {
- out << " * " << label.first << std::endl;
- }
- out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl;
- out << "-------------------------------------------------------------- " << std::endl;
+ out << "Variables: \t" << "rows: " << this->rowVariables.size() << " meta variables (" << rowVariableCount << " DD variables)" << ", columns: " << this->columnVariables.size() << " meta variables (" << columnVariableCount << " DD variables)";
}
template<storm::dd::DdType Type>
diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h
index 99dd17519..0d7fb70be 100644
--- a/src/models/symbolic/Model.h
+++ b/src/models/symbolic/Model.h
@@ -239,6 +239,35 @@ namespace storm {
*/
std::map<std::string, storm::expressions::Expression> const& getLabelToExpressionMap() const;
+ /*!
+ * Prints the information header (number of states and transitions) of the model to the specified stream.
+ *
+ * @param out The stream the information is to be printed to.
+ */
+ void printModelInformationHeaderToStream(std::ostream& out) const;
+
+ /*!
+ * Prints the information footer (reward models, labels) of the model to the
+ * specified stream.
+ *
+ * @param out The stream the information is to be printed to.
+ */
+ void printModelInformationFooterToStream(std::ostream& out) const;
+
+ /*!
+ * Prints information about the reward models to the specified stream.
+ *
+ * @param out The stream the information is to be printed to.
+ */
+ void printRewardModelsInformationToStream(std::ostream& out) const;
+
+ /*!
+ * Prints information about the DD variables to the specified stream.
+ *
+ * @param out The stream the information is to be printed to.
+ */
+ virtual void printDdVariableInformationToStream(std::ostream& out) const;
+
private:
// The manager responsible for the decision diagrams.
std::shared_ptr<storm::dd::DdManager<Type>> manager;
diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp
index 0125abaa2..1b080ecee 100644
--- a/src/models/symbolic/NondeterministicModel.cpp
+++ b/src/models/symbolic/NondeterministicModel.cpp
@@ -51,34 +51,21 @@ namespace storm {
template<storm::dd::DdType Type>
void NondeterministicModel<Type>::printModelInformationToStream(std::ostream& out) const {
- out << "-------------------------------------------------------------- " << std::endl;
- out << "Model type: \t" << this->getType() << " (symbolic)" << std::endl;
- out << "States: \t" << this->getNumberOfStates() << " (" << this->getReachableStates().getNodeCount() << " nodes)" << std::endl;
- out << "Transitions: \t" << this->getNumberOfTransitions() << " (" << this->getTransitionMatrix().getNodeCount() << " nodes)" << std::endl;
+ this->printModelInformationHeaderToStream(out);
out << "Choices: \t" << this->getNumberOfChoices() << std::endl;
-
- uint_fast64_t rowVariableCount = 0;
- for (auto const& metaVariable : this->getRowVariables()) {
- rowVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
- }
- uint_fast64_t columnVariableCount = 0;
- for (auto const& metaVariable : this->getColumnVariables()) {
- columnVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
- }
+ this->printModelInformationFooterToStream(out);
+ }
+
+ template<storm::dd::DdType Type>
+ void NondeterministicModel<Type>::printDdVariableInformationToStream(std::ostream& out) const {
uint_fast64_t nondeterminismVariableCount = 0;
for (auto const& metaVariable : this->getNondeterminismVariables()) {
nondeterminismVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
}
-
- out << "Variables: \t" << "rows: " << this->getRowVariables().size() << " meta variables (" << rowVariableCount << " DD variables)" << ", columns: " << this->getColumnVariables().size() << "meta variables (" << columnVariableCount << " DD variables), nondeterminism: " << this->getNondeterminismVariables().size() << " meta variables (" << nondeterminismVariableCount << " DD variables)" << std::endl;
- out << "Labels: \t" << this->getLabelToExpressionMap().size() << std::endl;
- for (auto const& label : this->getLabelToExpressionMap()) {
- out << " * " << label.first << std::endl;
- }
- out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl;
- out << "-------------------------------------------------------------- " << std::endl;
+ Model<Type>::printDdVariableInformationToStream(out);
+ out << ", nondeterminism: " << this->getNondeterminismVariables().size() << " meta variables (" << nondeterminismVariableCount << " DD variables)";
}
-
+
// Explicitly instantiate the template class.
template class NondeterministicModel<storm::dd::DdType::CUDD>;
diff --git a/src/models/symbolic/NondeterministicModel.h b/src/models/symbolic/NondeterministicModel.h
index 917c5e58e..dc5194320 100644
--- a/src/models/symbolic/NondeterministicModel.h
+++ b/src/models/symbolic/NondeterministicModel.h
@@ -80,6 +80,10 @@ namespace storm {
virtual void printModelInformationToStream(std::ostream& out) const override;
+ protected:
+
+ virtual void printDdVariableInformationToStream(std::ostream& out) const override;
+
private:
// The meta variables encoding the nondeterminism in the model.
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index adf89142e..47d44269a 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -10,7 +10,7 @@ namespace storm {
// Intentionally left empty.
}
- Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
+ Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), synchronizingActionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
// Initialize the internal mappings for fast information retrieval.
this->createMappings();
}
@@ -71,12 +71,12 @@ namespace storm {
return this->moduleName;
}
- std::set<uint_fast64_t> const& Module::getActionIndices() const {
- return this->actionIndices;
+ std::set<uint_fast64_t> const& Module::getSynchronizingActionIndices() const {
+ return this->synchronizingActionIndices;
}
bool Module::hasActionIndex(uint_fast64_t actionIndex) const {
- return this->actionIndices.find(actionIndex) != this->actionIndices.end();
+ return this->actionIndicesToCommandIndexMap.find(actionIndex) != this->actionIndicesToCommandIndexMap.end();
}
bool Module::isRenamedFromModule() const {
@@ -124,13 +124,17 @@ namespace storm {
this->actionIndicesToCommandIndexMap.emplace(actionIndex, std::set<uint_fast64_t>());
}
this->actionIndicesToCommandIndexMap[actionIndex].insert(i);
- this->actionIndices.insert(actionIndex);
+
+ // Only take the command into the set if it's non-synchronizing.
+ if (actionIndex != 0) {
+ this->synchronizingActionIndices.insert(actionIndex);
+ }
}
}
// For all actions that are "in the module", but for which no command exists, we add the mapping to an empty
// set of commands.
- for (auto const& actionIndex : this->actionIndices) {
+ for (auto const& actionIndex : this->synchronizingActionIndices) {
if (this->actionIndicesToCommandIndexMap.find(actionIndex) == this->actionIndicesToCommandIndexMap.end()) {
this->actionIndicesToCommandIndexMap[actionIndex] = std::set<uint_fast64_t>();
}
diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h
index 48d252576..bb8c3b8d4 100644
--- a/src/storage/prism/Module.h
+++ b/src/storage/prism/Module.h
@@ -141,11 +141,11 @@ namespace storm {
std::string const& getName() const;
/*!
- * Retrieves the set of action indices present in this module.
+ * Retrieves the set of synchronizing action indices present in this module.
*
- * @return the set of action indices present in this module.
+ * @return the set of synchronizing action indices present in this module.
*/
- std::set<uint_fast64_t> const& getActionIndices() const;
+ std::set<uint_fast64_t> const& getSynchronizingActionIndices() const;
/*!
* Retrieves whether or not this module contains a command labeled with the given action index.
@@ -237,7 +237,7 @@ namespace storm {
std::vector<storm::prism::Command> commands;
// The set of action indices present in this module.
- std::set<uint_fast64_t> actionIndices;
+ std::set<uint_fast64_t> synchronizingActionIndices;
// A map of actions to the set of commands labeled with this action.
std::map<uint_fast64_t, std::set<uint_fast64_t>> actionIndicesToCommandIndexMap;
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 1d54b3780..f398e8154 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -403,7 +403,7 @@ namespace storm {
for (unsigned int moduleIndex = 0; moduleIndex < this->getNumberOfModules(); moduleIndex++) {
Module const& module = this->getModule(moduleIndex);
- for (auto const& actionIndex : module.getActionIndices()) {
+ for (auto const& actionIndex : module.getSynchronizingActionIndices()) {
auto const& actionModuleIndicesPair = this->actionIndicesToModuleIndexMap.find(actionIndex);
if (actionModuleIndicesPair == this->actionIndicesToModuleIndexMap.end()) {
this->actionIndicesToModuleIndexMap[actionIndex] = std::set<uint_fast64_t>();
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index eedebbd0f..8e21b2325 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -59,50 +59,6 @@ namespace storm {
return value;
}
- // For floats we specialize this class and consider the comparison modulo some predefined precision.
- template<>
- class ConstantsComparator<float> {
- public:
- ConstantsComparator();
-
- ConstantsComparator(float precision);
-
- bool isOne(float const& value) const;
-
- bool isZero(float const& value) const;
-
- bool isEqual(float const& value1, float const& value2) const;
-
- bool isConstant(float const& value) const;
-
- private:
- // The precision used for comparisons.
- float precision;
- };
-
- // For doubles we specialize this class and consider the comparison modulo some predefined precision.
- template<>
- class ConstantsComparator<double> {
- public:
- ConstantsComparator();
-
- ConstantsComparator(double precision);
-
- bool isOne(double const& value) const;
-
- bool isZero(double const& value) const;
-
- bool isInfinity(double const& value) const;
-
- bool isEqual(double const& value1, double const& value2) const;
-
- bool isConstant(double const& value) const;
-
- private:
- // The precision used for comparisons.
- double precision;
- };
-
#ifdef STORM_HAVE_CARL
template<>
RationalFunction& simplify(RationalFunction& value);
@@ -184,7 +140,6 @@ namespace storm {
}
bool ConstantsComparator<double>::isOne(double const& value) const {
- std::cout << std::setprecision(10) << std::abs(value - one<double>()) << " prec: " << precision << std::endl;
return std::abs(value - one<double>()) <= precision;
}
@@ -279,8 +234,8 @@ namespace storm {
return std::move(matrixEntry);
}
- //explicit instantiations
- //double
+ // explicit instantiations
+ // double
template class ConstantsComparator<double>;
template double one();
@@ -295,7 +250,7 @@ namespace storm {
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
- //float
+ // float
template class ConstantsComparator<float>;
template float one();
@@ -310,7 +265,7 @@ namespace storm {
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry);
- //int
+ // int
template class ConstantsComparator<int>;
template int one();
diff --git a/src/utility/constants.h b/src/utility/constants.h
index 1b64aaef1..c91ea9fdf 100644
--- a/src/utility/constants.h
+++ b/src/utility/constants.h
@@ -30,7 +30,6 @@ namespace storm {
template<typename ValueType>
ValueType infinity();
-
template<typename ValueType>
ValueType pow(ValueType const& value, uint_fast64_t exponent);
@@ -53,6 +52,50 @@ namespace storm {
bool isInfinity(ValueType const& value) const;
};
+ // For floats we specialize this class and consider the comparison modulo some predefined precision.
+ template<>
+ class ConstantsComparator<float> {
+ public:
+ ConstantsComparator();
+
+ ConstantsComparator(float precision);
+
+ bool isOne(float const& value) const;
+
+ bool isZero(float const& value) const;
+
+ bool isEqual(float const& value1, float const& value2) const;
+
+ bool isConstant(float const& value) const;
+
+ private:
+ // The precision used for comparisons.
+ float precision;
+ };
+
+ // For doubles we specialize this class and consider the comparison modulo some predefined precision.
+ template<>
+ class ConstantsComparator<double> {
+ public:
+ ConstantsComparator();
+
+ ConstantsComparator(double precision);
+
+ bool isOne(double const& value) const;
+
+ bool isZero(double const& value) const;
+
+ bool isInfinity(double const& value) const;
+
+ bool isEqual(double const& value1, double const& value2) const;
+
+ bool isConstant(double const& value) const;
+
+ private:
+ // The precision used for comparisons.
+ double precision;
+ };
+
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
diff --git a/src/utility/vector.h b/src/utility/vector.h
index be9cc8f4c..8d4548267 100644
--- a/src/utility/vector.h
+++ b/src/utility/vector.h
@@ -165,6 +165,7 @@ namespace storm {
while (current < next) {
*targetIt += *sourceIt;
++targetIt;
+ ++current;
}
}
}
diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
index b0c7ba3a6..4747e90e1 100644
--- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
@@ -29,6 +29,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
#else
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -111,7 +112,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
#else
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
-
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
index db691e57a..96656c9ba 100644
--- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
@@ -32,6 +32,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -128,6 +129,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -250,6 +252,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("customers");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
index 74dec49a7..b8cbcd701 100644
--- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
@@ -23,6 +23,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coin_flips");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(13ul, model->getNumberOfStates());
@@ -128,6 +129,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(273ul, model->getNumberOfStates());
diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
index 0aee24604..945d4bc6f 100644
--- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
@@ -29,6 +29,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coinflips");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(169ul, model->getNumberOfStates());
@@ -125,6 +126,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(3172ul, model->getNumberOfStates());
diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
index 5c6472a88..adb100e27 100644
--- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
@@ -29,6 +29,7 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) {
#else
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -104,6 +105,7 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) {
#else
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -199,6 +201,7 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) {
#else
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("customers");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
index e22750386..cff5e8d3d 100644
--- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
@@ -31,6 +31,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -119,6 +120,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
@@ -224,6 +226,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("customers");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
index 851810db8..2a0d8cd7b 100644
--- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
@@ -24,6 +24,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coin_flips");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(13ul, model->getNumberOfStates());
@@ -129,6 +130,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(273ul, model->getNumberOfStates());
diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
index 7564037f0..4918451b7 100644
--- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
@@ -27,6 +27,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coinflips");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(169ul, model->getNumberOfStates());
@@ -123,6 +124,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(3172ul, model->getNumberOfStates());
diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
index 0aa11f575..574f1752c 100644
--- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
@@ -22,6 +22,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coin_flips");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(13ul, model->getNumberOfStates());
@@ -127,6 +128,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) {
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
+ options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(273ul, model->getNumberOfStates());