Hi,
I'm trying to learn spot, and I want to run an emptiness check on a
product of two automata which I will be creating by subclassing tgba.
The two automata have overlapping, but different, signatures i.e. atomic
propositions. If I understand correctly, I cannot achieve this by using
two different bdd_dicts, as the two automata passed to the product
object must share the same bdd_dict.
How does one deal with this problem in spot?
Thanks
Nikos
Hi,
I've been looking for a library that would allow me to provide a (lazy)
interface for enumerating the states of an automaton and doing
on-the-fly model checking. Spot looks like exactly what I need! (which
is great; I couldn't find any other tool supporting custom model
checking like this).
What I will need on top of this, is when the emptiness check fails, I'd
like to modify the automaton using the information provided by the check
and re-run the check. Changes to the automaton will be localized, so
destroying and rebuilding the objects relating to the emptiness check
seems unnecessarily expensive. Is there any way around this?
Best regards
Nikos Gorogiannis
