WIP (HOA-path) logic: HOAPathFormula

Note: syntax of the HOA path formula will change!

We have added checks for boundedGloballyFormulae hence the conflicts

 Conflicts:
	src/storm/logic/CloneVisitor.cpp
	src/storm/logic/Formula.cpp
	src/storm/logic/Formula.h
	src/storm/logic/FragmentSpecification.cpp
	src/storm/logic/FragmentSpecification.h
	src/storm/logic/LiftableTransitionRewardsVisitor.cpp
	src/storm/storage/jani/JSONExporter.cpp

src/storm/logic/CloneVisitor.cpp

@@ -176,5 +176,13 @@ namespace storm {
             return std::static_pointer_cast<Formula>(std::make_shared<UntilFormula>(left, right));
         }
 
+        boost::any CloneVisitor::visit(HOAPathFormula const& f, boost::any const& data) const {
+            std::shared_ptr<HOAPathFormula> result =  std::make_shared<HOAPathFormula>(f.getAutomatonFile());
+            for (auto& mapped : f.getAPMapping()) {
+                std::shared_ptr<Formula> clonedExpression = boost::any_cast<std::shared_ptr<Formula>>(mapped.second->accept(*this, data));
+                result->addAPMapping(mapped.first, clonedExpression);
+            }
+            return std::static_pointer_cast<Formula>(result);
+        }
     }
 }

src/storm/logic/CloneVisitor.h

@@ -35,6 +35,7 @@ namespace storm {
             virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
         };
         
     }

src/storm/logic/Formula.cpp

@@ -83,6 +83,10 @@ namespace storm {
             return false;
         }
 
+        bool Formula::isHOAPathFormula() const {
+            return false;
+        }
+
         bool Formula::isBinaryPathFormula() const {
             return false;
         }
@@ -289,6 +293,14 @@ namespace storm {
             return dynamic_cast<AtomicLabelFormula const&>(*this);
         }
 
+        HOAPathFormula& Formula::asHOAPathFormula() {
+            return dynamic_cast<HOAPathFormula&>(*this);
+        }
+
+        HOAPathFormula const& Formula::asHOAPathFormula() const {
+            return dynamic_cast<HOAPathFormula const&>(*this);
+        }
+
         UntilFormula& Formula::asUntilFormula() {
             return dynamic_cast<UntilFormula&>(*this);
         }

src/storm/logic/Formula.h

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

src/storm/logic/FormulaInformationVisitor.cpp

@@ -134,5 +134,13 @@ namespace storm {
             return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
         }
 
+        boost::any FormulaInformationVisitor::visit(HOAPathFormula const& f, boost::any const& data) const {
+            FormulaInformation info;
+            for (auto& mapped : f.getAPMapping()) {
+                info = info.join(boost::any_cast<FormulaInformation>(mapped.second->accept(*this, data)));
+            }
+            return info;
+        }
+
     }
 }

src/storm/logic/FormulaInformationVisitor.h

@@ -34,6 +34,7 @@ namespace storm {
             virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
         };
         
     }

src/storm/logic/FormulaVisitor.h

@@ -35,6 +35,7 @@ namespace storm {
             virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(UntilFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const = 0;
         };
         
     }

src/storm/logic/Formulas.h

@@ -28,6 +28,7 @@
 #include "storm/logic/UnaryPathFormula.h"
 #include "storm/logic/UnaryStateFormula.h"
 #include "storm/logic/UntilFormula.h"
+#include "storm/logic/HOAPathFormula.h"
 #include "storm/logic/ConditionalFormula.h"
 #include "storm/logic/ProbabilityOperatorFormula.h"
 #include "storm/logic/RewardOperatorFormula.h"

src/storm/logic/FormulasForwardDeclarations.h

@@ -36,6 +36,7 @@ namespace storm {
         class UnaryPathFormula;
         class UnaryStateFormula;
         class UntilFormula;
+        class HOAPathFormula;
     }
 }
 

src/storm/logic/FragmentChecker.cpp

@@ -322,5 +322,15 @@ namespace storm {
             result = result && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
             return result;
         }
+
+        boost::any FragmentChecker::visit(HOAPathFormula const& f, boost::any const& data) const {
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areHOAPathFormulasAllowed();
+            // TODO: check
+            for (auto& mapped : f.getAPMapping()) {
+                result = result && boost::any_cast<bool>(mapped.second->accept(*this, data));
+            }
+            return result;
+        }
     }
 }

src/storm/logic/FragmentChecker.h

