|
| | scc_partitioner (LTS_TYPE &l) |
| | Creates an scc partitioner for an LTS.
|
| |
| | ~scc_partitioner ()=default |
| | Destroys this partitioner.
|
| |
| void | replace_transition_system (const bool preserve_divergence_loops) |
| | The lts for which this partioner is created is replaced by the lts modulo the calculated partition.
|
| |
| std::size_t | num_eq_classes () const |
| | Gives the number of bisimulation equivalence classes of the LTS.
|
| |
| std::size_t | get_eq_class (const std::size_t s) const |
| | Gives the equivalence class number of a state. The equivalence class numbers range from 0 upto (and excluding) num_eq_classes().
|
| |
| bool | in_same_class (const std::size_t s, const std::size_t t) const |
| | Returns whether two states are in the same bisimulation equivalence class.
|
| |
template<class LTS_TYPE>
class mcrl2::lts::detail::scc_partitioner< LTS_TYPE >
This class contains an scc partitioner removing inert tau loops.
Definition at line 127 of file liblts_scc.h.
template<class LTS_TYPE >
Creates an scc partitioner for an LTS.
This scc partitioner calculates a partition of the state space of the transition system l using a straightforward algorithm found in A.V. Aho, J.E. Hopcroft and J.D. Ullman, Data structures and algorithms. Addison Wesley, 1987 on page 224. All states that reside on a loop of internal actions are put in the same equivalence class. The function l.is_tau is used to determine whether an action is internal. Partitioning is done immediately when an instance of this class is created. When applying the function replace_transition_system the automaton l is replaced by (aka shrinked to) the automaton modulo the calculated partition.
- Parameters
-
| [in] | l | reference to an LTS. |
Definition at line 210 of file liblts_scc.h.
template<class LTS_TYPE >
The lts for which this partioner is created is replaced by the lts modulo the calculated partition.
The number of states of the new lts becomes the number of equivalence classes. In each transition the start and end state are replaced by its equivalence class. If a transition has a tau label (which is checked using the function l.is_tau) then it is preserved if either from and to state are different, or preserve_divergence_loops is true. All non tau transitions are always preserved. The label numbers for preserved transitions are not changed.
- Parameters
-
| [in] | preserve_divergence_loops | If true preserve a tau loop on states that were part of a larger tau loop in the input transition system. Otherwise idle tau loops are removed. |
Definition at line 248 of file liblts_scc.h.
1.9.7