When debugging, the debugger normally breaks on an uncaught exception. But the PSharp runtime catches all exceptions, reports the stack trace and then exits. It would be nice if this did not happen when debugging.
It looks like there is a way to achieve this:
http://stackoverflow.com/questions/21824597/catch-exception-if-debugger-is-not-attached
You create your try-catch blocks like this:
[DebuggerStepThrough]
static public void DoSomeStep()
{
try
{
DoSomething();
}
catch( Exception exception )
{
Console.WriteLine( exception.Message );
if( Debugger.IsAttached == true )
{
throw;
}
}
}
The DebuggerStepThrough attribute ends up causing the debugger to break at the line where the exception was thrown originally (and not at the "throw" in the above method). The downside is that you cannot step through this method (without removing the attribute). However, it looks like you have a few small methods where you catch exceptions, so this seems like it would be fine: Do, ExecuteCurrentStateOnEntry, ExecuteCurrentStateOnExit (for both Machine and Monitor). And I doubt users will be stepping through these methods anyway.
Some comments suggest this only works if "Enable Just My Code (Managed Only)" is ticked, but I guess it's better than nothing.
Alternative: Only catch specific exceptions (e.g. TaskCanceledException) and add an unhandled exception event handler (or something similar).