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; 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); } }