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

Changed path for tests,

main
Matthias Volk 9 years ago
parent
f474e9cf7b
commit
072b316ad0
36 changed files with 313 additions and 313 deletions
Split View
  1. 84
      src/test/builder/DdJaniModelBuilderTest.cpp
  2. 72
      src/test/builder/DdPrismModelBuilderTest.cpp
  3. 42
      src/test/builder/ExplicitJaniModelBuilderTest.cpp
  4. 42
      src/test/builder/ExplicitJitJaniModelBuilderTest.cpp
  5. 40
      src/test/builder/ExplicitPrismModelBuilderTest.cpp
  6. 6
      src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
  7. 8
      src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  8. 2
      src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  9. 16
      src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
  10. 12
      src/test/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
  11. 8
      src/test/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
  12. 4
      src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  13. 8
      src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp
  14. 16
      src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
  15. 12
      src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
  16. 8
      src/test/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
  17. 4
      src/test/modelchecker/SparseExplorationModelCheckerTest.cpp
  18. 12
      src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
  19. 8
      src/test/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
  20. 26
      src/test/parser/AtomicPropositionLabelingParserTest.cpp
  21. 14
      src/test/parser/AutoParserTest.cpp
  22. 12
      src/test/parser/DeterministicModelParserTest.cpp
  23. 30
      src/test/parser/DeterministicSparseTransitionParserTest.cpp
  24. 6
      src/test/parser/MappedFileTest.cpp
  25. 6
      src/test/parser/MarkovAutomatonParserTest.cpp
  26. 8
      src/test/parser/MarkovAutomatonSparseTransitionParserTest.cpp
  27. 10
      src/test/parser/NondeterministicModelParserTest.cpp
  28. 30
      src/test/parser/NondeterministicSparseTransitionParserTest.cpp
  29. 18
      src/test/parser/PrismParserTest.cpp
  30. 10
      src/test/parser/SparseStateRewardParserTest.cpp
  31. 2
      src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
  32. 2
      src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
  33. 2
      src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp
  34. 16
      src/test/storage/PrismProgramTest.cpp
  35. 24
      src/test/utility/GraphTest.cpp
  36. 6
      src/test/utility/ModelInstantiatorTest.cpp

84
src/test/builder/DdJaniModelBuilderTest.cpp
View File

