From 2c17bdded71d098e42c70b1313ed03f34ec8100f Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 12 Dec 2016 17:22:06 +0100 Subject: [PATCH] fixes for JANI flattening tests --- src/storm/storage/jani/Model.cpp | 4 ++ src/storm/storage/jani/Model.h | 5 ++ src/test/storage/JaniModelTest.cpp | 98 +++++++++++++++--------------- 3 files changed, 58 insertions(+), 49 deletions(-) diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 0fca85982..f635e0aec 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -684,6 +684,10 @@ namespace storm { return automata[it->second]; } + Automaton& Model::getAutomaton(uint64_t index) { + return automata[index]; + } + Automaton const& Model::getAutomaton(std::string const& name) const { auto it = automatonToIndex.find(name); STORM_LOG_THROW(it != automatonToIndex.end(), storm::exceptions::InvalidOperationException, "Unable to retrieve unknown automaton '" << name << "'."); diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 607d03452..de3cf6657 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -234,6 +234,11 @@ namespace storm { */ Automaton& getAutomaton(std::string const& name); + /*! + * Retrieves the automaton with the given index. + */ + Automaton& getAutomaton(uint64_t index); + /*! * Retrieves the automaton with the given name. */ diff --git a/src/test/storage/JaniModelTest.cpp b/src/test/storage/JaniModelTest.cpp index 8b13f179c..6fd718a4e 100644 --- a/src/test/storage/JaniModelTest.cpp +++ b/src/test/storage/JaniModelTest.cpp @@ -4,79 +4,79 @@ #include "storm/utility/solver.h" -#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/janiModel.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 = program.toJani(); + storm::jani::Model janiModel = model.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(74, program.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, janiModel.getNumberOfAutomata()); + EXPECT_EQ(74, janiModel.getAutomaton(0).getNumberOfEdges()); } 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 = program.toJani(); + storm::jani::Model janiModel = model.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(179, program.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, janiModel.getNumberOfAutomata()); + EXPECT_EQ(179, janiModel.getAutomaton(0).getNumberOfEdges()); } 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 = program.toJani(); + storm::jani::Model janiModel = model.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(70, program.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, janiModel.getNumberOfAutomata()); + EXPECT_EQ(70, janiModel.getAutomaton(0).getNumberOfEdges()); } 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 = program.toJani(); + storm::jani::Model janiModel = model.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(5024, program.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, janiModel.getNumberOfAutomata()); + EXPECT_EQ(5024, janiModel.getAutomaton(0).getNumberOfEdges()); } 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 = program.toJani(); + storm::jani::Model janiModel = model.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(13, program.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, janiModel.getNumberOfAutomata()); + EXPECT_EQ(13, janiModel.getAutomaton(0).getNumberOfEdges()); } 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 = program.toJani(); + storm::jani::Model janiModel = model.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(16, program.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, janiModel.getNumberOfAutomata()); + EXPECT_EQ(16, janiModel.getAutomaton(0).getNumberOfEdges()); } #endif @@ -84,72 +84,72 @@ 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 = program.toJani(); + storm::jani::Model janiModel = model.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(74, program.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, janiModel.getNumberOfAutomata()); + EXPECT_EQ(74, janiModel.getAutomaton(0).getNumberOfEdges()); } 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 = program.toJani(); + storm::jani::Model janiModel = model.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(179, program.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, janiModel.getNumberOfAutomata()); + EXPECT_EQ(179, janiModel.getAutomaton(0).getNumberOfEdges()); } 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 = program.toJani(); + storm::jani::Model janiModel = model.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(70, program.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, janiModel.getNumberOfAutomata()); + EXPECT_EQ(70, janiModel.getAutomaton(0).getNumberOfEdges()); } 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 = program.toJani(); + storm::jani::Model janiModel = model.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(5024, program.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, janiModel.getNumberOfAutomata()); + EXPECT_EQ(5024, janiModel.getAutomaton(0).getNumberOfEdges()); } 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 = program.toJani(); + storm::jani::Model janiModel = model.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(13, program.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, janiModel.getNumberOfAutomata()); + EXPECT_EQ(13, janiModel.getAutomaton(0).getNumberOfEdges()); } 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 = program.toJani(); + storm::jani::Model janiModel = model.toJani(); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(16, program.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(model = janiModel.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, janiModel.getNumberOfAutomata()); + EXPECT_EQ(16, janiModel.getAutomaton(0).getNumberOfEdges()); } #endif