sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

fixed some janibuilder tests

main
TimQu 7 years ago
parent
aa6fd3cbb2
commit
a173cb68b8
2 changed files with 42 additions and 42 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 42
      src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp
  2. 42
      src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp

42
src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp
View File

@ -11,32 +11,32 @@
TEST(ExplicitJaniModelBuilderTest, Dtmc) { TEST(ExplicitJaniModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); 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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions()); EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"); 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<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions()); EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); 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<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions()); EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); 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<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions()); EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm"); 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<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(1728ul, model->getNumberOfStates());
EXPECT_EQ(2505ul, model->getNumberOfTransitions()); EXPECT_EQ(2505ul, model->getNumberOfTransitions());
@ -44,32 +44,32 @@ TEST(ExplicitJaniModelBuilderTest, Dtmc) {
TEST(ExplicitJaniModelBuilderTest, Ctmc) { TEST(ExplicitJaniModelBuilderTest, Ctmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); 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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions()); EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
janiModel = program.toJani();
janiModel = program.toJani().substituteConstantsFunctions();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions()); EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
janiModel = program.toJani();
janiModel = program.toJani().substituteConstantsFunctions();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions()); EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true);
janiModel = program.toJani();
janiModel = program.toJani().substituteConstantsFunctions();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions()); EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
janiModel = program.toJani();
janiModel = program.toJani().substituteConstantsFunctions();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions()); EXPECT_EQ(189ul, model->getNumberOfTransitions());
@ -77,38 +77,38 @@ TEST(ExplicitJaniModelBuilderTest, Ctmc) {
TEST(ExplicitJaniModelBuilderTest, Mdp) { TEST(ExplicitJaniModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); 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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions()); EXPECT_EQ(436ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm");
janiModel = program.toJani();
janiModel = program.toJani().substituteConstantsFunctions();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(364ul, model->getNumberOfStates()); EXPECT_EQ(364ul, model->getNumberOfStates());
EXPECT_EQ(654ul, model->getNumberOfTransitions()); EXPECT_EQ(654ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm");
janiModel = program.toJani();
janiModel = program.toJani().substituteConstantsFunctions();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(272ul, model->getNumberOfStates()); EXPECT_EQ(272ul, model->getNumberOfStates());
EXPECT_EQ(492ul, model->getNumberOfTransitions()); EXPECT_EQ(492ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm"); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm");
janiModel = program.toJani();
janiModel = program.toJani().substituteConstantsFunctions();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(1038ul, model->getNumberOfStates()); EXPECT_EQ(1038ul, model->getNumberOfStates());
EXPECT_EQ(1282ul, model->getNumberOfTransitions()); EXPECT_EQ(1282ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire3-0.5.nm"); 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<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(4093ul, model->getNumberOfStates()); EXPECT_EQ(4093ul, model->getNumberOfStates());
EXPECT_EQ(5585ul, model->getNumberOfTransitions()); EXPECT_EQ(5585ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-2.nm"); 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<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(37ul, model->getNumberOfStates());
EXPECT_EQ(59ul, model->getNumberOfTransitions()); EXPECT_EQ(59ul, model->getNumberOfTransitions());
@ -116,7 +116,7 @@ TEST(ExplicitJaniModelBuilderTest, Mdp) {
TEST(ExplicitJaniModelBuilderTest, Ma) { TEST(ExplicitJaniModelBuilderTest, Ma) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(5ul, model->getNumberOfStates());
@ -125,7 +125,7 @@ TEST(ExplicitJaniModelBuilderTest, Ma) {
EXPECT_EQ(4ul, model->as<storm::models::sparse::MarkovAutomaton<double>>()->getMarkovianStates().getNumberOfSetBits()); EXPECT_EQ(4ul, model->as<storm::models::sparse::MarkovAutomaton<double>>()->getMarkovianStates().getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma"); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma");
janiModel = program.toJani();
janiModel = program.toJani().substituteConstantsFunctions();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(5ul, model->getNumberOfStates());
EXPECT_EQ(13ul, model->getNumberOfTransitions()); EXPECT_EQ(13ul, model->getNumberOfTransitions());
@ -133,7 +133,7 @@ TEST(ExplicitJaniModelBuilderTest, Ma) {
EXPECT_EQ(5ul, model->as<storm::models::sparse::MarkovAutomaton<double>>()->getMarkovianStates().getNumberOfSetBits()); EXPECT_EQ(5ul, model->as<storm::models::sparse::MarkovAutomaton<double>>()->getMarkovianStates().getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma"); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma");
janiModel = program.toJani();
janiModel = program.toJani().substituteConstantsFunctions();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(14ul, model->getNumberOfTransitions()); EXPECT_EQ(14ul, model->getNumberOfTransitions());
@ -143,14 +143,14 @@ TEST(ExplicitJaniModelBuilderTest, Ma) {
TEST(ExplicitJaniModelBuilderTest, FailComposition) { TEST(ExplicitJaniModelBuilderTest, FailComposition) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition.nm"); 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<double>(janiModel).build(), storm::exceptions::WrongFormatException); ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(janiModel).build(), storm::exceptions::WrongFormatException);
} }
TEST(ExplicitJaniModelBuilderTest, IllegalSynchronizingWrites) { TEST(ExplicitJaniModelBuilderTest, IllegalSynchronizingWrites) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2-illegalSynchronizingWrite.nm"); 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; storm::generator::NextStateGeneratorOptions options;
options.setExplorationChecks(true); options.setExplorationChecks(true);
std::shared_ptr<storm::generator::NextStateGenerator<double, uint32_t>> nextStateGenerator = std::make_shared<storm::generator::JaniNextStateGenerator<double, uint32_t>>(janiModel, options); std::shared_ptr<storm::generator::NextStateGenerator<double, uint32_t>> nextStateGenerator = std::make_shared<storm::generator::JaniNextStateGenerator<double, uint32_t>>(janiModel, options);

42
src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp
View File

@ -11,32 +11,32 @@
TEST(ExplicitJitJaniModelBuilderTest, Dtmc) { TEST(ExplicitJitJaniModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); 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<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();; std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions()); EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions()); EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions()); EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions()); EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm"); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(1728ul, model->getNumberOfStates());
EXPECT_EQ(2505ul, model->getNumberOfTransitions()); EXPECT_EQ(2505ul, model->getNumberOfTransitions());
@ -45,32 +45,32 @@ TEST(ExplicitJitJaniModelBuilderTest, Dtmc) {
TEST(ExplicitJitJaniModelBuilderTest, Ctmc) { TEST(ExplicitJitJaniModelBuilderTest, Ctmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); 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<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();; std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions()); EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions()); EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions()); EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions()); EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions()); EXPECT_EQ(189ul, model->getNumberOfTransitions());
@ -78,38 +78,38 @@ TEST(ExplicitJitJaniModelBuilderTest, Ctmc) {
TEST(ExplicitJitJaniModelBuilderTest, Mdp) { TEST(ExplicitJitJaniModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); 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<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();; std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions()); EXPECT_EQ(436ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm");
janiModel = program.toJani();
janiModel = program.toJani().substituteConstantsFunctions();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(364ul, model->getNumberOfStates()); EXPECT_EQ(364ul, model->getNumberOfStates());
EXPECT_EQ(654ul, model->getNumberOfTransitions()); EXPECT_EQ(654ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(272ul, model->getNumberOfStates()); EXPECT_EQ(272ul, model->getNumberOfStates());
EXPECT_EQ(492ul, model->getNumberOfTransitions()); EXPECT_EQ(492ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm"); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(1038ul, model->getNumberOfStates()); EXPECT_EQ(1038ul, model->getNumberOfStates());
EXPECT_EQ(1282ul, model->getNumberOfTransitions()); EXPECT_EQ(1282ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire3-0.5.nm"); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(4093ul, model->getNumberOfStates()); EXPECT_EQ(4093ul, model->getNumberOfStates());
EXPECT_EQ(5585ul, model->getNumberOfTransitions()); EXPECT_EQ(5585ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-2.nm"); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(37ul, model->getNumberOfStates());
EXPECT_EQ(59ul, model->getNumberOfTransitions()); EXPECT_EQ(59ul, model->getNumberOfTransitions());
@ -117,7 +117,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Mdp) {
TEST(ExplicitJitJaniModelBuilderTest, Ma) { TEST(ExplicitJitJaniModelBuilderTest, Ma) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.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<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();; std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(5ul, model->getNumberOfStates());
@ -126,7 +126,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) {
EXPECT_EQ(4ul, model->as<storm::models::sparse::MarkovAutomaton<double>>()->getMarkovianStates().getNumberOfSetBits()); EXPECT_EQ(4ul, model->as<storm::models::sparse::MarkovAutomaton<double>>()->getMarkovianStates().getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma"); 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<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(5ul, model->getNumberOfStates());
EXPECT_EQ(13ul, model->getNumberOfTransitions()); EXPECT_EQ(13ul, model->getNumberOfTransitions());
@ -134,7 +134,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) {
EXPECT_EQ(5ul, model->as<storm::models::sparse::MarkovAutomaton<double>>()->getMarkovianStates().getNumberOfSetBits()); EXPECT_EQ(5ul, model->as<storm::models::sparse::MarkovAutomaton<double>>()->getMarkovianStates().getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma"); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma");
janiModel = program.toJani();
janiModel = program.toJani().substituteConstantsFunctions();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();; model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();;
EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(14ul, model->getNumberOfTransitions()); EXPECT_EQ(14ul, model->getNumberOfTransitions());
@ -144,14 +144,14 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) {
TEST(ExplicitJitJaniModelBuilderTest, FailComposition) { TEST(ExplicitJitJaniModelBuilderTest, FailComposition) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition.nm"); 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<double>(janiModel).build();, storm::exceptions::WrongFormatException); ASSERT_THROW(storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();, storm::exceptions::WrongFormatException);
} }
TEST(ExplicitJitJaniModelBuilderTest, IllegalSynchronizingWrites) { TEST(ExplicitJitJaniModelBuilderTest, IllegalSynchronizingWrites) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2-illegalSynchronizingWrite.nm"); 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; storm::builder::BuilderOptions options;
options.setExplorationChecks(true); options.setExplorationChecks(true);

Write Preview
Loading…
Cancel
Save