Parity Class Reference

Class of parity automata. More...

#include <Parity.hh>

Inheritance diagram for Parity:

Collaboration diagram for Parity:

Classes
class	Determ
	Helper class to perform DPW determinization. More...
struct	DotAttributes
class	OSPGame
	Helper class to solve 3-priority parity games. More...
class	Simul
	Helper class for simulation equivalence computation. More...

Public Member Functions
	Parity (Cudd mgr)
	Constructor.
	Parity (Cudd mgr, std::string const &filename, Verbosity::Level verbosity=Verbosity::Silent, bool noMdp=false)
	Constructor from HOA file.
	Parity (Cudd mgr, std::istream &is, Verbosity::Level verbosity=Verbosity::Silent, bool noMdp=false)
	Constructor from HOA stream.
void	addTransition (State source, State destination, BDD label, Priority priority)
	Adds a transition to a state of the automaton.
void	printDot (std::string graphname=std::string("parity"), std::string filename=std::string("-"), bool showtrees=false) const
	Converts automaton to dot format.
void	printDot (std::string graphname, DotAttributes const &attributes, std::string filename=std::string("-"), bool showtrees=false) const
	Converts automaton to dot format.
void	printHOA (std::string const &name=std::string("parity"), std::string filename=std::string("-")) const
	Writes automaton in HOA format.
std::vector< State >	getStates (void) const
	Returns the state set.
Priority	getPriority (State source, BDD label, State destination, bool silent=false) const
	Gets the priority of a transition. More...
Priority	getMaxPriority (void) const
	Gets maximum priority of automaton.
Priority	getMinPriority (void) const
	Gets minimum priority of automaton.
std::vector< EdgeSet >	edgePartition (void) const
	Returns the partition of the edges according to their priorities.
std::map< State, unsigned >	classifyStates (void) const
	Classify states according to the priorities of their transitions.
Parity	determinize (void) const
	Returns determinized automaton. More...
unsigned	CartonMaceiras (void)
	Reduces index of acceptance condition. More...
unsigned	minimumIndex (void)
	Reduces index of acceptance condition. More...
Parity	toLDPW (bool epsilonJumps=false) const
	Converts DPW to LDPW with priorities 0 and 1.
void	directSimulationRelation (std::set< StatePair > &simul) const
	Computes direct simulation relation. More...
void	directSimulationMinimization (void)
	Minimizes automaton based on direct simulation.
void	stateMinimization (void)
	Minimizes deterministic automaton based on state equivalence.
void	trim (void)
	Trims automaton of states on no accepting path.
void	makeComplete (void)
	Adds rejecting trap if necessary to make automaton complete.
void	safetyLiveness (Parity &safety, Parity &liveness) const
	Decomposes automaton into safety and liveness components.
bool	isTriviallyEmpty (void) const
	Checks whether the automaton is trivially empty.
bool	isTerminal (bool ignoreTransient=true) const
	Checks whether the automaton is terminal. More...
StateSet	getTrapStates (void) const
	Returns set of trap states. More...
void	unite (Parity const &second)
	Takes the nondeterministic union with another automaton.
Parity	complement (void) const
	Return complement of automaton.
void	solveOneStreettPairGame (StateSet const &spoilerStates, StateSet &dwinning, StateMap &dstrategy, StateMap &sstrategy) const
	Solve one-Streett-pair game. More...
bool	leadSimulates (void) const
	Checks whether automaton lead-simulates itself.
bool	fairSimulates (Parity const &other) const
	Checks whether automaton fair-simulates other.
bool	directSimulates (Parity const &other) const
	Checks whether automaton direct-simulates other.
Public Member Functions inherited from LTS< ParityTransition >
const_iterator	cbegin ()
	Returns a const_iterator pointing to the first state.
const_iterator	cend ()
	Returns a const_iterator pointing "just past the last" state.
	LTS (Cudd mgr)
	Constructor.
size_t	numStates (void) const
	Returns the number of states in the LTS.
Cudd	getManager (void) const
	Returns the BDD manager of the LTS.
void	addState (State s, Delta delta=Delta{})
	Adds a state to the LTS.
void	addTransition (State source, State destination, BDD const &label)
	Adds a transition to a state of the LTS.
void	makeInitial (State s)
	Makes a state initial.
State	getInitial (void) const
	Returns the initial state of the LTS.
void	addAtomicProposition (BDD proposition, std::string name)
	Adds atomic proposition to model.
std::string	getPropositionName (BDD proposition) const
	Returns name of an atomic proposition.
std::set< BDD, Util::BddCompare >	getAtomicPropositions (void) const
	Returns the set of atomic propositions.
State	getSuccessor (State source, BDD letter) const
	Returns successor of source state for input letter in deterministic LTS.
StateSet	getSuccessors (State source, BDD letter) const
	Returns states reachable from source for input letter.
StateSet	getEpsilonSuccessors (State source) const
	Returns states reachable from source via epsilon transitions.
bool	checkTransitions (void) const
	Checks sanity of transitions.
void	print (std::ostream &os=std::cout) const
	Stream insertion operator helper function.
void	letters (StateSet const &stateset, std::vector< BDD > &lv) const
	Returns the letters in the labels of a set of states. More...
std::vector< BDD >	getLetters (std::vector< State > const &statevec) const
	Alternate interface to letters.
