From c683934ea0f10088bc65343ef79ccbd2e224b6db Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 7 Aug 2015 19:53:58 +0200
Subject: [PATCH] removed debug output and fixed bug

Former-commit-id: 0c33f61bbea9dfe743c213ff0eecdad1eb3008d1
---
 src/builder/DdPrismModelBuilder.cpp           |  3 -
 src/parser/PrismParser.cpp                    |  9 +-
 src/storage/prism/Program.cpp                 |  4 +-
 .../builder/DdPrismModelBuilderTest.cpp       | 88 +++++++++----------
 4 files changed, 53 insertions(+), 51 deletions(-)

diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 13a6cb985..eae18d06e 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -613,7 +613,6 @@ namespace storm {
             }
             
             preparedProgram = preparedProgram.substituteConstants();
-            std::cout << "translating: " << preparedProgram << std::endl;
             
             // Start by initializing the structure used for storing all information needed during the model generation.
             // In particular, this creates the meta variables used to encode the model.
@@ -621,8 +620,6 @@ namespace storm {
 
             std::pair<storm::dd::Add<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo);
             storm::dd::Add<Type> transitionMatrix = transitionMatrixModulePair.first;
-            transitionMatrix.exportToDot("trans.dot");
-            std::cout << "trans: " << transitionMatrix << std::endl;
             ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second;
             
             // Finally, we build the DDs for a reward structure, if requested. It is important to do this now, because
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index bff8c71b8..ddb348249 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -378,7 +378,8 @@ namespace storm {
             if (!actionName.empty()) {
                 auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName);
                 if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
-                    globalProgramInformation.actionIndices[actionName] = globalProgramInformation.actionIndices.size();
+                    std::size_t nextIndex = globalProgramInformation.actionIndices.size();
+                    globalProgramInformation.actionIndices[actionName] = nextIndex;
                 }
             }
             
@@ -392,7 +393,8 @@ namespace storm {
                 // Register the action name if it has not appeared earlier.
                 auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName);
                 if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
-                    globalProgramInformation.actionIndices[actionName] = globalProgramInformation.actionIndices.size();
+                    std::size_t nextIndex = globalProgramInformation.actionIndices.size();
+                    globalProgramInformation.actionIndices[actionName] = nextIndex;
                 }
             }
             
@@ -518,7 +520,8 @@ namespace storm {
                     if (!newActionName.empty()) {
                         auto const& nameIndexPair = globalProgramInformation.actionIndices.find(newActionName);
                         if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
-                            globalProgramInformation.actionIndices[newActionName] = globalProgramInformation.actionIndices.size();
+                            std::size_t nextIndex = globalProgramInformation.actionIndices.size();
+                            globalProgramInformation.actionIndices[newActionName] = nextIndex;
                         }
                     }
                     
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 0b61fd795..4655f1bcc 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -13,8 +13,10 @@
 namespace storm {
     namespace prism {
         Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), manager(manager), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(), actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() {
+
+            // Start by creating the necessary mappings from the given ones.
             this->createMappings();
-            
+
             // Create a new initial construct if the corresponding flag was set.
             if (fixInitialConstruct) {
                 storm::expressions::Expression newInitialExpression = manager->boolean(true);
diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp
index 15f5b03ce..db6adc88f 100644
--- a/test/functional/builder/DdPrismModelBuilderTest.cpp
+++ b/test/functional/builder/DdPrismModelBuilderTest.cpp
@@ -72,50 +72,50 @@ TEST(DdPrismModelBuilderTest, Mdp) {
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
-//
-//    EXPECT_EQ(169, mdp->getNumberOfStates());
-//    EXPECT_EQ(436, mdp->getNumberOfTransitions());
-//    EXPECT_EQ(254, mdp->getNumberOfChoices());
-//    
-//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
-//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
-//
-//    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
-//    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
-//    
-//    EXPECT_EQ(364, mdp->getNumberOfStates());
-//    EXPECT_EQ(654, mdp->getNumberOfTransitions());
-//    EXPECT_EQ(573, mdp->getNumberOfChoices());
-//
-//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
-//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
-//    
-//    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
-//    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
-//    
-//    EXPECT_EQ(272, mdp->getNumberOfStates());
-//    EXPECT_EQ(492, mdp->getNumberOfTransitions());
-//    EXPECT_EQ(400, mdp->getNumberOfChoices());
-//    
-//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
-//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
-//    
-//    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
-//    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
-//    
-//    EXPECT_EQ(1038, mdp->getNumberOfStates());
-//    EXPECT_EQ(1282, mdp->getNumberOfTransitions());
-//    EXPECT_EQ(1054, mdp->getNumberOfChoices());
-//    
-//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
-//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
-//    
-//    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
-//    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
-//    
-//    EXPECT_EQ(4093, mdp->getNumberOfStates());
-//    EXPECT_EQ(5585, mdp->getNumberOfTransitions());
-//    EXPECT_EQ(5519, mdp->getNumberOfChoices());
+
+    EXPECT_EQ(169, mdp->getNumberOfStates());
+    EXPECT_EQ(436, mdp->getNumberOfTransitions());
+    EXPECT_EQ(254, mdp->getNumberOfChoices());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+
+    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
+    
+    EXPECT_EQ(364, mdp->getNumberOfStates());
+    EXPECT_EQ(654, mdp->getNumberOfTransitions());
+    EXPECT_EQ(573, mdp->getNumberOfChoices());
+
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+    
+    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
+    
+    EXPECT_EQ(272, mdp->getNumberOfStates());
+    EXPECT_EQ(492, mdp->getNumberOfTransitions());
+    EXPECT_EQ(400, mdp->getNumberOfChoices());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+    
+    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
+    
+    EXPECT_EQ(1038, mdp->getNumberOfStates());
+    EXPECT_EQ(1282, mdp->getNumberOfTransitions());
+    EXPECT_EQ(1054, mdp->getNumberOfChoices());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+    
+    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
+    
+    EXPECT_EQ(4093, mdp->getNumberOfStates());
+    EXPECT_EQ(5585, mdp->getNumberOfTransitions());
+    EXPECT_EQ(5519, mdp->getNumberOfChoices());
 
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);