From f0b58781b1725f1d1dd93a2b498e83e4387b6a26 Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Sun, 25 Jul 2021 10:01:24 +0200
Subject: [PATCH 1/2] added os operator to FormulaContext
---
src/storm/logic/FormulaContext.cpp | 16 ++++++++++++++++
src/storm/logic/FormulaContext.h | 6 ++++--
2 files changed, 20 insertions(+), 2 deletions(-)
create mode 100644 src/storm/logic/FormulaContext.cpp
diff --git a/src/storm/logic/FormulaContext.cpp b/src/storm/logic/FormulaContext.cpp
new file mode 100644
index 000000000..5bf9ba058
--- /dev/null
+++ b/src/storm/logic/FormulaContext.cpp
@@ -0,0 +1,16 @@
+#include "storm/logic/FormulaContext.h"
+
+namespace storm {
+ namespace logic {
+ std::ostream& operator<<(std::ostream& out, FormulaContext const& formulaContext) {
+ switch(formulaContext) {
+ case storm::logic::FormulaContext::Undefined: out << "Undefined"; break;
+ case storm::logic::FormulaContext::Probability: out << "Probability"; break;
+ case storm::logic::FormulaContext::Reward: out << "Reward"; break;
+ case storm::logic::FormulaContext::LongRunAverage: out << "LongRunAverage"; break;
+ case storm::logic::FormulaContext::Time: out << "Time"; break;
+ }
+ return out;
+ }
+ }
+}
diff --git a/src/storm/logic/FormulaContext.h b/src/storm/logic/FormulaContext.h
index 98786731d..c178a679d 100644
--- a/src/storm/logic/FormulaContext.h
+++ b/src/storm/logic/FormulaContext.h
@@ -1,11 +1,13 @@
#ifndef STORM_LOGIC_FORMULACONTEXT_H_
#define STORM_LOGIC_FORMULACONTEXT_H_
+#include <sstream>
+
namespace storm {
namespace logic {
-
+
enum class FormulaContext { Undefined, Probability, Reward, LongRunAverage, Time };
-
+ std::ostream& operator<<(std::ostream& out, FormulaContext const& formulaContext);
}
}
From f9d2df0b0a2e896547d6eb70dc83571cdd2369e3 Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Sun, 25 Jul 2021 15:28:14 +0200
Subject: [PATCH 2/2] move ConstantDataType and added ostream
---
src/storm-parsers/parser/ConstantDataType.cpp | 14 ++++++++++++++
src/storm-parsers/parser/ConstantDataType.h | 14 ++++++++++++++
src/storm-parsers/parser/FormulaParserGrammar.h | 5 +----
3 files changed, 29 insertions(+), 4 deletions(-)
create mode 100644 src/storm-parsers/parser/ConstantDataType.cpp
create mode 100644 src/storm-parsers/parser/ConstantDataType.h
diff --git a/src/storm-parsers/parser/ConstantDataType.cpp b/src/storm-parsers/parser/ConstantDataType.cpp
new file mode 100644
index 000000000..52ab7c9d9
--- /dev/null
+++ b/src/storm-parsers/parser/ConstantDataType.cpp
@@ -0,0 +1,14 @@
+#include "ConstantDataType.h"
+
+namespace storm {
+ namespace parser {
+ std::ostream& operator<<(std::ostream& out, ConstantDataType const& constantDataType) {
+ switch(constantDataType) {
+ case storm::parser::ConstantDataType::Bool: out << "Bool"; break;
+ case storm::parser::ConstantDataType::Integer: out << "Integer"; break;
+ case storm::parser::ConstantDataType::Rational: out << "Rational"; break;
+ }
+ return out;
+ }
+ }
+}
diff --git a/src/storm-parsers/parser/ConstantDataType.h b/src/storm-parsers/parser/ConstantDataType.h
new file mode 100644
index 000000000..b8e7aa975
--- /dev/null
+++ b/src/storm-parsers/parser/ConstantDataType.h
@@ -0,0 +1,14 @@
+#pragma once
+
+#include <sstream>
+
+namespace storm {
+ namespace parser {
+
+ enum class ConstantDataType {
+ Bool, Integer, Rational
+ };
+
+ std::ostream& operator<<(std::ostream& out, ConstantDataType const& constantDataType);
+ }
+}
diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h
index 75903d04a..9ea0e5355 100644
--- a/src/storm-parsers/parser/FormulaParserGrammar.h
+++ b/src/storm-parsers/parser/FormulaParserGrammar.h
@@ -10,6 +10,7 @@
#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"
@@ -148,10 +149,6 @@ namespace storm {
qi::rule<Iterator, std::vector<storm::jani::Property>(), Skipper> start;
- enum class ConstantDataType {
- Bool, Integer, Rational
- };
-
qi::rule<Iterator, qi::unused_type(), qi::locals<ConstantDataType>, Skipper> constantDefinition;
qi::rule<Iterator, std::string(), Skipper> identifier;
qi::rule<Iterator, std::string(), Skipper> formulaName;