You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This is a small feature request aimed probably at @AlexBork.
Currently, the BeliefExplorationPomdpModelChecker returns the computed result as BeliefExplorationPomdpModelChecker::Result struct which contains DTMC with states/choices labelled so that the strategy can be constructed from it. The problem is that if an external FSC was provided to the BeliefMdpExplorer it will only report that external FSC was used in a cut-off via the label "finite_mem" however no information about which memory node of the FSC was used is provided. This information is crucial to construct the strategy into an FSC, which would be great for the SAYNT algorithm (the current output is a bit of mess with many different objects).
This is a small feature request aimed probably at @AlexBork.
Currently, the BeliefExplorationPomdpModelChecker returns the computed result as BeliefExplorationPomdpModelChecker::Result struct which contains DTMC with states/choices labelled so that the strategy can be constructed from it. The problem is that if an external FSC was provided to the BeliefMdpExplorer it will only report that external FSC was used in a cut-off via the label "finite_mem" however no information about which memory node of the FSC was used is provided. This information is crucial to construct the strategy into an FSC, which would be great for the SAYNT algorithm (the current output is a bit of mess with many different objects).
I did some digging and it seems that at the level of belief exploration, this information is stored in the belief MDP https://github.com/moves-rwth/storm/blob/master/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp#L1255 in the form of "mem_node_X" label where X is the index of the used memory node, however when the DTMC for the result is created this information is dropped (here https://github.com/moves-rwth/storm/blob/master/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp#L652 and here https://github.com/moves-rwth/storm/blob/master/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp#L541) and is just replaced with the "finite_mem" label. Maybe we can just add this information to the end of the "finite_mem" label?
The text was updated successfully, but these errors were encountered: