It is possible to run the model-checking for AEFD displaying the tree

Set DISPLAY_TREE in LaunchProofFromAEFD to true to display the tree.
It is only possible for very small sets of states (hundreds).