From 4ca64a913afb7464ef0b2da724254524cc929234 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 19 Aug 2015 16:55:32 +0200 Subject: [PATCH] main executable compiling again, started to debug Former-commit-id: f255c48a3d7fce9ae8ef309cb9279904605d2ae6 --- src/builder/DdPrismModelBuilder.cpp | 6 ++--- src/builder/ExplicitPrismModelBuilder.cpp | 33 +++++++---------------- src/builder/ExplicitPrismModelBuilder.h | 9 ------- src/parser/PrismParser.cpp | 15 ++++++----- src/parser/PrismParser.h | 2 +- src/storage/prism/Program.cpp | 13 +++++---- src/storage/prism/Program.h | 10 +++---- src/utility/prism.h | 4 +++ 8 files changed, 39 insertions(+), 53 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 3c96e5db1..cae09f43c 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -79,7 +79,7 @@ namespace storm { */ void createMetaVariablesAndIdentities() { // Add synchronization variables. - for (auto const& actionIndex : program.getActionIndices()) { + for (auto const& actionIndex : program.getSynchronizingActionIndices()) { std::pair variablePair = manager->addMetaVariable(program.getActionName(actionIndex)); synchronizationMetaVariables.push_back(variablePair.first); allNondeterminismVariables.insert(variablePair.first); @@ -625,7 +625,7 @@ namespace storm { std::pair, typename DdPrismModelBuilder::ModuleDecisionDiagram> DdPrismModelBuilder::createSystemDecisionDiagram(GenerationInformation& generationInfo) { // Create the initial offset mapping. std::map synchronizingActionToOffsetMap; - for (auto const& actionIndex : generationInfo.program.getActionIndices()) { + for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) { synchronizingActionToOffsetMap[actionIndex] = 0; } @@ -639,7 +639,7 @@ namespace storm { STORM_LOG_TRACE("Translating module '" << currentModule.getName() << "'."); // Update the offset index. - for (auto const& actionIndex : generationInfo.program.getActionIndices()) { + for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) { if (system.hasSynchronizingAction(actionIndex)) { synchronizingActionToOffsetMap[actionIndex] = system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables; } diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index b7ee29e5d..406cfeef7 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -210,6 +210,8 @@ namespace storm { // Now that the program is fixed, we we need to substitute all constants with their concrete value. preparedProgram = preparedProgram.substituteConstants(); + std::cout << preparedProgram << std::endl; + // Select the appropriate reward models (after the constants have been substituted). std::vector> selectedRewardModels; for (auto const& rewardModel : preparedProgram.getRewardModels()) { @@ -401,7 +403,7 @@ namespace storm { 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::ExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator) { std::vector> result; - for (uint_fast64_t actionIndex : program.getActionIndices()) { + for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) { boost::optional>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(program, evaluator, actionIndex); // Only process this action label, if there is at least one feasible solution. @@ -421,8 +423,6 @@ namespace storm { std::unordered_map* newTargetStates = new std::unordered_map(); currentTargetStates->emplace(currentState, storm::utility::one()); - // FIXME: This does not check whether a global variable is written multiple times. While the - // behaviour for this is undefined anyway, a warning should be issued in that case. for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { storm::prism::Command const& command = *iteratorList[i]; @@ -563,7 +563,7 @@ namespace storm { transitionMatrixBuilder.newRowGroup(currentRow); } - bool labeledChoice = allUnlabeledChoices.empty() ? false : true; + bool labeledChoice = allUnlabeledChoices.empty() ? true : false; Choice const& globalChoice = labeledChoice ? allLabeledChoices.front() : allUnlabeledChoices.front(); auto builderIt = rewardModelBuilders.begin(); @@ -589,6 +589,10 @@ namespace storm { } } + for (auto const& stateProbabilityPair : globalChoice) { + transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); + } + if (commandLabels) { // Now add the resulting distribution as the only choice of the current state. choiceLabels.get().push_back(globalChoice.getChoiceLabels()); @@ -820,6 +824,8 @@ namespace storm { modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders); + modelComponents.transitionMatrix = transitionMatrixBuilder.build(); + // Now finalize all reward models. auto builderIt = rewardModelBuilders.begin(); for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { @@ -863,25 +869,6 @@ namespace storm { return result; } - template - std::vector ExplicitPrismModelBuilder::buildStateRewards(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& rewards, StateInformation const& stateInformation) { - storm::expressions::ExpressionEvaluator evaluator(program.getManager()); - - std::vector result(stateInformation.reachableStates.size()); - for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { - result[index] = storm::utility::zero(); - unpackStateIntoEvaluator(stateInformation.reachableStates[index], variableInformation, evaluator); - for (auto const& reward : rewards) { - - // Add this reward to the state if the state is included in the state reward. - if (evaluator.asBool(reward.getStatePredicateExpression())) { - result[index] += ValueType(evaluator.asRational(reward.getRewardValueExpression())); - } - } - } - return result; - } - // Explicitly instantiate the class. template class ExplicitPrismModelBuilder; diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index 8e4cd5e3a..c9fbac4c6 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -277,15 +277,6 @@ namespace storm { * @return The state labeling of the given program. */ static storm::models::sparse::StateLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation); - - /*! - * Builds the state rewards for the given state space. - * - * @param rewards A vector of state rewards to consider. - * @param stateInformation Information about the state space. - * @return A vector containing the state rewards for the state space. - */ - static std::vector buildStateRewards(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& rewards, StateInformation const& stateInformation); }; } // namespace adapters diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 78cc69a1a..3bc58ab88 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -34,6 +34,7 @@ namespace storm { PositionIteratorType first(input.begin()); PositionIteratorType iter = first; PositionIteratorType last(input.end()); + assert(first != last); // Create empty result; storm::prism::Program result; @@ -147,11 +148,11 @@ namespace storm { updateListDefinition.name("update list"); // This is a dummy command-definition (it ignores the actual contents of the command) that is overwritten when the parser is moved to the second run. - commandDefinition = (((qi::lit("[") > (-identifier)[qi::_a = qi::_1] > qi::lit("]")) + commandDefinition = (((qi::lit("[") > -identifier > qi::lit("]")) | - (qi::lit("<") > (-identifier)[qi::_a = qi::_1] > qi::lit(">")[qi::_b = true])) + (qi::lit("<") > -identifier > qi::lit(">")[qi::_a = true])) > +(qi::char_ - qi::lit(";")) - > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_r1)]; + > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_1, qi::_r1)]; commandDefinition.name("command definition"); moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > *commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)]; @@ -203,13 +204,13 @@ namespace storm { void PrismParser::moveToSecondRun() { // In the second run, we actually need to parse the commands instead of just skipping them, // so we adapt the rule for parsing commands. - commandDefinition = (((qi::lit("[") > (-identifier)[qi::_a = qi::_1] > qi::lit("]")) + commandDefinition = (((qi::lit("[") > -identifier > qi::lit("]")) | - (qi::lit("<") > (-identifier)[qi::_a = qi::_1] > qi::lit(">")[qi::_b = true])) + (qi::lit("<") > -identifier > qi::lit(">")[qi::_a = true])) > expressionParser > qi::lit("->") > updateListDefinition(qi::_r1) - > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_b, qi::_a, qi::_2, qi::_3, qi::_r1)]; + > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_1, qi::_2, qi::_3, qi::_r1)]; this->secondRun = true; this->expressionParser.setIdentifierMapping(&this->identifiers_); @@ -371,7 +372,7 @@ namespace storm { auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName); STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << realActionName << "'."); - return storm::prism::TransitionReward(nameIndexPair->second, actionName.get(), sourceStatePredicateExpression, targetStatePredicateExpression, rewardValueExpression, this->getFilename()); + return storm::prism::TransitionReward(nameIndexPair->second, realActionName, sourceStatePredicateExpression, targetStatePredicateExpression, rewardValueExpression, this->getFilename()); } storm::prism::Assignment PrismParser::createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const { diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index fb017734c..428b728f0 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -193,7 +193,7 @@ namespace storm { qi::rule, Skipper> integerVariableDefinition; // Rules for command definitions. - qi::rule, bool>, Skipper> commandDefinition; + qi::rule, Skipper> commandDefinition; qi::rule(GlobalProgramInformation&), Skipper> updateListDefinition; qi::rule updateDefinition; qi::rule(), Skipper> assignmentDefinitionList; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 31e5f1f71..1d54b3780 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -21,7 +21,7 @@ namespace storm { formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(), - actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() + synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() { // Start by creating the necessary mappings from the given ones. @@ -260,8 +260,8 @@ namespace storm { return this->actions; } - std::set const& Program::getActionIndices() const { - return this->actionIndices; + std::set const& Program::getSynchronizingActionIndices() const { + return this->synchronizingActionIndices; } std::string const& Program::getActionName(uint_fast64_t actionIndex) const { @@ -391,8 +391,12 @@ namespace storm { for (auto const& actionIndexPair : this->getActionNameToIndexMapping()) { this->actions.insert(actionIndexPair.first); - this->actionIndices.insert(actionIndexPair.second); this->indexToActionMap.emplace(actionIndexPair.second, actionIndexPair.first); + + // Only let all non-zero indices be synchronizing. + if (actionIndexPair.second != 0) { + this->synchronizingActionIndices.insert(actionIndexPair.second); + } } // Build the mapping from action names to module indices so that the lookup can later be performed quickly. @@ -794,7 +798,6 @@ namespace storm { } } - Program Program::simplify() { std::vector newModules; std::vector newConstants = this->getConstants(); diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 3d0d745b7..eea245684 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -245,11 +245,11 @@ namespace storm { std::set const& getActions() const; /*! - * Retrieves the set of action indices present in the program. + * Retrieves the set of synchronizing action indices present in the program. * - * @return The set of action indices present in the program. + * @return The set of synchronizing action indices present in the program. */ - std::set const& getActionIndices() const; + std::set const& getSynchronizingActionIndices() const; /*! * Retrieves the action name of the given action index. @@ -489,8 +489,8 @@ namespace storm { // The set of actions present in this program. std::set actions; - // The set of actions present in this program. - std::set actionIndices; + // The set of synchronizing actions present in this program. + std::set synchronizingActionIndices; // A map of actions to the set of modules containing commands labelled with this action. std::map> actionIndicesToModuleIndexMap; diff --git a/src/utility/prism.h b/src/utility/prism.h index c1c13347d..c3399a240 100644 --- a/src/utility/prism.h +++ b/src/utility/prism.h @@ -173,6 +173,10 @@ namespace storm { distribution[state] += value; } + std::size_t size() const { + return distribution.size(); + } + private: // The distribution that is associated with the choice. std::map distribution;