From a4ef3cf778bb2c06bc8c0ffdf2afd09392cc9d28 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 2 Jun 2016 16:55:41 +0200
Subject: [PATCH] added CTMC tests for JANI model builder

Former-commit-id: 783646bbed31e31e3ad970c154089564b0eb44a1
---
 .../builder/DdJaniModelBuilderTest.cpp        | 140 +++++++++++-------
 .../builder/DdPrismModelBuilderTest.cpp       |  15 --
 2 files changed, 83 insertions(+), 72 deletions(-)

diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp
index 1fe2d7e47..9d05bae3c 100644
--- a/test/functional/builder/DdJaniModelBuilderTest.cpp
+++ b/test/functional/builder/DdJaniModelBuilderTest.cpp
@@ -11,56 +11,45 @@
 #include "src/parser/PrismParser.h"
 #include "src/builder/DdJaniModelBuilder.h"
 
+#include "src/settings/SettingMemento.h"
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/IOSettings.h"
+
 TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
     storm::jani::Model janiModel = program.toJani(true);
     
     storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
-    auto t1 = std::chrono::high_resolution_clock::now();
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.translate();
-    auto t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "die: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(13ul, model->getNumberOfStates());
     EXPECT_EQ(20ul, model->getNumberOfTransitions());
     
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
     janiModel = program.toJani(true);
     builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    t1 = std::chrono::high_resolution_clock::now();
     model = builder.translate();
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "brp: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(677ul, model->getNumberOfStates());
     EXPECT_EQ(867ul, model->getNumberOfTransitions());
         
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
     janiModel = program.toJani(true);
     builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    t1 = std::chrono::high_resolution_clock::now();
     model = builder.translate();
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "crowds: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(8607ul, model->getNumberOfStates());
     EXPECT_EQ(15113ul, model->getNumberOfTransitions());
     
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
     janiModel = program.toJani(true);
     builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    t1 = std::chrono::high_resolution_clock::now();
     model = builder.translate();
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "lead: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(273ul, model->getNumberOfStates());
     EXPECT_EQ(397ul, model->getNumberOfTransitions());
     
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
     janiModel = program.toJani(true);
     
-    t1 = std::chrono::high_resolution_clock::now();
     builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
     model = builder.translate();
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "nand: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(1728ul, model->getNumberOfStates());
     EXPECT_EQ(2505ul, model->getNumberOfTransitions());
 }
@@ -70,78 +59,115 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
     storm::jani::Model janiModel = program.toJani(true);
     
     storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
-    auto t1 = std::chrono::high_resolution_clock::now();
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.translate();
-    auto t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "die: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(13ul, model->getNumberOfStates());
     EXPECT_EQ(20ul, model->getNumberOfTransitions());
     
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
     janiModel = program.toJani(true);
     builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    t1 = std::chrono::high_resolution_clock::now();
     model = builder.translate();
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "brp: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(677ul, model->getNumberOfStates());
     EXPECT_EQ(867ul, model->getNumberOfTransitions());
     
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
     janiModel = program.toJani(true);
     builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    t1 = std::chrono::high_resolution_clock::now();
     model = builder.translate();
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "crowds: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(8607ul, model->getNumberOfStates());
     EXPECT_EQ(15113ul, model->getNumberOfTransitions());
     
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
     janiModel = program.toJani(true);
     builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    t1 = std::chrono::high_resolution_clock::now();
     model = builder.translate();
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "lead: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(273ul, model->getNumberOfStates());
     EXPECT_EQ(397ul, model->getNumberOfTransitions());
     
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
     janiModel = program.toJani(true);
     builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    t1 = std::chrono::high_resolution_clock::now();
     model = builder.translate();
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "nand: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(1728ul, model->getNumberOfStates());
     EXPECT_EQ(2505ul, model->getNumberOfTransitions());
 }
 
