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