int	readVerbosity (void) const
	Returns the verbosity level of the LTS.
void	setVerbosity (int v)
	Sets the verbosity level of the LTS.
bool	isDeterministic (bool complete=true) const
	Checks whether the LTS is deterministic.
bool	isComplete (void) const
	Checks whether the LTS is complete.
SCCs	getSCCs (StateSet const &init, StateSet const &restriction, EdgeSet const &forbiddenEdges) const
	Computes the SCCs reachable from init and contained in restriction.
SCCs	getSCCs (StateSet const &init, StateSet const &restriction) const
	Computes the SCCs reachable from init and contained in restriction.
SCCs	getSCCs (StateSet const &restriction) const
	Computes the SCCs of the LTS contained in restriction.
SCCs	getSCCs (void) const
	Computes the SCCs of the LTS.
void	findTransient (std::vector< State > &transient, StateSet const &init, StateSet const &restriction) const
	Finds transient states of LTS reachable from init and contained in restriction.
void	findTransient (std::vector< State > &transient, StateSet const &restriction) const
	Finds transient states of LTS contained in restriction.
void	findTransient (std::vector< State > &transient) const
	Finds transient states of LTS.
std::map< State, State >	stateEquivalence (std::map< State, unsigned > const &outputClass) const
	Returns state equivalence relation.
void	trim (StateSet const &targets)
	Removes states with no path to target states.
void	trim (StateSet const &targets, SCCs const &sccs)
	Removes states with no path to target states. More...
void	printDot (std::string graphname=std::string("LTS")) const
	Writes LTS in dot format.
LTS	subsetsLTS (std::map< State, StateSet > &subsets) const
	Returns the result of the Rabin-Scott subset construction.
void	setEpsilonBDD (BDD const &e)
	Sets the epsilon proposition for LDBWs.
const BDD &	getEpsilonBDD (void) const
	Gets the epsilon proposition for LDBWs.
bool	hasEpsilonTransitions (void) const
	Checks whether there exist epsilon transitions.
LTS	product (LTS const &second)
	Returns the synchronous product of two LTSs.

Friends
class	Determ
class	Simul
class	OSPGame

Additional Inherited Members
Public Types inherited from LTS< ParityTransition >
using	Transition = ParityTransition
using	Edge = std::pair< State, Transition >
using	EdgeSet = std::set< Edge >
using	Delta = std::vector< Transition >
using	PairsStateBdd = std::set< std::pair< State, BDD >, Util::PairWithBddCompare< State > >
	Type of sets of pairs of state and BDD.
using	const_iterator = std::vector< State >::const_iterator
	Constant iterator type.
using	SCCs = std::vector< StateSet >
	Type of the collection of SCCs.
Protected Types inherited from LTS< ParityTransition >
using	TransitionMap = std::map< State, Delta >
Protected Member Functions inherited from LTS< ParityTransition >
void	mergeTransitions (void)
	Merge transitions that differ at most in their labels.
bool	isTrivial (StateSet const &scc, EdgeSet const &forbidden=EdgeSet{}) const
	Check whether an SCC is trivial.
void	pruneVarSet (void)
	Prune the variable set of unused atomic propositions.
Protected Attributes inherited from LTS< ParityTransition >
Cudd	mgr
int	verbosity
std::vector< State >	states
State	initialState
TransitionMap	transitions
std::set< BDD, Util::BddCompare >	varSet
BDD	epsilon

Detailed Description

Class of parity automata.

Accepting runs have odd maximum recurring priority. Priorities are attached to the transitions.

Member Function Documentation

CartonMaceiras()

unsigned Parity::CartonMaceiras

(

void

)

Reduces index of acceptance condition.

Returns

the length of the longest positive chain.

determinize()

Parity Parity::determinize

(

void

)

const

Returns determinized automaton.

Build a deterministic parity automaton from a nondeterministic parity automaton with prioritiess 0 and 1 (that is, a nondeterminstic Buechi automaton). Uses Piterman's algorithm.

directSimulationRelation()

void Parity::directSimulationRelation

(

std::set< StatePair > &

simul

)

const

Computes direct simulation relation.

Compute the set of pairs of states (p,q) such that they are in simulation relation and p != q.

getPriority()

Priority Parity::getPriority	(	State	source,
		BDD	label,
		State	destination,
		bool	silent = false
	)		const

Gets the priority of a transition.

In silent mode the function returns -1 if no transition with the given endpoints and label exists.

getTrapStates()

StateSet Parity::getTrapStates

(

void

)

const

Returns set of trap states.

No word is accepted from a trap state.

isTerminal()

bool Parity::isTerminal

(

bool

ignoreTransient = true

)

const

Checks whether the automaton is terminal.

If ignoreTransient is false, it returns false if there are transient accepting transitions.

minimumIndex()

unsigned Parity::minimumIndex

(

void

)

Reduces index of acceptance condition.

Returns

the length of the longest positive chain.

Avoids use of priority 0 if possible.

solveOneStreettPairGame()

void Parity::solveOneStreettPairGame	(	StateSet const &	spoilerStates,
		StateSet &	dwinning,
		StateMap &	dstrategy,
		StateMap &	sstrategy
	)		const

Solve one-Streett-pair game.

Returns

Strategy for duplicator.

---

The documentation for this class was generated from the following files:

• LTS/Parity.hh
• LTS/Parity.cc