Browse Source

Merge pull request 'Fix Formula Parser Debug Methods' (#25) from formula_parser_debug into main

Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/25
tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
dadcda9f0c
  1. 14
      src/storm-parsers/parser/ConstantDataType.cpp
  2. 14
      src/storm-parsers/parser/ConstantDataType.h
  3. 5
      src/storm-parsers/parser/FormulaParserGrammar.h
  4. 16
      src/storm/logic/FormulaContext.cpp
  5. 6
      src/storm/logic/FormulaContext.h

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

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

5
src/storm-parsers/parser/FormulaParserGrammar.h

@ -10,6 +10,7 @@
#include "storm/storage/jani/Property.h" #include "storm/storage/jani/Property.h"
#include "storm/logic/Formulas.h" #include "storm/logic/Formulas.h"
#include "storm-parsers/parser/ExpressionParser.h" #include "storm-parsers/parser/ExpressionParser.h"
#include "storm-parsers/parser/ConstantDataType.h"
#include "storm/modelchecker/results/FilterType.h" #include "storm/modelchecker/results/FilterType.h"
@ -148,10 +149,6 @@ namespace storm {
qi::rule<Iterator, std::vector<storm::jani::Property>(), Skipper> start; 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, qi::unused_type(), qi::locals<ConstantDataType>, Skipper> constantDefinition;
qi::rule<Iterator, std::string(), Skipper> identifier; qi::rule<Iterator, std::string(), Skipper> identifier;
qi::rule<Iterator, std::string(), Skipper> formulaName; qi::rule<Iterator, std::string(), Skipper> formulaName;

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

6
src/storm/logic/FormulaContext.h

@ -1,11 +1,13 @@
#ifndef STORM_LOGIC_FORMULACONTEXT_H_ #ifndef STORM_LOGIC_FORMULACONTEXT_H_
#define STORM_LOGIC_FORMULACONTEXT_H_ #define STORM_LOGIC_FORMULACONTEXT_H_
#include <sstream>
namespace storm { namespace storm {
namespace logic { namespace logic {
enum class FormulaContext { Undefined, Probability, Reward, LongRunAverage, Time }; enum class FormulaContext { Undefined, Probability, Reward, LongRunAverage, Time };
std::ostream& operator<<(std::ostream& out, FormulaContext const& formulaContext);
} }
} }

Loading…
Cancel
Save