12 Oct
2011
12 Oct
'11
1:05 a.m.
Hi Nikos,
On Wed, Oct 12, 2011 at 12:21 AM, Nikos Gorogiannis
<nikos.gorogiannis(a)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.
--
Alexandre Duret-Lutz