Functions
twa_graph_ptr	spot::sl (const_twa_graph_ptr aut)
	Close the automaton by allowing letters to be duplicated. More...

bool	spot::is_stutter_invariant (formula f, twa_graph_ptr aut_f=nullptr)
	Check if a formula is stutter invariant. More...

bool	spot::is_stutter_invariant (twa_graph_ptr aut_f, const_twa_graph_ptr aut_nf=nullptr, int algo=0)
	Check if an automaton has the stutter invariance property. More...

trival	spot::check_stutter_invariance (twa_graph_ptr aut_f, formula f=nullptr, bool do_not_determinize=false, bool find_counterexamples=false)
	Check whether aut is stutter-invariant. More...

int	spot::is_stutter_invariant_forward_closed (twa_graph_ptr aut, const std::vector< bool > &sistates)
	Test if the set of stutter-invariant states is forward-closed. More...

std::vector< bool >	spot::make_stutter_invariant_forward_closed_inplace (twa_graph_ptr aut, const std::vector< bool > &sistates)
	Change the automaton so its set of stutter-invariant state is forward-closed. More...

twa_graph_ptr	spot::sl2_inplace (twa_graph_ptr aut)
	Close the automaton by allowing letters to be duplicated. More...

twa_graph_ptr	spot::sl2 (const_twa_graph_ptr aut)
	Close the automaton by allowing letters to be duplicated. More...

twa_graph_ptr	spot::closure_inplace (twa_graph_ptr aut)
	Close the automaton by allowing duplicate letter removal. More...

twa_graph_ptr	spot::closure (const_twa_graph_ptr aut)
	Close the automaton by allowing duplicate letter removal. More...

std::vector< bool >	spot::stutter_invariant_states (const_twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr)
	Determinate the states that are stutter-invariant in pos. More...

std::vector< bool >	spot::stutter_invariant_states (const_twa_graph_ptr pos, formula f_pos)
	Determinate the states that are stutter-invariant in pos. More...

void	spot::highlight_stutter_invariant_states (twa_graph_ptr pos, formula f_pos, unsigned color=0)
	Highlight the states of pos that are stutter-invariant. More...

void	spot::highlight_stutter_invariant_states (twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr, unsigned color=0)
	Highlight the states of pos that are stutter-invariant. More...

std::vector< bdd >	spot::stutter_invariant_letters (const_twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr)
	Determinate the letters with which each state is stutter-invariant. More...

std::vector< bdd >	spot::stutter_invariant_letters (const_twa_graph_ptr pos, formula f_pos)
	Determinate the letters with which each state is stutter-invariant. More...

Detailed Description

Function Documentation

◆ check_stutter_invariance()

trival spot::check_stutter_invariance	(	twa_graph_ptr	aut_f,
		formula	f = `nullptr`,
		bool	do_not_determinize = `false`,
		bool	find_counterexamples = `false`
	)

#include <spot/twaalgos/stutter.hh>

Check whether aut is stutter-invariant.

This procedure requires the negation of aut_f to be computed. This is easily done of aut_f is deterministic or if a formula represented by aut_f is known. Otherwise aut_f will be complemented by determinization, which can be expansive. The determinization can be forbidden using the do_not_determinize flag.

If no complemented automaton could be constructed, the the result will be returned as trival::maybe().

If find_counterexamples is set and the automaton is found to be stutter-sensitive, then two named properties named "accepted-word" and "rejected-word" will be added to the automaton. Those sample words will be stutter-equivalent, and serve as a proof that the property is stutter-sensitive.

This variant of is_stutter_invariant() is used for the –check=stutter option of command-line tools.

◆ closure()

twa_graph_ptr spot::closure ( const_twa_graph_ptr aut )

#include <spot/twaalgos/stutter.hh>

Close the automaton by allowing duplicate letter removal.

This is done by adding shortcuts into the automaton. If (x,y) is a transition labeled by B, and (y,z) is a transition labeled by C, we add a transition (x,z) labeled by B∧C.

For more details about this function, see [39] .

The inplace version of the function modifies the input automaton.

◆ closure_inplace()

twa_graph_ptr spot::closure_inplace ( twa_graph_ptr aut )

#include <spot/twaalgos/stutter.hh>

Close the automaton by allowing duplicate letter removal.

