Replies: 9 comments 32 replies
-
Beta Was this translation helpful? Give feedback.
-
|
Probably it is desired to have both backward and forward compatibility regarding these schemas:
Another useful feature I have seen is to add an With a careful schema evolution, |
Beta Was this translation helpful? Give feedback.
-
|
I recall having conversations at some point about this with Ondrej Lengal (ondrik on GitHub). He might be interested to discuss this. |
Beta Was this translation helpful? Give feedback.
-
|
Thanks for adding me! I'll be very happy to support a unified DD serialization format. I recall trying My 2 cents:
|
Beta Was this translation helpful? Give feedback.
-
|
Thank you for involving me, I'll be happy to help. Having a common format for storing various DDs has been on my mind for a few years. We discussed at some point with @trolando but it didn't gain traction. Some point addressing the raised issues here:
There was an attempt for the format inspired by HOA and MATA formats at https://github.com/VeriFIT/bdd-format with examples of some DDs, which has been implemented by @fifixsandy in a fork of BuDDy that also supports MTBDDs https://github.com/VeriFIT/MoToBuddy. (let me tag @alaarman, who might also contribute) |
Beta Was this translation helpful? Give feedback.
-
|
A few comments, a bit unstructured:
So in my mind, you'd want to have a header with metadata, it would tell you what the roots are, what variables there are and maybe what order if there is an order, what types of nodes to expect (including leaf types). Then after the header, you'd just have all the nodes, maybe like this: That would be for a bdd with leaf types boolean and integer (mixed). Each node would have a unique id (the first integer), then a type, and depending on the type, the parameters. We would define a bunch of standard types like bdd, cbdd/czdd, zdd, tbdd, also mdd, etc. It's still a bit verbose to have a type of node in every line, but I don't really see a "nicer" way to do that if storing mixed types. And I haven't really thought yet of how to do edge labels in a meaningful way, especially if there would be multiple potential labels. Or we make this very simple: a node of type "bdd" always has three parameters: id, then-child, else-child. And a node of type "bddc" has a complement on the [true/false] edge. Or a node of type "bddc" has an extra fourth (or fifth) parameter with the complement edge. |
Beta Was this translation helpful? Give feedback.
-
|
Parts of this discussion relate to visualizing (and editing) BDDs. One of the PhD students at Eindhoven works on this ( I don't remember the name, but @nhusung should know ) ; their inputs/project might be of relevance. |
Beta Was this translation helpful? Give feedback.
-
|
I made a basic documents with goals here (allowed for suggestions only to avoid ad-robots taking over the discussion; if you want a direct edit permissions, please send me your account name and I'll add you). Please read and comment. |
Beta Was this translation helpful? Give feedback.
-
I've reviewed the discussion and noted that the main concerns are about generality and readability. I'd like to offer some historical context on the design of DDDMP, which might clarify a few points.
|
Beta Was this translation helpful? Give feedback.
Uh oh!
There was an error while loading. Please reload this page.
-
Moving the discussion here, started in #15.
@nhusung wrote:
@trolando wrote:
@doganulus wrote:
@ssoelvsten wrote:
Here we go :)
Beta Was this translation helpful? Give feedback.
All reactions