main executable compiling again, started to debug

Former-commit-id: f255c48a3d

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<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(program.getActionName(actionIndex));
                         synchronizationMetaVariables.push_back(variablePair.first);
                         allNondeterminismVariables.insert(variablePair.first);
@@ -625,7 +625,7 @@ namespace storm {
         std::pair<storm::dd::Add<Type>, typename DdPrismModelBuilder<Type>::ModuleDecisionDiagram> DdPrismModelBuilder<Type>::createSystemDecisionDiagram(GenerationInformation& generationInfo) {
             // Create the initial offset mapping.
             std::map<uint_fast64_t, uint_fast64_t> 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;
                     }

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<std::reference_wrapper<storm::prism::RewardModel const>> selectedRewardModels;
             for (auto const& rewardModel : preparedProgram.getRewardModels()) {
@@ -401,7 +403,7 @@ namespace storm {
         std::vector<Choice<ValueType>> ExplicitPrismModelBuilder<ValueType, IndexType>::getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) {
             std::vector<Choice<ValueType>> result;
             
-            for (uint_fast64_t actionIndex : program.getActionIndices()) {
+            for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) {
                 boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> 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<CompressedState, ValueType>* newTargetStates = new std::unordered_map<CompressedState, ValueType>();
                         currentTargetStates->emplace(currentState, storm::utility::one<ValueType>());
                         
-                        // 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<ValueType> 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 <typename ValueType, typename IndexType>
-        std::vector<ValueType> ExplicitPrismModelBuilder<ValueType, IndexType>::buildStateRewards(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<storm::prism::StateReward> const& rewards, StateInformation const& stateInformation) {
-            storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager());
-            
-            std::vector<ValueType> result(stateInformation.reachableStates.size());
-            for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
-                result[index] = storm::utility::zero<ValueType>();
-                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<double, uint32_t>;
         

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<ValueType> buildStateRewards(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<storm::prism::StateReward> const& rewards, StateInformation const& stateInformation);
         };
         
     } // namespace adapters

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 {

src/parser/PrismParser.h

@@ -193,7 +193,7 @@ namespace storm {
             qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> integerVariableDefinition;
             
             // Rules for command definitions.
-            qi::rule<Iterator, storm::prism::Command(GlobalProgramInformation&), qi::locals<boost::optional<std::string>, bool>, Skipper> commandDefinition;
+            qi::rule<Iterator, storm::prism::Command(GlobalProgramInformation&), qi::locals<bool>, Skipper> commandDefinition;
             qi::rule<Iterator, std::vector<storm::prism::Update>(GlobalProgramInformation&), Skipper> updateListDefinition;
             qi::rule<Iterator, storm::prism::Update(GlobalProgramInformation&), Skipper> updateDefinition;
             qi::rule<Iterator, std::vector<storm::prism::Assignment>(), Skipper> assignmentDefinitionList;

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<uint_fast64_t> const& Program::getActionIndices() const {
-            return this->actionIndices;
+        std::set<uint_fast64_t> 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<Module> newModules;
             std::vector<Constant> newConstants = this->getConstants();

src/storage/prism/Program.h

@@ -245,11 +245,11 @@ namespace storm {
             std::set<std::string> 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<uint_fast64_t> const& getActionIndices() const;
+            std::set<uint_fast64_t> 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<std::string> actions;
 
-            // The set of actions present in this program.
-            std::set<uint_fast64_t> actionIndices;
+            // The set of synchronizing actions present in this program.
+            std::set<uint_fast64_t> synchronizingActionIndices;
             
             // A map of actions to the set of modules containing commands labelled with this action.
             std::map<uint_fast64_t, std::set<uint_fast64_t>> actionIndicesToModuleIndexMap;

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<KeyType, ValueType, Compare> distribution;