diff --git a/src/test/builder/DdJaniModelBuilderTest.cpp b/src/test/builder/DdJaniModelBuilderTest.cpp
index 7e99bab6a..f5e858df0 100644
--- a/src/test/builder/DdJaniModelBuilderTest.cpp
+++ b/src/test/builder/DdJaniModelBuilderTest.cpp
@@ -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;
diff --git a/src/test/builder/DdPrismModelBuilderTest.cpp b/src/test/builder/DdPrismModelBuilderTest.cpp
index 771a77651..80d0c8894 100644
--- a/src/test/builder/DdPrismModelBuilderTest.cpp
+++ b/src/test/builder/DdPrismModelBuilderTest.cpp
@@ -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);
diff --git a/src/test/builder/ExplicitJaniModelBuilderTest.cpp b/src/test/builder/ExplicitJaniModelBuilderTest.cpp
index e1d16458b..b60de3b32 100644
--- a/src/test/builder/ExplicitJaniModelBuilderTest.cpp
+++ b/src/test/builder/ExplicitJaniModelBuilderTest.cpp
@@ -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);
diff --git a/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp b/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp
index 84551e1d1..47922cdc1 100644
--- a/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp
+++ b/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp
@@ -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);
diff --git a/src/test/builder/ExplicitPrismModelBuilderTest.cpp b/src/test/builder/ExplicitPrismModelBuilderTest.cpp
index 7de89918a..ef1ff7b22 100644
--- a/src/test/builder/ExplicitPrismModelBuilderTest.cpp
+++ b/src/test/builder/ExplicitPrismModelBuilderTest.cpp
@@ -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);
}
diff --git a/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
index 421a02bac..051da31c4 100644
--- a/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
+++ b/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
@@ -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();
diff --git a/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
index c0089989e..2ecb5466c 100644
--- a/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
+++ b/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
@@ -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);
diff --git a/src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
index 5fb94a691..aa04c70c6 100644
--- a/src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
+++ b/src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
@@ -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);
diff --git a/src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
index 9621793a2..4c16becc2 100644
--- a/src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
+++ b/src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
@@ -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);
diff --git a/src/test/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
index 08cabfe6d..b6984337c 100644
--- a/src/test/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
+++ b/src/test/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
@@ -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.
diff --git a/src/test/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/src/test/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
index db5a1c53e..0e6b52ada 100644
--- a/src/test/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
+++ b/src/test/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
@@ -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.
diff --git a/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
index 39ce2c2c7..bb2814569 100644
--- a/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
+++ b/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
@@ -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;
diff --git a/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp
index 37d9f7a55..7285c6420 100644
--- a/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp
+++ b/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp
@@ -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);
diff --git a/src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
index d10ad4de7..98304e6cf 100644
--- a/src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
+++ b/src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
@@ -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);
diff --git a/src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
index cc5312d47..a5cd89b2c 100644
--- a/src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
+++ b/src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
@@ -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.
diff --git a/src/test/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/src/test/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
index 4cd9ddea9..b6fc962e3 100644
--- a/src/test/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
+++ b/src/test/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
@@ -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.
diff --git a/src/test/modelchecker/SparseExplorationModelCheckerTest.cpp b/src/test/modelchecker/SparseExplorationModelCheckerTest.cpp
index fe9ea87d1..e73f203f2 100644
--- a/src/test/modelchecker/SparseExplorationModelCheckerTest.cpp
+++ b/src/test/modelchecker/SparseExplorationModelCheckerTest.cpp
@@ -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;
diff --git a/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
index 1a33562c9..b42efb432 100644
--- a/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
+++ b/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
@@ -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.
diff --git a/src/test/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/src/test/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
index a1916d44d..84e60f067 100644
--- a/src/test/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
+++ b/src/test/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
@@ -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.
diff --git a/src/test/parser/AtomicPropositionLabelingParserTest.cpp b/src/test/parser/AtomicPropositionLabelingParserTest.cpp
index 8bbeae9c4..7c9f3991a 100644
--- a/src/test/parser/AtomicPropositionLabelingParserTest.cpp
+++ b/src/test/parser/AtomicPropositionLabelingParserTest.cpp
@@ -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);
}
diff --git a/src/test/parser/AutoParserTest.cpp b/src/test/parser/AutoParserTest.cpp
index ebcc4c53e..383037880 100644
--- a/src/test/parser/AutoParserTest.cpp
+++ b/src/test/parser/AutoParserTest.cpp
@@ -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());
diff --git a/src/test/parser/DeterministicModelParserTest.cpp b/src/test/parser/DeterministicModelParserTest.cpp
index 2717359fa..4d4ab09c8 100644
--- a/src/test/parser/DeterministicModelParserTest.cpp
+++ b/src/test/parser/DeterministicModelParserTest.cpp
@@ -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);
}
diff --git a/src/test/parser/DeterministicSparseTransitionParserTest.cpp b/src/test/parser/DeterministicSparseTransitionParserTest.cpp
index 0da9e1b77..b2834d3d3 100644
--- a/src/test/parser/DeterministicSparseTransitionParserTest.cpp
+++ b/src/test/parser/DeterministicSparseTransitionParserTest.cpp
@@ -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);
}
diff --git a/src/test/parser/MappedFileTest.cpp b/src/test/parser/MappedFileTest.cpp
index 3f24ae547..73d7975f2 100644
--- a/src/test/parser/MappedFileTest.cpp
+++ b/src/test/parser/MappedFileTest.cpp
@@ -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"));
}
diff --git a/src/test/parser/MarkovAutomatonParserTest.cpp b/src/test/parser/MarkovAutomatonParserTest.cpp
index 7091253f9..4063afcb9 100644
--- a/src/test/parser/MarkovAutomatonParserTest.cpp
+++ b/src/test/parser/MarkovAutomatonParserTest.cpp
@@ -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);
}
diff --git a/src/test/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/src/test/parser/MarkovAutomatonSparseTransitionParserTest.cpp
index da317f32d..fd02dd652 100644
--- a/src/test/parser/MarkovAutomatonSparseTransitionParserTest.cpp
+++ b/src/test/parser/MarkovAutomatonSparseTransitionParserTest.cpp
@@ -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);
}
diff --git a/src/test/parser/NondeterministicModelParserTest.cpp b/src/test/parser/NondeterministicModelParserTest.cpp
index 51d0cec06..329541559 100644
--- a/src/test/parser/NondeterministicModelParserTest.cpp
+++ b/src/test/parser/NondeterministicModelParserTest.cpp
@@ -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);
}
diff --git a/src/test/parser/NondeterministicSparseTransitionParserTest.cpp b/src/test/parser/NondeterministicSparseTransitionParserTest.cpp
index 91a2961cf..a73b28e01 100644
--- a/src/test/parser/NondeterministicSparseTransitionParserTest.cpp
+++ b/src/test/parser/NondeterministicSparseTransitionParserTest.cpp
@@ -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);
}
diff --git a/src/test/parser/PrismParserTest.cpp b/src/test/parser/PrismParserTest.cpp
index 6ee1884ca..44abf1da5 100644
--- a/src/test/parser/PrismParserTest.cpp
+++ b/src/test/parser/PrismParserTest.cpp
@@ -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) {
diff --git a/src/test/parser/SparseStateRewardParserTest.cpp b/src/test/parser/SparseStateRewardParserTest.cpp
index 14f39ddc6..0f2f6856f 100644
--- a/src/test/parser/SparseStateRewardParserTest.cpp
+++ b/src/test/parser/SparseStateRewardParserTest.cpp
@@ -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);
}
diff --git a/src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
index a310e2950..26cf1f053 100644
--- a/src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
+++ b/src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
@@ -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();
diff --git a/src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
index 62aa3e308..200492041 100644
--- a/src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
+++ b/src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
@@ -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();
diff --git a/src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp
index 171e6d5a2..0186f640e 100644
--- a/src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp
+++ b/src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp
@@ -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();
diff --git a/src/test/storage/PrismProgramTest.cpp b/src/test/storage/PrismProgramTest.cpp
index 0f2ada511..eb7efb09c 100644
--- a/src/test/storage/PrismProgramTest.cpp
+++ b/src/test/storage/PrismProgramTest.cpp
@@ -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());
}
diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp
index 75b122905..ad213e5b2 100644
--- a/src/test/utility/GraphTest.cpp
+++ b/src/test/utility/GraphTest.cpp
@@ -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();
diff --git a/src/test/utility/ModelInstantiatorTest.cpp b/src/test/utility/ModelInstantiatorTest.cpp
index 06309490f..1e53008ff 100644
--- a/src/test/utility/ModelInstantiatorTest.cpp
+++ b/src/test/utility/ModelInstantiatorTest.cpp
@@ -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