#include "storm/modelchecker/lexicographic/spotHelper/spotProduct.h"
#include <deque>
#include "storm/exceptions/ExpressionEvaluationException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/logic/Formulas.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/utility/macros.h"
#include "storm/adapters/SpotAdapter.h"

Include dependency graph for spotProduct.cpp:

Classes
struct	storm::modelchecker::helper::lexicographic::spothelper::product_state_hash

Namespaces
namespace	storm
	LabParser.cpp.

namespace	storm::modelchecker

namespace	storm::modelchecker::helper

namespace	storm::modelchecker::helper::lexicographic

namespace	storm::modelchecker::helper::lexicographic::spothelper

Typedefs
typedef std::pair< unsigned, unsigned >	storm::modelchecker::helper::lexicographic::spothelper::product_state

typedef std::vector< std::pair< unsigned, unsigned > >	storm::modelchecker::helper::lexicographic::spothelper::product_states

Enumerations
enum	storm::modelchecker::helper::lexicographic::spothelper::acc_op { storm::modelchecker::helper::lexicographic::spothelper::and_acc , storm::modelchecker::helper::lexicographic::spothelper::or_acc , storm::modelchecker::helper::lexicographic::spothelper::xor_acc , storm::modelchecker::helper::lexicographic::spothelper::xnor_acc }

Functions
std::shared_ptr< storm::automata::DeterministicAutomaton >	storm::modelchecker::helper::lexicographic::spothelper::ltl2daSpotProduct (storm::logic::MultiObjectiveFormula const &formula, storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap &extracted, std::vector< uint > &acceptanceConditions)
	Function that creates a determinitistic automaton with Streett-acceptance condition.

Classes

Namespaces

Typedefs

Enumerations

Functions