This gallery shows the summaries of NASA dataset. We observe different sizes among the summaries. Clearly, the most compact one is the Weak, whilist the Strong is a little bit more complex. Then we can see that type-then-data approach leads to bigger but still somewhat helpful summaries. On the other hand, bisimulation-based summaries are too complicated to give any insights to the human user, we weren’t even able to plot them.
