An implementation of the emptiness-check algorithm for a product between a TA and a Kripke structure.
More...
|
| ta_check (const const_ta_product_ptr &a, option_map o=option_map()) |
|
bool | check (bool disable_second_pass=false, bool disable_heuristic_for_livelock_detection=false) |
| Check whether the TA product automaton contains an accepting run: it detects the two kinds of accepting runs: Buchi-accepting runs and livelock-accepting runs. This emptiness check algorithm can also check a product using the generalized form of TA. More...
|
|
bool | livelock_detection (const const_ta_product_ptr &t) |
| Check whether the product automaton contains a livelock-accepting run Return false if the product automaton accepts no livelock-accepting run, otherwise true. More...
|
|
std::ostream & | print_stats (std::ostream &os) const |
| Print statistics, if any. More...
|
|
void | set_states (unsigned n) |
|
void | inc_states () |
|
void | inc_transitions () |
|
void | inc_depth (unsigned n=1) |
|
void | dec_depth (unsigned n=1) |
|
unsigned | states () const |
|
unsigned | transitions () const |
|
unsigned | max_depth () const |
|
unsigned | depth () const |
|
unsigned | get (const char *str) const |
|
An implementation of the emptiness-check algorithm for a product between a TA and a Kripke structure.
@InProceedings{ geldenhuys.06.spin,
author = {Jaco Geldenhuys and Henri Hansen},
title = {Larger Automata and Less Work for {LTL} Model Checking},
booktitle = {Proceedings of the 13th International SPIN Workshop
(SPIN'06)},
year = {2006},
pages = {53--70},
series = {Lecture Notes in Computer Science},
volume = {3925},
publisher = {Springer}
}
the implementation of spot::ta_check::check() is inspired from the two-pass algorithm of the paper above:
- the fist-pass detect all Buchi-accepting cycles and includes the heuristic proposed in the paper to detect some livelock-accepting cycles.
- the second-pass detect all livelock-accepting cycles. In addition, we add some optimizations to the fist pass: 1- Detection of all cycles containing a least one state that is both livelock and Buchi accepting states 2- Detection of all livelock-accepting cycles containing a least one state (k,t) such as its "TA component" t is a livelock-accepting state that has no successors in the TA automaton.
The implementation of the algorithm of each pass is a SCC-based algorithm inspired from spot::gtec.hh.See the paper cited above.