Classes
struct	product_state_hash

Typedefs
typedef std::pair< unsigned, unsigned >	product_state

typedef std::vector< std::pair< unsigned, unsigned > >	product_states

Enumerations
enum	acc_op { and_acc , or_acc , xor_acc , xnor_acc }

Functions
std::shared_ptr< storm::automata::DeterministicAutomaton >	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.

Typedef Documentation

◆ product_state

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

Definition at line 15 of file spotProduct.cpp.

◆ product_states

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

Definition at line 28 of file spotProduct.cpp.

Enumeration Type Documentation

◆ acc_op

enum storm::modelchecker::helper::lexicographic::spothelper::acc_op

Enumerator
and_acc
or_acc
xor_acc
xnor_acc

Definition at line 27 of file spotProduct.cpp.

Function Documentation

◆ ltl2daSpotProduct()

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.

That is done based on a multi-objective formula. For each subformula, a new automaton is created and directly merged into a big product-automaton. Spot is used as tool for this, however, currently it has to be an adapted version of Spot.

Parameters

formula	the multi-objective formula
extracted	extracted atomic propositions (is empty in the beginning, and will be filled in the function)
acceptanceConditions	indication which formula has which streett pairs as acceptance condition

Returns

Definition at line 30 of file spotProduct.cpp.

Classes

Typedefs

Enumerations