-//TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
-//    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
-//    
-//    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
-//    EXPECT_EQ(13ul, model->getNumberOfStates());
-//    EXPECT_EQ(20ul, model->getNumberOfTransitions());
-//    
-//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
-//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
-//    EXPECT_EQ(677ul, model->getNumberOfStates());
-//    EXPECT_EQ(867ul, model->getNumberOfTransitions());
-//    
-//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
-//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
-//    EXPECT_EQ(8607ul, model->getNumberOfStates());
-//    EXPECT_EQ(15113ul, model->getNumberOfTransitions());
-//    
-//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
-//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
-//    EXPECT_EQ(273ul, model->getNumberOfStates());
-//    EXPECT_EQ(397ul, model->getNumberOfTransitions());
-//    
-//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
-//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
-//    EXPECT_EQ(1728ul, model->getNumberOfStates());
-//    EXPECT_EQ(2505ul, model->getNumberOfTransitions());
-//}
\ No newline at end of file
+TEST(DdJaniModelBuilderTest_Sylvan, Ctmc) {
+    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
+    
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
+    storm::jani::Model janiModel = program.toJani(true);
+    storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.translate();
+    EXPECT_EQ(276ul, model->getNumberOfStates());
+    EXPECT_EQ(1120ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
+    janiModel = program.toJani(true);
+    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
+    model = builder.translate();
+    EXPECT_EQ(3478ul, model->getNumberOfStates());
+    EXPECT_EQ(14639ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
+    janiModel = program.toJani(true);
+    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
+    model = builder.translate();
+    EXPECT_EQ(12ul, model->getNumberOfStates());
+    EXPECT_EQ(22ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
+    janiModel = program.toJani(true);
+    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
+    model = builder.translate();
+    EXPECT_EQ(810ul, model->getNumberOfStates());
+    EXPECT_EQ(3699ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
+    janiModel = program.toJani(true);
+    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
+    model = builder.translate();
+    EXPECT_EQ(66ul, model->getNumberOfStates());
+    EXPECT_EQ(189ul, model->getNumberOfTransitions());
+}
+
+TEST(DdJaniModelBuilderTest_Cudd, Ctmc) {
+    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
+    
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
+    storm::jani::Model janiModel = program.toJani(true);
+    storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.translate();
+    EXPECT_EQ(276ul, model->getNumberOfStates());
+    EXPECT_EQ(1120ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
+    janiModel = program.toJani(true);
+    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
+    model = builder.translate();
+    EXPECT_EQ(3478ul, model->getNumberOfStates());
+    EXPECT_EQ(14639ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
+    janiModel = program.toJani(true);
+    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
+    model = builder.translate();
+    EXPECT_EQ(12ul, model->getNumberOfStates());
+    EXPECT_EQ(22ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
+    janiModel = program.toJani(true);
+    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
+    model = builder.translate();
+    EXPECT_EQ(810ul, model->getNumberOfStates());
+    EXPECT_EQ(3699ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
+    janiModel = program.toJani(true);
+    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
+    model = builder.translate();
+    EXPECT_EQ(66ul, model->getNumberOfStates());
+    EXPECT_EQ(189ul, model->getNumberOfTransitions());
+}
\ No newline at end of file
diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp
index dc78c5c59..ccf16c1ff 100644
--- a/test/functional/builder/DdPrismModelBuilderTest.cpp
+++ b/test/functional/builder/DdPrismModelBuilderTest.cpp
@@ -13,42 +13,27 @@
 TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
     
-    auto t1 = std::chrono::high_resolution_clock::now();
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
-    auto t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "die: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(13ul, model->getNumberOfStates());
     EXPECT_EQ(20ul, model->getNumberOfTransitions());
     
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
-    t1 = std::chrono::high_resolution_clock::now();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "brp: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(677ul, model->getNumberOfStates());
     EXPECT_EQ(867ul, model->getNumberOfTransitions());
     
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
-    t1 = std::chrono::high_resolution_clock::now();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "crowds: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(8607ul, model->getNumberOfStates());
     EXPECT_EQ(15113ul, model->getNumberOfTransitions());
 
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
-    t1 = std::chrono::high_resolution_clock::now();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "lead: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(273ul, model->getNumberOfStates());
     EXPECT_EQ(397ul, model->getNumberOfTransitions());
     
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
-    t1 = std::chrono::high_resolution_clock::now();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
-    t2 = std::chrono::high_resolution_clock::now();
-    std::cout << "nand: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
     EXPECT_EQ(1728ul, model->getNumberOfStates());
     EXPECT_EQ(2505ul, model->getNumberOfTransitions());
 }