suyjuris / obst Goto Github PK

Hi, I am using the version hosted on the chair webpage and spotted what could possibly be a minor bug. It can be reproduced as follows:

1. Create formulae x1 & x2 and x1 | x2. This should create an MTBDD with terminals b and c.
2. Take union of b and c.
3. Step all the way to the end. The following message is shown

Merging node %1 with c
Done.

I would have expected to see something like "Merging node b U c with c".

Hi, I've found this project very helpful for my study of binary decision diagrams. I think there can be a few improvements in the numbering and labeling system, but I'm mostly filing this issue just to say that I like the application and give my approval.

1. Are the numbers intended to be interpreted as like a binary encodings of a truth table, row-by-row? A readme explanation or just a reference to the numbering system would be helpful.

2. The variable names seem to be assigned in a way that is not consistent with the input formula. In the given screenshot, a formula with four variables displays five variables in the BDD (as if every node gets a new variable). Usually BDD diagrams have consistent variable names row-by-row. (reference attached).