From a976352b8cdf78cb01ba3845965c47f2ce0424b4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 22 Dec 2016 16:48:38 +0100 Subject: [PATCH] some fixes to make tests pass --- src/storm/storage/expressions/Expression.cpp | 2 + .../GameBasedDtmcModelCheckerTest.cpp | 176 +----------------- .../GameBasedMdpModelCheckerTest.cpp | 94 ++++++---- 3 files changed, 63 insertions(+), 209 deletions(-) diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp index b980cab0a..bb3dca82f 100644 --- a/src/storm/storage/expressions/Expression.cpp +++ b/src/storm/storage/expressions/Expression.cpp @@ -246,9 +246,11 @@ namespace storm { Expression operator&&(Expression const& first, Expression const& second) { assertSameManager(first.getBaseExpression(), second.getBaseExpression()); if (first.isTrue()) { + STORM_LOG_THROW(second.hasBooleanType(), storm::exceptions::InvalidTypeException, "Operator requires boolean operands."); return second; } if (second.isTrue()) { + STORM_LOG_THROW(first.hasBooleanType(), storm::exceptions::InvalidTypeException, "Operator requires boolean operands."); return first; } return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And))); diff --git a/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp b/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp index aee1eeb24..4cc504f39 100644 --- a/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp +++ b/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp @@ -19,30 +19,15 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); + auto checker = std::make_shared>>(program); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - auto checker = std::make_shared>>(program); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); storm::modelchecker::CheckTask task(*formula, true); std::unique_ptr result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); @@ -51,7 +36,6 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) { task = storm::modelchecker::CheckTask(*formula, true); result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); @@ -60,7 +44,6 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) { task = storm::modelchecker::CheckTask(*formula, true); result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::getModule().getPrecision()); @@ -71,27 +54,13 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); + auto checker = std::make_shared>>(program); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); storm::modelchecker::CheckTask task(*formula, true); std::unique_ptr result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); @@ -100,7 +69,6 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) { task = storm::modelchecker::CheckTask(*formula, true); result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); @@ -109,177 +77,43 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) { task = storm::modelchecker::CheckTask(*formula, true); result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::getModule().getPrecision()); } -TEST(GameBasedDtmcModelCheckerTest, Crowds_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_EQ(8607ul, model->getNumberOfStates()); - EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - auto checker = std::make_shared>>(program); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - storm::modelchecker::CheckTask task(*formula, true); - - std::unique_ptr result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.33288236360191303, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - task = storm::modelchecker::CheckTask(*formula, true); - - result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.15222081144084315, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - task = storm::modelchecker::CheckTask(*formula, true); - - result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.3215392962289586, quantitativeResult3[0], storm::settings::getModule().getPrecision()); -} - -TEST(GameBasedDtmcModelCheckerTest, Crowds_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_EQ(8607ul, model->getNumberOfStates()); - EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - auto checker = std::make_shared>>(program); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - storm::modelchecker::CheckTask task(*formula, true); - - std::unique_ptr result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - // FIXME: precision not optimal. - EXPECT_NEAR(0.33288236360191303, quantitativeResult1[0], 10 * storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - task = storm::modelchecker::CheckTask(*formula, true); - - result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - // FIXME: precision not optimal. - EXPECT_NEAR(0.15222081144084315, quantitativeResult2[0], 10 * storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - task = storm::modelchecker::CheckTask(*formula, true); - - result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - // FIXME: precision not optimal. - EXPECT_NEAR(0.3215392962289586, quantitativeResult3[0], 10 * storm::settings::getModule().getPrecision()); -} - TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); + program = program.substituteConstants(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(273ul, model->getNumberOfStates()); - EXPECT_EQ(397ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); auto checker = std::make_shared>>(program); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); storm::modelchecker::CheckTask task(*formula, true); std::unique_ptr result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - task = storm::modelchecker::CheckTask(*formula, true); - - result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.99999989760000074, quantitativeResult2[0], storm::settings::getModule().getPrecision()); } TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Sylvan) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); - + program = program.substituteConstants(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(273ul, model->getNumberOfStates()); - EXPECT_EQ(397ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); auto checker = std::make_shared>>(program); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); storm::modelchecker::CheckTask task(*formula, true); std::unique_ptr result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - task = storm::modelchecker::CheckTask(*formula, true); - - result = checker->check(task); - //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.99999989760000074, quantitativeResult2[0], storm::settings::getModule().getPrecision()); } diff --git a/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp b/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp index 71f86a62f..441b03b37 100644 --- a/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp +++ b/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp @@ -87,55 +87,73 @@ TEST(GameBasedMdpModelCheckerTest, Dice_Cudd) { EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule().getPrecision()); } -TEST(GameBasedMdpModelCheckerTest, AsynchronousLeader_Cudd) { - std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"; - +TEST(GameBasedMdpModelCheckerTest, Dice_Sylvan) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"; + storm::prism::Program program = storm::parseProgram(programFile); - // Build the die model + + // Build the die model #ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; + storm::builder::DdPrismModelBuilder::Options options; #else - typename storm::builder::DdPrismModelBuilder::Options options; + typename storm::builder::DdPrismModelBuilder::Options options; #endif - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - - ASSERT_EQ(3172ull, model->getNumberOfStates()); - ASSERT_EQ(7144ull, model->getNumberOfTransitions()); - - std::shared_ptr> mdp = model->as>(); - auto mdpModelchecker = std::make_shared>>(program); - - // A parser that we use for conveniently constructing the formulas. + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); + + ASSERT_EQ(model->getNumberOfStates(), 169ull); + ASSERT_EQ(model->getNumberOfTransitions(), 436ull); + + std::shared_ptr> mdp = model->as>(); + auto mdpModelchecker = std::make_shared>>(program); + + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - storm::modelchecker::CheckTask task(*formula, true); - + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + storm::modelchecker::CheckTask task(*formula, true); + std::unique_ptr result = mdpModelchecker->check(task); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - task = storm::modelchecker::CheckTask(*formula, true); - + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + result = mdpModelchecker->check(task); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - task = storm::modelchecker::CheckTask(*formula, true); - + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + result = mdpModelchecker->check(task); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - task = storm::modelchecker::CheckTask(*formula, true); - + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + result = mdpModelchecker->check(task); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::getModule().getPrecision()); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = mdpModelchecker->check(task); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); + task = storm::modelchecker::CheckTask(*formula, true); + + result = mdpModelchecker->check(task); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule().getPrecision()); }