Enable CIF to mCRL2 translation for BDD representation in CIF
It would be helpful to be able to transform CIF specifications to mCRL2 that contain the CIF BDD node representation. These specifications are obtained when performing databased synthesis with the nodes
BDD output option. The specification contains type, tuple, list, and function definitions that the translation should handle (see example below). Not sure if a generic translation for functions is possible, or whether one can be made specifically for bdd_eval
.
type bdd_node_type = tuple(int var; int low; int high);
type bdd_nodes_type = list[0] bdd_node_type;
const bdd_nodes_type bdd_nodes = <list[0] bdd_node_type>[];
alg bool bdd_value0 = A.l1;
alg bool bdd_value1 = A.l2;
alg list[2] bool bdd_values = [bdd_value0, bdd_value1];
func bool bdd_eval(int idx; list[2] bool values):
bdd_node_type node;
bool val;
while idx >= 0:
node := bdd_nodes[idx];
val := values[node[var]];
idx := if val: node[high] else node[low] end;
end
return idx = -1;
end
...