diff --git a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp index 95b690e96..f98834a20 100644 --- a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp @@ -11,32 +11,32 @@ TEST(ExplicitJaniModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - storm::jani::Model janiModel = program.toJani(); + storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); @@ -44,32 +44,32 @@ TEST(ExplicitJaniModelBuilderTest, Dtmc) { TEST(ExplicitJaniModelBuilderTest, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); - storm::jani::Model janiModel = program.toJani(); + storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); @@ -77,38 +77,38 @@ TEST(ExplicitJaniModelBuilderTest, Ctmc) { TEST(ExplicitJaniModelBuilderTest, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); - storm::jani::Model janiModel = program.toJani(); + storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(364ul, model->getNumberOfStates()); EXPECT_EQ(654ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(272ul, model->getNumberOfStates()); EXPECT_EQ(492ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(1038ul, model->getNumberOfStates()); EXPECT_EQ(1282ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire3-0.5.nm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(4093ul, model->getNumberOfStates()); EXPECT_EQ(5585ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-2.nm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(59ul, model->getNumberOfTransitions()); @@ -116,7 +116,7 @@ TEST(ExplicitJaniModelBuilderTest, Mdp) { TEST(ExplicitJaniModelBuilderTest, Ma) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.ma"); - storm::jani::Model janiModel = program.toJani(); + storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(5ul, model->getNumberOfStates()); @@ -125,7 +125,7 @@ TEST(ExplicitJaniModelBuilderTest, Ma) { EXPECT_EQ(4ul, model->as>()->getMarkovianStates().getNumberOfSetBits()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfTransitions()); @@ -133,7 +133,7 @@ TEST(ExplicitJaniModelBuilderTest, Ma) { EXPECT_EQ(5ul, model->as>()->getMarkovianStates().getNumberOfSetBits()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(14ul, model->getNumberOfTransitions()); @@ -143,14 +143,14 @@ TEST(ExplicitJaniModelBuilderTest, Ma) { TEST(ExplicitJaniModelBuilderTest, FailComposition) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition.nm"); - storm::jani::Model janiModel = program.toJani(); + storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); ASSERT_THROW(storm::builder::ExplicitModelBuilder(janiModel).build(), storm::exceptions::WrongFormatException); } TEST(ExplicitJaniModelBuilderTest, IllegalSynchronizingWrites) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2-illegalSynchronizingWrite.nm"); - storm::jani::Model janiModel = program.toJani(); + storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); storm::generator::NextStateGeneratorOptions options; options.setExplorationChecks(true); std::shared_ptr> nextStateGenerator = std::make_shared>(janiModel, options); diff --git a/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp index c5c0eec05..d8a0c403d 100644 --- a/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp @@ -11,32 +11,32 @@ TEST(ExplicitJitJaniModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - storm::jani::Model janiModel = program.toJani(); + storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); @@ -45,32 +45,32 @@ TEST(ExplicitJitJaniModelBuilderTest, Dtmc) { TEST(ExplicitJitJaniModelBuilderTest, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); - storm::jani::Model janiModel = program.toJani(); + storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); @@ -78,38 +78,38 @@ TEST(ExplicitJitJaniModelBuilderTest, Ctmc) { TEST(ExplicitJitJaniModelBuilderTest, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); - storm::jani::Model janiModel = program.toJani(); + storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(364ul, model->getNumberOfStates()); EXPECT_EQ(654ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(272ul, model->getNumberOfStates()); EXPECT_EQ(492ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(1038ul, model->getNumberOfStates()); EXPECT_EQ(1282ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire3-0.5.nm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(4093ul, model->getNumberOfStates()); EXPECT_EQ(5585ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-2.nm"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(59ul, model->getNumberOfTransitions()); @@ -117,7 +117,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Mdp) { TEST(ExplicitJitJaniModelBuilderTest, Ma) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.ma"); - storm::jani::Model janiModel = program.toJani(); + storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(5ul, model->getNumberOfStates()); @@ -126,7 +126,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) { EXPECT_EQ(4ul, model->as>()->getMarkovianStates().getNumberOfSetBits()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfTransitions()); @@ -134,7 +134,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) { EXPECT_EQ(5ul, model->as>()->getMarkovianStates().getNumberOfSetBits()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma"); - janiModel = program.toJani(); + janiModel = program.toJani().substituteConstantsFunctions(); model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();; EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(14ul, model->getNumberOfTransitions()); @@ -144,14 +144,14 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) { TEST(ExplicitJitJaniModelBuilderTest, FailComposition) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition.nm"); - storm::jani::Model janiModel = program.toJani(); + storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); ASSERT_THROW(storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build();, storm::exceptions::WrongFormatException); } TEST(ExplicitJitJaniModelBuilderTest, IllegalSynchronizingWrites) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2-illegalSynchronizingWrite.nm"); - storm::jani::Model janiModel = program.toJani(); + storm::jani::Model janiModel = program.toJani().substituteConstantsFunctions(); storm::builder::BuilderOptions options; options.setExplorationChecks(true);