From 8db3819553944401ebbe70e2f429aefcde069ba0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 12 Dec 2016 21:23:53 +0100 Subject: [PATCH] Jani model tests (flattening) now passing --- src/test/storage/JaniModelTest.cpp | 50 +++++++++++++++--------------- 1 file changed, 25 insertions(+), 25 deletions(-) diff --git a/src/test/storage/JaniModelTest.cpp b/src/test/storage/JaniModelTest.cpp index 6fd718a4e..613e491de 100644 --- a/src/test/storage/JaniModelTest.cpp +++ b/src/test/storage/JaniModelTest.cpp @@ -4,17 +4,17 @@ #include "storm/utility/solver.h" -#include "storm/storage/jani/janiModel.h" +#include "storm/storage/jani/Model.h" #ifdef STORM_HAVE_MSAT TEST(JaniModelTest, FlattenModules) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm")); - storm::jani::Model janiModel = model.toJani(); + storm::jani::Model janiModel = program.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1, janiModel.getNumberOfAutomata()); EXPECT_EQ(74, janiModel.getAutomaton(0).getNumberOfEdges()); } @@ -22,11 +22,11 @@ TEST(JaniModelTest, FlattenModules) { TEST(JaniModelTest, FlattenModules_Wlan_Mathsat) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm")); - storm::jani::Model janiModel = model.toJani(); + storm::jani::Model janiModel = program.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1, janiModel.getNumberOfAutomata()); EXPECT_EQ(179, janiModel.getAutomaton(0).getNumberOfEdges()); } @@ -34,11 +34,11 @@ TEST(JaniModelTest, FlattenModules_Wlan_Mathsat) { TEST(JaniModelTest, FlattenModules_Csma_Mathsat) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm")); - storm::jani::Model janiModel = model.toJani(); + storm::jani::Model janiModel = program.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1, janiModel.getNumberOfAutomata()); EXPECT_EQ(70, janiModel.getAutomaton(0).getNumberOfEdges()); } @@ -46,11 +46,11 @@ TEST(JaniModelTest, FlattenModules_Csma_Mathsat) { TEST(JaniModelTest, FlattenModules_Firewire_Mathsat) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm")); - storm::jani::Model janiModel = model.toJani(); + storm::jani::Model janiModel = program.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1, janiModel.getNumberOfAutomata()); EXPECT_EQ(5024, janiModel.getAutomaton(0).getNumberOfEdges()); } @@ -58,11 +58,11 @@ TEST(JaniModelTest, FlattenModules_Firewire_Mathsat) { TEST(JaniModelTest, FlattenModules_Coin_Mathsat) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm")); - storm::jani::Model janiModel = model.toJani(); + storm::jani::Model janiModel = program.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1, janiModel.getNumberOfAutomata()); EXPECT_EQ(13, janiModel.getAutomaton(0).getNumberOfEdges()); } @@ -70,11 +70,11 @@ TEST(JaniModelTest, FlattenModules_Coin_Mathsat) { TEST(JaniModelTest, FlattenModules_Dice_Mathsat) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm")); - storm::jani::Model janiModel = model.toJani(); + storm::jani::Model janiModel = program.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1, janiModel.getNumberOfAutomata()); EXPECT_EQ(16, janiModel.getAutomaton(0).getNumberOfEdges()); } @@ -84,11 +84,11 @@ TEST(JaniModelTest, FlattenModules_Dice_Mathsat) { TEST(JaniModelTest, FlattenModules_Leader_Z3) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm")); - storm::jani::Model janiModel = model.toJani(); + storm::jani::Model janiModel = program.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1, janiModel.getNumberOfAutomata()); EXPECT_EQ(74, janiModel.getAutomaton(0).getNumberOfEdges()); } @@ -96,11 +96,11 @@ TEST(JaniModelTest, FlattenModules_Leader_Z3) { TEST(JaniModelTest, FlattenModules_Wlan_Z3) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm")); - storm::jani::Model janiModel = model.toJani(); + storm::jani::Model janiModel = program.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1, janiModel.getNumberOfAutomata()); EXPECT_EQ(179, janiModel.getAutomaton(0).getNumberOfEdges()); } @@ -108,11 +108,11 @@ TEST(JaniModelTest, FlattenModules_Wlan_Z3) { TEST(JaniModelTest, FlattenModules_Csma_Z3) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm")); - storm::jani::Model janiModel = model.toJani(); + storm::jani::Model janiModel = program.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1, janiModel.getNumberOfAutomata()); EXPECT_EQ(70, janiModel.getAutomaton(0).getNumberOfEdges()); } @@ -120,11 +120,11 @@ TEST(JaniModelTest, FlattenModules_Csma_Z3) { TEST(JaniModelTest, FlattenModules_Firewire_Z3) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm")); - storm::jani::Model janiModel = model.toJani(); + storm::jani::Model janiModel = program.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1, janiModel.getNumberOfAutomata()); EXPECT_EQ(5024, janiModel.getAutomaton(0).getNumberOfEdges()); } @@ -132,11 +132,11 @@ TEST(JaniModelTest, FlattenModules_Firewire_Z3) { TEST(JaniModelTest, FlattenModules_Coin_Z3) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm")); - storm::jani::Model janiModel = model.toJani(); + storm::jani::Model janiModel = program.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1, janiModel.getNumberOfAutomata()); EXPECT_EQ(13, janiModel.getAutomaton(0).getNumberOfEdges()); } @@ -144,11 +144,11 @@ TEST(JaniModelTest, FlattenModules_Coin_Z3) { TEST(JaniModelTest, FlattenModules_Dice_Z3) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm")); - storm::jani::Model janiModel = model.toJani(); + storm::jani::Model janiModel = program.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1, janiModel.getNumberOfAutomata()); EXPECT_EQ(16, janiModel.getAutomaton(0).getNumberOfEdges()); }