Segmentation fault when analyzing fault tree

[QuestionableDocumentation]

Hi,

I encountered a "Segmentation fault (core dumped)" error with no further additional error message when attempting to analyse a fault tree where the root is not equivalent to the "top level event". The fault tree in question is segmentationFault.txt (as txt because git doesn't support dft), the code used to analyse was as follows:

dft=stormpy.dft.load_dft_galileo_file("./example.dft")
stormpy.dft.analyze_dft(dft, [stormpy.parse_properties("P=? [F<=1 \"failed\" ]")[0].raw_formula])

While it is of course possible to work around this issue by removing all nodes "above" the top level event prior to the analysis, I still wanted to report this issue in case this behaviour is not intended.

[volkm]

Thanks for the error report. The issue was actually not related to the root node but to a missing check during the symmetry reduction. It will be fixed with https://github.com/moves-rwth/storm/pull/580.

One remark for your case where the root node is not the actual top level event of the tree: Storm will still build the state space corresponding to the top level event but terminates as soon as the root node is failed. That means the state space can be unnecessarily large. If you want to only consider the subtree under the root node, you can simplify the tree beforehand. You can use the dftlib Python library to simplify the fault tree. Both the original and the simplified fault tree will give you the same results.