From 8985ad77cfd7ad83007897466d672a8bfea4ae82 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 7 Aug 2015 14:16:45 +0200
Subject: [PATCH 1/6] added first debug output to track down bug
Former-commit-id: ad333216c1bd16837a6c4de5c253637bbeb481c4
---
src/builder/DdPrismModelBuilder.cpp | 1 +
.../builder/DdPrismModelBuilderTest.cpp | 88 +++++++++----------
2 files changed, 45 insertions(+), 44 deletions(-)
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index eae18d06e..07a5f1100 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -620,6 +620,7 @@ namespace storm {
std::pair<storm::dd::Add<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo);
storm::dd::Add<Type> transitionMatrix = transitionMatrixModulePair.first;
+ transitionMatrix.exportToDot("trans.dot");
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/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp
index ea88d24f1..15f5b03ce 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);
From b2cec6395a21352b10269ebeef3bfeea293b613e Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 7 Aug 2015 14:34:17 +0200
Subject: [PATCH 2/6] more debug output
Former-commit-id: ff8f9b5a81717d597e1b423f82d7f77b22af84eb
---
src/builder/DdPrismModelBuilder.cpp | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 07a5f1100..69aea3119 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -621,6 +621,8 @@ 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 << "nnz: " << transitionMatrix.getNonZeroCount() << std::endl;
+ std::cout << "node: " << transitionMatrix.getNodeCount() << 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
@@ -651,6 +653,9 @@ namespace storm {
transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables);
}
storm::dd::Bdd<Type> reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrixBdd);
+ reachableStates.exportToDot("reach.dot");
+ std::cout << "reach nnz: " << reachableStates.getNonZeroCount() << std::endl;
+ std::cout << "reach node: " << reachableStates.getNodeCount() << std::endl;
storm::dd::Add<Type> reachableStatesAdd = reachableStates.toAdd();
transitionMatrix *= reachableStatesAdd;
if (stateAndTransitionRewards) {
From 507331d8a92fbf3dc8e45bf16a8013347cbb9bbd Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 7 Aug 2015 14:47:56 +0200
Subject: [PATCH 3/6] more debug output
Former-commit-id: acb7f9ea2f17ee903b05436aa3088640d92feb2a
---
src/builder/DdPrismModelBuilder.cpp | 4 +---
src/storage/dd/CuddAdd.cpp | 8 +++++++-
2 files changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 69aea3119..2d94be7cc 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -623,6 +623,7 @@ namespace storm {
transitionMatrix.exportToDot("trans.dot");
std::cout << "nnz: " << transitionMatrix.getNonZeroCount() << std::endl;
std::cout << "node: " << transitionMatrix.getNodeCount() << std::endl;
+ 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
@@ -653,9 +654,6 @@ namespace storm {
transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables);
}
storm::dd::Bdd<Type> reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrixBdd);
- reachableStates.exportToDot("reach.dot");
- std::cout << "reach nnz: " << reachableStates.getNonZeroCount() << std::endl;
- std::cout << "reach node: " << reachableStates.getNodeCount() << std::endl;
storm::dd::Add<Type> reachableStatesAdd = reachableStates.toAdd();
transitionMatrix *= reachableStatesAdd;
if (stateAndTransitionRewards) {
diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp
index 5eaded696..dbee2e94a 100644
--- a/src/storage/dd/CuddAdd.cpp
+++ b/src/storage/dd/CuddAdd.cpp
@@ -1,5 +1,6 @@
#include <cstring>
#include <algorithm>
+#include <boost/algorithm/string/join.hpp>
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"
@@ -1055,7 +1056,12 @@ namespace storm {
}
std::ostream& operator<<(std::ostream& out, const Add<DdType::CUDD>& add) {
- add.exportToDot();
+ out << "ADD with " << add.getNonZeroCount() << " nnz, " << add.getNodeCount() << " nodes, " << add.getLeafCount() << " leaves" << std::endl;
+ std::vector<std::string> variableNames;
+ for (auto const& variable : add.getContainedMetaVariables()) {
+ variableNames.push_back(variable.getName());
+ }
+ out << "contained variables: " << boost::algorithm::join(variableNames, ", ") << std::endl;
return out;
}
From 08747378d5b64e7e650eb9eacb434307f6e28de0 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 7 Aug 2015 15:00:01 +0200
Subject: [PATCH 4/6] workplace switch
Former-commit-id: eab2c2bc9e49aa4392294107528e9e398f074130
---
src/builder/DdPrismModelBuilder.cpp | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 2d94be7cc..13a6cb985 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -613,6 +613,7 @@ 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 +622,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 << "nnz: " << transitionMatrix.getNonZeroCount() << std::endl;
- std::cout << "node: " << transitionMatrix.getNodeCount() << std::endl;
std::cout << "trans: " << transitionMatrix << std::endl;
ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second;
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 5/6] 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);
From 21627fbab439aa79535f62e012624f7f466c3b13 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 10 Aug 2015 00:23:47 +0200
Subject: [PATCH 6/6] Started to get rid of some warnings. In particular this
means making the compiler more silent for third-party stuff.
Former-commit-id: 2b6ca07d06186e7c90644fbc9d4ec4d0d09aff31
---
CMakeLists.txt | 9 ++++++---
resources/3rdparty/cudd-2.5.0/CMakeLists.txt | 6 +++++-
resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc | 8 ++++----
resources/3rdparty/glpk-4.53/CMakeLists.txt | 2 +-
.../prctl/SparseMdpPrctlModelChecker.cpp | 1 -
.../SparseDtmcEliminationModelChecker.cpp | 14 --------------
src/parser/AutoParser.cpp | 2 +-
7 files changed, 17 insertions(+), 25 deletions(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index a1b8c29b3..c0179e39d 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -114,8 +114,10 @@ if(CMAKE_COMPILER_IS_GNUCC)
set(STORM_COMPILED_BY "GCC")
# Set standard flags for GCC
set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
+ set(CMAKE_C_FLAGS_RELEASE "${CMAKE_C_FLAGS_RELEASE} -funroll-loops")
add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE)
- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic")
+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic -Wno-deprecated-declarations")
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic -Wno-deprecated-declarations")
# Turn on popcnt instruction if desired (yes by default)
if (STORM_USE_POPCNT)
@@ -123,7 +125,7 @@ if(CMAKE_COMPILER_IS_GNUCC)
endif(STORM_USE_POPCNT)
# Set the no-strict-aliasing target for GCC
- set_source_files_properties(${CONVERSIONHELPER_TARGET} PROPERTIES COMPILE_FLAGS " -fno-strict-aliasing ")
+ set_source_files_properties(${CONVERSIONHELPER_TARGET} PROPERTIES COMPILE_FLAGS " -fno-strict-aliasing")
elseif(MSVC)
set(STORM_COMPILED_BY "MSVC")
# required for GMM to compile, ugly error directive in their code
@@ -146,7 +148,7 @@ else(CLANG)
# As CLANG is not set as a variable, we need to set it in case we have not matched another compiler.
set (CLANG ON)
# Set standard flags for clang
- set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O3")
+ set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4")
if(UNIX AND NOT APPLE AND NOT USE_LIBCXX)
set(CLANG_STDLIB libstdc++)
message(STATUS "StoRM - Linking against libstdc++")
@@ -162,6 +164,7 @@ else(CLANG)
add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-unused-variable -ftemplate-depth=1024")
+ set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic")
# Turn on popcnt instruction if desired (yes by default)
if (STORM_USE_POPCNT)
diff --git a/resources/3rdparty/cudd-2.5.0/CMakeLists.txt b/resources/3rdparty/cudd-2.5.0/CMakeLists.txt
index 4d08513de..c9f821a21 100644
--- a/resources/3rdparty/cudd-2.5.0/CMakeLists.txt
+++ b/resources/3rdparty/cudd-2.5.0/CMakeLists.txt
@@ -20,9 +20,13 @@ include_directories("${PROJECT_SOURCE_DIR}/src/nanotrav")
include_directories("${PROJECT_SOURCE_DIR}/src/st")
include_directories("${PROJECT_SOURCE_DIR}/src/util")
-if(MSVC)
+if(CMAKE_COMPILER_IS_GNUCC)
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-function")
+elseif(MSVC)
# required for GMM to compile, ugly error directive in their code
add_definitions(/D_SCL_SECURE_NO_DEPRECATE /D_CRT_SECURE_NO_WARNINGS)
+else(CLANG)
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-function")
endif()
# Since we do not target Alphas, this symbol is always set
diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc
index 3262108aa..b8f7d3983 100644
--- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc
+++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc
@@ -2815,7 +2815,7 @@ Cudd::Walsh(
size_t n = x.size();
DdNode **X = new DdNode *[n];
DdNode **Y = new DdNode *[n];
- for (int i = 0; i < n; i++) {
+ for (size_t i = 0; i < n; i++) {
X[i] = x[i].getNode();
Y[i] = y[i].getNode();
}
@@ -3612,7 +3612,7 @@ ADD::SwapVariables(
DdManager *mgr = p->manager;
DdNode **X = new DdNode *[n];
DdNode **Y = new DdNode *[n];
- for (int i = 0; i < n; i++) {
+ for (size_t i = 0; i < n; i++) {
X[i] = x[i].node;
Y[i] = y[i].node;
}
@@ -3646,7 +3646,7 @@ BDD::SwapVariables(
DdManager *mgr = p->manager;
DdNode **X = new DdNode *[n];
DdNode **Y = new DdNode *[n];
- for (int i = 0; i < n; i++) {
+ for (size_t i = 0; i < n; i++) {
X[i] = x[i].node;
Y[i] = y[i].node;
}
@@ -3666,7 +3666,7 @@ BDD::AdjPermuteX(
size_t n = x.size();
DdManager *mgr = p->manager;
DdNode **X = new DdNode *[n];
- for (int i = 0; i < n; i++) {
+ for (size_t i = 0; i < n; i++) {
X[i] = x[i].node;
}
DdNode *result = Cudd_bddAdjPermuteX(mgr, node, X, static_cast<int>(n));
diff --git a/resources/3rdparty/glpk-4.53/CMakeLists.txt b/resources/3rdparty/glpk-4.53/CMakeLists.txt
index b09ec9e1c..24ee34121 100644
--- a/resources/3rdparty/glpk-4.53/CMakeLists.txt
+++ b/resources/3rdparty/glpk-4.53/CMakeLists.txt
@@ -53,7 +53,7 @@ message(STATUS "GLPK - CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}")
if(CMAKE_COMPILER_IS_GNUCC)
message(STATUS "GLPK - Using Compiler Configuration: GCC")
# Set standard flags for GCC
- set(CMAKE_C_FLAGS "${CMAKE_CXX_FLAGS} -Wno-return-type")
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-return-type -Wno-parentheses -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-value -Wno-unused-function -Wno-address -Wno-unused-label")
add_definitions(-DHAVE_CONFIG_H=1)
elseif(MSVC)
message(STATUS "GLPK - Using Compiler Configuration: MSVC")
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
index 518d21972..adf65d728 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@@ -343,7 +343,6 @@ namespace storm {
// Get some data members for convenience.
typename storm::storage::SparseMatrix<ValueType> const& transitionMatrix = this->getModel().getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
- ValueType one = storm::utility::one<ValueType>();
ValueType zero = storm::utility::zero<ValueType>();
//first calculate LRA for the Maximal End Components.
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index e4087ad52..498370e02 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -692,23 +692,10 @@ namespace storm {
return maximalDepth;
}
- namespace {
- static int chunkCounter = 0;
- static int counter = 0;
- }
-
template<typename ValueType>
void SparseDtmcEliminationModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) {
auto eliminationStart = std::chrono::high_resolution_clock::now();
- ++counter;
- STORM_LOG_TRACE("Eliminating state " << state << ".");
- if (counter > matrix.getNumberOfRows() / 10) {
- ++chunkCounter;
- STORM_LOG_INFO("Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl);
- counter = 0;
- }
-
bool hasSelfLoop = false;
ValueType loopProbability = storm::utility::zero<ValueType>();
@@ -752,7 +739,6 @@ namespace storm {
// Now connect the predecessors of the state being eliminated with its successors.
typename FlexibleSparseMatrix::row_type& currentStatePredecessors = backwardTransitions.getRow(state);
- std::size_t numberOfPredecessors = currentStatePredecessors.size();
std::size_t predecessorForwardTransitionCount = 0;
// In case we have a constrained elimination, we need to keep track of the new predecessors.
diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp
index 23764fd61..065ad4327 100644
--- a/src/parser/AutoParser.cpp
+++ b/src/parser/AutoParser.cpp
@@ -69,7 +69,7 @@ namespace storm {
#ifdef WINDOWS
sscanf_s(filehintBuffer, formatString.c_str(), hint, STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1);
#else
- int ret = sscanf(filehintBuffer, formatString.c_str(), hint);
+ sscanf(filehintBuffer, formatString.c_str(), hint);
#endif
for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);