spot
2.1.2
|
Check whether the language of a product (spot::ta_product) between a Kripke structure and a TA is empty. It works also for the product using Generalized TA (GTA and SGTA). More...
Modules | |
Emptiness-check algorithms | |
Classes | |
class | spot::state_ta_product |
A state for spot::ta_product. More... | |
class | spot::ta_product |
A lazy product between a Testing automaton and a Kripke structure. (States are computed on the fly.) More... | |
Check whether the language of a product (spot::ta_product) between a Kripke structure and a TA is empty. It works also for the product using Generalized TA (GTA and SGTA).
you should call spot::ta_check::check() to check the product automaton. If spot::ta_check::check() returns false, then the product automaton was found empty. Otherwise the automaton accepts some run.
This is based on the following paper.