From 21b9d7381648401aefe3dd9adf562575076fb413 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 24 Aug 2020 22:24:55 +0200 Subject: [PATCH] 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 | 8 ++ src/storm/logic/CloneVisitor.h | 1 + src/storm/logic/Formula.cpp | 12 +++ src/storm/logic/Formula.h | 79 ++++++++-------- src/storm/logic/FormulaInformationVisitor.cpp | 8 ++ src/storm/logic/FormulaInformationVisitor.h | 1 + src/storm/logic/FormulaVisitor.h | 1 + src/storm/logic/Formulas.h | 1 + src/storm/logic/FormulasForwardDeclarations.h | 1 + src/storm/logic/FragmentChecker.cpp | 10 +++ src/storm/logic/FragmentChecker.h | 1 + src/storm/logic/FragmentSpecification.cpp | 10 +++ src/storm/logic/FragmentSpecification.h | 4 + src/storm/logic/HOAPathFormula.cpp | 90 +++++++++++++++++++ src/storm/logic/HOAPathFormula.h | 54 +++++++++++ .../LiftableTransitionRewardsVisitor.cpp | 9 ++ .../logic/LiftableTransitionRewardsVisitor.h | 1 + src/storm/logic/ToExpressionVisitor.cpp | 3 + src/storm/logic/ToExpressionVisitor.h | 1 + src/storm/storage/jani/JSONExporter.cpp | 4 + src/storm/storage/jani/JSONExporter.h | 1 + 21 files changed, 262 insertions(+), 38 deletions(-) create mode 100644 src/storm/logic/HOAPathFormula.cpp create mode 100644 src/storm/logic/HOAPathFormula.h diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index 57c8ce377..15499c9d9 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -176,5 +176,13 @@ namespace storm { return std::static_pointer_cast(std::make_shared(left, right)); } + boost::any CloneVisitor::visit(HOAPathFormula const& f, boost::any const& data) const { + std::shared_ptr result = std::make_shared(f.getAutomatonFile()); + for (auto& mapped : f.getAPMapping()) { + std::shared_ptr clonedExpression = boost::any_cast>(mapped.second->accept(*this, data)); + result->addAPMapping(mapped.first, clonedExpression); + } + return std::static_pointer_cast(result); + } } } diff --git a/src/storm/logic/CloneVisitor.h b/src/storm/logic/CloneVisitor.h index 61578bdca..954d46db4 100644 --- a/src/storm/logic/CloneVisitor.h +++ b/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; }; } diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index b4e6c13bc..553e15b89 100644 --- a/src/storm/logic/Formula.cpp +++ b/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(*this); } + HOAPathFormula& Formula::asHOAPathFormula() { + return dynamic_cast(*this); + } + + HOAPathFormula const& Formula::asHOAPathFormula() const { + return dynamic_cast(*this); + } + UntilFormula& Formula::asUntilFormula() { return dynamic_cast(*this); } diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 62aab0dde..0014baef4 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -21,17 +21,17 @@ namespace storm { // Forward-declare fragment specification for isInFragment() method. class FragmentSpecification; - + // Forward-declare formula information class for info() method. class FormulaInformation; - + class Formula : public std::enable_shared_from_this { public: // Make the destructor virtual to allow deletion of objects of subclasses via a pointer to this class. virtual ~Formula() { // Intentionally left empty. }; - + friend std::ostream& operator<<(std::ostream& out, Formula const& formula); // Basic formula types. @@ -39,14 +39,14 @@ namespace storm { virtual bool isStateFormula() const; virtual bool isConditionalProbabilityFormula() const; virtual bool isConditionalRewardFormula() const; - + virtual bool isProbabilityPathFormula() const; virtual bool isRewardPathFormula() const; virtual bool isTimePathFormula() const; virtual bool isBinaryBooleanStateFormula() const; virtual bool isUnaryBooleanStateFormula() const; - + virtual bool isMultiObjectiveFormula() const; virtual bool isQuantileFormula() const; @@ -95,34 +95,34 @@ namespace storm { // Accessors for the return type of a formula. virtual bool hasQualitativeResult() const; virtual bool hasQuantitativeResult() const; - + bool isInFragment(FragmentSpecification const& fragment) const; FormulaInformation info() const; virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data = boost::any()) const = 0; - + static std::shared_ptr getTrueFormula(); bool isInitialFormula() const; - + PathFormula& asPathFormula(); PathFormula const& asPathFormula() const; - + StateFormula& asStateFormula(); StateFormula const& asStateFormula() const; - + MultiObjectiveFormula& asMultiObjectiveFormula(); MultiObjectiveFormula const& asMultiObjectiveFormula() const; - + QuantileFormula& asQuantileFormula(); QuantileFormula const& asQuantileFormula() const; - + BinaryStateFormula& asBinaryStateFormula(); BinaryStateFormula const& asBinaryStateFormula() const; - + UnaryStateFormula& asUnaryStateFormula(); UnaryStateFormula const& asUnaryStateFormula() const; - + BinaryBooleanStateFormula& asBinaryBooleanStateFormula(); BinaryBooleanStateFormula const& asBinaryBooleanStateFormula() const; @@ -131,25 +131,28 @@ namespace storm { BooleanLiteralFormula& asBooleanLiteralFormula(); BooleanLiteralFormula const& asBooleanLiteralFormula() const; - + AtomicExpressionFormula& asAtomicExpressionFormula(); AtomicExpressionFormula const& asAtomicExpressionFormula() const; - + AtomicLabelFormula& asAtomicLabelFormula(); AtomicLabelFormula const& asAtomicLabelFormula() const; - + UntilFormula& asUntilFormula(); UntilFormula const& asUntilFormula() const; - + + HOAPathFormula& asHOAPathFormula(); + HOAPathFormula const& asHOAPathFormula() const; + BoundedUntilFormula& asBoundedUntilFormula(); BoundedUntilFormula const& asBoundedUntilFormula() const; - + EventuallyFormula& asEventuallyFormula(); EventuallyFormula const& asEventuallyFormula() const; - + EventuallyFormula& asReachabilityProbabilityFormula(); EventuallyFormula const& asReachabilityProbabilityFormula() const; - + EventuallyFormula& asReachabilityRewardFormula(); EventuallyFormula const& asReachabilityRewardFormula() const; @@ -161,16 +164,16 @@ namespace storm { GloballyFormula& asGloballyFormula(); GloballyFormula const& asGloballyFormula() const; - + BinaryPathFormula& asBinaryPathFormula(); BinaryPathFormula const& asBinaryPathFormula() const; - + UnaryPathFormula& asUnaryPathFormula(); UnaryPathFormula const& asUnaryPathFormula() const; - + ConditionalFormula& asConditionalFormula(); ConditionalFormula const& asConditionalFormula() const; - + NextFormula& asNextFormula(); NextFormula const& asNextFormula() const; @@ -182,36 +185,36 @@ namespace storm { TimeOperatorFormula& asTimeOperatorFormula(); TimeOperatorFormula const& asTimeOperatorFormula() const; - + CumulativeRewardFormula& asCumulativeRewardFormula(); CumulativeRewardFormula const& asCumulativeRewardFormula() const; - + TotalRewardFormula& asTotalRewardFormula(); TotalRewardFormula const& asTotalRewardFormula() const; - + InstantaneousRewardFormula& asInstantaneousRewardFormula(); InstantaneousRewardFormula const& asInstantaneousRewardFormula() const; - + LongRunAverageRewardFormula& asLongRunAverageRewardFormula(); LongRunAverageRewardFormula const& asLongRunAverageRewardFormula() const; - + ProbabilityOperatorFormula& asProbabilityOperatorFormula(); ProbabilityOperatorFormula const& asProbabilityOperatorFormula() const; - + RewardOperatorFormula& asRewardOperatorFormula(); RewardOperatorFormula const& asRewardOperatorFormula() const; - + OperatorFormula& asOperatorFormula(); OperatorFormula const& asOperatorFormula() const; - + std::vector> getAtomicExpressionFormulas() const; std::vector> getAtomicLabelFormulas() const; std::set getUsedVariables() const; std::set getReferencedRewardModels() const; - + std::shared_ptr asSharedPointer(); std::shared_ptr asSharedPointer() const; - + std::shared_ptr substitute(std::map const& substitution) const; std::shared_ptr substitute(std::function const& expressionSubstitution) const; std::shared_ptr substitute(std::map const& labelSubstitution) const; @@ -228,10 +231,10 @@ namespace storm { * @return An equivalent expression. */ storm::expressions::Expression toExpression(storm::expressions::ExpressionManager const& manager, std::map const& labelToExpressionMapping = {}) const; - + std::string toString() const; virtual std::ostream& writeToStream(std::ostream& out) const = 0; - + virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const; virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const; virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const; @@ -240,7 +243,7 @@ namespace storm { private: // Currently empty. }; - + std::ostream& operator<<(std::ostream& out, Formula const& formula); } } diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp index 41417eeed..471503e2a 100644 --- a/src/storm/logic/FormulaInformationVisitor.cpp +++ b/src/storm/logic/FormulaInformationVisitor.cpp @@ -134,5 +134,13 @@ namespace storm { return boost::any_cast(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast(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(mapped.second->accept(*this, data))); + } + return info; + } + } } diff --git a/src/storm/logic/FormulaInformationVisitor.h b/src/storm/logic/FormulaInformationVisitor.h index ecf5a1ab7..a1f3a3fb0 100644 --- a/src/storm/logic/FormulaInformationVisitor.h +++ b/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; }; } diff --git a/src/storm/logic/FormulaVisitor.h b/src/storm/logic/FormulaVisitor.h index 23673ff50..b1c6db105 100644 --- a/src/storm/logic/FormulaVisitor.h +++ b/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; }; } diff --git a/src/storm/logic/Formulas.h b/src/storm/logic/Formulas.h index cc59b93b6..47ceae22a 100644 --- a/src/storm/logic/Formulas.h +++ b/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" diff --git a/src/storm/logic/FormulasForwardDeclarations.h b/src/storm/logic/FormulasForwardDeclarations.h index 1a6611f13..41aca3c3b 100644 --- a/src/storm/logic/FormulasForwardDeclarations.h +++ b/src/storm/logic/FormulasForwardDeclarations.h @@ -36,6 +36,7 @@ namespace storm { class UnaryPathFormula; class UnaryStateFormula; class UntilFormula; + class HOAPathFormula; } } diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index df79d22a5..0c76dec44 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -322,5 +322,15 @@ namespace storm { result = result && boost::any_cast(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(data); + bool result = inherited.getSpecification().areHOAPathFormulasAllowed(); + // TODO: check + for (auto& mapped : f.getAPMapping()) { + result = result && boost::any_cast(mapped.second->accept(*this, data)); + } + return result; + } } } diff --git a/src/storm/logic/FragmentChecker.h b/src/storm/logic/FragmentChecker.h index 0b0d179aa..e027f7c46 100644 --- a/src/storm/logic/FragmentChecker.h +++ b/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; }; } diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index dc93f7f9c..445ae0b8c 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/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; } diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index f097e940f..5f656695e 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/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; diff --git a/src/storm/logic/HOAPathFormula.cpp b/src/storm/logic/HOAPathFormula.cpp new file mode 100644 index 000000000..915f4f13d --- /dev/null +++ b/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) { + 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>& atomicExpressionFormulas) const { + for (auto& mapped : getAPMapping()) { + mapped.second->gatherAtomicExpressionFormulas(atomicExpressionFormulas); + } + } + + void HOAPathFormula::gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const { + for (auto& mapped : getAPMapping()) { + mapped.second->gatherAtomicLabelFormulas(atomicLabelFormulas); + } + } + + void HOAPathFormula::gatherReferencedRewardModels(std::set& 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; + } + } +} diff --git a/src/storm/logic/HOAPathFormula.h b/src/storm/logic/HOAPathFormula.h new file mode 100644 index 000000000..81352243e --- /dev/null +++ b/src/storm/logic/HOAPathFormula.h @@ -0,0 +1,54 @@ +#pragma once + +#include "storm/logic/PathFormula.h" +#include "storm/logic/FormulaContext.h" + +#include +#include + +namespace storm { + namespace automata { + // fwd + class DeterministicAutomaton; + } + + namespace logic { + class HOAPathFormula : public PathFormula { + public: + typedef std::map> 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); + + 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>& atomicExpressionFormulas) const override; + virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + + std::shared_ptr readAutomaton() const; + + private: + std::string automatonFile; + ap_to_formula_map apToFormulaMap; + + FormulaContext context; + }; + } +} + diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp index a61dccf7c..5a0219242 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp @@ -147,6 +147,15 @@ namespace storm { return boost::any_cast(f.getLeftSubformula().accept(*this, data)) && boost::any_cast(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(ap.second->accept(*this, data))) { + return false; + } + } + return true; + } + bool LiftableTransitionRewardsVisitor::rewardModelHasTransitionRewards(std::string const& rewardModelName) const { if (symbolicModelDescription.hasModel()) { if (symbolicModelDescription.isJaniModel()) { diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.h b/src/storm/logic/LiftableTransitionRewardsVisitor.h index 52a791237..db5530cad 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.h +++ b/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; diff --git a/src/storm/logic/ToExpressionVisitor.cpp b/src/storm/logic/ToExpressionVisitor.cpp index 1e6852d84..41688ad8e 100644 --- a/src/storm/logic/ToExpressionVisitor.cpp +++ b/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."); + } } } diff --git a/src/storm/logic/ToExpressionVisitor.h b/src/storm/logic/ToExpressionVisitor.h index b68b5c438..eb7e261f2 100644 --- a/src/storm/logic/ToExpressionVisitor.h +++ b/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; }; } diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 2e900bb92..f89e1cab5 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/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; diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index cee374f02..c14524f69 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/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) { }