From 73a2491dfb4cb7610b2ef04bc35a9ca93534a30f Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 20 Aug 2015 22:45:19 +0200 Subject: [PATCH] more bugfixes Former-commit-id: 5afecd5a216bfe363a08781eb523babc8b928f74 --- src/builder/DdPrismModelBuilder.cpp | 28 ++++++---- src/builder/DdPrismModelBuilder.h | 4 +- src/builder/ExplicitPrismModelBuilder.cpp | 16 ++++-- src/models/symbolic/Model.cpp | 48 ++++++++++++++--- src/models/symbolic/Model.h | 29 ++++++++++ src/models/symbolic/NondeterministicModel.cpp | 31 ++++------- src/models/symbolic/NondeterministicModel.h | 4 ++ src/storage/prism/Module.cpp | 16 +++--- src/storage/prism/Module.h | 8 +-- src/storage/prism/Program.cpp | 2 +- src/utility/constants.cpp | 53 ++----------------- src/utility/constants.h | 45 +++++++++++++++- src/utility/vector.h | 1 + .../GmmxxCtmcCslModelCheckerTest.cpp | 3 +- .../GmmxxHybridCtmcCslModelCheckerTest.cpp | 3 ++ .../GmmxxHybridDtmcPrctlModelCheckerTest.cpp | 2 + .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 2 + .../NativeCtmcCslModelCheckerTest.cpp | 3 ++ .../NativeHybridCtmcCslModelCheckerTest.cpp | 3 ++ .../NativeHybridDtmcPrctlModelCheckerTest.cpp | 2 + .../NativeHybridMdpPrctlModelCheckerTest.cpp | 2 + .../SymbolicDtmcPrctlModelCheckerTest.cpp | 2 + 22 files changed, 198 insertions(+), 109 deletions(-) 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 - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, boost::optional synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset) { + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, uint_fast64_t synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset) { std::vector 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 typename DdPrismModelBuilder::ModuleDecisionDiagram DdPrismModelBuilder::createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map const& synchronizingActionToOffsetMap) { // Start by creating the action DD for the independent action. - ActionDecisionDiagram independentActionDd = createActionDecisionDiagram(generationInfo, module, boost::optional(), 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 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::Add DdPrismModelBuilder::getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, boost::optional const& synchronizationAction) { + storm::dd::Add DdPrismModelBuilder::getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, uint_fast64_t actionIndex) { storm::dd::Add 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 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 const& commandDds); @@ -185,7 +185,7 @@ namespace storm { static ModuleDecisionDiagram createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map const& synchronizingActionToOffsetMap); - static storm::dd::Add getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, boost::optional const& synchronizationAction = boost::optional()); + static storm::dd::Add getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, uint_fast64_t actionIndex = 0); static storm::dd::Add 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 comparator; // Initialize a queue and insert the initial state. @@ -650,7 +648,17 @@ namespace storm { if (deterministicModel) { Choice globalChoice; - std::unordered_map 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()); + } + + if (rewardModelIt->get().hasStateActionRewards()) { + builderIt->stateActionRewardVector.push_back(storm::utility::zero()); + } + } // 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()); 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()); 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 + #include "src/exceptions/IllegalArgumentException.h" #include "src/adapters/AddExpressionAdapter.h" @@ -164,11 +166,47 @@ namespace storm { template void Model::printModelInformationToStream(std::ostream& out) const { + this->printModelInformationHeaderToStream(out); + this->printModelInformationFooterToStream(out); + } + + template + void Model::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 + void Model::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 + void Model::printRewardModelsInformationToStream(std::ostream& out) const { + if (this->rewardModels.size()) { + std::vector rewardModelNames; + std::for_each(this->rewardModels.cbegin(), this->rewardModels.cend(), + [&rewardModelNames] (typename std::pair 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 + void Model::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 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 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> 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 void NondeterministicModel::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 + void NondeterministicModel::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::printDdVariableInformationToStream(out); + out << ", nondeterminism: " << this->getNondeterminismVariables().size() << " meta variables (" << nondeterminismVariableCount << " DD variables)"; } - + // Explicitly instantiate the template class. template class NondeterministicModel; 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 const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& renamedFromModule, std::map 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 const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& renamedFromModule, std::map 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 const& Module::getActionIndices() const { - return this->actionIndices; + std::set 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()); } 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(); } 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 const& getActionIndices() const; + std::set 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 commands; // The set of action indices present in this module. - std::set actionIndices; + std::set synchronizingActionIndices; // A map of actions to the set of commands labeled with this action. std::map> 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(); 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 { - 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 { - 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::isOne(double const& value) const { - std::cout << std::setprecision(10) << std::abs(value - one()) << " prec: " << precision << std::endl; return std::abs(value - one()) <= precision; } @@ -279,8 +234,8 @@ namespace storm { return std::move(matrixEntry); } - //explicit instantiations - //double + // explicit instantiations + // double template class ConstantsComparator; template double one(); @@ -295,7 +250,7 @@ namespace storm { template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - //float + // float template class ConstantsComparator; template float one(); @@ -310,7 +265,7 @@ namespace storm { template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - //int + // int template class ConstantsComparator; 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 ValueType infinity(); - template 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 { + 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 { + 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 storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& 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::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_repairs"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); @@ -111,7 +112,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { #else typename storm::builder::ExplicitPrismModelBuilder::Options options; #endif - + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("up"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::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::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_repairs"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); @@ -128,6 +129,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("up"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); @@ -250,6 +252,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("customers"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::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::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coin_flips"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(13ul, model->getNumberOfStates()); @@ -128,6 +129,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_rounds"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::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::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coinflips"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(169ul, model->getNumberOfStates()); @@ -125,6 +126,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("rounds"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::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::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_repairs"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); @@ -104,6 +105,7 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) { #else typename storm::builder::ExplicitPrismModelBuilder::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("up"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); @@ -199,6 +201,7 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) { #else typename storm::builder::ExplicitPrismModelBuilder::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("customers"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::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::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_repairs"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); @@ -119,6 +120,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("up"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); @@ -224,6 +226,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("customers"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::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::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coin_flips"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(13ul, model->getNumberOfStates()); @@ -129,6 +130,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_rounds"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::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::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coinflips"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(169ul, model->getNumberOfStates()); @@ -123,6 +124,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("rounds"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::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::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("coin_flips"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(13ul, model->getNumberOfStates()); @@ -127,6 +128,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { #else typename storm::builder::DdPrismModelBuilder::Options options; #endif + options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_rounds"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); EXPECT_EQ(273ul, model->getNumberOfStates());