Pierre pierreganty@gmail.com writes:

Dear Spot devs,

I am not sure how I am supposed to work with Kripke structures (which I imported using ltsmin) or `twa_product` (which I obtained using `otf_product` on the Kripke structure).

Most of the automata operations in Spot work on twa_graph, i.e., automata stored explicitly as graphs. These automata have a very convenient interface to iterate over states, edges, etc.

However twa_graph is also a subclass of twa, i.e., an automaton that does not presume how its states are stored (or computed), and that only supports some on-the-fly exploration of its state-space. Writing algorithms using this on-the-fly twa interface is cumbersome, so there are very few algorithms available using this interface: basically you can do - on-the-fly products (via spot::otf_product()) - on-the-fly emptiness (restricted to Fin-less acceptance, via the twa::is_empty() method or the twa::accepting_run() and twa::accepting_word() methods), - and you have some function that explore the full state-space to compute its size (spot::stats_reachable()).

Of course the combination of these functions is enough to write some syntactic sugar like twa::intersects(twa2) or twa::intersecting_run(twa2) or twa::intersecting_word(twa2), which can be convenient when writing a model-checker.

The Kripke structures generated from ltsmin and twa_product are subclasses of twa, so you are restricted to the above operations. Essentially, those classes where introduced to demonstrate how to write a model-checker, so you have exactly the features needed to achieve this.

Now, because is_empty(), accepting_run(), accepting_word, intersects(), intersecting_run(), intersecting_word() are all defined in the twa class, it somehow made sense to me to introduce exclusive_run() and exclusive_word() at the same level. However the truth is that these functions need to complement one (if lucky) or maybe the two involved automata to answer, and such complementations cannot currently be done on-the-fly. In practice, the implementation has to convert at least one argument, maybe both, to a twa_graph before doing the job. Retrospectively, I'm not sure it was a good decision to expose this method at the twa level; it's mostly for convenience as this is the kind of method I would expect to be used only mostly interactively.

spot::contains(), spot::are_equivalent() are currently only defined on twa_graph because they involve some complementation that we can't do on-the-fly. But looking at this now, I think we could allow the right argument of contains() to be a twa: this one does not need to be complemented. This would allow implementing a model-checker (without generation of counterexample) as contains(formula, kripke).

In the screenshot below I can invoke 'exclusive_word' with no problems on a `kripke` and `twa_product` but the same is not true for 'contains' which returns a type error. The way I found to invoke 'contains' without errors is to use 'save' and then 'automaton' to read that same file again in order to get `twa_graph` as expected by `contains`. I am not sure this workaround is what the devs had in mind.

You should be able to convert any twa B (this includes kripke and twa_product) into a twa_graph A with

A = spot.make_twa_graph(B, spot.twa_prop_set.all())