@@ -35,6 +35,7 @@ namespace storm {
             virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
         };
         
     }

src/storm/logic/FragmentSpecification.cpp

@@ -168,6 +168,7 @@ namespace storm {
             nextFormula = false;
             untilFormula = false;
             boundedUntilFormula = false;
+            hoaPathFormula = false;
 
             atomicExpressionFormula = false;
             atomicLabelFormula = false;
@@ -326,6 +327,15 @@ namespace storm {
             return *this;
         }
 
+        bool FragmentSpecification::areHOAPathFormulasAllowed() const {
+            return hoaPathFormula;
+        }
+
+        FragmentSpecification& FragmentSpecification::setHOAPathFormulasAllowed(bool newValue) {
+            this->hoaPathFormula = newValue;
+            return *this;
+        }
+
         bool FragmentSpecification::areAtomicExpressionFormulasAllowed() const {
             return atomicExpressionFormula;
         }

src/storm/logic/FragmentSpecification.h

@@ -55,6 +55,9 @@ namespace storm {
             bool areBoundedGloballyFormulasAllowed() const;
             FragmentSpecification& setBoundedGloballyFormulasAllowed(bool newValue);
 
+            bool areHOAPathFormulasAllowed() const;
+            FragmentSpecification& setHOAPathFormulasAllowed(bool newValue);
+
             bool areAtomicExpressionFormulasAllowed() const;
             FragmentSpecification& setAtomicExpressionFormulasAllowed(bool newValue);
 
@@ -180,6 +183,7 @@ namespace storm {
             bool untilFormula;
             bool boundedUntilFormula;
             bool boundedGloballyFormula;
+            bool hoaPathFormula;
 
             bool atomicExpressionFormula;
             bool atomicLabelFormula;

src/storm/logic/HOAPathFormula.cpp

@@ -0,0 +1,90 @@
+#include "storm/logic/HOAPathFormula.h"
+#include "storm/logic/FormulaVisitor.h"
+
+#include "storm/utility/macros.h"
+#include "storm/automata/DeterministicAutomaton.h"
+#include "storm/exceptions/ExpressionEvaluationException.h"
+#include "storm/exceptions/IllegalArgumentException.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+#include "storm/exceptions/FileIoException.h"
+
+namespace storm {
+    namespace logic {
+        HOAPathFormula::HOAPathFormula(const std::string& automatonFile, FormulaContext context) : automatonFile(automatonFile), context(context) {
+            STORM_LOG_THROW(context == FormulaContext::Probability, storm::exceptions::InvalidPropertyException, "Invalid context for formula.");
+        }
+
+        FormulaContext const& HOAPathFormula::getContext() const {
+            return context;
+        }
+
+        const std::string& HOAPathFormula::getAutomatonFile() const {
+            return automatonFile;
+        }
+
+        const HOAPathFormula::ap_to_formula_map &HOAPathFormula::getAPMapping() const {
+            return apToFormulaMap;
+        }
+
+        void HOAPathFormula::addAPMapping(const std::string& ap, const std::shared_ptr<Formula const>& formula) {
+            STORM_LOG_THROW(apToFormulaMap.find(ap) == apToFormulaMap.end(), storm::exceptions::IllegalArgumentException, "HOA path formula: Mapping for atomic proposition \"" + ap + "\" already exists.");
+            apToFormulaMap[ap] = formula;
+        }
+
+        bool HOAPathFormula::isProbabilityPathFormula() const {
+            return true;
+        }
+
+        bool HOAPathFormula::isHOAPathFormula() const {
+            return true;
+        }
+
+        bool HOAPathFormula::hasQuantitativeResult() const {
+            return true;
+        }
+
+        boost::any HOAPathFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+
+        void HOAPathFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+            for (auto& mapped : getAPMapping()) {
+                mapped.second->gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+            }
+        }
+
+        void HOAPathFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
+            for (auto& mapped : getAPMapping()) {
+                mapped.second->gatherAtomicLabelFormulas(atomicLabelFormulas);
+            }
+        }
+
+        void HOAPathFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
+            for (auto& mapped : getAPMapping()) {
+                mapped.second->gatherReferencedRewardModels(referencedRewardModels);
+            }
+        }
+
+        storm::automata::DeterministicAutomaton::ptr HOAPathFormula::readAutomaton() const {
+            std::ifstream in(automatonFile);
+            STORM_LOG_THROW(in.good(), storm::exceptions::FileIoException, "Can not open '" << automatonFile << "' for reading.");
+            storm::automata::DeterministicAutomaton::ptr automaton = storm::automata::DeterministicAutomaton::parse(in);
+            for (auto& ap : automaton->getAPSet().getAPs()) {
+                STORM_LOG_THROW(apToFormulaMap.find(ap) != apToFormulaMap.end(), storm::exceptions::ExpressionEvaluationException, "For '" << automatonFile << "' HOA automaton, expression for atomic proposition '" << ap << "' is missing.");
+            }
+            return automaton;
+        }
+
+
+        std::ostream& HOAPathFormula::writeToStream(std::ostream& out) const {
+            out << "HOA: { ";
+            out << "\"" <<  automatonFile << "\"";
+            for (auto& mapping : apToFormulaMap) {
+                out << ", \"" << mapping.first << "\" -> ";
+                mapping.second->writeToStream(out);
+            }
+            out << " }";
+            return out;
+        }
+    }
+}

