Fix validation of assumptions/use it

src/storm-pars/analysis/AssumptionMaker.cpp

@@ -8,7 +8,7 @@ namespace storm {
     namespace analysis {
         typedef std::shared_ptr<storm::expressions::BinaryRelationExpression> AssumptionType;
         template<typename ValueType>
-        AssumptionMaker<ValueType>::AssumptionMaker(storm::analysis::AssumptionChecker<ValueType>* assumptionChecker, uint_fast64_t numberOfStates, bool validate) {
+        AssumptionMaker<ValueType>::AssumptionMaker(AssumptionChecker<ValueType>* assumptionChecker, uint_fast64_t numberOfStates, bool validate) {
             this->numberOfStates = numberOfStates;
             this->assumptionChecker = assumptionChecker;
             this->validate = validate;
@@ -21,7 +21,7 @@ namespace storm {
 
 
         template <typename ValueType>
-        std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, AssumptionStatus> AssumptionMaker<ValueType>::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice) {
+        std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, AssumptionStatus> AssumptionMaker<ValueType>::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice) {
             std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, 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<storm::expressions::BinaryRelationExpression> assumption2
                     = std::make_shared<storm::expressions::BinaryRelationExpression>(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<storm::expressions::BinaryRelationExpression> assumption3
                     = std::make_shared<storm::expressions::BinaryRelationExpression>(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;

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<ValueType>* checker, uint_fast64_t numberOfStates, bool validate);
+            AssumptionMaker( AssumptionChecker<ValueType>* checker, uint_fast64_t numberOfStates, bool validate);
 
-            std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice);
+            std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice);
 
         private:
-            storm::analysis::AssumptionChecker<ValueType>* assumptionChecker;
+            AssumptionChecker<ValueType>* assumptionChecker;
 
             std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
 

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);

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<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
+    ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
+    model = simplifier.getSimplifiedModel();
+    dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+
+    ASSERT_EQ(dtmc->getNumberOfStates(), 193ull);
+    ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull);
+
+    auto *extender = new storm::analysis::LatticeExtender<storm::RationalFunction>(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<storm::RationalFunction>(formulas[0], dtmc, 3);
+    // This one does not validate the assumptions!
+    auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(&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]";