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

fixed tests that used the prism model builder

tempestpy_adaptions
TimQu 8 years ago
parent
759e351e95
commit
f762491ce4
13 changed files with 63 additions and 63 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 38
      src/test/builder/ExplicitJaniModelBuilderTest.cpp
  2. 38
      src/test/builder/ExplicitPrismModelBuilderTest.cpp
  3. 6
      src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
  4. 8
      src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  5. 2
      src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  6. 4
      src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  7. 8
      src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp
  8. 2
      src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
  9. 2
      src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
  10. 2
      src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp
  11. 8
      src/test/utility/GraphTest.cpp
  12. 2
      src/test/utility/KSPTest.cpp
  13. 6
      src/test/utility/ModelInstantiatorTest.cpp

38
src/test/builder/ExplicitJaniModelBuilderTest.cpp
View File

@ -14,31 +14,31 @@ TEST(ExplicitJaniModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
storm::jani::Model janiModel = program.toJani();
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().getModel();
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();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
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();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
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();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
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();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
EXPECT_EQ(1728ul, model->getNumberOfStates());
EXPECT_EQ(2505ul, model->getNumberOfTransitions());
}
@ -50,31 +50,31 @@ TEST(ExplicitJaniModelBuilderTest, Ctmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
storm::jani::Model janiModel = program.toJani();
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().getModel();
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions());
}
@ -83,37 +83,37 @@ 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();
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().getModel();
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();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
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();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
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();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
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();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
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();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
EXPECT_EQ(37ul, model->getNumberOfStates());
EXPECT_EQ(59ul, model->getNumberOfTransitions());
}
@ -122,7 +122,7 @@ TEST(ExplicitJaniModelBuilderTest, Ma) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.ma");
storm::jani::Model janiModel = program.toJani();
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().getModel();
EXPECT_EQ(5ul, model->getNumberOfStates());
EXPECT_EQ(8ul, model->getNumberOfTransitions());
ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
@ -130,7 +130,7 @@ TEST(ExplicitJaniModelBuilderTest, Ma) {
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
EXPECT_EQ(5ul, model->getNumberOfStates());
EXPECT_EQ(13ul, model->getNumberOfTransitions());
ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
@ -138,7 +138,7 @@ TEST(ExplicitJaniModelBuilderTest, Ma) {
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build().getModel();
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(14ul, model->getNumberOfTransitions());
ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));

38
src/test/builder/ExplicitPrismModelBuilderTest.cpp
View File

@ -11,27 +11,27 @@
TEST(ExplicitPrismModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(1728ul, model->getNumberOfStates());
EXPECT_EQ(2505ul, model->getNumberOfTransitions());
}
@ -42,27 +42,27 @@ TEST(ExplicitPrismModelBuilderTest, Ctmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions());
}
@ -70,32 +70,32 @@ TEST(ExplicitPrismModelBuilderTest, Ctmc) {
TEST(ExplicitPrismModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(364ul, model->getNumberOfStates());
EXPECT_EQ(654ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(272ul, model->getNumberOfStates());
EXPECT_EQ(492ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(1038ul, model->getNumberOfStates());
EXPECT_EQ(1282ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire3-0.5.nm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(4093ul, model->getNumberOfStates());
EXPECT_EQ(5585ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-2.nm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(37ul, model->getNumberOfStates());
EXPECT_EQ(59ul, model->getNumberOfTransitions());
}
@ -103,21 +103,21 @@ TEST(ExplicitPrismModelBuilderTest, Mdp) {
TEST(ExplicitPrismModelBuilderTest, Ma) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.ma");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(5ul, model->getNumberOfStates());
EXPECT_EQ(8ul, model->getNumberOfTransitions());
ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
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");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(5ul, model->getNumberOfStates());
EXPECT_EQ(13ul, model->getNumberOfTransitions());
ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
EXPECT_EQ(5ul, model->as<storm::models::sparse::MarkovAutomaton<double>>()->getMarkovianStates().getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
model = storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(14ul, model->getNumberOfTransitions());
ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));

6
src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
View File

@ -69,7 +69,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) {
storm::generator::NextStateGeneratorOptions options;
options.setBuildAllLabels().setBuildAllRewardModels();
std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model = storm::builder::ExplicitModelBuilder<storm::RationalNumber>(program, options).build();
std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model = storm::builder::ExplicitModelBuilder<storm::RationalNumber>(program, options).build().getModel();
// A parser that we use for conveniently constructing the formulas.
@ -118,7 +118,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm");
storm::generator::NextStateGeneratorOptions options;
options.setBuildAllLabels().setBuildAllRewardModels();
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build();
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build().getModel();
// A parser that we use for conveniently constructing the formulas.
@ -403,7 +403,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Conditional) {
storm::generator::NextStateGeneratorOptions options;
options.setBuildAllLabels().setBuildAllRewardModels();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build().getModel();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
ASSERT_EQ(4ul, model->getNumberOfStates());
ASSERT_EQ(5ul, model->getNumberOfTransitions());

8
src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
View File

@ -31,7 +31,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
// Build the model.
storm::generator::NextStateGeneratorOptions options;
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("num_repairs")).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("num_repairs")).build().getModel();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@ -107,7 +107,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("up")).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("up")).build().getModel();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@ -169,7 +169,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@ -210,7 +210,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("customers")).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("customers")).build().getModel();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();

