On left
Status → shows states tried, all unique states and depth of the tries, i.e. how many levels deep of finding new routes (states) to take.
Properties
Global
Shows the properties we are looking to achieve i.e. no doublespend all membership sets converge and so on.
Path of actions
Here you manually click on messages in any order you wish. If you select Per State in the checkbox you will see for every message we are either green or we found a counterexample.
I usually though click the run to completion and it does that automatically, but for early testing, it’s good to have the manual option.
If we find a counterexample, it looks like this (I will make a bug) Below you will see the counterexample it found. I clicked on that to show you this picture. You can see the sequence diagram of messages it sent to get the counterexample (bug). It also shows the state of all nodes, what they know etc.
If you go through the path of actions you can see the sequence diagram filling up and there you will find the bug.
Then of course you work out why and then fix it 
It’s very very good