src/storm/logic/HOAPathFormula.h

@@ -0,0 +1,54 @@
+#pragma once
+
+#include "storm/logic/PathFormula.h"
+#include "storm/logic/FormulaContext.h"
+
+#include <map>
+#include <memory>
+
+namespace storm {
+    namespace automata {
+      // fwd
+      class DeterministicAutomaton;
+    }
+
+    namespace logic {
+        class HOAPathFormula  : public PathFormula {
+        public:
+            typedef std::map<std::string, std::shared_ptr<Formula const>> ap_to_formula_map;
+
+            HOAPathFormula(const std::string& automatonFile, FormulaContext context = FormulaContext::Probability);
+
+            virtual ~HOAPathFormula() {
+                // Intentionally left empty.
+            }
+
+            FormulaContext const& getContext() const;
+            const std::string& getAutomatonFile() const;
+            const ap_to_formula_map &getAPMapping() const;
+
+            void addAPMapping(const std::string& ap, const std::shared_ptr<Formula const>& formula);
+
+            virtual bool isHOAPathFormula() const override;
+            virtual bool isProbabilityPathFormula() const override;
+            virtual bool hasQuantitativeResult() const override;
+
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+
+            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
+            virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+
+	    std::shared_ptr<storm::automata::DeterministicAutomaton> readAutomaton() const;
+
+        private:
+            std::string automatonFile;
+            ap_to_formula_map apToFormulaMap;
+
+            FormulaContext context;
+        };
+    }
+}
+

src/storm/logic/LiftableTransitionRewardsVisitor.cpp

@@ -147,6 +147,15 @@ namespace storm {
             return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this));
         }
 
+        boost::any LiftableTransitionRewardsVisitor::visit(HOAPathFormula const& f, boost::any const& data) const {
+            for (auto const& ap : f.getAPMapping()) {
+                if (!boost::any_cast<bool>(ap.second->accept(*this, data))) {
+                    return false;
+                }
+            }
+            return true;
+        }
+
         bool LiftableTransitionRewardsVisitor::rewardModelHasTransitionRewards(std::string const& rewardModelName) const {
             if (symbolicModelDescription.hasModel()) {
                 if (symbolicModelDescription.isJaniModel()) {

src/storm/logic/LiftableTransitionRewardsVisitor.h

@@ -41,6 +41,7 @@ namespace storm {
             virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
+	    virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
         
         private:
             storm::storage::SymbolicModelDescription const& symbolicModelDescription;

src/storm/logic/ToExpressionVisitor.cpp

@@ -129,5 +129,8 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
         }
         
+        boost::any ToExpressionVisitor::visit(HOAPathFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
     }
 }

src/storm/logic/ToExpressionVisitor.h

@@ -35,6 +35,7 @@ namespace storm {
             virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
         };
         
     }

src/storm/storage/jani/JSONExporter.cpp

@@ -596,6 +596,10 @@ namespace storm {
             return opDecl;
         }
 
+        boost::any FormulaToJaniJson::visit(storm::logic::HOAPathFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support HOA path formulae");
+        }
+
         std::string operatorTypeToJaniString(storm::expressions::OperatorType optype) {
 
             using OpType = storm::expressions::OperatorType;

src/storm/storage/jani/JSONExporter.h

@@ -72,6 +72,7 @@ namespace storm {
             virtual boost::any visit(storm::logic::TotalRewardFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const;
+            virtual boost::any visit(storm::logic::HOAPathFormula const& f, boost::any const& data) const;
       
         private:
             FormulaToJaniJson(storm::jani::Model const& model) : model(model), stateExitRewards(false) { }