From c52fcba6a27eb4a8effc092c9c955920971dbe5f Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Thu, 19 Nov 2020 18:08:51 +0100
Subject: [PATCH] added multiple Visitor methods for gameFormulas
---
src/storm/logic/CloneVisitor.cpp | 18 +-
src/storm/logic/CloneVisitor.h | 1 +
src/storm/logic/Formula.cpp | 246 +++++++++---------
src/storm/logic/Formula.h | 7 +-
src/storm/logic/FormulaInformationVisitor.cpp | 18 +-
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 +
.../LiftableTransitionRewardsVisitor.cpp | 18 +-
.../logic/LiftableTransitionRewardsVisitor.h | 1 +
src/storm/logic/ToExpressionVisitor.cpp | 36 +--
src/storm/logic/ToExpressionVisitor.h | 1 +
src/storm/storage/jani/JSONExporter.cpp | 10 +-
src/storm/storage/jani/JSONExporter.h | 1 +
17 files changed, 208 insertions(+), 164 deletions(-)
diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp
index cb24e7d8b..8c8d82ca2 100644
--- a/src/storm/logic/CloneVisitor.cpp
+++ b/src/storm/logic/CloneVisitor.cpp
@@ -76,30 +76,36 @@ namespace storm {
return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext()));
}
}
-
+
boost::any CloneVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<TimeOperatorFormula>(subformula, f.getOperatorInformation()));
}
-
+
boost::any CloneVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<GloballyFormula>(subformula));
}
-
+
+ boost::any CloneVisitor::visit(GameFormula const& f, boost::any const& data) const {
+ STORM_PRINT_AND_LOG("CloneVisitor called for GameFormula\n");
+ std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+ return std::static_pointer_cast<Formula>(std::make_shared<GameFormula>(f.getCoalition(), subformula));
+ }
+
boost::any CloneVisitor::visit(InstantaneousRewardFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<InstantaneousRewardFormula>(f));
}
-
+
boost::any CloneVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageOperatorFormula>(subformula, f.getOperatorInformation()));
}
-
+
boost::any CloneVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageRewardFormula>(f));
}
-
+
boost::any CloneVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
std::vector<std::shared_ptr<Formula const>> subformulas;
for(auto const& subF : f.getSubformulas()){
diff --git a/src/storm/logic/CloneVisitor.h b/src/storm/logic/CloneVisitor.h
index 4b1d620ee..5ff29e816 100644
--- a/src/storm/logic/CloneVisitor.h
+++ b/src/storm/logic/CloneVisitor.h
@@ -22,6 +22,7 @@ namespace storm {
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(GameFormula const& f, boost::any const& data) const override;
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp
index 58970c77b..0a310713d 100644
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@@ -14,313 +14,317 @@ namespace storm {
bool Formula::isPathFormula() const {
return false;
}
-
+
bool Formula::isStateFormula() const {
return false;
}
-
+
bool Formula::isMultiObjectiveFormula() const {
return false;
}
-
+
bool Formula::isQuantileFormula() const {
return false;
}
-
+
bool Formula::isBinaryStateFormula() const {
return false;
}
-
+
bool Formula::isUnaryStateFormula() const {
return false;
}
-
+
bool Formula::isBinaryBooleanStateFormula() const {
return false;
}
-
+
bool Formula::isUnaryBooleanStateFormula() const {
return false;
}
-
+
bool Formula::isBooleanLiteralFormula() const {
return false;
}
-
+
bool Formula::isTrueFormula() const {
return false;
}
-
+
bool Formula::isFalseFormula() const {
return false;
}
-
+
bool Formula::isAtomicExpressionFormula() const {
return false;
}
-
+
bool Formula::isAtomicLabelFormula() const {
return false;
}
-
+
bool Formula::isUntilFormula() const {
return false;
}
-
+
bool Formula::isBoundedUntilFormula() const {
return false;
}
-
+
bool Formula::isEventuallyFormula() const {
return false;
}
-
+
bool Formula::isReachabilityProbabilityFormula() const {
return false;
}
-
+
bool Formula::isGloballyFormula() const {
return false;
}
-
+
bool Formula::isBinaryPathFormula() const {
return false;
}
-
+
bool Formula::isUnaryPathFormula() const {
return false;
}
-
+
bool Formula::isConditionalProbabilityFormula() const {
return false;
}
-
+
bool Formula::isConditionalRewardFormula() const {
return false;
}
-
+
bool Formula::isProbabilityPathFormula() const {
return false;
}
-
+
bool Formula::isRewardPathFormula() const {
return false;
}
-
+
bool Formula::isTimePathFormula() const {
return false;
}
-
+
bool Formula::isNextFormula() const {
return false;
}
-
+
bool Formula::isLongRunAverageOperatorFormula() const {
return false;
}
-
+
bool Formula::isTimeOperatorFormula() const {
return false;
}
-
+
bool Formula::isCumulativeRewardFormula() const {
return false;
}
-
+
bool Formula::isInstantaneousRewardFormula() const {
return false;
}
-
+
bool Formula::isReachabilityRewardFormula() const {
return false;
}
-
+
bool Formula::isLongRunAverageRewardFormula() const {
return false;
}
-
+
bool Formula::isTotalRewardFormula() const {
return false;
}
-
+
bool Formula::isReachabilityTimeFormula() const {
return false;
}
-
+
+ bool Formula::isGameFormula() const {
+ return false;
+ }
+
bool Formula::isProbabilityOperatorFormula() const {
return false;
}
-
+
bool Formula::isRewardOperatorFormula() const {
return false;
}
-
+
bool Formula::isOperatorFormula() const {
return false;
}
-
+
bool Formula::hasQualitativeResult() const {
return true;
}
-
+
bool Formula::hasQuantitativeResult() const {
return false;
}
-
+
bool Formula::isInFragment(FragmentSpecification const& fragment) const {
FragmentChecker checker;
return checker.conformsToSpecification(*this, fragment);
}
-
+
FormulaInformation Formula::info() const {
FormulaInformationVisitor visitor;
return visitor.getInformation(*this);
}
-
+
std::shared_ptr<Formula const> Formula::getTrueFormula() {
return std::shared_ptr<Formula const>(new BooleanLiteralFormula(true));
}
-
+
bool Formula::isInitialFormula() const {
return this->isAtomicLabelFormula() && this->asAtomicLabelFormula().getLabel() == "init";
}
-
+
PathFormula& Formula::asPathFormula() {
return dynamic_cast<PathFormula&>(*this);
}
-
+
PathFormula const& Formula::asPathFormula() const {
return dynamic_cast<PathFormula const&>(*this);
}
-
+
StateFormula& Formula::asStateFormula() {
return dynamic_cast<StateFormula&>(*this);
}
-
+
StateFormula const& Formula::asStateFormula() const {
return dynamic_cast<StateFormula const&>(*this);
}
-
+
MultiObjectiveFormula& Formula::asMultiObjectiveFormula() {
return dynamic_cast<MultiObjectiveFormula&>(*this);
}
-
+
MultiObjectiveFormula const& Formula::asMultiObjectiveFormula() const {
return dynamic_cast<MultiObjectiveFormula const&>(*this);
}
-
+
QuantileFormula& Formula::asQuantileFormula() {
return dynamic_cast<QuantileFormula&>(*this);
}
-
+
QuantileFormula const& Formula::asQuantileFormula() const {
return dynamic_cast<QuantileFormula const&>(*this);
}
-
+
BinaryStateFormula& Formula::asBinaryStateFormula() {
return dynamic_cast<BinaryStateFormula&>(*this);
}
-
+
BinaryStateFormula const& Formula::asBinaryStateFormula() const {
return dynamic_cast<BinaryStateFormula const&>(*this);
}
-
+
UnaryStateFormula& Formula::asUnaryStateFormula() {
return dynamic_cast<UnaryStateFormula&>(*this);
}
-
+
UnaryStateFormula const& Formula::asUnaryStateFormula() const {
return dynamic_cast<UnaryStateFormula const&>(*this);
}
-
+
ConditionalFormula& Formula::asConditionalFormula() {
return dynamic_cast<ConditionalFormula&>(*this);
}
-
+
ConditionalFormula const& Formula::asConditionalFormula() const {
return dynamic_cast<ConditionalFormula const&>(*this);
}
-
+
BinaryBooleanStateFormula& Formula::asBinaryBooleanStateFormula() {
return dynamic_cast<BinaryBooleanStateFormula&>(*this);
}
-
+
BinaryBooleanStateFormula const& Formula::asBinaryBooleanStateFormula() const {
return dynamic_cast<BinaryBooleanStateFormula const&>(*this);
}
-
+
UnaryBooleanStateFormula& Formula::asUnaryBooleanStateFormula() {
return dynamic_cast<UnaryBooleanStateFormula&>(*this);
}
-
+
UnaryBooleanStateFormula const& Formula::asUnaryBooleanStateFormula() const {
return dynamic_cast<UnaryBooleanStateFormula const&>(*this);
}
-
+
BooleanLiteralFormula& Formula::asBooleanLiteralFormula() {
return dynamic_cast<BooleanLiteralFormula&>(*this);
}
-
+
BooleanLiteralFormula const& Formula::asBooleanLiteralFormula() const {
return dynamic_cast<BooleanLiteralFormula const&>(*this);
}
-
+
AtomicExpressionFormula& Formula::asAtomicExpressionFormula() {
return dynamic_cast<AtomicExpressionFormula&>(*this);
}
-
+
AtomicExpressionFormula const& Formula::asAtomicExpressionFormula() const {
return dynamic_cast<AtomicExpressionFormula const&>(*this);
}
-
+
AtomicLabelFormula& Formula::asAtomicLabelFormula() {
return dynamic_cast<AtomicLabelFormula&>(*this);
}
-
+
AtomicLabelFormula const& Formula::asAtomicLabelFormula() const {
return dynamic_cast<AtomicLabelFormula const&>(*this);
}
-
+
UntilFormula& Formula::asUntilFormula() {
return dynamic_cast<UntilFormula&>(*this);
}
-
+
UntilFormula const& Formula::asUntilFormula() const {
return dynamic_cast<UntilFormula const&>(*this);
}
-
+
BoundedUntilFormula& Formula::asBoundedUntilFormula() {
return dynamic_cast<BoundedUntilFormula&>(*this);
}
-
+
BoundedUntilFormula const& Formula::asBoundedUntilFormula() const {
return dynamic_cast<BoundedUntilFormula const&>(*this);
}
-
+
EventuallyFormula& Formula::asEventuallyFormula() {
return dynamic_cast<EventuallyFormula&>(*this);
}
-
+
EventuallyFormula const& Formula::asEventuallyFormula() const {
return dynamic_cast<EventuallyFormula const&>(*this);
}
-
+
EventuallyFormula& Formula::asReachabilityRewardFormula() {
return dynamic_cast<EventuallyFormula&>(*this);
}
-
+
EventuallyFormula const& Formula::asReachabilityRewardFormula() const {
return dynamic_cast<EventuallyFormula const&>(*this);
}
-
+
EventuallyFormula& Formula::asReachabilityProbabilityFormula() {
return dynamic_cast<EventuallyFormula&>(*this);
}
-
+
EventuallyFormula const& Formula::asReachabilityProbabilityFormula() const {
return dynamic_cast<EventuallyFormula const&>(*this);
}
-
+
EventuallyFormula& Formula::asReachabilityTimeFormula() {
return dynamic_cast<EventuallyFormula&>(*this);
}
@@ -328,160 +332,160 @@ namespace storm {
EventuallyFormula const& Formula::asReachabilityTimeFormula() const {
return dynamic_cast<EventuallyFormula const&>(*this);
}
-
+
GloballyFormula& Formula::asGloballyFormula() {
return dynamic_cast<GloballyFormula&>(*this);
}
-
+
GloballyFormula const& Formula::asGloballyFormula() const {
return dynamic_cast<GloballyFormula const&>(*this);
}
-
+
BinaryPathFormula& Formula::asBinaryPathFormula() {
return dynamic_cast<BinaryPathFormula&>(*this);
}
-
+
BinaryPathFormula const& Formula::asBinaryPathFormula() const {
return dynamic_cast<BinaryPathFormula const&>(*this);
}
-
+
UnaryPathFormula& Formula::asUnaryPathFormula() {
return dynamic_cast<UnaryPathFormula&>(*this);
}
-
+
UnaryPathFormula const& Formula::asUnaryPathFormula() const {
return dynamic_cast<UnaryPathFormula const&>(*this);
}
-
+
NextFormula& Formula::asNextFormula() {
return dynamic_cast<NextFormula&>(*this);
}
-
+
NextFormula const& Formula::asNextFormula() const {
return dynamic_cast<NextFormula const&>(*this);
}
-
+
LongRunAverageOperatorFormula& Formula::asLongRunAverageOperatorFormula() {
return dynamic_cast<LongRunAverageOperatorFormula&>(*this);
}
-
+
LongRunAverageOperatorFormula const& Formula::asLongRunAverageOperatorFormula() const {
return dynamic_cast<LongRunAverageOperatorFormula const&>(*this);
}
-
+
TimeOperatorFormula& Formula::asTimeOperatorFormula() {
return dynamic_cast<TimeOperatorFormula&>(*this);
}
-
+
TimeOperatorFormula const& Formula::asTimeOperatorFormula() const {
return dynamic_cast<TimeOperatorFormula const&>(*this);
}
-
+
CumulativeRewardFormula& Formula::asCumulativeRewardFormula() {
return dynamic_cast<CumulativeRewardFormula&>(*this);
}
-
+
CumulativeRewardFormula const& Formula::asCumulativeRewardFormula() const {
return dynamic_cast<CumulativeRewardFormula const&>(*this);
}
-
+
TotalRewardFormula& Formula::asTotalRewardFormula() {
return dynamic_cast<TotalRewardFormula&>(*this);
}
-
+
TotalRewardFormula const& Formula::asTotalRewardFormula() const {
return dynamic_cast<TotalRewardFormula const&>(*this);
}
-
+
InstantaneousRewardFormula& Formula::asInstantaneousRewardFormula() {
return dynamic_cast<InstantaneousRewardFormula&>(*this);
}
-
+
InstantaneousRewardFormula const& Formula::asInstantaneousRewardFormula() const {
return dynamic_cast<InstantaneousRewardFormula const&>(*this);
}
-
+
LongRunAverageRewardFormula& Formula::asLongRunAverageRewardFormula() {
return dynamic_cast<LongRunAverageRewardFormula&>(*this);
}
-
+
LongRunAverageRewardFormula const& Formula::asLongRunAverageRewardFormula() const {
return dynamic_cast<LongRunAverageRewardFormula const&>(*this);
}
-
+
ProbabilityOperatorFormula& Formula::asProbabilityOperatorFormula() {
return dynamic_cast<ProbabilityOperatorFormula&>(*this);
}
-
+
ProbabilityOperatorFormula const& Formula::asProbabilityOperatorFormula() const {
return dynamic_cast<ProbabilityOperatorFormula const&>(*this);
}
-
+
RewardOperatorFormula& Formula::asRewardOperatorFormula() {
return dynamic_cast<RewardOperatorFormula&>(*this);
}
-
+
RewardOperatorFormula const& Formula::asRewardOperatorFormula() const {
return dynamic_cast<RewardOperatorFormula const&>(*this);
}
-
+
OperatorFormula& Formula::asOperatorFormula() {
return dynamic_cast<OperatorFormula&>(*this);
}
-
+
OperatorFormula const& Formula::asOperatorFormula() const {
return dynamic_cast<OperatorFormula const&>(*this);
}
-
+
std::vector<std::shared_ptr<AtomicExpressionFormula const>> Formula::getAtomicExpressionFormulas() const {
std::vector<std::shared_ptr<AtomicExpressionFormula const>> result;
this->gatherAtomicExpressionFormulas(result);
return result;
}
-
+
std::vector<std::shared_ptr<AtomicLabelFormula const>> Formula::getAtomicLabelFormulas() const {
std::vector<std::shared_ptr<AtomicLabelFormula const>> result;
this->gatherAtomicLabelFormulas(result);
return result;
}
-
+
std::set<storm::expressions::Variable> Formula::getUsedVariables() const {
std::set<storm::expressions::Variable> usedVariables;
this->gatherUsedVariables(usedVariables);
return usedVariables;
}
-
+
std::set<std::string> Formula::getReferencedRewardModels() const {
std::set<std::string> referencedRewardModels;
this->gatherReferencedRewardModels(referencedRewardModels);
return referencedRewardModels;
}
-
+
std::shared_ptr<Formula> Formula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
storm::expressions::JaniExpressionSubstitutionVisitor<std::map<storm::expressions::Variable, storm::expressions::Expression>> v(substitution);
return substitute([&v](storm::expressions::Expression const& exp) {return v.substitute(exp);});
}
-
+
std::shared_ptr<Formula> Formula::substitute(std::function<storm::expressions::Expression(storm::expressions::Expression const&)> const& expressionSubstitution) const {
ExpressionSubstitutionVisitor visitor;
return visitor.substitute(*this, expressionSubstitution);
}
-
+
std::shared_ptr<Formula> Formula::substitute(std::map<std::string, storm::expressions::Expression> const& labelSubstitution) const {
LabelSubstitutionVisitor visitor(labelSubstitution);
return visitor.substitute(*this);
}
-
+
std::shared_ptr<Formula> Formula::substitute(std::map<std::string, std::string> const& labelSubstitution) const {
LabelSubstitutionVisitor visitor(labelSubstitution);
return visitor.substitute(*this);
}
-
+
std::shared_ptr<Formula> Formula::substituteRewardModelNames(std::map<std::string, std::string> const& rewardModelNameSubstitution) const {
RewardModelNameSubstitutionVisitor visitor(rewardModelNameSubstitution);
return visitor.substitute(*this);
}
-
+
storm::expressions::Expression Formula::toExpression(storm::expressions::ExpressionManager const& manager, std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping) const {
ToExpressionVisitor visitor;
if (labelToExpressionMapping.empty()) {
@@ -490,37 +494,37 @@ namespace storm {
return visitor.toExpression(*this->substitute(labelToExpressionMapping), manager);
}
}
-
+
std::shared_ptr<Formula const> Formula::asSharedPointer() {
return this->shared_from_this();
}
-
+
std::shared_ptr<Formula const> Formula::asSharedPointer() const {
return this->shared_from_this();
}
-
+
void Formula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>&) const {
return;
}
-
+
void Formula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>&) const {
return;
}
-
+
void Formula::gatherReferencedRewardModels(std::set<std::string>&) const {
return;
}
-
+
void Formula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
return;
}
-
+
std::string Formula::toString() const {
std::stringstream str2;
writeToStream(str2);
return str2.str();
}
-
+
std::ostream& operator<<(std::ostream& out, Formula const& formula) {
return formula.writeToStream(out);
}
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index dc6396e71..8fabb4fe0 100644
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@@ -78,10 +78,13 @@ namespace storm {
virtual bool isReachabilityRewardFormula() const;
virtual bool isLongRunAverageRewardFormula() const;
virtual bool isTotalRewardFormula() const;
-
+
// Expected time formulas.
virtual bool isReachabilityTimeFormula() const;
-
+
+ // Game formulas.
+ virtual bool isGameFormula() const;
+
// Type checks for abstract intermediate classes.
virtual bool isBinaryPathFormula() const;
virtual bool isBinaryStateFormula() const;
diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp
index e4e9a15ed..41976aa57 100644
--- a/src/storm/logic/FormulaInformationVisitor.cpp
+++ b/src/storm/logic/FormulaInformationVisitor.cpp
@@ -60,36 +60,40 @@ namespace storm {
}
return result;
}
-
+
boost::any FormulaInformationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this, data);
}
-
+
boost::any FormulaInformationVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this, data);
}
-
+
boost::any FormulaInformationVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this, data);
}
-
+
+ boost::any FormulaInformationVisitor::visit(GameFormula const& f, boost::any const& data) const {
+ return f.getSubformula().accept(*this, data);
+ }
+
boost::any FormulaInformationVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const {
return FormulaInformation();
}
-
+
boost::any FormulaInformationVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
FormulaInformation result;
result.setContainsLongRunFormula(true);
result.join(boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data)));
return result;
}
-
+
boost::any FormulaInformationVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const {
FormulaInformation result;
result.setContainsLongRunFormula(true);
return result;
}
-
+
boost::any FormulaInformationVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
FormulaInformation result;
for(auto const& subF : f.getSubformulas()){
diff --git a/src/storm/logic/FormulaInformationVisitor.h b/src/storm/logic/FormulaInformationVisitor.h
index 7ba8b70b9..617386961 100644
--- a/src/storm/logic/FormulaInformationVisitor.h
+++ b/src/storm/logic/FormulaInformationVisitor.h
@@ -21,6 +21,7 @@ namespace storm {
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(GameFormula const& f, boost::any const& data) const override;
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
diff --git a/src/storm/logic/FormulaVisitor.h b/src/storm/logic/FormulaVisitor.h
index 1eaf6791d..6bf5b8c50 100644
--- a/src/storm/logic/FormulaVisitor.h
+++ b/src/storm/logic/FormulaVisitor.h
@@ -22,6 +22,7 @@ namespace storm {
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const = 0;
+ virtual boost::any visit(GameFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const = 0;
diff --git a/src/storm/logic/Formulas.h b/src/storm/logic/Formulas.h
index bdda5c863..f054794e7 100644
--- a/src/storm/logic/Formulas.h
+++ b/src/storm/logic/Formulas.h
@@ -8,6 +8,7 @@
#include "storm/logic/BoundedUntilFormula.h"
#include "storm/logic/CumulativeRewardFormula.h"
#include "storm/logic/EventuallyFormula.h"
+#include "storm/logic/GameFormula.h"
#include "storm/logic/GloballyFormula.h"
#include "storm/logic/InstantaneousRewardFormula.h"
#include "storm/logic/NextFormula.h"
diff --git a/src/storm/logic/FormulasForwardDeclarations.h b/src/storm/logic/FormulasForwardDeclarations.h
index 170316fc7..2d1661418 100644
--- a/src/storm/logic/FormulasForwardDeclarations.h
+++ b/src/storm/logic/FormulasForwardDeclarations.h
@@ -17,6 +17,7 @@ namespace storm {
class EventuallyFormula;
class TimeOperatorFormula;
class GloballyFormula;
+ class GameFormula;
class InstantaneousRewardFormula;
class LongRunAverageOperatorFormula;
class LongRunAverageRewardFormula;
diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp
index b669e75bd..fb95572f9 100644
--- a/src/storm/logic/FragmentChecker.cpp
+++ b/src/storm/logic/FragmentChecker.cpp
@@ -188,12 +188,18 @@ namespace storm {
result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
return result;
}
-
+
+ boost::any FragmentChecker::visit(GameFormula const& f, boost::any const& data) const {
+ InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+ bool result = inherited.getSpecification().areCoalitionOperatorsAllowed();
+ return result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+ }
+
boost::any FragmentChecker::visit(InstantaneousRewardFormula const&, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
return inherited.getSpecification().areInstantaneousRewardFormulasAllowed();
}
-
+
boost::any FragmentChecker::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areLongRunAverageOperatorsAllowed();
diff --git a/src/storm/logic/FragmentChecker.h b/src/storm/logic/FragmentChecker.h
index 485a205aa..c6e6100ee 100644
--- a/src/storm/logic/FragmentChecker.h
+++ b/src/storm/logic/FragmentChecker.h
@@ -22,6 +22,7 @@ namespace storm {
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(GameFormula const& f, boost::any const& data) const override;
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
index 99eeb444b..bdb8ba58e 100644
--- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
+++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
@@ -62,31 +62,35 @@ namespace storm {
}
return true;
}
-
+
boost::any LiftableTransitionRewardsVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this, data);
}
-
+
boost::any LiftableTransitionRewardsVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this, data);
}
-
+
boost::any LiftableTransitionRewardsVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this, data);
}
-
+
+ boost::any LiftableTransitionRewardsVisitor::visit(GameFormula const& f, boost::any const& data) const {
+ return true;
+ }
+
boost::any LiftableTransitionRewardsVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const {
return true;
}
-
+
boost::any LiftableTransitionRewardsVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this, data);
}
-
+
boost::any LiftableTransitionRewardsVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const {
return true;
}
-
+
boost::any LiftableTransitionRewardsVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
bool result = true;
for (auto const& subF : f.getSubformulas()){
diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.h b/src/storm/logic/LiftableTransitionRewardsVisitor.h
index c09f9c25b..bbac6b7c2 100644
--- a/src/storm/logic/LiftableTransitionRewardsVisitor.h
+++ b/src/storm/logic/LiftableTransitionRewardsVisitor.h
@@ -28,6 +28,7 @@ namespace storm {
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(GameFormula const& f, boost::any const& data) const override;
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
diff --git a/src/storm/logic/ToExpressionVisitor.cpp b/src/storm/logic/ToExpressionVisitor.cpp
index 27ea1fa6b..8eb8444fc 100644
--- a/src/storm/logic/ToExpressionVisitor.cpp
+++ b/src/storm/logic/ToExpressionVisitor.cpp
@@ -46,67 +46,71 @@ namespace storm {
}
return result;
}
-
+
boost::any ToExpressionVisitor::visit(BoundedUntilFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(ConditionalFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(CumulativeRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(EventuallyFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(TimeOperatorFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(GloballyFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
+ boost::any ToExpressionVisitor::visit(GameFormula const&, boost::any const&) const {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+ }
+
boost::any ToExpressionVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(LongRunAverageOperatorFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(MultiObjectiveFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(QuantileFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(NextFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(ProbabilityOperatorFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(RewardOperatorFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(TotalRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
-
+
boost::any ToExpressionVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
storm::expressions::Expression subexpression = boost::any_cast<storm::expressions::Expression>(f.getSubformula().accept(*this, data));
switch (f.getOperator()) {
diff --git a/src/storm/logic/ToExpressionVisitor.h b/src/storm/logic/ToExpressionVisitor.h
index 345698f5a..675dbbcba 100644
--- a/src/storm/logic/ToExpressionVisitor.h
+++ b/src/storm/logic/ToExpressionVisitor.h
@@ -22,6 +22,7 @@ namespace storm {
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(GameFormula const& f, boost::any const& data) const override;
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageRewardFormula 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 79748e5da..4236f4c6f 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -324,18 +324,22 @@ namespace storm {
}
return opDecl;
}
-
+
boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const {
ExportJsonType opDecl;
opDecl["op"] = "G";
opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data));
return opDecl;
}
-
+
+ boost::any FormulaToJaniJson::visit(storm::logic::GameFormula const& f, boost::any const& data) const {
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We currently do not support conversion of game formulas to Jani. (Does jani support games?)");
+ }
+
boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an instanteneous reward formula");
}
-
+
boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const {
ExportJsonType opDecl;
if(f.hasBound()) {
diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h
index 7c11358c6..9408cff82 100644
--- a/src/storm/storage/jani/JSONExporter.h
+++ b/src/storm/storage/jani/JSONExporter.h
@@ -57,6 +57,7 @@ namespace storm {
virtual boost::any visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const;
+ virtual boost::any visit(storm::logic::GameFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::GloballyFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const;