From b7357c2cf99e66a17a84181e5a9867116f988688 Mon Sep 17 00:00:00 2001 From: masawei Date: Sun, 10 Aug 2014 22:23:15 +0200 Subject: [PATCH] Testing, noticed that vectors of pointers are not good. Changing that. Former-commit-id: 460854c49ce25cc56351b1bf68457f146fc3da2c --- src/formula/AbstractFilter.h | 8 +- test/functional/modelchecker/FilterTest.cpp | 93 ++++++++++++++++++--- 2 files changed, 86 insertions(+), 15 deletions(-) diff --git a/src/formula/AbstractFilter.h b/src/formula/AbstractFilter.h index 0d03d3b0d..d0f9aa60e 100644 --- a/src/formula/AbstractFilter.h +++ b/src/formula/AbstractFilter.h @@ -71,17 +71,15 @@ public: } void addAction(action::AbstractAction* action) { - actions.push_back(action); + if(action != nullptr) { + actions.push_back(action); + } } void removeAction() { actions.pop_back(); } - action::AbstractAction* getAction(uint_fast64_t pos) const { - return actions[pos]; - } - uint_fast64_t getActionCount() const { return actions.size(); } diff --git a/test/functional/modelchecker/FilterTest.cpp b/test/functional/modelchecker/FilterTest.cpp index e8ce4b156..65fa50e7a 100644 --- a/test/functional/modelchecker/FilterTest.cpp +++ b/test/functional/modelchecker/FilterTest.cpp @@ -16,9 +16,9 @@ #include "src/formula/ltl/LtlFilter.h" #include "src/parser/PrctlParser.h" -#include +#include -typedef typename storm::property::prctl::PrctlFilter::Result Result; +typedef typename storm::property::action::AbstractAction::Result Result; TEST(PrctlFilterTest, generalFunctionality) { // Test filter queries of increasing complexity. @@ -70,14 +70,87 @@ TEST(PrctlFilterTest, generalFunctionality) { ASSERT_FALSE(result.selection[7]); // Test the sorting. - ASSERT_EQ(3, result.stateMap[0]); - ASSERT_EQ(4, result.stateMap[1]); - ASSERT_EQ(1, result.stateMap[2]); - ASSERT_EQ(0, result.stateMap[3]); - ASSERT_EQ(2, result.stateMap[4]); - ASSERT_EQ(5, result.stateMap[5]); - ASSERT_EQ(6, result.stateMap[6]); - ASSERT_EQ(7, result.stateMap[7]); + ASSERT_EQ(6, result.stateMap[0]); + ASSERT_EQ(7, result.stateMap[1]); + ASSERT_EQ(3, result.stateMap[2]); + ASSERT_EQ(4, result.stateMap[3]); + ASSERT_EQ(1, result.stateMap[4]); + ASSERT_EQ(0, result.stateMap[5]); + ASSERT_EQ(2, result.stateMap[6]); + ASSERT_EQ(5, result.stateMap[7]); + + // Get the probability for reaching a 'd' state only for those states that have a probability to do so of at most 0.5. + // Sorted by value; lowest first. + input = "filter[bound(<, 0.5); sort(value, ascending)](F d)"; + ASSERT_NO_THROW( + formula = storm::parser::PrctlParser::parsePrctlFormula(input) + ); + + result = formula->evaluate(mc); + + // Test the selection. + ASSERT_EQ(4, result.selection.getNumberOfSetBits()); + ASSERT_FALSE(result.selection[0]); + ASSERT_FALSE(result.selection[1]); + ASSERT_FALSE(result.selection[2]); + ASSERT_TRUE(result.selection[3]); + ASSERT_FALSE(result.selection[4]); + ASSERT_TRUE(result.selection[5]); + ASSERT_TRUE(result.selection[6]); + ASSERT_TRUE(result.selection[7]); + + // Test the sorting. + ASSERT_EQ(5, result.stateMap[0]); + ASSERT_EQ(6, result.stateMap[1]); + ASSERT_EQ(7, result.stateMap[2]); + ASSERT_EQ(3, result.stateMap[3]); + ASSERT_EQ(4, result.stateMap[4]); + ASSERT_EQ(1, result.stateMap[5]); + ASSERT_EQ(0, result.stateMap[6]); + ASSERT_EQ(2, result.stateMap[7]); + + // Get the three highest indexed states reaching an 'a' state with probability at most 0.3. + input = "filter[sort(value); range(5,7); sort(index, descending)](P<=0.3(F a))"; + ASSERT_NO_THROW( + formula = storm::parser::PrctlParser::parsePrctlFormula(input) + ); + + result = formula->evaluate(mc); + + // Test the selection. + ASSERT_EQ(3, result.selection.getNumberOfSetBits()); + ASSERT_FALSE(result.selection[0]); + ASSERT_FALSE(result.selection[1]); + ASSERT_FALSE(result.selection[2]); + ASSERT_TRUE(result.selection[3]); + ASSERT_FALSE(result.selection[4]); + ASSERT_FALSE(result.selection[5]); + ASSERT_TRUE(result.selection[6]); + ASSERT_TRUE(result.selection[7]); + + // Test the sorting. + ASSERT_EQ(7, result.stateMap[0]); + ASSERT_EQ(6, result.stateMap[1]); + ASSERT_EQ(5, result.stateMap[2]); + ASSERT_EQ(4, result.stateMap[3]); + ASSERT_EQ(3, result.stateMap[4]); + ASSERT_EQ(2, result.stateMap[5]); + ASSERT_EQ(1, result.stateMap[6]); + ASSERT_EQ(0, result.stateMap[7]); + +} + +TEST(PrctlFilterTest, Safety) { + // Setup model and modelchecker. + storm::models::Dtmc model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab"); + storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(model, new storm::solver::GmmxxLinearEquationSolver()); + + // Make a stub formula as child. + auto apFormula = std::make_shared>("a"); + + auto formula = std::make_shared>(apFormula, nullptr); + + ASSERT_NO_THROW(formula->check(mc)); }