@ -18,7 +18,7 @@
#include "storm/settings/modules/IOSettings.h"
TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
@ -26,25 +26,25 @@ TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/brp-16-2.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/nand-5-2.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
@ -53,7 +53,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
}
TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
@ -61,25 +61,25 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/brp-16-2.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/nand-5-2.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(1728ul, model->getNumberOfStates());
@ -90,32 +90,32 @@ TEST(DdJaniModelBuilderTest_Sylvan, Ctmc) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel);
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/fms2.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(66ul, model->getNumberOfStates());
@ -126,32 +126,32 @@ TEST(DdJaniModelBuilderTest_Cudd, Ctmc) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel);
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/fms2.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(66ul, model->getNumberOfStates());
@ -159,7 +159,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Ctmc) {
}
TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel);
@ -171,7 +171,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
EXPECT_EQ(254ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader3.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
@ -182,7 +182,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
EXPECT_EQ(573ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
@ -193,7 +193,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
EXPECT_EQ(400ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/csma2-2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
@ -204,7 +204,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/firewire3-0.5.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
@ -215,7 +215,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
@ -228,7 +228,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
}
TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel);
@ -240,7 +240,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
EXPECT_EQ(254ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader3.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
@ -251,7 +251,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
EXPECT_EQ(573ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
@ -262,7 +262,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
EXPECT_EQ(400ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/csma2-2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
@ -273,7 +273,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/firewire3-0.5.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
@ -284,7 +284,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
@ -297,21 +297,21 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
}
TEST(DdJaniModelBuilderTest_Cudd, IllegalSynchronizingWrites) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2-illegalSynchronizingWrite.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel), storm::exceptions::WrongFormatException);
}
TEST(DdJaniModelBuilderTest_Sylvan, IllegalSynchronizingWrites) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2-illegalSynchronizingWrite.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel), storm::exceptions::WrongFormatException);
}
TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/SmallPrismTest.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/SmallPrismTest.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
@ -367,7 +367,7 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) {
}
TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/SmallPrismTest.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/SmallPrismTest.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
@ -423,7 +423,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
}
TEST(DdJaniModelBuilderTest_Sylvan, Composition) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/system_composition.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
@ -436,7 +436,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Composition) {
EXPECT_EQ(61ul, mdp->getNumberOfTransitions());
EXPECT_EQ(61ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/system_composition2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -448,7 +448,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, Composition) {
}
TEST(DdJaniModelBuilderTest_Cudd, Composition) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/system_composition.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
@ -461,7 +461,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Composition) {
EXPECT_EQ(61ul, mdp->getNumberOfTransitions());
EXPECT_EQ(61ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/system_composition2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -473,7 +473,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Composition) {
}
TEST(DdJaniModelBuilderTest_Cudd, InputEnabling) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/SmallPrismTest2.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/SmallPrismTest2.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
@ -505,7 +505,7 @@ TEST(DdJaniModelBuilderTest_Cudd, InputEnabling) {
}
TEST(DdJaniModelBuilderTest_Sylvan, InputEnabling) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/SmallPrismTest2.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/SmallPrismTest2.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;

72
src/test/builder/DdPrismModelBuilderTest.cpp
View File

@ -12,32 +12,32 @@
#include "storm/builder/DdPrismModelBuilder.h"
TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/brp-16-2.pm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/nand-5-2.pm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_EQ(1728ul, model->getNumberOfStates());
@ -45,32 +45,32 @@ TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) {
}
TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/brp-16-2.pm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/nand-5-2.pm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_EQ(1728ul, model->getNumberOfStates());
@ -81,32 +81,32 @@ TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/fms2.sm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_EQ(66ul, model->getNumberOfStates());
@ -117,32 +117,32 @@ TEST(DdPrismModelBuilderTest_Cudd, Ctmc) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/fms2.sm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_EQ(66ul, model->getNumberOfStates());
@ -150,7 +150,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Ctmc) {
}
TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
@ -161,7 +161,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
EXPECT_EQ(254ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader3.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -171,7 +171,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
EXPECT_EQ(573ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -181,7 +181,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
EXPECT_EQ(400ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/csma2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -191,7 +191,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/firewire3-0.5.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -201,7 +201,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -213,7 +213,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
}
TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
@ -224,7 +224,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
EXPECT_EQ(254ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader3.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -234,7 +234,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
EXPECT_EQ(573ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -244,7 +244,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
EXPECT_EQ(400ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/csma2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -254,7 +254,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/firewire3-0.5.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -264,7 +264,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -276,7 +276,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
}
TEST(DdPrismModelBuilderTest_Sylvan, Composition) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/system_composition.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
@ -288,7 +288,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Composition) {
EXPECT_EQ(61ul, mdp->getNumberOfTransitions());
EXPECT_EQ(61ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/system_composition2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@ -300,7 +300,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Composition) {
}
TEST(DdPrismModelBuilderTest_Cudd, Composition) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/system_composition.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
@ -312,7 +312,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Composition) {
EXPECT_EQ(61ul, mdp->getNumberOfTransitions());
EXPECT_EQ(61ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/system_composition2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);

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

@ -11,32 +11,32 @@
#include "storm/settings/modules/IOSettings.h"
TEST(ExplicitJaniModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::jani::Model janiModel = program.toJani();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/brp-16-2.pm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/nand-5-2.pm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(1728ul, model->getNumberOfStates());
@ -47,32 +47,32 @@ TEST(ExplicitJaniModelBuilderTest, Ctmc) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
storm::jani::Model janiModel = program.toJani();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/fms2.sm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(66ul, model->getNumberOfStates());
@ -80,38 +80,38 @@ TEST(ExplicitJaniModelBuilderTest, Ctmc) {
}
TEST(ExplicitJaniModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
storm::jani::Model janiModel = program.toJani();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader3.nm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(364ul, model->getNumberOfStates());
EXPECT_EQ(654ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2.nm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(272ul, model->getNumberOfStates());
EXPECT_EQ(492ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/csma2-2.nm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(1038ul, model->getNumberOfStates());
EXPECT_EQ(1282ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/firewire3-0.5.nm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(4093ul, model->getNumberOfStates());
EXPECT_EQ(5585ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-2.nm");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(37ul, model->getNumberOfStates());
@ -119,7 +119,7 @@ TEST(ExplicitJaniModelBuilderTest, Mdp) {
}
TEST(ExplicitJaniModelBuilderTest, Ma) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/simple.ma");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/simple.ma");
storm::jani::Model janiModel = program.toJani();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
@ -128,7 +128,7 @@ TEST(ExplicitJaniModelBuilderTest, Ma) {
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_CPP_TESTS_BASE_PATH "/functional/builder/hybrid_states.ma");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/hybrid_states.ma");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(5ul, model->getNumberOfStates());
@ -136,7 +136,7 @@ TEST(ExplicitJaniModelBuilderTest, Ma) {
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_CPP_TESTS_BASE_PATH "/functional/builder/stream2.ma");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/stream2.ma");
janiModel = program.toJani();
model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
EXPECT_EQ(12ul, model->getNumberOfStates());
@ -146,14 +146,14 @@ TEST(ExplicitJaniModelBuilderTest, Ma) {
}
TEST(ExplicitJaniModelBuilderTest, FailComposition) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/system_composition.nm");
storm::jani::Model janiModel = program.toJani();
ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(janiModel).build(), storm::exceptions::WrongFormatException);
}
TEST(ExplicitJaniModelBuilderTest, IllegalSynchronizingWrites) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2-illegalSynchronizingWrite.nm");
storm::jani::Model janiModel = program.toJani();
storm::generator::NextStateGeneratorOptions options;
options.setExplorationChecks(true);

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

@ -11,32 +11,32 @@
#include "storm/settings/modules/IOSettings.h"
TEST(ExplicitJitJaniModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::jani::Model janiModel = program.toJani();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/brp-16-2.pm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/nand-5-2.pm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(1728ul, model->getNumberOfStates());
@ -47,32 +47,32 @@ TEST(ExplicitJitJaniModelBuilderTest, Ctmc) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
storm::jani::Model janiModel = program.toJani();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/fms2.sm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(66ul, model->getNumberOfStates());
@ -80,38 +80,38 @@ TEST(ExplicitJitJaniModelBuilderTest, Ctmc) {
}
TEST(ExplicitJitJaniModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
storm::jani::Model janiModel = program.toJani();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader3.nm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(364ul, model->getNumberOfStates());
EXPECT_EQ(654ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2.nm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(272ul, model->getNumberOfStates());
EXPECT_EQ(492ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/csma2-2.nm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(1038ul, model->getNumberOfStates());
EXPECT_EQ(1282ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/firewire3-0.5.nm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(4093ul, model->getNumberOfStates());
EXPECT_EQ(5585ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-2.nm");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(37ul, model->getNumberOfStates());
@ -119,7 +119,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Mdp) {
}
TEST(ExplicitJitJaniModelBuilderTest, Ma) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/simple.ma");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/simple.ma");
storm::jani::Model janiModel = program.toJani();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
@ -128,7 +128,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) {
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_CPP_TESTS_BASE_PATH "/functional/builder/hybrid_states.ma");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/hybrid_states.ma");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(5ul, model->getNumberOfStates());
@ -136,7 +136,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) {
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_CPP_TESTS_BASE_PATH "/functional/builder/stream2.ma");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/stream2.ma");
janiModel = program.toJani();
model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
EXPECT_EQ(12ul, model->getNumberOfStates());
@ -146,14 +146,14 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) {
}
TEST(ExplicitJitJaniModelBuilderTest, FailComposition) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/system_composition.nm");
storm::jani::Model janiModel = program.toJani();
ASSERT_THROW(storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build(), storm::exceptions::WrongFormatException);
}
TEST(ExplicitJitJaniModelBuilderTest, IllegalSynchronizingWrites) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2-illegalSynchronizingWrite.nm");
storm::jani::Model janiModel = program.toJani();
storm::builder::BuilderOptions options;
options.setExplorationChecks(true);

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

@ -9,28 +9,28 @@
#include "storm/settings/modules/IOSettings.h"
TEST(ExplicitPrismModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/brp-16-2.pm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/nand-5-2.pm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(1728ul, model->getNumberOfStates());
EXPECT_EQ(2505ul, model->getNumberOfTransitions());
@ -40,68 +40,68 @@ TEST(ExplicitPrismModelBuilderTest, Ctmc) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/fms2.sm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions());
}
TEST(ExplicitPrismModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader3.nm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(364ul, model->getNumberOfStates());
EXPECT_EQ(654ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2.nm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(272ul, model->getNumberOfStates());
EXPECT_EQ(492ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/csma2-2.nm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(1038ul, model->getNumberOfStates());
EXPECT_EQ(1282ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/firewire3-0.5.nm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(4093ul, model->getNumberOfStates());
EXPECT_EQ(5585ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-2.nm");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(37ul, model->getNumberOfStates());
EXPECT_EQ(59ul, model->getNumberOfTransitions());
}
TEST(ExplicitPrismModelBuilderTest, Ma) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/simple.ma");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/simple.ma");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(5ul, model->getNumberOfStates());
@ -109,14 +109,14 @@ TEST(ExplicitPrismModelBuilderTest, Ma) {
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_CPP_TESTS_BASE_PATH "/functional/builder/hybrid_states.ma");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/hybrid_states.ma");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
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_CPP_TESTS_BASE_PATH "/functional/builder/stream2.ma");
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/stream2.ma");
model = storm::builder::ExplicitModelBuilder<double>(program).build();
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(14ul, model->getNumberOfTransitions());
@ -125,7 +125,7 @@ TEST(ExplicitPrismModelBuilderTest, Ma) {
}
TEST(ExplicitPrismModelBuilderTest, FailComposition) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/system_composition.nm");
ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(program).build(), storm::exceptions::WrongFormatException);
}

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

@ -65,7 +65,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) {
#ifdef STORM_HAVE_CARL
TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::generator::NextStateGeneratorOptions options;
options.setBuildAllLabels().setBuildAllRewardModels();
@ -115,7 +115,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) {
}
TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/parametric_die.pm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/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();
@ -399,7 +399,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, LRA) {
}
TEST(EigenDtmcPrctlModelCheckerTest, Conditional) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/test_conditional.pm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/modelchecker/test_conditional.pm");
storm::generator::NextStateGeneratorOptions options;
options.setBuildAllLabels().setBuildAllRewardModels();

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

@ -25,7 +25,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -102,7 +102,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -164,7 +164,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -205,7 +205,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula const> formula(nullptr);

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

@ -292,7 +292,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) {
}
TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/test_conditional.pm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/modelchecker/test_conditional.pm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(true, true)).build();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);

16
src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
View File

@ -28,7 +28,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -126,7 +126,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -224,7 +224,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -304,7 +304,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -384,7 +384,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -421,7 +421,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -465,7 +465,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -554,7 +554,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula const> formula(nullptr);

12
src/test/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
View File

@ -21,7 +21,7 @@
TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -85,7 +85,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) {
}
TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -149,7 +149,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
}
TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -196,7 +196,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) {
}
TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -243,7 +243,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
}
TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -298,7 +298,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
}
TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.

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

