we are currently working on a paper about the Dafny Visual Studio extension. Independently, I agree that it could be helpful to produce a video to showcase the various new features.
If you need help with the BVD tool window in particular, this paper might be helpful:
. We have simplified the original BVD user interface that is presented in this paper, but we would appreciate any suggestions for making the interface even simpler or more intuitive.
If you are mainly struggling with the Dafny user interface for selecting errors (red dots) and states of the counterexample trace for the selected error (blue dots), let me give you a quick overview:
1) You can click on a red dot to select an error. This will open up the BVD tool window and it will display blue dots in the program text to represent states of the counterexample trace for this particular error. It will automatically select the last state
of the counterexample trace.
2) Now, you can click on any of the blue to select a different state which will be visualized in the BVD tool window. You can also inspect the values of a variable in the selected state by simply hovering over this variable in the program text.
Again, if you have any suggestions for improving the user interface, please let us know.