12 Oct
2011
12 Oct
'11
10:27 a.m.
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(a)eecs.qmul.ac.uk> wrote:
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
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.