This is done by adding shortcuts into the automaton. If (x,y) is a transition labeled by B, and (y,z) is a transition labeled by C, we add a transition (x,z) labeled by B∧C.

For more details about this function, see [39] .

The inplace version of the function modifies the input automaton.

◆ highlight_stutter_invariant_states() [1/2]

void spot::highlight_stutter_invariant_states	(	twa_graph_ptr	pos,
		const_twa_graph_ptr	neg = `nullptr`,
		unsigned	color = `0`
	)

#include <spot/twaalgos/stutter.hh>

Highlight the states of pos that are stutter-invariant.

A state is stutter-invariant if the language recognized from this state is stutter-invariant, or if the state can only be reached by passing though a stutter-invariant state.

The algorithm needs to compute the complement of pos. You can avoid that costly operation by either supplying the complement automaton, or supplying a formula for the (positive) automaton.

The color argument is an index in a predefined set of colors.

This function simply works by calling stutter_invariant_states(), and using the resulting vector to setup the "highlight-states" property of the automaton.

◆ highlight_stutter_invariant_states() [2/2]

void spot::highlight_stutter_invariant_states	(	twa_graph_ptr	pos,
		formula	f_pos,
		unsigned	color = `0`
	)

#include <spot/twaalgos/stutter.hh>

Highlight the states of pos that are stutter-invariant.

A state is stutter-invariant if the language recognized from this state is stutter-invariant, or if the state can only be reached by passing though a stutter-invariant state.

The algorithm needs to compute the complement of pos. You can avoid that costly operation by either supplying the complement automaton, or supplying a formula for the (positive) automaton.

The color argument is an index in a predefined set of colors.

This function simply works by calling stutter_invariant_states(), and using the resulting vector to setup the "highlight-states" property of the automaton.

◆ is_stutter_invariant() [1/2]

bool spot::is_stutter_invariant	(	formula	f,
		twa_graph_ptr	aut_f = `nullptr`
	)

#include <spot/twaalgos/stutter.hh>

Check if a formula is stutter invariant.

It first calls spot::formula::is_syntactic_stutter_invariant() to test for the absence of X, but if some X is found, is an automaton-based check is performed to detect reliably (and rather efficiently) whether the language is actually stutter-invariant.

If you already have an automaton for f, passing it at a second argument will save some time. If you also have an automaton for the negation of f, it is better to use the overload of is_stutter_invariant() that takes two automata.

The prop_stutter_invariant() property of aut_f is set as a side-effect.

For more details about this function, see [39] .

◆ is_stutter_invariant() [2/2]

bool spot::is_stutter_invariant	(	twa_graph_ptr	aut_f,
		const_twa_graph_ptr	aut_nf = `nullptr`,
		int	algo = `0`
	)

#include <spot/twaalgos/stutter.hh>

Check if an automaton has the stutter invariance property.

The automaton-based check requires the complement automaton to be built. If you have one, passing it as the second argument will avoid a costly determinization in case aut_f is non-deterministic.

The prop_stutter_invariant() property of aut_f is set as a side-effect.

For more details about this function, see [39] .

◆ is_stutter_invariant_forward_closed()

int spot::is_stutter_invariant_forward_closed	(	twa_graph_ptr	aut,
		const std::vector< bool > &	sistates
	)

#include <spot/twaalgos/stutter.hh>

Test if the set of stutter-invariant states is forward-closed.

Test if the set of states returned by spot::stutter_invariant_states() is closed by the successor relation. I.e., the successor of an SI-state is an SI-state.

This function returns -1 is sistates is forward closed, or it will return the number of a state that is not an SI-state but has a predecessor that is an SI-state.

The sistate vector should be a vector computed for aut using spot::stutter_invariant_states().

◆ make_stutter_invariant_forward_closed_inplace()

std::vector<bool> spot::make_stutter_invariant_forward_closed_inplace	(	twa_graph_ptr	aut,
		const std::vector< bool > &	sistates
	)

#include <spot/twaalgos/stutter.hh>

Change the automaton so its set of stutter-invariant state is forward-closed.

See also: spot::is_stutter_invariant_forward_closed()

The sistate vector should be a vector computed for aut using spot::stutter_invariant_states(). The automaton aut will be fixed in place by duplicating problematic states, and an updated copy of the sistates vector will be returned.

