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