2
src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
View File

@ -294,7 +294,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) {
TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/test_conditional.pm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(true, true)).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(true, true)).build().getModel();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
ASSERT_EQ(4ul, model->getNumberOfStates());
ASSERT_EQ(5ul, model->getNumberOfTransitions());

4
src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -199,7 +199,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) {
storm::generator::NextStateGeneratorOptions options;
options.setBuildAllLabels();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build().getModel();
EXPECT_EQ(4ull, model->getNumberOfStates());
EXPECT_EQ(11ull, model->getNumberOfTransitions());
@ -251,7 +251,7 @@ TEST(DISABLED_GmmxxMdpPrctlModelCheckerTest, TinyRewards) {
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(true, true)).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(true, true)).build().getModel();
EXPECT_EQ(3ull, model->getNumberOfStates());
EXPECT_EQ(4ull, model->getNumberOfTransitions());

8
src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp
View File

@ -26,7 +26,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("num_repairs")).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("num_repairs")).build().getModel();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@ -97,7 +97,7 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) {
// Build the model.
storm::generator::NextStateGeneratorOptions options;
options.addRewardModel("up").setBuildAllLabels();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build().getModel();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@ -152,7 +152,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@ -186,7 +186,7 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model with the customers reward structure.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true).addRewardModel("customers")).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true).addRewardModel("customers")).build().getModel();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();

2
src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
View File

@ -26,7 +26,7 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) {
// Customize and perform model-building.
storm::generator::NextStateGeneratorOptions options;
options.setBuildAllLabels().setBuildChoiceLabels(true);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build().getModel()->as<storm::models::sparse::Mdp<double>>();
boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02);
EXPECT_NE(perms, boost::none);

2
src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
View File

@ -29,7 +29,7 @@ TEST(SmtPermissiveSchedulerTest, DISABLED_DieSelection) {
// Customize and perform model-building.
storm::generator::NextStateGeneratorOptions options(formula02b);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build().getModel()->as<storm::models::sparse::Mdp<double>>();
// boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms = storm::ps::computePermissiveSchedulerViaSMT<>(*mdp, formula02);
// EXPECT_NE(perms, boost::none);

2
src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp
View File

@ -14,7 +14,7 @@ TEST(NondeterministicModelBisimulationDecomposition, TwoDice) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
// Build the die model without its reward model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel();
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>();

8
src/test/utility/GraphTest.cpp
View File

@ -596,7 +596,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) {
TEST(GraphTest, ExplicitProb01) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
@ -618,7 +618,7 @@ TEST(GraphTest, ExplicitProb01) {
TEST(GraphTest, ExplicitProb01MinMax) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -634,7 +634,7 @@ TEST(GraphTest, ExplicitProb01MinMax) {
modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -656,7 +656,7 @@ TEST(GraphTest, ExplicitProb01MinMax) {
modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build().getModel();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);

2
src/test/utility/KSPTest.cpp
View File

@ -17,7 +17,7 @@ std::shared_ptr<storm::models::sparse::Model<double>> buildExampleModel() {
std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm";
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath);
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
return storm::builder::ExplicitModelBuilder<double>(program).build();
return storm::builder::ExplicitModelBuilder<double>(program).build().getModel();
}
// NOTE: these are hardcoded (obviously), but the model's state indices might change

6
src/test/utility/ModelInstantiatorTest.cpp
View File

@ -30,7 +30,7 @@ TEST(ModelInstantiatorTest, BrpProb) {
ASSERT_TRUE(formulas.size()==1);
// Parametric model
storm::generator::NextStateGeneratorOptions options(*formulas.front());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build().getModel()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
EXPECT_FALSE(dtmc->hasRewardModel());
@ -148,7 +148,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
ASSERT_TRUE(formulas.size()==1);
// Parametric model
storm::generator::NextStateGeneratorOptions options(*formulas.front());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build().getModel()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
@ -218,7 +218,7 @@ TEST(ModelInstantiatorTest, Consensus) {
ASSERT_TRUE(formulas.size()==1);
// Parametric model
storm::generator::NextStateGeneratorOptions options(*formulas.front());
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> mdp = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build()->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> mdp = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build().getModel()->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>> modelInstantiator(*mdp);

Write Preview
Loading…
Cancel
Save