diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 6dc5e312b..ce88522eb 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -1,5 +1,15 @@ #include "src/builder/ExplicitPrismModelBuilder.h" +#include + +#include "src/models/Dtmc.h" +#include "src/models/Ctmc.h" +#include "src/models/Mdp.h" +#include "src/models/Ctmdp.h" + +#include "src/utility/macros.h" +#include "src/exceptions/WrongFormatException.h" + namespace storm { namespace builder { template @@ -21,11 +31,11 @@ namespace storm { uint_fast64_t ExplicitPrismModelBuilder::VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const { auto const& booleanIndex = booleanVariableToIndexMap.find(variable); if (booleanIndex != booleanVariableToIndexMap.end()) { - return booleanVariables[booleanIndex].bitOffset; + return booleanVariables[booleanIndex->second].bitOffset; } auto const& integerIndex = integerVariableToIndexMap.find(variable); if (integerIndex != integerVariableToIndexMap.end()) { - return integerVariables[integerIndex].bitOffset; + return integerVariables[integerIndex->second].bitOffset; } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable."); } @@ -34,7 +44,7 @@ namespace storm { uint_fast64_t ExplicitPrismModelBuilder::VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const { auto const& integerIndex = integerVariableToIndexMap.find(variable); if (integerIndex != integerVariableToIndexMap.end()) { - return integerVariables[integerIndex].bitWidth; + return integerVariables[integerIndex->second].bitWidth; } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable."); } @@ -45,7 +55,7 @@ namespace storm { } template - std::unique_ptr> ExplicitPrismModelBuilder::translateProgram(storm::prism::Program program, bool rewards, std::string const& rewardModelName, std::string const& constantDefinitionString) { + std::unique_ptr> ExplicitPrismModelBuilder::translateProgram(storm::prism::Program program, bool commandLabels, bool rewards, std::string const& rewardModelName, std::string const& constantDefinitionString) { // Start by defining the undefined constants in the model. // First, we need to parse the constant definition string. std::map constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); @@ -70,7 +80,7 @@ namespace storm { } } - ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel); + ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel, commandLabels); std::unique_ptr> result; switch (program.getModelType()) { @@ -87,8 +97,7 @@ namespace storm { result = std::unique_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; default: - LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: cannot handle this model type."); - throw storm::exceptions::WrongFormatException() << "Error while creating model from probabilistic program: cannot handle this model type."; + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model from probabilistic program: cannot handle this model type."); break; } @@ -200,7 +209,7 @@ namespace storm { } template - static std::vector> ExplicitPrismModelBuilder::getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue) { + std::vector> ExplicitPrismModelBuilder::getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator) { std::vector> result; // Iterate over all modules. @@ -219,9 +228,13 @@ namespace storm { continue; } - result.push_back(Choice()); + result.push_back(Choice(0, choiceLabeling)); Choice& choice = result.back(); - choice.addChoiceLabel(command.getGlobalIndex()); + + // Remember the command labels only if we were asked to. + if (choiceLabeling) { + choice.addChoiceLabel(command.getGlobalIndex()); + } // Iterate over all updates of the current command. double probabilitySum = 0; @@ -239,14 +252,15 @@ namespace storm { } // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(std::abs(1 - probabilitySum) < storm::settings::generalSettings().getPrecision(), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); + STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); } } return result; } - static std::vector> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue) { + template + std::vector> ExplicitPrismModelBuilder::getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator) { std::vector> result; for (uint_fast64_t actionIndex : program.getActionIndices()) { @@ -295,14 +309,17 @@ namespace storm { // At this point, we applied all commands of the current command combination and newTargetStates // contains all target states and their respective probabilities. That means we are now ready to // add the choice to the list of transitions. - result.push_back(Choice(actionIndex)); + result.push_back(Choice(actionIndex, choiceLabeling)); // Now create the actual distribution. Choice& choice = result.back(); - // Add the labels of all commands to this choice. - for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { - choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex()); + // Remember the command labels only if we were asked to. + if (choiceLabeling) { + // Add the labels of all commands to this choice. + for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { + choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex()); + } } double probabilitySum = 0; @@ -313,7 +330,7 @@ namespace storm { } // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(std::abs(1 - probabilitySum) <= storm::settings::generalSettings().getPrecision(), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); + 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. delete currentTargetStates; @@ -339,8 +356,16 @@ namespace storm { return result; } - static std::vector> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder) { - std::vector> choiceLabels; + template + boost::optional>> ExplicitPrismModelBuilder::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder) { + // Create choice labels, if requested, + boost::optional>> choiceLabels; + if (commandLabels) { + choiceLabels = std::vector>(); + } + + // A comparator that can be used to check whether we actually have distributions. + storm::utility::ConstantsComparator comparator; // Initialize a queue and insert the initial state. std::queue stateQueue; @@ -365,12 +390,12 @@ namespace storm { // Get the current state and unpack it. storm::storage::BitVector currentState = stateQueue.front(); stateQueue.pop(); - ValueType stateIndex = stateInformation.stateToIndexMap.getValue(currentState); + ValueType stateIndex = stateInformation.stateStorage.getValue(currentState); unpackStateIntoEvaluator(currentState, variableInformation, evaluator); // Retrieve all choices for the current state. - std::vector> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState, evaluator, stateQueue); - std::vector> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState, evaluator, stateQueue); + std::vector> allUnlabeledChoices = getUnlabeledTransitions(program, discreteTimeModel, stateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator); + std::vector> allLabeledChoices = getLabeledTransitions(program, discreteTimeModel, stateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator); uint_fast64_t totalNumberOfChoices = allUnlabeledChoices.size() + allLabeledChoices.size(); @@ -378,24 +403,83 @@ namespace storm { // requested and issue an error otherwise. if (totalNumberOfChoices == 0) { if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) { - // Insert empty choice labeling for added self-loop transitions. - choiceLabels.push_back(boost::container::flat_set()); + if (commandLabels) { + // Insert empty choice labeling for added self-loop transitions. + choiceLabels.get().push_back(boost::container::flat_set()); + } + if (!deterministicModel) { + transitionMatrixBuilder.newRowGroup(currentRow); + transitionRewardMatrixBuilder.newRowGroup(currentRow); + } + transitionMatrixBuilder.addNextValue(currentRow, stateIndex, storm::utility::one()); ++currentRow; } else { - LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); - throw storm::exceptions::WrongFormatException() << "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."; + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); } + } else if (totalNumberOfChoices == 1) { + Choice globalChoice; + + if (!deterministicModel) { + transitionMatrixBuilder.newRowGroup(currentRow); + transitionRewardMatrixBuilder.newRowGroup(currentRow); + } + + std::map stateToRewardMap; + if (!allUnlabeledChoices.empty()) { + globalChoice = allUnlabeledChoices.front(); + for (auto const& stateProbabilityPair : globalChoice) { + // Now add all rewards that match this choice. + for (auto const& transitionReward : transitionRewards) { + if (!transitionReward.isLabeled() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { + stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); + } + } + } + } else { + globalChoice = allLabeledChoices.front(); + + for (auto const& stateProbabilityPair : globalChoice) { + // Now add all rewards that match this choice. + for (auto const& transitionReward : transitionRewards) { + if (transitionReward.isLabeled() && transitionReward.getActionIndex() == globalChoice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { + stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); + } + } + } + } + + if (commandLabels) { + // Now add the resulting distribution as the only choice of the current state. + choiceLabels.get().push_back(globalChoice.getChoiceLabels()); + } + + for (auto const& stateProbabilityPair : globalChoice) { + transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); + } + + // Add all transition rewards to the matrix and add dummy entry if there is none. + if (!stateToRewardMap.empty()) { + for (auto const& stateRewardPair : stateToRewardMap) { + transitionRewardMatrixBuilder.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); + } + } + + ++currentRow; } else { // Then, based on whether the model is deterministic or not, either add the choices individually // or compose them to one choice. if (deterministicModel) { Choice globalChoice; - std::map stateToRewardMap; + + std::map stateToRewardMap; // Combine all the choices and scale them with the total number of choices of the current state. for (auto const& choice : allUnlabeledChoices) { - globalChoice.addChoiceLabels(choice.getChoiceLabels()); + if (commandLabels) { + globalChoice.addChoiceLabels(choice.getChoiceLabels()); + } + for (auto const& stateProbabilityPair : choice) { globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices; @@ -408,13 +492,16 @@ namespace storm { } } for (auto const& choice : allLabeledChoices) { - globalChoice.addChoiceLabels(choice.getChoiceLabels()); + if (commandLabels) { + globalChoice.addChoiceLabels(choice.getChoiceLabels()); + } + for (auto const& stateProbabilityPair : choice) { globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices; // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { - if (transitionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { + if (transitionReward.isLabeled() && transitionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); } } @@ -422,15 +509,17 @@ namespace storm { } - // Now add the resulting distribution as the only choice of the current state. - choiceLabels.push_back(globalChoice.getChoiceLabels()); + if (commandLabels) { + // Now add the resulting distribution as the only choice of the current state. + choiceLabels.get().push_back(globalChoice.getChoiceLabels()); + } for (auto const& stateProbabilityPair : globalChoice) { transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); } // Add all transition rewards to the matrix and add dummy entry if there is none. - if (stateToRewardMap.size() > 0) { + if (!stateToRewardMap.empty()) { for (auto const& stateRewardPair : stateToRewardMap) { transitionRewardMatrixBuilder.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); } @@ -445,7 +534,9 @@ namespace storm { // First, process all unlabeled choices. for (auto const& choice : allUnlabeledChoices) { std::map stateToRewardMap; - choiceLabels.emplace_back(std::move(choice.getChoiceLabels())); + if (commandLabels) { + choiceLabels.get().emplace_back(std::move(choice.getChoiceLabels())); + } for (auto const& stateProbabilityPair : choice) { transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); @@ -472,7 +563,9 @@ namespace storm { // Then, process all labeled choices. for (auto const& choice : allLabeledChoices) { std::map stateToRewardMap; - choiceLabels.emplace_back(std::move(choice.getChoiceLabels())); + if (commandLabels) { + choiceLabels.get().emplace_back(std::move(choice.getChoiceLabels())); + } for (auto const& stateProbabilityPair : choice) { transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); @@ -487,7 +580,7 @@ namespace storm { } // Add all transition rewards to the matrix and add dummy entry if there is none. - if (stateToRewardMap.size() > 0) { + if (!stateToRewardMap.empty()) { for (auto const& stateRewardPair : stateToRewardMap) { transitionRewardMatrixBuilder.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); } @@ -502,7 +595,8 @@ namespace storm { return choiceLabels; } - static ModelComponents buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel) { + template + typename ExplicitPrismModelBuilder::ModelComponents ExplicitPrismModelBuilder::buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel, bool commandLabels) { ModelComponents modelComponents; uint_fast64_t bitOffset = 0; @@ -543,11 +637,12 @@ namespace storm { // Determine whether we have to combine different choices to one or whether this model can have more than // one choice per state. bool deterministicModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC; + bool discreteTimeModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP; // Build the transition and reward matrices. storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); - modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder); + modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, commandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, transitionRewardMatrixBuilder); // Finalize the resulting matrices. modelComponents.transitionMatrix = transitionMatrixBuilder.build(); @@ -562,7 +657,8 @@ namespace storm { return modelComponents; } - static storm::models::AtomicPropositionsLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) { + template + storm::models::AtomicPropositionsLabeling ExplicitPrismModelBuilder::buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) { storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager()); std::vector const& labels = program.getLabels(); @@ -592,7 +688,8 @@ namespace storm { return result; } - static std::vector buildStateRewards(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& rewards, StateInformation const& stateInformation) { + template + std::vector ExplicitPrismModelBuilder::buildStateRewards(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& rewards, StateInformation const& stateInformation) { storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager()); std::vector result(stateInformation.reachableStates.size()); diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index c752224b1..ee35e4108 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -2,7 +2,6 @@ #define STORM_ADAPTERS_EXPLICITPRISMMODELBUILDER_H #include -#include #include #include #include @@ -10,23 +9,18 @@ #include #include #include -#include #include "src/storage/prism/Program.h" #include "src/storage/expressions/SimpleValuation.h" #include "src/storage/expressions/ExprtkExpressionEvaluator.h" #include "src/storage/BitVectorHashMap.h" -#include "src/utility/PrismUtility.h" #include "src/models/AbstractModel.h" -#include "src/models/Dtmc.h" -#include "src/models/Ctmc.h" -#include "src/models/Mdp.h" -#include "src/models/Ctmdp.h" #include "src/models/AtomicPropositionsLabeling.h" #include "src/storage/SparseMatrix.h" #include "src/settings/SettingsManager.h" -#include "src/utility/macros.h" -#include "src/exceptions/WrongFormatException.h" + +#include "src/utility/ConstantsComparator.h" +#include "src/utility/PrismUtility.h" namespace storm { namespace builder { @@ -122,7 +116,7 @@ namespace storm { storm::storage::SparseMatrix transitionRewardMatrix; // A vector that stores a labeling for each choice. - std::vector> choiceLabeling; + boost::optional>> choiceLabeling; }; /*! @@ -135,7 +129,7 @@ namespace storm { * @param rewardModel The reward model that is to be built. * @return The explicit model that was given by the probabilistic program. */ - static std::unique_ptr> translateProgram(storm::prism::Program program, bool rewards = true, std::string const& rewardModelName = "", std::string const& constantDefinitionString = ""); + static std::unique_ptr> translateProgram(storm::prism::Program program, bool commandLabels = false, bool rewards = true, std::string const& rewardModelName = "", std::string const& constantDefinitionString = ""); private: static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExprtkExpressionEvaluator& evaluator); @@ -192,9 +186,9 @@ namespace storm { */ static boost::optional>>> getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExprtkExpressionEvaluator const& evaluator, uint_fast64_t const& actionIndex); - static std::vector> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue); + static std::vector> getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator); - static std::vector> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue); + static std::vector> getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator); /*! * Builds the transition matrix and the transition reward matrix based for the given program. * @@ -211,7 +205,7 @@ namespace storm { * @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin * and a vector containing the labels associated with each choice. */ - static std::vector> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder); + static boost::optional>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder); /*! * Explores the state space of the given program and returns the components of the model as a result. @@ -220,7 +214,7 @@ namespace storm { * @param rewardModel The reward model that is to be considered. * @return A structure containing the components of the resulting model. */ - static ModelComponents buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel); + static ModelComponents buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel, bool commandLabels = false); /*! * Builds the state labeling for the given program. diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 3ce4b1892..66943f399 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -302,6 +302,8 @@ private: bool checkValidityOfProbabilityMatrix() { if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) { // not square + std::cout << "rows: " << this->getTransitionMatrix().getRowCount() << std::endl; + std::cout << "cols: " << this->getTransitionMatrix().getColumnCount() << std::endl; LOG4CPLUS_ERROR(logger, "Probability matrix is not square."); return false; } diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp index 6163b83c9..4f1ab9174 100644 --- a/src/storage/BitVectorHashMap.cpp +++ b/src/storage/BitVectorHashMap.cpp @@ -133,7 +133,7 @@ namespace storm { ValueType BitVectorHashMap::getValue(storm::storage::BitVector const& key) const { std::pair flagBucketPair = this->findBucket(key); STORM_LOG_ASSERT(flagBucketPair.first, "Unknown key."); - return flagBucketPair.second; + return values[flagBucketPair.second]; } template diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 8373d286a..3a9b19906 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -100,7 +100,7 @@ namespace storm { lastRow = row; } - + lastColumn = column; // Finally, set the element and increase the current size. diff --git a/src/utility/PrismUtility.h b/src/utility/PrismUtility.h index b3a78c364..5f5e716d3 100644 --- a/src/utility/PrismUtility.h +++ b/src/utility/PrismUtility.h @@ -1,7 +1,12 @@ #ifndef STORM_UTILITY_PRISMUTILITY #define STORM_UTILITY_PRISMUTILITY +#include +#include + +#include "src/storage/expressions/ExpressionManager.h" #include "src/storage/prism/Program.h" +#include "src/utility/OsDetection.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" @@ -12,10 +17,19 @@ namespace storm { template> struct Choice { public: - Choice(uint_fast64_t actionIndex = 0) : distribution(), actionIndex(actionIndex), choiceLabels() { - // Intentionally left empty. + Choice(uint_fast64_t actionIndex = 0, bool createChoiceLabels = false) : distribution(), actionIndex(actionIndex), choiceLabels(nullptr) { + if (createChoiceLabels) { + choiceLabels = std::shared_ptr>(new boost::container::flat_set()); + } } + Choice(Choice const& other) = default; + Choice& operator=(Choice const& other) = default; +#ifndef WINDOWS + Choice(Choice&& other) = default; + Choice& operator=(Choice&& other) = default; +#endif + /*! * Returns an iterator to the first element of this choice. * @@ -83,7 +97,7 @@ namespace storm { * @param label The label to associate with this choice. */ void addChoiceLabel(uint_fast64_t label) { - choiceLabels.insert(label); + choiceLabels->insert(label); } /*! @@ -103,7 +117,7 @@ namespace storm { * @return The set of labels associated with this choice. */ boost::container::flat_set const& getChoiceLabels() const { - return choiceLabels; + return *choiceLabels; } /*! @@ -159,7 +173,7 @@ namespace storm { uint_fast64_t actionIndex; // The labels that are associated with this choice. - boost::container::flat_set choiceLabels; + std::shared_ptr> choiceLabels; }; static std::map parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) { diff --git a/src/utility/cli.h b/src/utility/cli.h index ce3c16167..2f559277a 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -266,7 +266,7 @@ namespace storm { storm::prism::Program program = storm::parser::PrismParser::parse(programFile); // Then, build the model from the symbolic description. - result = storm::adapters::ExplicitPrismModelBuilder::translateProgram(program, true, settings.isSymbolicRewardModelNameSet() ? settings.getSymbolicRewardModelName() : "", constants); + result = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet(), true, settings.isSymbolicRewardModelNameSet() ? settings.getSymbolicRewardModelName() : "", constants); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); }