From d22d1daaa6d583ae57372d62c59c62521f0142c9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 15 Sep 2016 19:35:03 +0200 Subject: [PATCH] adapted more tests Former-commit-id: 4d75a4fe5009fcd3b64abed2c55bce6e8fa987a5 [formerly ad1ad61873261e1442a037567f2180ba3678289d] Former-commit-id: d359f2c9c14f7ffa6c32537cdd67f9ac338a9e9c --- .../GmmxxHybridDtmcPrctlModelCheckerTest.cpp | 31 +++++++++------ .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 21 ++++++---- .../NativeHybridCtmcCslModelCheckerTest.cpp | 25 ++++++++---- .../NativeHybridDtmcPrctlModelCheckerTest.cpp | 21 ++++++---- .../NativeHybridMdpPrctlModelCheckerTest.cpp | 13 +++++-- .../SymbolicDtmcPrctlModelCheckerTest.cpp | 19 ++++++--- .../SymbolicMdpPrctlModelCheckerTest.cpp | 13 +++++-- test/functional/utility/GraphTest.cpp | 39 ++++++++++++------- 8 files changed, 119 insertions(+), 63 deletions(-) diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index ac2c7dcb7..53e992fd3 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -12,6 +12,7 @@ #include "src/builder/DdPrismModelBuilder.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/StandardRewardModel.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" @@ -19,8 +20,9 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) { - storm::prism::Program program = 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 "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -80,8 +82,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -141,8 +144,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { - storm::prism::Program program = 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 "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -185,8 +189,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -229,8 +234,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { - storm::prism::Program program = 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 "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -281,8 +287,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 1733fa40f..eb00b67cd 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -10,6 +10,7 @@ #include "src/parser/PrismParser.h" #include "src/parser/FormulaParser.h" #include "src/builder/DdPrismModelBuilder.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Mdp.h" #include "src/models/symbolic/StandardRewardModel.h" @@ -21,8 +22,9 @@ #include "src/settings/modules/GmmxxEquationSolverSettings.h" TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) { - storm::prism::Program program = 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 "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -118,8 +120,9 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) { } TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -215,8 +218,9 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { } TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::prism::Program program = 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 "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -294,8 +298,9 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { } TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 5f744cc68..5d8391f5c 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -6,6 +6,7 @@ #include "src/logic/Formulas.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/storage/dd/DdType.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/models/symbolic/StandardRewardModel.h" @@ -25,7 +26,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { std::unique_ptr 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::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -122,7 +124,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { std::unique_ptr 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::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -219,7 +222,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) { std::unique_ptr 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::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -298,7 +302,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { std::unique_ptr 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::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -377,7 +382,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) { std::unique_ptr 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::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -413,7 +419,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) { std::unique_ptr 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::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -456,7 +463,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) { std::unique_ptr 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::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -546,7 +554,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { std::unique_ptr 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::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index cd6d87afb..ac419c04b 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -4,6 +4,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/solver/NativeLinearEquationSolver.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -14,13 +15,12 @@ #include "src/models/symbolic/Dtmc.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" - #include "src/settings/modules/GmmxxEquationSolverSettings.h" - #include "src/settings/modules/NativeEquationSolverSettings.h" TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_CUDD) { - storm::prism::Program program = 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 "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -81,7 +81,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_CUDD) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -142,7 +143,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_CUDD) { - storm::prism::Program program = 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 "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -186,7 +188,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_CUDD) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -230,7 +233,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_CUDD) { - storm::prism::Program program = 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 "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -282,7 +286,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_CUDD) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index 1762c098f..1fe89c609 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -7,6 +7,7 @@ #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/parser/FormulaParser.h" #include "src/parser/PrismParser.h" #include "src/builder/DdPrismModelBuilder.h" @@ -19,7 +20,8 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { - storm::prism::Program program = 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 "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -115,7 +117,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { } TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -211,7 +214,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { } TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::prism::Program program = 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 "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -290,7 +294,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { } TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 3d1f3621f..c5ff7e1d1 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -4,6 +4,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/utility/solver.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" @@ -18,7 +19,8 @@ #include "src/settings/modules/GeneralSettings.h" TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) { - storm::prism::Program program = 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 "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -79,7 +81,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) { } TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -141,7 +144,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { } TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { - storm::prism::Program program = 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 "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -185,7 +189,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { } TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -232,7 +237,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { } TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { - storm::prism::Program program = 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 "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -284,7 +290,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { } TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index efe1b3283..ea024ccb7 100644 --- a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -3,6 +3,7 @@ #include "src/logic/Formulas.h" #include "src/utility/solver.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" @@ -18,7 +19,8 @@ #include "src/settings/modules/GeneralSettings.h" TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { - storm::prism::Program program = 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 "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -115,7 +117,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { } TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -212,7 +215,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { } TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::prism::Program program = 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 "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -291,7 +295,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { } TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 2813e1a9b..e8c2e26fc 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/parser/PrismParser.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Mdp.h" @@ -16,7 +17,8 @@ #include "src/storage/dd/DdManager.h" TEST(GraphTest, SymbolicProb01_Cudd) { - storm::prism::Program program = 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 "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -37,7 +39,8 @@ TEST(GraphTest, SymbolicProb01_Cudd) { } TEST(GraphTest, SymbolicProb01_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -58,7 +61,8 @@ TEST(GraphTest, SymbolicProb01_Sylvan) { } TEST(GraphTest, SymbolicProb01MinMax_Cudd) { - storm::prism::Program program = 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 "/functional/builder/leader3.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -75,7 +79,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); } - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -100,7 +105,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount()); } - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -119,7 +125,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { } TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { - storm::prism::Program program = 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 "/functional/builder/leader3.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -136,7 +143,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); } - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -161,7 +169,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount()); } - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -180,7 +189,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { } TEST(GraphTest, ExplicitProb01) { - storm::prism::Program program = 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 "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -201,7 +211,8 @@ TEST(GraphTest, ExplicitProb01) { } TEST(GraphTest, ExplicitProb01MinMax) { - storm::prism::Program program = 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 "/functional/builder/leader3.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -216,7 +227,8 @@ TEST(GraphTest, ExplicitProb01MinMax) { EXPECT_EQ(0ul, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -237,7 +249,8 @@ TEST(GraphTest, ExplicitProb01MinMax) { EXPECT_EQ(83ul, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -249,4 +262,4 @@ TEST(GraphTest, ExplicitProb01MinMax) { ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff"))); EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits()); -} \ No newline at end of file +}