search

moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
136 stars 75 forks source link

Contribution guide #492

Open saona-raimundo opened 10 months ago

saona-raimundo commented 10 months ago

I would kike to contribute a new algorithm, but there is no contribution guide. How should I proceed?

volkm commented 10 months ago

Can you give us some details which type of algorithm you plan to add? Then we can give you some suggestions and pointers. An overview of some developer guidelines can be found in doc/developers.md.

saona-raimundo commented 10 months ago

The algorithm is a variant of Value Iteration for Markov Decision Processes. The main development was designed for reachability problems, but it also works for shortest stochastic path objectives. The closest related algorithm is optimistic value iteration (https://doi.org/10.1007/978-3-030-53291-8_26). Naturally, we believe our approach is significantly different. Our last implementation efforts were using STORM's codebase and we run the algorithm on the QVBS benchmark set.

We will submit to ICALP a paper soon. Let me know what you think.

sjunges commented 10 months ago

Hey,

It would be great to have this algorithm in Storm.

Things that may be good to clarify before we work on a pull request:

Also, as we would need to maintain the code, having it well documented and having some unit tests is quite essential.

Furthermore, if it is a variant of value iteration, it would be great if we could work towards integrating it in the solver interfaces of Storm. This is, however, not a strict requirement.

saona-raimundo commented 10 months ago

Thanks for the response

Does the new algorithm introduce any new dependencies to the storm code base?

No.

Does it modify any of the existing data structures for matrices etc or provide new data structures for storing things that we already store?

No

Also, as we would need to maintain the code, having it well documented and having some unit tests is quite essential.

Sure, we will provide unit tests.

Furthermore, if it is a variant of value iteration, it would be great if we could work towards integrating it in the solver interfaces of Storm. This is, however, not a strict requirement.

Sure, we agree.

How would you like to proceed?

sjunges commented 10 months ago

That sounds good. Is your code in a state that you want to show this? Then I would suggest you open a pull-request.

saona-raimundo commented 9 months ago

Thank you! With the other authors, we decided to contribute the implementation only after receiving a notification from the conference we submitted to, which is at the end of March. Sorry for the trouble, we will come back to a pull-request then.