13 Oct
2011
13 Oct
'11
4:19 p.m.
Sorry for the delay.
(I'm currently attending ATVA'11 at Taipei.)
On Wed, Oct 12, 2011 at 4:27 PM, Nikos Gorogiannis
<nikos.gorogiannis(a)eecs.qmul.ac.uk> wrote:
While we are on the subject can I ask another newbie
question: the support
conditions for transitions are given as bdds, but does this mean that they
can be arbitrary propositions, or must they be (equivalent to) conjunctions
of literals?
The labels of the transitions can be any Boolean formula. For instance in
an automaton with AP={a,b} you could have a state with two outgoing transitions
labelled respectively with (a&b)|(!a&!b) and (!a)|b. These labels are
returned by the
current_condition() method of the tgba_succ_iterator class.
There is a different thing that we call "support conditions" in Spot, so I'm
not
really sure what you are talking about. The support conditions of a *state*,
is a Boolean formula that should be implied by the label of each of the outgoing
transitions. This is returned by the support_conditions() method of
the tgba class.
The common way to implement this is to return the disjunction of the labels
of all of the outgoing transitions. With the above example we have
((a&b)|(!a&!b))|((!a)|b) = (!a)|b
but another simpler implementation is to always return bddtrue...
The purpose of this method was to enable a small optimization when a product
of tgba involves a symbolic (i.e., bdd-encoded) tgba. You probably should not
care about it.
--
Alexandre Duret-Lutz