Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
JaniParser.cpp File Reference
#include "JaniParser.h"
#include "storm/storage/jani/Automaton.h"
#include "storm/storage/jani/AutomatonComposition.h"
#include "storm/storage/jani/Edge.h"
#include "storm/storage/jani/EdgeDestination.h"
#include "storm/storage/jani/Location.h"
#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/ModelType.h"
#include "storm/storage/jani/ParallelComposition.h"
#include "storm/storage/jani/Property.h"
#include "storm/storage/jani/TemplateEdge.h"
#include "storm/storage/jani/expressions/JaniExpressions.h"
#include "storm/storage/jani/visitor/CompositionInformationVisitor.h"
#include "storm/storage/jani/visitor/JaniExpressionSubstitutionVisitor.h"
#include "storm/storage/jani/types/ArrayType.h"
#include "storm/storage/jani/types/BasicType.h"
#include "storm/storage/jani/types/ClockType.h"
#include "storm/storage/jani/types/ContinuousType.h"
#include "storm/storage/jani/types/JaniType.h"
#include "storm/logic/BinaryBooleanPathFormula.h"
#include "storm/logic/RewardAccumulationEliminationVisitor.h"
#include "storm/logic/UnaryBooleanPathFormula.h"
#include "storm/exceptions/FileIoException.h"
#include "storm/exceptions/InvalidJaniException.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/modelchecker/results/FilterType.h"
#include <algorithm>
#include <boost/lexical_cast.hpp>
#include <fstream>
#include <iostream>
#include <optional>
#include <sstream>
#include "storm/io/file.h"
#include "storm/utility/macros.h"
Include dependency graph for JaniParser.cpp:

Go to the source code of this file.

Namespaces

namespace  storm
namespace  storm::parser
 Contains all file parsers and helper classes.

Functions

template<typename ValueType>
std::string storm::parser::getString (typename JaniParser< ValueType >::Json const &structure, std::string const &errorInfo)
template<typename ValueType>
bool storm::parser::getBoolean (typename JaniParser< ValueType >::Json const &structure, std::string const &errorInfo)
template<typename ValueType>
uint64_t storm::parser::getUnsignedInt (typename JaniParser< ValueType >::Json const &structure, std::string const &errorInfo)
template<typename ValueType>
int64_t storm::parser::getSignedInt (typename JaniParser< ValueType >::Json const &structure, std::string const &errorInfo)
void storm::parser::insertLowerUpperTimeBounds (std::vector< std::optional< storm::logic::TimeBound > > &lowerBounds, std::vector< std::optional< storm::logic::TimeBound > > &upperBounds, storm::jani::PropertyInterval const &pi)
std::shared_ptr< storm::logic::Formula const > storm::parser::makeBinaryBooleanFormula (storm::logic::BinaryBooleanOperatorType oper, std::shared_ptr< storm::logic::Formula const > const &left, std::shared_ptr< storm::logic::Formula const > const &right, storm::logic::FormulaContext context)
std::shared_ptr< storm::logic::Formula const > storm::parser::makeUnaryBooleanFormula (storm::logic::UnaryBooleanOperatorType oper, std::shared_ptr< storm::logic::Formula const > const &sub, storm::logic::FormulaContext context)
void storm::parser::ensureNumberOfArguments (uint64_t expected, uint64_t actual, std::string const &opstring, std::string const &errorInfo)
 Helper for parse expression.
void storm::parser::ensureBooleanType (storm::expressions::Expression const &expr, std::string const &opstring, unsigned argNr, std::string const &errorInfo)
 Helper for parse expression.
void storm::parser::ensureNumericalType (storm::expressions::Expression const &expr, std::string const &opstring, unsigned argNr, std::string const &errorInfo)
 Helper for parse expression.
void storm::parser::ensureIntegerType (storm::expressions::Expression const &expr, std::string const &opstring, unsigned argNr, std::string const &errorInfo)
 Helper for parse expression.
void storm::parser::ensureArrayType (storm::expressions::Expression const &expr, std::string const &opstring, unsigned argNr, std::string const &errorInfo)
 Helper for parse expression.
template<typename ValueType>
std::vector< storm::jani::SynchronizationVector > storm::parser::parseSyncVectors (typename JaniParser< ValueType >::Json const &syncVectorStructure)

Variables

template<typename ValueType>
const bool storm::parser::JaniParser< ValueType >::defaultVariableTransient = false
const std::string storm::parser::VARIABLE_AUTOMATON_DELIMITER = "_"
template class STORM_PARSERS_API storm::parser::JaniParser< double >
template class STORM_PARSERS_API storm::parser::JaniParser< storm::RationalNumber >