@ -22,7 +22,7 @@
#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -121,7 +121,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
}
TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -219,7 +219,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
}
TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader4.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -299,7 +299,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
}
TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader4.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.

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

@ -192,7 +192,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
}
TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/scheduler_generation.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/modelchecker/scheduler_generation.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
@ -244,7 +244,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) {
}
TEST(GmmxxMdpPrctlModelCheckerTest, TinyRewards) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/tiny_rewards.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/modelchecker/tiny_rewards.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;

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

@ -21,7 +21,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -90,7 +90,7 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -147,7 +147,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -181,7 +181,7 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);

16
src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
View File

@ -26,7 +26,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -124,7 +124,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/cluster2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -222,7 +222,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -302,7 +302,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/embedded2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -382,7 +382,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -419,7 +419,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/polling2.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -463,7 +463,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
@ -554,7 +554,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
// Parse the model description.
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/tandem5.sm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);

12
src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
View File

@ -19,7 +19,7 @@
#include "storm/settings/modules/NativeEquationSolverSettings.h"
TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_CUDD) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -81,7 +81,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_CUDD) {
}
TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -143,7 +143,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
}
TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_CUDD) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -188,7 +188,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_CUDD) {
}
TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -233,7 +233,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
}
TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_CUDD) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -286,7 +286,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_CUDD) {
}
TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.

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

@ -20,7 +20,7 @@
#include "storm/settings/modules/NativeEquationSolverSettings.h"
TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -117,7 +117,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
}
TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -214,7 +214,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
}
TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader4.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -294,7 +294,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
}
TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader4.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.

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

@ -13,7 +13,7 @@
#include "storm/models/sparse/StandardRewardModel.h"
TEST(SparseExplorationModelCheckerTest, Dice) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
@ -65,7 +65,7 @@ TEST(SparseExplorationModelCheckerTest, Dice) {
TEST(SparseExplorationModelCheckerTest, AsynchronousLeader) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader4.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;

12
src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
View File

@ -19,7 +19,7 @@
#include "storm/settings/modules/GeneralSettings.h"
TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -81,7 +81,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) {
}
TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -144,7 +144,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {
}
TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -189,7 +189,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
}
TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -237,7 +237,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
}
TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -290,7 +290,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
}
TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.

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

@ -19,7 +19,7 @@
#include "storm/settings/modules/GeneralSettings.h"
TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -117,7 +117,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) {
}
TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -215,7 +215,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) {
}
TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader4.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
@ -295,7 +295,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
}
TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader4.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.

26
src/test/parser/AtomicPropositionLabelingParserTest.cpp
View File

