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

tests updated to respect headers now missing in parsers 

Former-commit-id: fb6703d9b5 [formerly 5f89b42a60]
Former-commit-id: 1751efe563
main
sjunges 9 years ago
parent
e7dc0a049b
commit
7ef857137e
11 changed files with 92 additions and 39 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 16
      test/functional/logic/FragmentCheckerTest.cpp
  2. 33
      test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
  3. 2
      test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  4. 24
      test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  5. 1
      test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
  6. 27
      test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
  7. 1
      test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
  8. 8
      test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
  9. 16
      test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
  10. 1
      test/functional/parser/FormulaParserTest.cpp
  11. 2
      test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp

16
test/functional/logic/FragmentCheckerTest.cpp
View File

@ -3,12 +3,14 @@
#include "src/parser/FormulaParser.h"
#include "src/logic/FragmentChecker.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/storage/expressions/ExpressionManager.h"
TEST(FragmentCheckerTest, Propositional) {
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification prop = storm::logic::propositional();
storm::parser::FormulaParser formulaParser;
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
@ -37,10 +39,11 @@ TEST(FragmentCheckerTest, Propositional) {
}
TEST(FragmentCheckerTest, Pctl) {
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification pctl = storm::logic::pctl();
storm::parser::FormulaParser formulaParser;
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
@ -57,10 +60,11 @@ TEST(FragmentCheckerTest, Pctl) {
}
TEST(FragmentCheckerTest, Prctl) {
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification prctl = storm::logic::prctl();
storm::parser::FormulaParser formulaParser;
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
@ -83,10 +87,11 @@ TEST(FragmentCheckerTest, Prctl) {
}
TEST(FragmentCheckerTest, Csl) {
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification csl = storm::logic::csl();
storm::parser::FormulaParser formulaParser;
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
@ -106,10 +111,11 @@ TEST(FragmentCheckerTest, Csl) {
}
TEST(FragmentCheckerTest, Csrl) {
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification csrl = storm::logic::csrl();
storm::parser::FormulaParser formulaParser;
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));

33
test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
View File

@ -15,12 +15,15 @@
#include "src/parser/AutoParser.h"
#include "src/parser/PrismParser.h"
#include "src/builder/ExplicitModelBuilder.h"
#include "src/storage/expressions/ExpressionManager.h"
TEST(EigenDtmcPrctlModelCheckerTest, Die) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
@ -69,7 +72,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model = storm::builder::ExplicitModelBuilder<storm::RationalNumber>(program, options).build();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
@ -116,7 +121,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
@ -168,7 +175,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
@ -205,7 +214,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
@ -241,7 +252,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, LRASingleBscc) {
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(2, 2, 2);
@ -321,7 +334,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, LRA) {
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(15, 15, 20, true);
@ -398,7 +413,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, Conditional) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::make_unique<storm::solver::EigenLinearEquationSolverFactory<double>>());
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);

2
test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
View File

@ -18,6 +18,8 @@
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/storage/expressions/ExpressionManager.h"
TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
// 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);

24
test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
View File

@ -15,12 +15,14 @@
#include "src/parser/AutoParser.h"
#include "src/parser/PrismParser.h"
#include "src/builder/ExplicitModelBuilder.h"
#include "src/storage/expressions/ExpressionManager.h"
TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
@ -66,7 +68,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
@ -103,7 +107,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
@ -139,7 +145,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(2, 2, 2);
@ -219,7 +227,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) {
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(15, 15, 20, true);
@ -294,7 +304,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::make_unique<storm::solver::GmmxxLinearEquationSolverFactory<double>>());
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);

1
test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
View File

@ -21,6 +21,7 @@
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/storage/expressions/ExpressionManager.h"
TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.

27
test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
View File

@ -13,18 +13,21 @@
#include "src/models/symbolic/Dtmc.h"
#include "src/models/symbolic/StandardRewardModel.h"
#include "src/storage/SymbolicModelDescription.h"
#include "src/storage/expressions/ExpressionManager.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(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) {
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;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
// Build the die model with its reward model.
#ifdef WINDOWS
@ -86,7 +89,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
// Build the die model with its reward model.
#ifdef WINDOWS
@ -148,7 +153,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) {
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
@ -193,7 +200,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
@ -238,7 +247,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
// Build the die model with its reward model.
#ifdef WINDOWS
@ -291,7 +302,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
// Build the die model with its reward model.
#ifdef WINDOWS

1
test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
View File

@ -26,6 +26,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.

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

@ -22,7 +22,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) {
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
@ -91,7 +91,7 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) {
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
@ -148,7 +148,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) {
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
@ -182,7 +182,7 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) {
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model with the customers reward structure.

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

@ -28,7 +28,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
// Parse the model description.
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());
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
@ -126,7 +126,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
// Parse the model description.
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());
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
@ -224,7 +224,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
// Parse the model description.
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());
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
@ -304,7 +304,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
// Parse the model description.
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());
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
@ -384,7 +384,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) {
// Parse the model description.
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());
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
@ -421,7 +421,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
// Parse the model description.
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());
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
@ -465,7 +465,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
// Parse the model description.
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());
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model with the customers reward structure.
@ -556,7 +556,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) {
// Parse the model description.
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());
storm::parser::FormulaParser formulaParser(program);
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model with the customers reward structure.

1
test/functional/parser/FormulaParserTest.cpp
View File

@ -3,6 +3,7 @@
#include "src/parser/FormulaParser.h"
#include "src/logic/FragmentSpecification.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/storage/expressions/ExpressionManager.h"
TEST(FormulaParserTest, LabelTest) {
storm::parser::FormulaParser formulaParser;

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

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

Write Preview
Loading…
Cancel
Save