Hi Alexandre,
On 12/10/11 00:05, Alexandre Duret-Lutz wrote:
Hi Nikos,
On Wed, Oct 12, 2011 at 12:21 AM, Nikos Gorogiannis nikos.gorogiannis@eecs.qmul.ac.uk wrote:
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.
You should use the same bdd_dict for all your automata. Each automaton will simplify register different (overlapping) sets of atomic propositions.
The purpose of the bdd_dict class is to ensure that the BDD variable assigned to each of the atomic proposition is the same in all automata sharing a bdd_dict. It does not force the automata to use the same set of atomic propositions.
Oh, I see now. Thanks for your response.
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?
Thanks! Nikos