From c388d1c8fe2d0cfe2b1ee4b24d09848c7eb471fd Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 19 Sep 2018 14:18:42 +0200 Subject: [PATCH] making sure that functions in jani models and formulas in prism programs are substituted before flattening the model --- .../abstraction/GameBasedMdpModelChecker.cpp | 2 +- src/test/storm/storage/JaniModelTest.cpp | 12 ++++++++++ src/test/storm/storage/PrismProgramTest.cpp | 24 +++++++++---------- 3 files changed, 25 insertions(+), 13 deletions(-) diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index f2cb7a3d2..5fdc39a05 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -58,7 +58,7 @@ namespace storm { // Flatten the modules if there is more than one. if (originalProgram.getNumberOfModules() > 1) { - preprocessedModel = originalProgram.flattenModules(this->smtSolverFactory); + preprocessedModel = originalProgram.substituteFormulas().flattenModules(this->smtSolverFactory); } else { preprocessedModel = originalProgram; } diff --git a/src/test/storm/storage/JaniModelTest.cpp b/src/test/storm/storage/JaniModelTest.cpp index c7a6b5c11..a18aa279c 100644 --- a/src/test/storm/storage/JaniModelTest.cpp +++ b/src/test/storm/storage/JaniModelTest.cpp @@ -14,6 +14,7 @@ TEST(JaniModelTest, FlattenComposition) { std::shared_ptr smtSolverFactory = std::make_shared(); + janiModel.substituteFunctions(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges()); @@ -26,6 +27,7 @@ TEST(JaniModelTest, FlattenComposition_Wlan_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); + janiModel.substituteFunctions(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges()); @@ -38,6 +40,7 @@ TEST(JaniModelTest, FlattenComposition_Csma_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); + janiModel.substituteFunctions(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges()); @@ -50,6 +53,7 @@ TEST(JaniModelTest, FlattenComposition_Firewire_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); + janiModel.substituteFunctions(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges()); @@ -62,6 +66,7 @@ TEST(JaniModelTest, FlattenComposition_Coin_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); + janiModel.substituteFunctions(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges()); @@ -74,6 +79,7 @@ TEST(JaniModelTest, FlattenComposition_Dice_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); + janiModel.substituteFunctions(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); EXPECT_EQ(16ull, janiModel.getAutomaton(0).getNumberOfEdges()); @@ -88,6 +94,7 @@ TEST(JaniModelTest, FlattenComposition_Leader_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); + janiModel.substituteFunctions(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges()); @@ -100,6 +107,7 @@ TEST(JaniModelTest, FlattenComposition_Wlan_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); + janiModel.substituteFunctions(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges()); @@ -112,6 +120,7 @@ TEST(JaniModelTest, FlattenComposition_Csma_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); + janiModel.substituteFunctions(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges()); @@ -124,6 +133,7 @@ TEST(JaniModelTest, FlattenComposition_Firewire_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); + janiModel.substituteFunctions(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges()); @@ -136,6 +146,7 @@ TEST(JaniModelTest, FlattenComposition_Coin_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); + janiModel.substituteFunctions(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges()); @@ -148,6 +159,7 @@ TEST(JaniModelTest, FlattenComposition_Dice_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); + janiModel.substituteFunctions(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); EXPECT_EQ(16ull, janiModel.getAutomaton(0).getNumberOfEdges()); diff --git a/src/test/storm/storage/PrismProgramTest.cpp b/src/test/storm/storage/PrismProgramTest.cpp index e860fa997..86246f632 100644 --- a/src/test/storm/storage/PrismProgramTest.cpp +++ b/src/test/storm/storage/PrismProgramTest.cpp @@ -13,7 +13,7 @@ TEST(PrismProgramTest, FlattenModules) { std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory)); EXPECT_EQ(1ull, program.getNumberOfModules()); EXPECT_EQ(74ull, program.getModule(0).getNumberOfCommands()); } @@ -24,7 +24,7 @@ TEST(PrismProgramTest, FlattenModules_Wlan_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory)); EXPECT_EQ(1ull, program.getNumberOfModules()); EXPECT_EQ(179ull, program.getModule(0).getNumberOfCommands()); } @@ -35,7 +35,7 @@ TEST(PrismProgramTest, FlattenModules_Csma_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory)); EXPECT_EQ(1ull, program.getNumberOfModules()); EXPECT_EQ(70ull, program.getModule(0).getNumberOfCommands()); } @@ -46,7 +46,7 @@ TEST(PrismProgramTest, FlattenModules_Firewire_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory)); EXPECT_EQ(1ull, program.getNumberOfModules()); EXPECT_EQ(5024ull, program.getModule(0).getNumberOfCommands()); } @@ -57,7 +57,7 @@ TEST(PrismProgramTest, FlattenModules_Coin_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory)); EXPECT_EQ(1ull, program.getNumberOfModules()); EXPECT_EQ(13ull, program.getModule(0).getNumberOfCommands()); } @@ -68,7 +68,7 @@ TEST(PrismProgramTest, FlattenModules_Dice_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory)); EXPECT_EQ(1ull, program.getNumberOfModules()); EXPECT_EQ(16ull, program.getModule(0).getNumberOfCommands()); } @@ -81,7 +81,7 @@ TEST(PrismProgramTest, FlattenModules_Leader_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory)); EXPECT_EQ(1ull, program.getNumberOfModules()); EXPECT_EQ(74ull, program.getModule(0).getNumberOfCommands()); } @@ -92,7 +92,7 @@ TEST(PrismProgramTest, FlattenModules_Wlan_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory)); EXPECT_EQ(1ull, program.getNumberOfModules()); EXPECT_EQ(179ull, program.getModule(0).getNumberOfCommands()); } @@ -103,7 +103,7 @@ TEST(PrismProgramTest, FlattenModules_Csma_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory)); EXPECT_EQ(1ull, program.getNumberOfModules()); EXPECT_EQ(70ull, program.getModule(0).getNumberOfCommands()); } @@ -114,7 +114,7 @@ TEST(PrismProgramTest, FlattenModules_Firewire_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory)); EXPECT_EQ(1ull, program.getNumberOfModules()); EXPECT_EQ(5024ull, program.getModule(0).getNumberOfCommands()); } @@ -125,7 +125,7 @@ TEST(PrismProgramTest, FlattenModules_Coin_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory)); EXPECT_EQ(1ull, program.getNumberOfModules()); EXPECT_EQ(13ull, program.getModule(0).getNumberOfCommands()); } @@ -136,7 +136,7 @@ TEST(PrismProgramTest, FlattenModules_Dice_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory)); EXPECT_EQ(1ull, program.getNumberOfModules()); EXPECT_EQ(16ull, program.getModule(0).getNumberOfCommands()); }