spot  2.7.2
Functions
Stutter-invariance checks and related functions

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 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 
)

#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().

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

@InProceedings{   michaud.15.spin,
  author        = {Thibaud Michaud and Alexandre Duret-Lutz},
  title         = {Practical Stutter-Invariance Checks for
                  {$\omega$}-Regular Languages},
  booktitle     = {Proceedings of the 22th International SPIN
                  Symposium on Model Checking of Software (SPIN'15)},
  year          = 2015,
  pages         = {84--101},
  series        = {Lecture Notes in Computer Science},
  volume        = 9232,
  publisher     = {Springer},
  month         = aug
}

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

@InProceedings{   michaud.15.spin,
  author        = {Thibaud Michaud and Alexandre Duret-Lutz},
  title         = {Practical Stutter-Invariance Checks for
                  {$\omega$}-Regular Languages},
  booktitle     = {Proceedings of the 22th International SPIN
                  Symposium on Model Checking of Software (SPIN'15)},
  year          = 2015,
  pages         = {84--101},
  series        = {Lecture Notes in Computer Science},
  volume        = 9232,
  publisher     = {Springer},
  month         = aug
}

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,
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.

◆ highlight_stutter_invariant_states() [2/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.

◆ 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

@InProceedings{   michaud.15.spin,
  author        = {Thibaud Michaud and Alexandre Duret-Lutz},
  title         = {Practical Stutter-Invariance Checks for
                  {$\omega$}-Regular Languages},
  booktitle     = {Proceedings of the 22th International SPIN
                  Symposium on Model Checking of Software (SPIN'15)},
  year          = 2015,
  pages         = {84--101},
  series        = {Lecture Notes in Computer Science},
  volume        = 9232,
  publisher     = {Springer},
  month         = aug
}

◆ 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

@InProceedings{   michaud.15.spin,
  author        = {Thibaud Michaud and Alexandre Duret-Lutz},
  title         = {Practical Stutter-Invariance Checks for
                  {$\omega$}-Regular Languages},
  booktitle     = {Proceedings of the 22th International SPIN
                  Symposium on Model Checking of Software (SPIN'15)},
  year          = 2015,
  pages         = {84--101},
  series        = {Lecture Notes in Computer Science},
  volume        = 9232,
  publisher     = {Springer},
  month         = aug
}

◆ 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

@InProceedings{   michaud.15.spin,
  author        = {Thibaud Michaud and Alexandre Duret-Lutz},
  title         = {Practical Stutter-Invariance Checks for
                  {$\omega$}-Regular Languages},
  booktitle     = {Proceedings of the 22th International SPIN
                  Symposium on Model Checking of Software (SPIN'15)},
  year          = 2015,
  pages         = {84--101},
  series        = {Lecture Notes in Computer Science},
  volume        = 9232,
  publisher     = {Springer},
  month         = aug
}

◆ 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

@InProceedings{   michaud.15.spin,
  author        = {Thibaud Michaud and Alexandre Duret-Lutz},
  title         = {Practical Stutter-Invariance Checks for
                  {$\omega$}-Regular Languages},
  booktitle     = {Proceedings of the 22th International SPIN
                  Symposium on Model Checking of Software (SPIN'15)},
  year          = 2015,
  pages         = {84--101},
  series        = {Lecture Notes in Computer Science},
  volume        = 9232,
  publisher     = {Springer},
  month         = aug
}

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

@InProceedings{   michaud.15.spin,
  author        = {Thibaud Michaud and Alexandre Duret-Lutz},
  title         = {Practical Stutter-Invariance Checks for
                  {$\omega$}-Regular Languages},
  booktitle     = {Proceedings of the 22th International SPIN
                  Symposium on Model Checking of Software (SPIN'15)},
  year          = 2015,
  pages         = {84--101},
  series        = {Lecture Notes in Computer Science},
  volume        = 9232,
  publisher     = {Springer},
  month         = aug
}

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.


Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13