Merge pull request #137 from tquatmann/ltl

LTL Model Checking
Also includes a reset of
	src/storm-parsers/parser/FormulaParserGrammar.cpp
	src/storm-parsers/parser/FormulaParserGrammar.h
since there have been to many changes to fix them individually. Will
follow up with a commit to introduce shield and smg formula parsing

 Conflicts:
	src/storm-parsers/parser/FormulaParserGrammar.cpp
	src/storm-parsers/parser/FormulaParserGrammar.h
	src/storm/logic/CloneVisitor.cpp
	src/storm/logic/Formula.h
	src/storm/logic/FragmentChecker.cpp
	src/storm/logic/FragmentSpecification.cpp
	src/storm/logic/FragmentSpecification.h
	src/storm/logic/LiftableTransitionRewardsVisitor.cpp
	src/storm/logic/ToPrefixStringVisitor.cpp
	src/storm/logic/ToPrefixStringVisitor.h
	src/storm/modelchecker/AbstractModelChecker.cpp
	src/storm/modelchecker/AbstractModelChecker.h
	src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
	src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
	src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
	src/storm/storage/MaximalEndComponent.cpp
	src/storm/storage/Scheduler.cpp
	src/storm/storage/Scheduler.h
	src/storm/storage/jani/JSONExporter.cpp
	src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp

src/storm-parsers/parser/FormulaParserGrammar.cpp

@@ -176,8 +176,6 @@ namespace storm {
             formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":");
             formulaName.name("formula name");
 
-
-
             constantDefinition = (qi::lit("const") > -(qi::lit("int")[qi::_a = ConstantDataType::Integer] | qi::lit("bool")[qi::_a = ConstantDataType::Bool] | qi::lit("double")[qi::_a = ConstantDataType::Rational]) >> identifier >> -(qi::lit("=") > expressionParser))[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a, qi::_2)];
             constantDefinition.name("constant definition");
 

src/storm-parsers/parser/FormulaParserGrammar.h

@@ -10,7 +10,6 @@
 #include "storm/storage/jani/Property.h"
 #include "storm/logic/Formulas.h"
 #include "storm-parsers/parser/ExpressionParser.h"
-#include "storm-parsers/parser/ConstantDataType.h"
 
 #include "storm/modelchecker/results/FilterType.h"
 
@@ -243,9 +242,6 @@ namespace storm {
             storm::logic::PlayerCoalition createPlayerCoalition(std::vector<boost::variant<std::string, storm::storage::PlayerIndex>> const& playerIds) const;
             std::shared_ptr<storm::logic::Formula const> createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
 
-            std::pair<storm::logic::ShieldComparison, double> createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value);
-            std::shared_ptr<storm::logic::ShieldExpression const> createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional<std::pair<storm::logic::ShieldComparison, double>> comparisonStruct);
-
             bool areConstantDefinitionsAllowed() const;
             void addConstant(std::string const& name, ConstantDataType type, boost::optional<storm::expressions::Expression> const& expression);
             void addProperty(std::vector<storm::jani::Property>& properties, boost::optional<std::string> const& name, std::shared_ptr<storm::logic::Formula const> const& formula);

src/storm/logic/Formula.h