@ -24,7 +24,7 @@ TEST(AtomicPropositionLabelingParserTest, BasicParsing) {
// This test is based on a test case from the original MRMC.
// Parsing the file
storm::models::sparse::StateLabeling labeling = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(12, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general.lab");
storm::models::sparse::StateLabeling labeling = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(12, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general.lab");
// Checking whether all propositions are in the labelling
@ -81,27 +81,27 @@ TEST(AtomicPropositionLabelingParserTest, BasicParsing) {
TEST(AtomicPropositionLabelingParserTest, NoDeclarationTagHeader) {
// No #DECLARATION tag in file
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/noDeclarationTag.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/labParser/noDeclarationTag.lab"), storm::exceptions::WrongFormatException);
}
TEST(AtomicPropositionLabelingParserTest, NoEndTagHeader) {
// No #END tag in file.
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/noEndTag.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/labParser/noEndTag.lab"), storm::exceptions::WrongFormatException);
}
TEST(AtomicPropositionLabelingParserTest, MisspelledDeclarationTagHeader) {
// The #DECLARATION tag is misspelled.
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/declarationMisspell.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/labParser/declarationMisspell.lab"), storm::exceptions::WrongFormatException);
}
TEST(AtomicPropositionLabelingParserTest, MisspelledEndTagHeader) {
// The #END tag is misspelled.
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/endMisspell.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/labParser/endMisspell.lab"), storm::exceptions::WrongFormatException);
}
TEST(AtomicPropositionLabelingParserTest, NoLabelDeclaredNoneGiven) {
// No label between #DECLARATION and #END and no labels given.
storm::models::sparse::StateLabeling labeling = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(13, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/noLabelsDecNoneGiven.lab");
storm::models::sparse::StateLabeling labeling = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(13, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/labParser/noLabelsDecNoneGiven.lab");
ASSERT_EQ(0ul, labeling.getNumberOfLabels());
for(uint_fast64_t i = 0; i < 13; i++) {
ASSERT_TRUE(labeling.getLabelsOfState(i).empty());
@ -110,36 +110,36 @@ TEST(AtomicPropositionLabelingParserTest, NoLabelDeclaredNoneGiven) {
TEST(AtomicPropositionLabelingParserTest, UndeclaredLabelsGiven) {
// Undeclared labels given.
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/undeclaredLabelsGiven.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/labParser/undeclaredLabelsGiven.lab"), storm::exceptions::WrongFormatException);
}
TEST(AtomicPropositionLabelingParserTest, LabelForNonExistentState) {
// The index of one of the state that are to be labeled is higher than the number of states in the model.
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/labelForNonexistentState.lab"), storm::exceptions::OutOfRangeException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/labParser/labelForNonexistentState.lab"), storm::exceptions::OutOfRangeException);
}
// Note: As implemented at the moment, each label given for a state in any line is set to true for that state (logical or over all lines for that state).
// This behavior might not be ideal as multiple lines for one state are not necessary and might indicate a corrupt or wrong file.
TEST(AtomicPropositionLabelingParserTest, DoubledLines) {
// There are multiple lines attributing labels to the same state.
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(6, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/doubledLines.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(6, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/labParser/doubledLines.lab"), storm::exceptions::WrongFormatException);
// There is a line for a state that has been skipped.
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(6, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/doubledLinesSkipped.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(6, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/labParser/doubledLinesSkipped.lab"), storm::exceptions::WrongFormatException);
}
TEST(AtomicPropositionLabelingParserTest, WrongProposition) {
// Swapped the state index and the label at one entry.
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/swappedStateAndProposition.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/labParser/swappedStateAndProposition.lab"), storm::exceptions::WrongFormatException);
}
TEST(AtomicPropositionLabelingParserTest, Whitespaces) {
// Different configurations of allowed whitespaces are tested.
// First parse the labeling file without added whitespaces and obtain the hash of its parsed representation.
storm::models::sparse::StateLabeling labeling = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(13, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/withoutWhitespaces.lab");
storm::models::sparse::StateLabeling labeling = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(13, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/labParser/withoutWhitespaces.lab");
// Now parse the labeling file with the added whitespaces and compare the hashes.
storm::models::sparse::StateLabeling labeling2 = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(13, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/withWhitespaces.lab");
storm::models::sparse::StateLabeling labeling2 = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(13, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/labParser/withWhitespaces.lab");
ASSERT_TRUE(labeling == labeling2);
}

14
src/test/parser/AutoParserTest.cpp
View File

@ -13,7 +13,7 @@ TEST(AutoParserTest, NonExistingFile) {
TEST(AutoParserTest, BasicParsing) {
// Parse model, which is a Dtmc.
std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/dtmc.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab");
std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/autoParser/dtmc.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/autoParser.lab");
// Test if parsed correctly.
ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType());
@ -26,40 +26,40 @@ TEST(AutoParserTest, BasicParsing) {
TEST(AutoParserTest, WrongHint) {
// The hint given describes the content but does not conform to the format.
ASSERT_THROW(storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/wrongHint.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/autoParser/wrongHint.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/autoParser.lab"), storm::exceptions::WrongFormatException);
}
TEST(AutoParserTest, NoHint) {
// There is no hint contained in the given file, so the parser cannot decide which kind of model it is.
ASSERT_THROW(storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/noHint.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/autoParser/noHint.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/autoParser.lab"), storm::exceptions::WrongFormatException);
}
TEST(AutoParserTest, Decision) {
// Test if the AutoParser recognizes each model kind and correctly parses it.
// Dtmc
std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/dtmc.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab");
std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/autoParser/dtmc.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/autoParser.lab");
ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType());
ASSERT_EQ(12ul, modelPtr->getNumberOfStates());
ASSERT_EQ(26ul, modelPtr->getNumberOfTransitions());
// Ctmc
modelPtr.reset();
modelPtr = storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/ctmc.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab");
modelPtr = storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/autoParser/ctmc.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/autoParser.lab");
ASSERT_EQ(storm::models::ModelType::Ctmc, modelPtr->getType());
ASSERT_EQ(12ul, modelPtr->getNumberOfStates());
ASSERT_EQ(26ul, modelPtr->getNumberOfTransitions());
// Mdp
modelPtr.reset();
modelPtr = storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/mdp.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab");
modelPtr = storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/autoParser/mdp.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/autoParser.lab");
ASSERT_EQ(storm::models::ModelType::Mdp, modelPtr->getType());
ASSERT_EQ(12ul, modelPtr->getNumberOfStates());
ASSERT_EQ(28ul, modelPtr->getNumberOfTransitions());
// MA
modelPtr.reset();
modelPtr = storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/ma.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab");
modelPtr = storm::parser::AutoParser<>::parseModel(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/autoParser/ma.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/autoParser.lab");
ASSERT_EQ(storm::models::ModelType::MarkovAutomaton, modelPtr->getType());
ASSERT_EQ(12ul, modelPtr->getNumberOfStates());
ASSERT_EQ(27ul, modelPtr->getNumberOfTransitions());

12
src/test/parser/DeterministicModelParserTest.cpp
View File

@ -21,7 +21,7 @@ TEST(DeterministicModelParserTest, NonExistingFile) {
TEST(DeterministicModelParserTest, BasicDtmcParsing) {
// Parse a Dtmc and check the result.
storm::models::sparse::Dtmc<double> dtmc(storm::parser::DeterministicModelParser<>::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew"));
storm::models::sparse::Dtmc<double> dtmc(storm::parser::DeterministicModelParser<>::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_general.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/dtmc_general.lab", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/dtmc_general.state.rew", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/dtmc_general.trans.rew"));
ASSERT_EQ(8ul, dtmc.getNumberOfStates());
ASSERT_EQ(16ul, dtmc.getNumberOfTransitions());
@ -52,7 +52,7 @@ TEST(DeterministicModelParserTest, BasicDtmcParsing) {
TEST(DeterministicModelParserTest, BasicCtmcParsing) {
// Parse a Ctmc and check the result.
storm::models::sparse::Ctmc<double> ctmc(storm::parser::DeterministicModelParser<>::parseCtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew"));
storm::models::sparse::Ctmc<double> ctmc(storm::parser::DeterministicModelParser<>::parseCtmc(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_general.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/dtmc_general.lab", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/dtmc_general.state.rew", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/dtmc_general.trans.rew"));
ASSERT_EQ(8ul, ctmc.getNumberOfStates());
ASSERT_EQ(16ul, ctmc.getNumberOfTransitions());
@ -85,14 +85,14 @@ TEST(DeterministicModelParserTest, MismatchedFiles) {
// Test file combinations that do not match, i.e. differing number of states, transitions, etc.
// The labeling file contains a label for a non existent state.
ASSERT_THROW(storm::parser::DeterministicModelParser<>::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_general.lab"), storm::exceptions::OutOfRangeException);
ASSERT_THROW(storm::parser::DeterministicModelParser<>::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/dtmc_general.lab"), storm::exceptions::OutOfRangeException);
// The state reward file contains a reward for a non existent state.
ASSERT_THROW(storm::parser::DeterministicModelParser<>::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_mismatched.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.state.rew"), storm::exceptions::OutOfRangeException);
ASSERT_THROW(storm::parser::DeterministicModelParser<>::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/dtmc_mismatched.lab", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/dtmc_general.state.rew"), storm::exceptions::OutOfRangeException);
// The transition reward file contains rewards for a non existent state.
ASSERT_THROW(storm::parser::DeterministicModelParser<>::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_mismatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew"), storm::exceptions::OutOfRangeException);
ASSERT_THROW(storm::parser::DeterministicModelParser<>::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/dtmc_mismatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/dtmc_general.trans.rew"), storm::exceptions::OutOfRangeException);
// The transition reward file contains rewards for a non existent transition
ASSERT_THROW(storm::parser::DeterministicModelParser<>::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_mismatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_mismatched.trans.rew"), storm::exceptions::OutOfRangeException);
ASSERT_THROW(storm::parser::DeterministicModelParser<>::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/dtmc_mismatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/dtmc_mismatched.trans.rew"), storm::exceptions::OutOfRangeException);
}

30
src/test/parser/DeterministicSparseTransitionParserTest.cpp
View File

@ -30,7 +30,7 @@ TEST(DeterministicSparseTransitionParserTest, NonExistingFile) {
TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
// Parse a deterministic transitions file and test the resulting matrix.
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra");
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_general.tra");
ASSERT_EQ(8ul, transitionMatrix.getColumnCount());
ASSERT_EQ(21ul, transitionMatrix.getEntryCount());
@ -105,9 +105,9 @@ TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
TEST(DeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) {
// First parse a transition file. Then parse a transition reward file for the resulting transition matrix.
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra");
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_general.tra");
storm::storage::SparseMatrix<double> rewardMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew", transitionMatrix);
storm::storage::SparseMatrix<double> rewardMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/dtmc_general.trans.rew", transitionMatrix);
ASSERT_EQ(8ul, rewardMatrix.getColumnCount());
ASSERT_EQ(17ul, rewardMatrix.getEntryCount());
@ -171,22 +171,22 @@ TEST(DeterministicSparseTransitionParserTest, Whitespaces) {
// Test the resilience of the parser against whitespaces.
// Do so by comparing the hash of the matrix resulting from the file without whitespaces with the hash of the matrix resulting from the file with whitespaces.
uint_fast64_t correctHash = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra").hash();
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_whitespaces.tra");
uint_fast64_t correctHash = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_general.tra").hash();
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_whitespaces.tra");
ASSERT_EQ(correctHash, transitionMatrix.hash());
// Do the same for the corresponding transition rewards file (with and without whitespaces)
correctHash = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew", transitionMatrix).hash();
ASSERT_EQ(correctHash, storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_whitespaces.trans.rew", transitionMatrix).hash());
correctHash = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/dtmc_general.trans.rew", transitionMatrix).hash();
ASSERT_EQ(correctHash, storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/dtmc_whitespaces.trans.rew", transitionMatrix).hash());
}
TEST(DeterministicSparseTransitionParserTest, MixedTransitionOrder) {
// Since the MatrixBuilder needs sequential input of new elements reordering of transitions or states should throw an exception.
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mixedStateOrder.tra"), storm::exceptions::InvalidArgumentException);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_mixedStateOrder.tra"), storm::exceptions::InvalidArgumentException);
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra");
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_mixedStateOrder.trans.rew", transitionMatrix), storm::exceptions::InvalidArgumentException);
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_general.tra");
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/dtmc_mixedStateOrder.trans.rew", transitionMatrix), storm::exceptions::InvalidArgumentException);
}
TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) {
@ -194,7 +194,7 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) {
std::unique_ptr<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(false);
// Parse a transitions file with the fixDeadlocks Flag set and test if it works.
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra");
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_deadlock.tra");
ASSERT_EQ(9ul, transitionMatrix.getColumnCount());
ASSERT_EQ(23ul, transitionMatrix.getEntryCount());
@ -217,19 +217,19 @@ TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) {
// Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception.
std::unique_ptr<storm::settings::SettingMemento> dontFixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(true);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_deadlock.tra"), storm::exceptions::WrongFormatException);
}
TEST(DeterministicSparseTransitionParserTest, DoubledLines) {
// There is a redundant line in the transition file. As the transition already exists this should throw an exception.
// Note: If two consecutive lines are doubled no exception is thrown.
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_doubledLines.tra"), storm::exceptions::InvalidArgumentException);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_doubledLines.tra"), storm::exceptions::InvalidArgumentException);
}
TEST(DeterministicSparseTransitionParserTest, RewardForNonExistentTransition) {
// First parse a transition file. Then parse a transition reward file for the resulting transition matrix.
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra");
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/dtmc_general.tra");
// There is a reward for a transition that does not exist in the transition matrix.
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_rewardForNonExTrans.trans.rew", transitionMatrix), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/dtmc_rewardForNonExTrans.trans.rew", transitionMatrix), storm::exceptions::WrongFormatException);
}

6
src/test/parser/MappedFileTest.cpp
View File

@ -21,7 +21,7 @@ TEST(MappedFileTest, NonExistingFile) {
TEST(MappedFileTest, BasicFunctionality) {
// Open a file and test if the content is loaded as expected.
storm::parser::MappedFile file(STORM_CPP_TESTS_BASE_PATH "/functional/parser/testStringFile.txt");
storm::parser::MappedFile file(STORM_CPP_TESTS_BASE_PATH "/parser/testStringFile.txt");
std::string testString = "This is a test string.";
char const* dataPtr = file.getData();
for(char const* testStringPtr = testString.c_str(); testStringPtr - testString.c_str() < 22; testStringPtr++) {
@ -41,12 +41,12 @@ TEST(MappedFileTest, ExistsAndReadble) {
// Test the fileExistsAndIsReadable() method under various circumstances.
// File exists and is readable.
ASSERT_TRUE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_CPP_TESTS_BASE_PATH "/functional/parser/testStringFile.txt"));
ASSERT_TRUE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_CPP_TESTS_BASE_PATH "/parser/testStringFile.txt"));
// File does not exist.
ASSERT_FALSE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"));
// File exists but is not readable.
// TODO: Find portable solution to providing a situation in which a file exists but is not readable.
//ASSERT_FALSE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_CPP_TESTS_BASE_PATH "/functional/parser/unreadableFile.txt"));
//ASSERT_FALSE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_CPP_TESTS_BASE_PATH "/parser/unreadableFile.txt"));
}

6
src/test/parser/MarkovAutomatonParserTest.cpp
View File

@ -13,7 +13,7 @@ TEST(MarkovAutomatonParserTest, NonExistingFile) {
TEST(MarkovAutomatonParserTest, BasicParsing) {
// Get the parsing result.
storm::models::sparse::MarkovAutomaton<double> result = storm::parser::MarkovAutomatonParser<>::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/ma_general.state.rew");
storm::models::sparse::MarkovAutomaton<double> result = storm::parser::MarkovAutomatonParser<>::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/ma_general.lab", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/ma_general.state.rew");
// Test sizes and counts.
ASSERT_EQ(6ul, result.getNumberOfStates());
@ -57,8 +57,8 @@ TEST(MarkovAutomatonParserTest, MismatchedFiles) {
// Test file combinations that do not match, i.e. differing number of states, transitions, etc.
// The labeling file contains a label for a non existent state.
ASSERT_THROW(storm::parser::MarkovAutomatonParser<>::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_mismatched.lab"), storm::exceptions::OutOfRangeException);
ASSERT_THROW(storm::parser::MarkovAutomatonParser<>::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/ma_mismatched.lab"), storm::exceptions::OutOfRangeException);
// The state reward file contains a reward for a non existent state.
ASSERT_THROW(storm::parser::MarkovAutomatonParser<>::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/ma_mismatched.state.rew"), storm::exceptions::OutOfRangeException);
ASSERT_THROW(storm::parser::MarkovAutomatonParser<>::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/ma_general.lab", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/ma_mismatched.state.rew"), storm::exceptions::OutOfRangeException);
}

8
src/test/parser/MarkovAutomatonSparseTransitionParserTest.cpp
View File

@ -31,7 +31,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, NonExistingFile) {
TEST(MarkovAutomatonSparseTransitionParserTest, BasicParsing) {
// The file that will be used for the test.
std::string filename = STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general.tra";
std::string filename = STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/ma_general.tra";
// Execute the parser.
typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result = storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(filename);
@ -109,7 +109,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, BasicParsing) {
TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) {
// The file that will be used for the test.
std::string filename = STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_whitespaces.tra";
std::string filename = STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/ma_whitespaces.tra";
// Execute the parser.
typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result = storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(filename);
@ -190,7 +190,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) {
std::unique_ptr<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(false);
// Parse a Markov Automaton transition file with the fixDeadlocks Flag set and test if it works.
typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result = storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock.tra");
typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result = storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/ma_deadlock.tra");
// Test if the result is consistent with the parsed Markov Automaton.
storm::storage::SparseMatrix<double> resultMatrix(result.transitionMatrixBuilder.build());
@ -208,5 +208,5 @@ TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) {
// Try to parse a Markov Automaton transition file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception.
std::unique_ptr<storm::settings::SettingMemento> dontFixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(true);
ASSERT_THROW(storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock.tra"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/ma_deadlock.tra"), storm::exceptions::WrongFormatException);
}

10
src/test/parser/NondeterministicModelParserTest.cpp
View File

@ -16,7 +16,7 @@ TEST(NondeterministicModelParserTest, NonExistingFile) {
TEST(NondeterministicModelParserTest, BasicMdpParsing) {
// Parse a Mdp and check the result.
storm::models::sparse::Mdp<double> mdp(storm::parser::NondeterministicModelParser<>::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew"));
storm::models::sparse::Mdp<double> mdp(storm::parser::NondeterministicModelParser<>::parseMdp(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/mdp_general.lab", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/mdp_general.state.rew", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/mdp_general.trans.rew"));
ASSERT_EQ(6ul, mdp.getNumberOfStates());
ASSERT_EQ(22ul, mdp.getNumberOfTransitions());
@ -50,14 +50,14 @@ TEST(NondeterministicModelParserTest, MismatchedFiles) {
// Test file combinations that do not match, i.e. differing number of states, transitions, etc.
// The labeling file contains a label for a non existent state.
ASSERT_THROW(storm::parser::NondeterministicModelParser<>::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_general.lab"), storm::exceptions::OutOfRangeException);
ASSERT_THROW(storm::parser::NondeterministicModelParser<>::parseMdp(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/mdp_general.lab"), storm::exceptions::OutOfRangeException);
// The state reward file contains a reward for a non existent state.
ASSERT_THROW(storm::parser::NondeterministicModelParser<>::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_mismatched.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.state.rew"), storm::exceptions::OutOfRangeException);
ASSERT_THROW(storm::parser::NondeterministicModelParser<>::parseMdp(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/mdp_mismatched.lab", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/mdp_general.state.rew"), storm::exceptions::OutOfRangeException);
// The transition reward file contains rewards for a non existent state.
ASSERT_THROW(storm::parser::NondeterministicModelParser<>::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_mismatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew"), storm::exceptions::OutOfRangeException);
ASSERT_THROW(storm::parser::NondeterministicModelParser<>::parseMdp(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/mdp_mismatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/mdp_general.trans.rew"), storm::exceptions::OutOfRangeException);
// The transition reward file contains rewards for a non existent transition
ASSERT_THROW(storm::parser::NondeterministicModelParser<>::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_mismatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_mismatched.trans.rew"), storm::exceptions::OutOfRangeException);
ASSERT_THROW(storm::parser::NondeterministicModelParser<>::parseMdp(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/mdp_mismatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/mdp_mismatched.trans.rew"), storm::exceptions::OutOfRangeException);
}

30
src/test/parser/NondeterministicSparseTransitionParserTest.cpp
View File

@ -31,7 +31,7 @@ TEST(NondeterministicSparseTransitionParserTest, NonExistingFile) {
TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
// Parse a nondeterministic transitions file and test the result.
storm::storage::SparseMatrix<double> result(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra"));
storm::storage::SparseMatrix<double> result(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general.tra"));
// Test the row mapping, i.e. at which row which state starts.
ASSERT_EQ(6ul, result.getRowGroupCount());
@ -121,8 +121,8 @@ TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) {
// Parse a nondeterministic transitions file and test the result.
storm::storage::SparseMatrix<double> modelInformation(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra"));
storm::storage::SparseMatrix<double> result(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew", modelInformation));
storm::storage::SparseMatrix<double> modelInformation(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general.tra"));
storm::storage::SparseMatrix<double> result(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/mdp_general.trans.rew", modelInformation));
// Test the transition matrix.
ASSERT_EQ(6ul, result.getColumnCount());
@ -187,8 +187,8 @@ TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing)
TEST(NondeterministicSparseTransitionParserTest, Whitespaces) {
// Test the resilience of the parser against whitespaces.
// Do so by comparing the hashes of the transition matices and the rowMapping vectors element by element.
storm::storage::SparseMatrix<double> correctResult(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra"));
storm::storage::SparseMatrix<double> whitespaceResult = storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_whitespaces.tra");
storm::storage::SparseMatrix<double> correctResult(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general.tra"));
storm::storage::SparseMatrix<double> whitespaceResult = storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_whitespaces.tra");
ASSERT_EQ(correctResult.hash(), whitespaceResult.hash());
ASSERT_EQ(correctResult.getRowGroupIndices().size(), whitespaceResult.getRowGroupIndices().size());
for(uint_fast64_t i = 0; i < correctResult.getRowGroupIndices().size(); i++) {
@ -196,16 +196,16 @@ TEST(NondeterministicSparseTransitionParserTest, Whitespaces) {
}
// Do the same (minus the unused rowMapping) for the corresponding transition rewards file (with and without whitespaces)
uint_fast64_t correctHash = storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew", correctResult).hash();
ASSERT_EQ(correctHash, storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_whitespaces.trans.rew", whitespaceResult).hash());
uint_fast64_t correctHash = storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/mdp_general.trans.rew", correctResult).hash();
ASSERT_EQ(correctHash, storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/mdp_whitespaces.trans.rew", whitespaceResult).hash());
}
TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) {
// Since the MatrixBuilder needs sequential input of new elements reordering of transitions or states should throw an exception.
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mixedStateOrder.tra"), storm::exceptions::InvalidArgumentException);
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_mixedStateOrder.tra"), storm::exceptions::InvalidArgumentException);
storm::storage::SparseMatrix<double> modelInformation = storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra");
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_mixedStateOrder.trans.rew", modelInformation), storm::exceptions::InvalidArgumentException);
storm::storage::SparseMatrix<double> modelInformation = storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general.tra");
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/mdp_mixedStateOrder.trans.rew", modelInformation), storm::exceptions::InvalidArgumentException);
}
TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) {
@ -213,7 +213,7 @@ TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) {
std::unique_ptr<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(false);
// Parse a transitions file with the fixDeadlocks Flag set and test if it works.
storm::storage::SparseMatrix<double> result(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra"));
storm::storage::SparseMatrix<double> result(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_deadlock.tra"));
ASSERT_EQ(8ul, result.getRowGroupIndices().size());
ASSERT_EQ(9ul, result.getRowGroupIndices()[5]);
@ -253,19 +253,19 @@ TEST(NondeterministicSparseTransitionParserTest, DontFixDeadlocks) {
// Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception.
std::unique_ptr<storm::settings::SettingMemento> dontFixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(true);
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_deadlock.tra"), storm::exceptions::WrongFormatException);
}
TEST(NondeterministicSparseTransitionParserTest, DoubledLines) {
// There is a redundant line in the transition file. As the transition already exists this should throw an exception.
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_doubledLines.tra"), storm::exceptions::InvalidArgumentException);
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_doubledLines.tra"), storm::exceptions::InvalidArgumentException);
}
TEST(NondeterministicSparseTransitionParserTest, RewardForNonExistentTransition) {
// First parse a transition file. Then parse a transition reward file for the resulting transition matrix.
storm::storage::SparseMatrix<double> transitionResult = storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra");
storm::storage::SparseMatrix<double> transitionResult = storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general.tra");
// There is a reward for a transition that does not exist in the transition matrix.
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_rewardForNonExTrans.trans.rew", transitionResult), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/mdp_rewardForNonExTrans.trans.rew", transitionResult), storm::exceptions::WrongFormatException);
}

18
src/test/parser/PrismParserTest.cpp
View File

@ -4,15 +4,15 @@
TEST(PrismParser, StandardModelTest) {
storm::prism::Program result;
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/crowds5_5.pm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/csma2_2.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/firewire.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3_5.pm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/two_dice.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/coin2.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/crowds5_5.pm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/csma2_2.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/die.pm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/firewire.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/leader3.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/leader3_5.pm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/two_dice.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/wlan0_collide.nm"));
}
TEST(PrismParser, SimpleTest) {

10
src/test/parser/SparseStateRewardParserTest.cpp
View File

@ -30,7 +30,7 @@ double round(double val, int precision) {
TEST(SparseStateRewardParserTest, BasicParsing) {
// Get the parsing result.
std::vector<double> result = storm::parser::SparseStateRewardParser<>::parseSparseStateReward(100, STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/state_reward_parser_basic.state.rew");
std::vector<double> result = storm::parser::SparseStateRewardParser<>::parseSparseStateReward(100, STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/state_reward_parser_basic.state.rew");
// Now test if the correct value were parsed.
for (int i = 0; i < 100; i++) {
@ -41,7 +41,7 @@ TEST(SparseStateRewardParserTest, BasicParsing) {
TEST(SparseStateRewardParserTest, Whitespaces) {
// Get the parsing result.
std::vector<double> result = storm::parser::SparseStateRewardParser<>::parseSparseStateReward(100, STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/state_reward_parser_whitespaces.state.rew");
std::vector<double> result = storm::parser::SparseStateRewardParser<>::parseSparseStateReward(100, STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/state_reward_parser_whitespaces.state.rew");
// Now test if the correct value were parsed.
for (int i = 0; i < 100; i++) {
@ -51,13 +51,13 @@ TEST(SparseStateRewardParserTest, Whitespaces) {
TEST(SparseStateRewardParserTest, DoubledLines) {
// There are multiple lines attributing a reward to the same state.
ASSERT_THROW(storm::parser::SparseStateRewardParser<>::parseSparseStateReward(11, STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/state_reward_parser_doubledLines.state.rew"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::SparseStateRewardParser<>::parseSparseStateReward(11, STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/state_reward_parser_doubledLines.state.rew"), storm::exceptions::WrongFormatException);
// There is a line for a state that has been skipped.
ASSERT_THROW(storm::parser::SparseStateRewardParser<>::parseSparseStateReward(11, STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/state_reward_parser_doubledLinesSkipped.state.rew"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::SparseStateRewardParser<>::parseSparseStateReward(11, STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/state_reward_parser_doubledLinesSkipped.state.rew"), storm::exceptions::WrongFormatException);
}
TEST(SparseStateRewardParserTest, RewardForNonExistentState) {
// The index of one of the state that are to be given rewards is higher than the number of states in the model.
ASSERT_THROW(storm::parser::SparseStateRewardParser<>::parseSparseStateReward(99, STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/state_reward_parser_basic.state.rew"), storm::exceptions::OutOfRangeException);
ASSERT_THROW(storm::parser::SparseStateRewardParser<>::parseSparseStateReward(99, STORM_CPP_TESTS_BASE_PATH "/parser/rew_files/state_reward_parser_basic.state.rew"), storm::exceptions::OutOfRangeException);
}

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

@ -13,7 +13,7 @@
#ifdef STORM_HAVE_GUROBI
TEST(MilpPermissiveSchedulerTest, DieSelection) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_c1.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die_c1.nm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
auto formula02 = formulaParser.parseSingleFormulaFromString("P>=0.10 [ F \"one\"]")->asProbabilityOperatorFormula();

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

@ -14,7 +14,7 @@
#if defined(STORM_HAVE_MSAT) || defined(STORM_HAVE_Z3)
TEST(SmtPermissiveSchedulerTest, DieSelection) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_c1.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die_c1.nm");
storm::parser::FormulaParser formulaParser(program);
// auto formula02 = formulaParser.parseSingleFormulaFromString("P>=0.10 [ F \"one\"]")->asProbabilityOperatorFormula();

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

@ -11,7 +11,7 @@
#include "storm/models/sparse/StandardRewardModel.h"
TEST(NondeterministicModelBisimulationDecomposition, TwoDice) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/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();

16
src/test/storage/PrismProgramTest.cpp
View File

@ -9,7 +9,7 @@
#ifdef STORM_HAVE_MSAT
TEST(PrismProgramTest, FlattenModules) {
storm::prism::Program result;
ASSERT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm"));
ASSERT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/leader3.nm"));
std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory(new storm::utility::solver::MathsatSmtSolverFactory());
@ -17,7 +17,7 @@ TEST(PrismProgramTest, FlattenModules) {
EXPECT_EQ(1, result.getNumberOfModules());
EXPECT_EQ(74, result.getModule(0).getNumberOfCommands());
ASSERT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm"));
ASSERT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/wlan0_collide.nm"));
ASSERT_NO_THROW(result = result.flattenModules(smtSolverFactory));
EXPECT_EQ(1, result.getNumberOfModules());
@ -29,21 +29,21 @@ TEST(PrismProgramTest, ConvertToJani) {
storm::prism::Program prismProgram;
storm::jani::Model janiModel;
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm"));
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/leader3.nm"));
ASSERT_NO_THROW(janiModel = prismProgram.toJani());
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm"));
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/parser/prism/wlan0_collide.nm"));
ASSERT_NO_THROW(janiModel = prismProgram.toJani());
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"));
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/brp-16-2.pm"));
ASSERT_NO_THROW(janiModel = prismProgram.toJani());
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"));
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm"));
ASSERT_NO_THROW(janiModel = prismProgram.toJani());
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"));
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm"));
ASSERT_NO_THROW(janiModel = prismProgram.toJani());
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"));
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/nand-5-2.pm"));
ASSERT_NO_THROW(janiModel = prismProgram.toJani());
}

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

@ -17,7 +17,7 @@
#include "storm/storage/dd/DdManager.h"
TEST(GraphTest, SymbolicProb01_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
@ -39,7 +39,7 @@ TEST(GraphTest, SymbolicProb01_Cudd) {
}
TEST(GraphTest, SymbolicProb01_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
@ -61,7 +61,7 @@ TEST(GraphTest, SymbolicProb01_Sylvan) {
}
TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader3.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
@ -79,7 +79,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount());
}
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
@ -105,7 +105,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount());
}
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/csma2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
@ -125,7 +125,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
}
TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader3.nm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
@ -143,7 +143,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount());
}
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
@ -169,7 +169,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount());
}
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/csma2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
@ -189,7 +189,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
}
TEST(GraphTest, ExplicitProb01) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/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();
@ -211,7 +211,7 @@ TEST(GraphTest, ExplicitProb01) {
}
TEST(GraphTest, ExplicitProb01MinMax) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/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();
@ -227,7 +227,7 @@ TEST(GraphTest, ExplicitProb01MinMax) {
EXPECT_EQ(0ul, statesWithProbability01.first.getNumberOfSetBits());
EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/coin2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
@ -249,7 +249,7 @@ TEST(GraphTest, ExplicitProb01MinMax) {
EXPECT_EQ(83ul, statesWithProbability01.first.getNumberOfSetBits());
EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/csma2-2.nm");
program = modelDescription.preprocess().asPrismProgram();
model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();

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

@ -20,7 +20,7 @@
TEST(ModelInstantiatorTest, BrpProb) {
carl::VariablePool::getInstance().clear();
std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm";
std::string programFile = STORM_CPP_TESTS_BASE_PATH "/utility/brp16_2.pm";
std::string formulaAsString = "P=? [F s=5 ]";
// Program and formula
@ -138,7 +138,7 @@ TEST(ModelInstantiatorTest, BrpProb) {
TEST(ModelInstantiatorTest, Brp_Rew) {
carl::VariablePool::getInstance().clear();
std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm";
std::string programFile = STORM_CPP_TESTS_BASE_PATH "/utility/brp16_2.pm";
std::string formulaAsString = "R=? [F ((s=5) | (s=0&srep=3)) ]";
// Program and formula
@ -208,7 +208,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
TEST(ModelInstantiatorTest, Consensus) {
carl::VariablePool::getInstance().clear();
std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/coin2_2.pm";
std::string programFile = STORM_CPP_TESTS_BASE_PATH "/utility/coin2_2.pm";
std::string formulaAsString = "Pmin=? [F \"finished\"&\"all_coins_equal_1\" ]";
// Program and formula

Write Preview
|||||||
100:0
Loading…
Cancel
Save