26 Oct
2011
26 Oct
'11
6:54 p.m.
On Tue, Oct 25, 2011 at 12:35 PM, Nikos Gorogiannis
<nikos.gorogiannis(a)eecs.qmul.ac.uk> wrote:
OK, I should have checked the source. The text on what
to implement when
interfacing with Spot suggests that this may be necessary but does not
provide any details so I assumed I had to implement the method.
Thanks for pointing this out. I have updated the page at
http://spot.lip6.fr/wiki/InterfacingSpot
with a note about this, and a couple of other points that have been
introduced in 0.7 but were not explicit on this page:
- states should be released using their destroy() method, and not using delete
- another way to interface with Spot is to subclass the kripke
class, whose interface is simpler that that of tgba.
It makes sense that the transitions of the product may
not be projectable
back onto the original automaton. In any case I can do without them, as my
automaton is very deterministic and by looking at the states I can deduce
the transitions as you say.
Yes. Maybe instead of trying to change project_run(), we could change
replay_tgba_run() and teach it to follow transitions that are
"compatible" with the run, instead of looking for exact matches.
The reason I used replayrun instead of print_tgba_run
is the hint in the
documentation that print_tgba_run may print something which is not an actual
accepting run. I assume that this only applies to bit-hashing emptiness
checks, but couldn't know for sure.
Thank for mentioning this, I will reword this documentation of print_tgba_run.
The idea is that a `tgba_run` object is just a sequence of states with
some labels
and acceptance conditions to display between. You could actually build one by
picking random states, labels, and acceptance conditions, and that may not
correspond to an actual run. Still, print_tgba_run() would print it;
and that's what
I meant with "even if it does not corresponds to an actual run of the
automaton".
> (I'll probably have a snapshot ready in a
couple of days.)
Here:
http://www.lrde.epita.fr/dload/spot/spot-snapshot.tar.gz
Beware that this development version will compile with optimization
disabled and assertions turned on.
If you want speed, you should configure it with --disable-devel
The top of the NEWS file says this:
* Major new features:
- Spot can read DiVinE models. See iface/dve2/README for details.
- The genltl tool can now output 20 differents LTL formula families.
It also replace the LTLcounter Perl scripts.
* Major interface changes:
- The destructor of all states is now private. Any code that looks like
"delete some_state;" will cause an compile error and should be
updated to "some_state->destroy();". This new syntax is supported
since version 0.7.
- The experimental Nips interface has been removed.
* Minor changes:
- The dotty_reachable() function has a new option "assume_sba" that
can be used for rendering automata with state-based acceptance.
In that case, acceptance states are displayed with a double
circle. ltl2tgba (both command line and on-line) Use it to display
degeneralized automata.
- Identifiers used to name atomic proposition can contain dots.
E.g.: X.Y is now an atomic proposition, while it was understood
as X&Y in previous versions.
* Internal improvements:
- The on-line ltl2tgba CGI script uses a cache to produce faster
answers.
- Better memory management for the states of explicit automata.
Thanks to the aforementioned ->destroy() change, we can avoid
cloning explicit states.
- tgba_product has learned how to be faster when one of the operands
is a Kripke structure (15% speedup).
- The reduction rule for "a M b" has been improved: it can be
reduced to "a & b" if "a" is a pure eventuallity.
- More useless acceptance conditions are removed by SCC simplifications.
* Bug fixes:
- Safra complementation has been fixed in cases where more than
one acceptance conditions where needed to convert the
deterministic Streett automaton as a TGBA.
- The degeneralization is now idempotent. Previously degeneralizing
an already degeneralized automaton could add some states.
- The degeneralization now has a deterministic behavior. Previously
it was possible to obtain different output depending on the
memory layout.
--
Alexandre Duret-Lutz