Storm 2.0 meets Sylvan 2.0

[sjunges]

Oh btw I'm working on a pretty major version update on Sylvan, see this issue. It's going to break everything. If you want to see certain things as Storm is certainly a major user, do let me know.

Originally posted by @trolando in #274

My big wish would basically be that we can have the necessary modifications we require on top of sylvan 2.0 rather than within sylvan. That makes it so much easier to maintain.

Specifics (top of my head):

• It would be great if one can avoid modifying sylvan when adding new leaf types. We have our polynomials, we might soon want to add intervals. But keeping sylvan up to date is a pain because we changed stuff.
• There are potentially a number of operations we want to backport. Not sure?
• I think the sylvan cmake is quite good, yet we had to change quite a bit, some of which are due to the additional dependencies we have. It may be worth investing a bit into making sure we don't need to modify the build system.
• ARM multi-threading support (even when slower)

[trolando]

The ARM multi-threading support should be done now, I fixed the operation cache problem now. I'll cherry-pick the fix unto the master branch. (Now done in version 1.9.0.)

I agree that in principle, it should be completely unnecessary to change Sylvan to

• add leaf types
• add operations, including using the operation cache, adding to sylvan_stats, etc
• ideally, use currently defined MTBDD operations with different leaf types

And yes, CMakeLists should be such that it works well in the presence of other systems and dependencies. I have been making changes over time, I don't know what version you're currently using.

Backported operations are very welcome, so other users of Sylvan can make use of the functionality.

[trolando]

Here are some "old notes" I found...

- some functions: Floor, Ceil, Minimum, Maximum
- sylvan_mtbdd_storm
- export of BDD seems broken (missing deref?)
- storm wrappers
- research: MTBDD vs stochastic Petri nets
- document: how to extend Sylvan in a clean manner
- sylvan can't count number of minterms

These notes are from 2019, I have no idea what it all means.

[trolando]

I just release version 1.9.0 of Sylvan, which should have a "perfect" CMakeLists.txt file.

[tquatmann]

For reference, here is a list of all the changes we currently made on top of sylvan 1.7.1 (commit b08d75eb56461178a614188ad94cbab211adc253).

It might be worth to skim over these and see if some of them can be avoided by pushing things into main sylvan. In particular sylvan_mtbdd_storm and sylvan_bdd_storm.

[sjunges]

Note that the CMake scripts have been modified based on a more recent version of sylvan :-)

[trolando]

Right. I had a very quick (10 sec) cursory glance and noticed you removed the sylvan namespaces? Why is that? I thought that would actually be good for C++...

[tquatmann]

This was done like 8 years ago. and I couldn't find any commit message adressing this. I can only make guesses at this point.

I believe in combination with external "C", the namespace sylvan {..} doesn't really help to keep the global namespace clean (see here).

So there is no real benefit of using the namespace. In particular, all function names are prefixed by sylvan_ anyways and sylvan::sylvan_foo() is unnecessarily verbose.

[trolando]

Right, I may want to remove that namespace declaration anyway. Not sure if I should even have these C++ things in C headers anyway.

But I'm also going to change the naming convention in Sylvan 2.0, to use things like bdd_and instead of sylvan_and. But something like sylvan_init would stay the same.