spot
2.7

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) 
Check whether aut is stutterinvariant. More...  
int  spot::is_stutter_invariant_forward_closed (twa_graph_ptr aut, const std::vector< bool > &sistates) 
Test if the set of stutterinvariant states is forwardclosed. 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 stutterinvariant state is forwardclosed. 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 stutterinvariant in pos. More...  
std::vector< bool >  spot::stutter_invariant_states (const_twa_graph_ptr pos, formula f_pos) 
Determinate the states that are stutterinvariant 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 stutterinvariant. 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 stutterinvariant. 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 stutterinvariant. More...  
std::vector< bdd >  spot::stutter_invariant_letters (const_twa_graph_ptr pos, formula f_pos) 
Determinate the letters with which each state is stutterinvariant. More...  
trival spot::check_stutter_invariance  (  twa_graph_ptr  aut_f, 
formula  f = nullptr , 

bool  do_not_determinize = false 

) 
#include <spot/twaalgos/stutter.hh>
Check whether aut is stutterinvariant.
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().
This variant of is_stutter_invariant() is used for the –check=stutter option of commandline tools.
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
@InProceedings{ michaud.15.spin, author = {Thibaud Michaud and Alexandre DuretLutz}, title = {Practical StutterInvariance Checks for {$\omega$}Regular Languages}, booktitle = {Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15)}, year = 2015, pages = {84101}, series = {Lecture Notes in Computer Science}, volume = 9232, publisher = {Springer}, month = aug }
The inplace version of the function modifies the input automaton.
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
@InProceedings{ michaud.15.spin, author = {Thibaud Michaud and Alexandre DuretLutz}, title = {Practical StutterInvariance Checks for {$\omega$}Regular Languages}, booktitle = {Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15)}, year = 2015, pages = {84101}, series = {Lecture Notes in Computer Science}, volume = 9232, publisher = {Springer}, month = aug }
The inplace version of the function modifies the input automaton.
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 stutterinvariant.
A state is stutterinvariant if the language recognized from this state is stutterinvariant, or if the state can only be reached by passing though a stutterinvariant 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 "highlightstates" property of the automaton.
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 stutterinvariant.
A state is stutterinvariant if the language recognized from this state is stutterinvariant, or if the state can only be reached by passing though a stutterinvariant 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 "highlightstates" property of the automaton.
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 automatonbased check is performed to detect reliably (and rather efficiently) whether the language is actually stutterinvariant.
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 sideeffect.
For more details about this function, see
@InProceedings{ michaud.15.spin, author = {Thibaud Michaud and Alexandre DuretLutz}, title = {Practical StutterInvariance Checks for {$\omega$}Regular Languages}, booktitle = {Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15)}, year = 2015, pages = {84101}, series = {Lecture Notes in Computer Science}, volume = 9232, publisher = {Springer}, month = aug }
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 automatonbased 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 nondeterministic.
The prop_stutter_invariant() property of aut_f is set as a sideeffect.
For more details about this function, see
@InProceedings{ michaud.15.spin, author = {Thibaud Michaud and Alexandre DuretLutz}, title = {Practical StutterInvariance Checks for {$\omega$}Regular Languages}, booktitle = {Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15)}, year = 2015, pages = {84101}, series = {Lecture Notes in Computer Science}, volume = 9232, publisher = {Springer}, month = aug }
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 stutterinvariant states is forwardclosed.
Test if the set of states returned by spot::stutter_invariant_states() is closed by the successor relation. I.e., the successor of an SIstate is an SIstate.
This function returns 1 is sistates is forward closed, or it will return the number of a state that is not an SIstate but has a predecessor that is an SIstate.
The sistate vector should be a vector computed for aut using spot::stutter_invariant_states().
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 stutterinvariant state is forwardclosed.
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.
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 selfloop using the same letter. For more details about this function, see
@InProceedings{ michaud.15.spin, author = {Thibaud Michaud and Alexandre DuretLutz}, title = {Practical StutterInvariance Checks for {$\omega$}Regular Languages}, booktitle = {Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15)}, year = 2015, pages = {84101}, series = {Lecture Notes in Computer Science}, volume = 9232, publisher = {Springer}, month = aug }
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
@InProceedings{ michaud.15.spin, author = {Thibaud Michaud and Alexandre DuretLutz}, title = {Practical StutterInvariance Checks for {$\omega$}Regular Languages}, booktitle = {Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15)}, year = 2015, pages = {84101}, series = {Lecture Notes in Computer Science}, volume = 9232, publisher = {Springer}, month = aug }
The inplace version of the function modifies the input automaton.
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
@InProceedings{ michaud.15.spin, author = {Thibaud Michaud and Alexandre DuretLutz}, title = {Practical StutterInvariance Checks for {$\omega$}Regular Languages}, booktitle = {Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15)}, year = 2015, pages = {84101}, series = {Lecture Notes in Computer Science}, volume = 9232, publisher = {Springer}, month = aug }
The inplace version of the function modifies the input automaton.
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 stutterinvariant.
A state q is stutterinvariant 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.
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 stutterinvariant.
A state q is stutterinvariant 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.
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 stutterinvariant in pos.
A state is stutterinvariant if the language recognized from this state is stutterinvariant, or if the state can only be reached by passing though a stutterinvariant 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.
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 stutterinvariant in pos.
A state is stutterinvariant if the language recognized from this state is stutterinvariant, or if the state can only be reached by passing though a stutterinvariant 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.