@@ -149,6 +149,9 @@ namespace storm {
             HOAPathFormula& asHOAPathFormula();
             HOAPathFormula const& asHOAPathFormula() const;
 
+            HOAPathFormula& asHOAPathFormula();
+            HOAPathFormula const& asHOAPathFormula() const;
+
             BoundedUntilFormula& asBoundedUntilFormula();
             BoundedUntilFormula const& asBoundedUntilFormula() const;
 

src/storm/logic/FragmentSpecification.cpp

@@ -114,6 +114,35 @@ namespace storm {
             return rpatl;
         }
 
+        FragmentSpecification prctl() {
+            FragmentSpecification prctl = pctl();
+
+            prctl.setRewardOperatorsAllowed(true);
+            prctl.setCumulativeRewardFormulasAllowed(true);
+            prctl.setInstantaneousFormulasAllowed(true);
+            prctl.setReachabilityRewardFormulasAllowed(true);
+            prctl.setLongRunAverageOperatorsAllowed(true);
+            prctl.setStepBoundedCumulativeRewardFormulasAllowed(true);
+            prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true);
+
+            return prctl;
+        }
+
+        FragmentSpecification prctlstar() {
+            FragmentSpecification prctlstar = pctlstar();
+
+            prctlstar.setRewardOperatorsAllowed(true);
+            prctlstar.setCumulativeRewardFormulasAllowed(true);
+            prctlstar.setInstantaneousFormulasAllowed(true);
+            prctlstar.setReachabilityRewardFormulasAllowed(true);
+            prctlstar.setLongRunAverageOperatorsAllowed(true);
+            prctlstar.setStepBoundedCumulativeRewardFormulasAllowed(true);
+            prctlstar.setTimeBoundedCumulativeRewardFormulasAllowed(true);
+
+            return prctlstar;
+
+        }
+
         FragmentSpecification csl() {
             FragmentSpecification csl = pctl();
 

src/storm/logic/FragmentSpecification.h

@@ -249,6 +249,8 @@ namespace storm {
         // Flat PCTL.
         FragmentSpecification flatPctl();
 
+        // rPATL for SMGs
+        FragmentSpecification rpatl();
         // PCTL*
         FragmentSpecification pctlstar();
 
@@ -258,9 +260,6 @@ namespace storm {
         // PCTL* + cumulative, instantaneous, reachability and long-run rewards.
         FragmentSpecification prctlstar();
 
-        // rPATL for SMGs
-        FragmentSpecification rpatl();
-
         // Regular CSL.
         FragmentSpecification csl();
 

src/storm/logic/LiftableTransitionRewardsVisitor.cpp

@@ -30,7 +30,6 @@ namespace storm {
             return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
         }
 
-
         boost::any LiftableTransitionRewardsVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const {
             return true;
         }

src/storm/logic/ToPrefixStringVisitor.cpp

@@ -59,10 +59,6 @@ namespace storm {
             return result;
         }
 
-        boost::any ToPrefixStringVisitor::visit(BoundedGloballyFormula const&, boost::any const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
-        }
-
         boost::any ToPrefixStringVisitor::visit(BoundedUntilFormula const&, boost::any const&) const {
             STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
         }

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -141,8 +141,36 @@ namespace storm {
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
 
+        template<typename SparseDtmcModelType>
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::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());
+            
+            auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); };
+            auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker);
+            std::vector<ValueType> numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets);
+            
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+        }
+
+        template<typename SparseDtmcModelType>
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeLTLProbabilities(Environment const& env, CheckTask<storm::logic::PathFormula, ValueType> const& checkTask) {
+            storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
+
+            storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix());
+            storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel());
+            
+            auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); };
+            std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker);
+
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+        }
+
         template<typename SparseDtmcModelType>
         std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
+
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             if (rewardPathFormula.isMultiDimensional() || rewardPathFormula.getTimeBoundReference().isRewardBound()) {
                 STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking non-trivial bounded until probabilities can only be computed for the initial states of the model.");

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -28,6 +28,7 @@
 
 #include "storm/shields/ShieldHandling.h"
 
+#include "storm/settings/modules/GeneralSettings.h"
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
 #include "storm/storage/expressions/Expressions.h"

src/storm/storage/Scheduler.cpp

@@ -224,6 +224,18 @@ namespace storm {
                             continue;
                         }
 
+                        // Indent if this is not the first memory state
+                        if (firstMemoryState) {
+                            firstMemoryState = false;
+                        } else {
+                            out << std::setw(widthOfStates) << "";
+                            out << "    ";
+                        }
+                        // Print the memory state info
+                        if (!isMemorylessScheduler()) {
+                            out << "m="<< memoryState << std::setw(8) << "";
+                        }
+
                     // Print choice info
                     SchedulerChoice<ValueType> const& choice = schedulerChoices[memoryState][state];
                     if (choice.isDefined()) {
@@ -282,7 +294,28 @@ namespace storm {
                             }
                         }
 
-                    stateString << std::endl;
+                        // Print memory updates
+                        if(!isMemorylessScheduler()) {
+                            out << std::setw(widthOfStates) << "";
+                            // The memory updates do not depend on the actual choice, they only depend on the current model- and memory state as well as the successor model state.
+                            for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
+                                uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first;
+                                bool firstUpdate = true;
+                                for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) {
+                                    if (firstUpdate) {
+                                        firstUpdate = false;
+                                    } else {
+                                        out << ", ";
+                                    }
+                                    out << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
+                                    // out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
+                                }
+
+                            }
+
+                        }
+
+                        out << std::endl;
                     }
 
                     stateString << stateString.str();

src/storm/storage/Scheduler.h

@@ -139,7 +139,6 @@ namespace storm {
              */
             void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false, bool skipDontCareStates = false) const;
 
-
             /*!
              * Prints the scheduler in json format to the given output stream.
              */

src/storm/storage/jani/JSONExporter.cpp

@@ -711,7 +711,7 @@ namespace storm {
                 return opDecl;
             }
         }
-        
+
         boost::any ExpressionToJson::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) {
             ExportJsonType opDecl;
             opDecl["op"] = operatorTypeToJaniString(expression.getOperator());