Explain all the arrow and box types that can occur in the graphs in the GUI

[cascremers]

There are a lot of note and edge types in the GUI graphs. The meaning of some is relatively straightforward, but that's not the case for all of them. We should document them.

[rsasse]

To add to the relevance of this issue: we run into that with the students in the FMSec course at ETH regularly. We explain it in the exercises, but it would be good to have it fully documented for everyone! This includes, but is not limited to:

a box = rule instance; l -[a]->r where is top, a is middle, and r is bottom.

arrows come in many colors/formats:

• light grey means persistent fact is used (between particular facts in source and destination)
• black means linear fact is consumed (between particular facts in source and destination)
• dotted means a time point relation (between rule instances!),
• red is adversarial deduction
• green dashed: the dreaded "open chain" or "partial deconstruction" [this is mentioned in Chapter 7, and is the only arrow mentioned]

There are also circles/ovals which represent adversary computations

Possibly explain the difference of the simplified and not simplified views (top right corner)

Related to this, the graph output is presented as PNG which prevents searching. It might be nice to also have an SVG or similar graph output that is searchable. This is more of a tool enhancement than documentation change though.

[xiangliu1995]

What do the different colors of boxes mean?