From 73a514a9c7d315de5acd18e4c5747086beeb03cb Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Fri, 10 May 2019 14:16:22 +0200 Subject: [PATCH] Fix validation of assumptions/use it --- src/storm-pars/analysis/AssumptionMaker.cpp | 27 ++++++-- src/storm-pars/analysis/AssumptionMaker.h | 6 +- .../analysis/MonotonicityChecker.cpp | 4 +- .../analysis/AssumptionMakerTest.cpp | 68 +++++++++++++++++++ 4 files changed, 95 insertions(+), 10 deletions(-) diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index e2828db50..bdac30bb2 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -8,7 +8,7 @@ namespace storm { namespace analysis { typedef std::shared_ptr AssumptionType; template - AssumptionMaker::AssumptionMaker(storm::analysis::AssumptionChecker* assumptionChecker, uint_fast64_t numberOfStates, bool validate) { + AssumptionMaker::AssumptionMaker(AssumptionChecker* assumptionChecker, uint_fast64_t numberOfStates, bool validate) { this->numberOfStates = numberOfStates; this->assumptionChecker = assumptionChecker; this->validate = validate; @@ -21,7 +21,7 @@ namespace storm { template - std::map, AssumptionStatus> AssumptionMaker::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice) { + std::map, AssumptionStatus> AssumptionMaker::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice) { std::map, AssumptionStatus> result; // TODO: alleen maar als validate true is results genereren @@ -32,21 +32,38 @@ namespace storm { var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Greater)); // TODO: dischargen gebasseerd op monotonicity - auto result1 = assumptionChecker->validateAssumption(assumption1, lattice); + AssumptionStatus result1; + AssumptionStatus result2; + AssumptionStatus result3; + if (validate) { + result1 = assumptionChecker->validateAssumption(assumption1, lattice); + } else { + result1 = AssumptionStatus::UNKNOWN; + } result[assumption1] = result1; + std::shared_ptr assumption2 = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Greater)); - auto result2 = assumptionChecker->validateAssumption(assumption2, lattice); + + if (validate) { + result2 = assumptionChecker->validateAssumption(assumption2, lattice); + } else { + result2 = AssumptionStatus::UNKNOWN; + } result[assumption2] = result2; std::shared_ptr assumption3 = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Equal)); - auto result3 = assumptionChecker->validateAssumption(assumption3, lattice); + if (validate) { + result3 = assumptionChecker->validateAssumption(assumption3, lattice); + } else { + result3 = AssumptionStatus::UNKNOWN; + } result[assumption3] = result3; return result; diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h index 72d0255dc..2f52b85de 100644 --- a/src/storm-pars/analysis/AssumptionMaker.h +++ b/src/storm-pars/analysis/AssumptionMaker.h @@ -26,12 +26,12 @@ namespace storm { * @param checker The AssumptionChecker which checks the assumptions at sample points. * @param numberOfStates The number of states of the model. */ - AssumptionMaker( storm::analysis::AssumptionChecker* checker, uint_fast64_t numberOfStates, bool validate); + AssumptionMaker( AssumptionChecker* checker, uint_fast64_t numberOfStates, bool validate); - std::map, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice); + std::map, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice); private: - storm::analysis::AssumptionChecker* assumptionChecker; + AssumptionChecker* assumptionChecker; std::shared_ptr expressionManager; diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index d96c358de..64543de48 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -332,14 +332,14 @@ namespace storm { // TODO: checkend at ie niet invalid is criticalTuple = extender->extendLattice(latticeCopy, assumption2.first); - if (somewhereMonotonicity(std::get<0>(criticalTuple))) { + if (assumption2.second != AssumptionStatus::INVALID && somewhereMonotonicity(std::get<0>(criticalTuple))) { auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptionsCopy); result.insert(map.begin(), map.end()); } criticalTuple = extender->extendLattice(latticeCopy2, assumption3.first); - if (somewhereMonotonicity(std::get<0>(criticalTuple))) { + if (assumption3.second != AssumptionStatus::INVALID && somewhereMonotonicity(std::get<0>(criticalTuple))) { auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptionsCopy2); diff --git a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp index a7603ca09..bcdac1227 100644 --- a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp @@ -28,6 +28,7 @@ #include "storm-parsers/api/storm-parsers.h" +//TODO: voor als validate uit staat TEST(AssumptionMakerTest, Brp_without_bisimulation) { std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; std::string formulaAsString = "P=? [F s=4 & i=N ]"; @@ -94,6 +95,73 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation) { EXPECT_TRUE(foundThird); } +TEST(AssumptionMakerTest, Brp_without_bisimulation_no_validation) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P=? [F s=4 & i=N ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); + + auto *extender = new storm::analysis::LatticeExtender(dtmc); + auto criticalTuple = extender->toLattice(formulas); + ASSERT_EQ(183, std::get<1>(criticalTuple)); + ASSERT_EQ(186, std::get<2>(criticalTuple)); + + auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmc, 3); + // This one does not validate the assumptions! + auto assumptionMaker = storm::analysis::AssumptionMaker(&assumptionChecker, dtmc->getNumberOfStates(), false); + auto result = assumptionMaker.createAndCheckAssumption(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple)); + + EXPECT_EQ(3, result.size()); + + bool foundFirst = false; + bool foundSecond = false; + bool foundThird = false; + for (auto itr = result.begin(); itr != result.end(); ++itr) { + if (!foundFirst && itr->first->getFirstOperand()->asVariableExpression().getVariable().getName() == "183") { + EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("186", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); + foundFirst = true; + } else if (!foundSecond && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater) { + EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); + foundSecond = true; + } else if (!foundThird && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { + EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Equal, itr->first->getRelationType()); + foundThird = true; + } else { + EXPECT_TRUE(false); + } + } + EXPECT_TRUE(foundFirst); + EXPECT_TRUE(foundSecond); + EXPECT_TRUE(foundThird); +} + TEST(AssumptionMakerTest, Simple1) { std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm"; std::string formulaAsString = "P=? [F s=3]";