timbeurskens / rsbdd Goto Github PK

When evaluating the following formula:

if exists a # a <=> b then b <=> c else false | c

The symbol.id index does not match the free_vars range.
This could be resolved by implementing a remapping function from symbol.id to an index in free_vars.
Runtime does not matter as long as the number of unique variables does not exceed the number of nodes in a BDD. The number of nodes in a BDD given n variables ranges between 2 and 2^n. This means a sub-exponential runtime for the lookup table is acceptable.

Parser errors are currently formatted as debug prints of error structs.
It would be preferable to have

1. A clear, textural representation of the parse error;
2. The location at which the error occurred;

In the current implementation, the hash (and equivalence) of a node depends on the hash of all child-nodes, making the hash computation more expensive than needed. By storing the hash (and liveliness flags) of all child nodes in the parent node, we can optimize the hash computation significantly.

BDDs can be quite efficient in solving the model checking problem. By translating a kripke-structure to a boolean formula we can verify LTL/CTL properties on the model. The RsBDD DSL can be used as an intermediate output.

example:

nu X # [all a # a in X,all b # b in X,all c # c in X]>0 & (if (all a # a in X) then (X & -a) else X) & (if (all b # b in X) then (X & -b) else X) & (if (all c # c in X) then (X & -c) else X)

Currently variable ordering is determined automatically which sometimes yields sub-optimal results.
The CLI should provide an option for customized variable ordering (e.g. by providing an ordered, comma-separated list of variables).