allow HOA formulas for cslstar and pctlstar

Conflicts:
	src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

src/storm/logic/FragmentSpecification.cpp

@@ -52,6 +52,7 @@ namespace storm {
             pctlstar.setUnaryBooleanPathFormulasAllowed(true);
             pctlstar.setNestedOperatorsAllowed(true);
             pctlstar.setNestedPathFormulasAllowed(true);
+            pctlstar.setHOAPathFormulasAllowed(true);
 
             return pctlstar;
         }
@@ -128,6 +129,7 @@ namespace storm {
             cslstar.setUnaryBooleanPathFormulasAllowed(true);
             cslstar.setNestedOperatorsAllowed(true);
             cslstar.setNestedPathFormulasAllowed(true);
+            cslstar.setHOAPathFormulasAllowed(true);
 
             return cslstar;
         }

src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -132,8 +132,8 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, ValueType> const& checkTask) {
             storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula();
             
-            storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix());
-            storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel());
+            storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(this->getModel().getTransitionMatrix());
+            storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel());
             
             auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); };
             auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker);

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -160,8 +160,8 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, ValueType> const& checkTask) {
             storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula();
 
-            storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix());
-            storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel());
+            storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(this->getModel().getTransitionMatrix());
+            storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel());
 
             auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); };
             auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker);

src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp

@@ -525,4 +525,32 @@ namespace {
 #endif
 
     }
+
+    TYPED_TEST(CtmcCslModelCheckerTest, HOAProbabilitiesPolling) {
+        // "P=? [ F "target" & (X s=1)]"
+        std::string formulasString = "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> \"target\", \"p1\" -> (s=1) }]";
+        // "P=? [!(s=1) U (s=1)]"
+        formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> !(s=1) , \"p1\" -> \"target\" }]";
+
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(12ul, model->getNumberOfStates());
+        EXPECT_EQ(22ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+
+        // Not supported in all engines (Hybrid,  PrismDd, JaniDd)
+        if (TypeParam::engine == CtmcEngine::PrismSparse || TypeParam::engine == CtmcEngine::JaniSparse || TypeParam::engine == CtmcEngine::JitSparse) {
+            result = checker->check(tasks[0]);
+            EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+
+            result = checker->check(tasks[1]);
+            EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        } else {
+            EXPECT_FALSE(checker->canHandle(tasks[0]));
+        }
+
+    }
 }

src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp

@@ -387,4 +387,32 @@ namespace {
         GTEST_SKIP();
 #endif
     }
+
+    TYPED_TEST(MarkovAutomatonCslModelCheckerTest, HOASimple) {
+        // "P=? [ F (s=3) & (X s=1)]"
+        std::string formulasString = "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s>1), \"p1\" -> !(s=1) }]";
+        // "P=? [ (s=2) U (s=1)]"
+        formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (s=2), \"p1\" -> (s=1) }]";
+
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple.ma", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(5ul, model->getNumberOfStates());
+        EXPECT_EQ(8ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+
+        // Not supported in all engines (Hybrid,  PrismDd, JaniDd)
+        if (TypeParam::engine == MaEngine::PrismSparse || TypeParam::engine == MaEngine::JaniSparse || TypeParam::engine == MaEngine::JitSparse) {
+            result = checker->check(tasks[0]);
+            EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+
+            result = checker->check(tasks[1]);
+            EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        } else {
+            EXPECT_FALSE(checker->canHandle(tasks[0]));
+        }
+
+    }
 }

src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp

@@ -787,5 +787,33 @@ namespace {
 
     }
 
+    TYPED_TEST(MdpPrctlModelCheckerTest, HOADice) {
+        // "P=? [ F "three" & (X s=1)]"
+        std::string formulasString = "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> \"three\", \"p1\" -> s2=1 }]";
+        // "P=? [!(s2=6) U "done"]"
+        formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> !(s2=6), \"p1\" -> \"done\" }]";
+
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(169ul, model->getNumberOfStates());
+        EXPECT_EQ(436ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+
+        // Not supported in all engines (Hybrid,  PrismDd, JaniDd)
+        if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse || TypeParam::engine == MdpEngine::JitSparse) {
+            result = checker->check(tasks[0]);
+            EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+
+            result = checker->check(tasks[1]);
+            EXPECT_NEAR(this->parseNumber("3/4"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        } else {
+            EXPECT_FALSE(checker->canHandle(tasks[0]));
+        }
+
+    }
+
 
 }