Browse Source

added first debug output to track down bug

Former-commit-id: ad333216c1
tempestpy_adaptions
dehnert 9 years ago
parent
commit
8985ad77cf
  1. 1
      src/builder/DdPrismModelBuilder.cpp
  2. 88
      test/functional/builder/DdPrismModelBuilderTest.cpp

1
src/builder/DdPrismModelBuilder.cpp

@ -620,6 +620,7 @@ namespace storm {
std::pair<storm::dd::Add<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo); std::pair<storm::dd::Add<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo);
storm::dd::Add<Type> transitionMatrix = transitionMatrixModulePair.first; storm::dd::Add<Type> transitionMatrix = transitionMatrixModulePair.first;
transitionMatrix.exportToDot("trans.dot");
ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second; ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second;
// Finally, we build the DDs for a reward structure, if requested. It is important to do this now, because // Finally, we build the DDs for a reward structure, if requested. It is important to do this now, because

88
test/functional/builder/DdPrismModelBuilderTest.cpp

@ -72,50 +72,50 @@ TEST(DdPrismModelBuilderTest, Mdp) {
EXPECT_TRUE(model->getType() == storm::models::ModelType::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>>(); 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"); 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); model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);

Loading…
Cancel
Save