Fix double free problem when working with interactive belief explorer

[TheGreatfpmK]

When running our CAV'23 algorithm SAYNT in PAYNT, which uses Storm's POMDP model checker we have been getting a double free error at the end. From my debugging, I found the issue is caused by exposing a shared_ptr object via the bound function "BeliefExplorationPomdpModelChecker::getInteractiveBeliefExplorer". In the current implementation, we need this object to update the cut-off values used in belief MDP model checking.

Even though the documentation of pybind11 says that "pybind11 supports std::unique_ptr and std::shared_ptr right out of the box", this has been reported to be untrue: pybind/pybind11#5058. The issue seems to be acknowledged by the authors as in the pybind11 repository there's a branch called smart_holder (more info here) which is being kept up-to-date with the master branch but contains a reworked implementation for smart pointers. One possible solution to this problem would be to use this branch, but I haven't tried that, so I can't confirm whether this helps.

This fix avoids accessing the BeliefMdpExplorer object from the function mentioned above by creating a bind to a newly created function "BeliefExplorationPomdpModelChecker::setFMSchedValueList" (see moves-rwth/storm#623) that will then proceed to call "storm::builder::BeliefMdpExplorer<Pomdp, ValueType>::setFMSchedValueList" inside Storm to achieve the same functionality.

If we agree this is a good fix, I will also remove the binding for the BeliefMdpExplorer class and the function "BeliefExplorationPomdpModelChecker::getInteractiveBeliefExplorer" as these are the culprits for the double free issue.

Depends on moves-rwth/storm#623

@AlexBork do you agree with this solution (please look at the PR in Storm as well)?

[TheGreatfpmK]

I added the link to PR in Storm related to this fix.

And while we are fixing SAYNT, I would also like to resolve this issue: #158

[TheGreatfpmK]

Can we please rerun the checks here to get this merged since we already merged the Storm part?

[sjunges]

I started the jobs again.

[volkm]

The tests are currently still failing, because the docker image was not yet updated. This only happens once per day. I will restart the tests tomorrow morning.

[TheGreatfpmK]

Ok thank you guys!

[volkm]

One last request: can you set the Storm version to 1.9.1 here? That way we indicate that it is not compatible with the latest release anymore.

[TheGreatfpmK]

Done!

[AlexBork]

Thanks, LGTM and the checks now run through :)