spot  2.4.2
Modules | Classes

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

Detailed Description

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.


Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Sat Nov 25 2017 02:13:16 for spot by doxygen 1.8.13