This function will detect the cases where not change to aut is necessary at a cost that is very close to spot::is_stutter_invariant_forward_closed(), so calling this last function first is useless.

◆ sl()

twa_graph_ptr spot::sl ( const_twa_graph_ptr aut )

#include <spot/twaalgos/stutter.hh>

Close the automaton by allowing letters to be duplicated.

Any letter that enters a state will spawn a copy of this state with a self-loop using the same letter. For more details about this function, see [39] .

◆ sl2()

twa_graph_ptr spot::sl2 ( const_twa_graph_ptr aut )

#include <spot/twaalgos/stutter.hh>

Close the automaton by allowing letters to be duplicated.

For any transition (s,d) labeled by a letter ℓ, we add a state x and three transitions (s,x), (x,x), (x,d) all labeled by ℓ. For more details about this function, see [39] .

The inplace version of the function modifies the input automaton.

◆ sl2_inplace()

twa_graph_ptr spot::sl2_inplace ( twa_graph_ptr aut )

#include <spot/twaalgos/stutter.hh>

Close the automaton by allowing letters to be duplicated.

For any transition (s,d) labeled by a letter ℓ, we add a state x and three transitions (s,x), (x,x), (x,d) all labeled by ℓ. For more details about this function, see [39] .

The inplace version of the function modifies the input automaton.

◆ stutter_invariant_letters() [1/2]

std::vector<bdd> spot::stutter_invariant_letters	(	const_twa_graph_ptr	pos,
		const_twa_graph_ptr	neg = `nullptr`
	)

#include <spot/twaalgos/stutter.hh>

Determinate the letters with which each state is stutter-invariant.

A state q is stutter-invariant for ℓ iff the membership to L(q) of any word starting with ℓ is unchanged by duplicating any letter, or removing a duplicate letter.

The algorithm needs to compute the complement of pos. You can avoid that costly operation by either supplying the complement automaton, or supplying a formula for the (positive) automaton.

◆ stutter_invariant_letters() [2/2]

std::vector<bdd> spot::stutter_invariant_letters	(	const_twa_graph_ptr	pos,
		formula	f_pos
	)

#include <spot/twaalgos/stutter.hh>

Determinate the letters with which each state is stutter-invariant.

A state q is stutter-invariant for ℓ iff the membership to L(q) of any word starting with ℓ is unchanged by duplicating any letter, or removing a duplicate letter.

The algorithm needs to compute the complement of pos. You can avoid that costly operation by either supplying the complement automaton, or supplying a formula for the (positive) automaton.

◆ stutter_invariant_states() [1/2]

std::vector<bool> spot::stutter_invariant_states	(	const_twa_graph_ptr	pos,
		const_twa_graph_ptr	neg = `nullptr`
	)

#include <spot/twaalgos/stutter.hh>

Determinate the states that are stutter-invariant in pos.

A state is stutter-invariant if the language recognized from this state is stutter-invariant, or if the state can only be reached by passing though a stutter-invariant state.

The algorithm needs to compute the complement of pos. You can avoid that costly operation by either supplying the complement automaton, or supplying a formula for the (positive) automaton.

◆ stutter_invariant_states() [2/2]

std::vector<bool> spot::stutter_invariant_states	(	const_twa_graph_ptr	pos,
		formula	f_pos
	)

#include <spot/twaalgos/stutter.hh>

Determinate the states that are stutter-invariant in pos.

A state is stutter-invariant if the language recognized from this state is stutter-invariant, or if the state can only be reached by passing though a stutter-invariant state.

The algorithm needs to compute the complement of pos. You can avoid that costly operation by either supplying the complement automaton, or supplying a formula for the (positive) automaton.

Functions

Detailed Description

Function Documentation

◆ check_stutter_invariance()

◆ closure()

◆ closure_inplace()

◆ highlight_stutter_invariant_states() [1/2]

◆ highlight_stutter_invariant_states() [2/2]

◆ is_stutter_invariant() [1/2]

◆ is_stutter_invariant() [2/2]

◆ is_stutter_invariant_forward_closed()

◆ make_stutter_invariant_forward_closed_inplace()

◆ sl()

◆ sl2()

◆ sl2_inplace()

◆ stutter_invariant_letters() [1/2]

◆ stutter_invariant_letters() [2/2]

◆ stutter_invariant_states() [1/2]

◆ stutter_invariant_states() [2/2]