SpotProduct.h File Reference

#include "storm/automata/DeterministicAutomaton.h"
#include "storm/logic/ExtractMaximalStateFormulasVisitor.h"
#include "storm/logic/MultiObjectiveFormula.h"

Include dependency graph for SpotProduct.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

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

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< uint64_t > &acceptanceConditions)
	Function that creates a determinitistic automaton with Streett-acceptance condition.