fixed bug with formatting unhandled exceptions (#187)

Source/Core/Actors/ActorExecutionContext.cs

@@ -1419,14 +1419,14 @@ namespace Microsoft.Coyote.Actors
                 else if (op is ActorOperation actorOp)
                 {
                     message = string.Format(CultureInfo.InvariantCulture,
-                        $"Unhandled exception. {exception.GetType()} was thrown in actor {actorOp.Name}, " +
+                        $"Unhandled exception '{exception.GetType()}' was thrown in actor '{actorOp.Name}', " +
                         $"'{exception.Source}':\n" +
                         $"   {exception.Message}\n" +
                         $"The stack trace is:\n{exception.StackTrace}");
                 }
                 else
                 {
-                    message = string.Format(CultureInfo.InvariantCulture, $"Unhandled exception. {exception}");
+                    message = CoyoteRuntime.FormatUnhandledException(exception);
                 }
 
                 if (message != null)

Source/Core/Runtime/CoyoteRuntime.cs

@@ -588,11 +588,10 @@ namespace Microsoft.Coyote.Runtime
             {
                 if (context.Options.HasFlag(OperationExecutionOptions.FailOnException))
                 {
-                    this.Assert(false, "Unhandled exception. {0}", ex);
+                    this.Assert(false, FormatUnhandledException(ex));
                 }
                 else
                 {
-                    // Unwrap and cache the exception to propagate it.
                     exception = UnwrapException(ex);
                     this.ReportThrownException(exception);
                 }
@@ -2269,7 +2268,7 @@ namespace Microsoft.Coyote.Runtime
                     // TODO: add some tests for this, so that we check that a task (or lock) that
                     // was cached and reused from prior iteration indeed cannot cause the runtime
                     // to hang anymore.
-                    message = string.Format(CultureInfo.InvariantCulture, $"Unhandled exception. {ece}");
+                    message = string.Format(CultureInfo.InvariantCulture, $"Handled benign exception: {ece}");
                 }
             }
             else if (exception is TaskSchedulerException)
@@ -2284,7 +2283,7 @@ namespace Microsoft.Coyote.Runtime
             }
             else
             {
-                message = string.Format(CultureInfo.InvariantCulture, $"Unhandled exception. {exception}");
+                message = FormatUnhandledException(exception);
             }
 
             if (message != null)
@@ -2305,14 +2304,21 @@ namespace Microsoft.Coyote.Runtime
                 exception = exception.InnerException;
             }
 
-            if (exception is AggregateException)
+            if (exception is AggregateException aex)
             {
-                exception = exception.InnerException;
+                exception = aex.InnerException;
             }
 
             return exception;
         }
 
+        /// <summary>
+        /// Formats the specified unhandled exception.
+        /// </summary>
+        internal static string FormatUnhandledException(Exception ex) => string.Format(CultureInfo.InvariantCulture,
+            $"Unhandled exception '{ex.GetType()}' was thrown in '{ex.Source}':\n" +
+            $"   {ex.Message}\nThe stack trace is:\n{ex.StackTrace}");
+
         /// <summary>
         /// Reports the specified thrown exception.
         /// </summary>

Tests/Tests.BugFinding/Tasks/TaskInterleavingsTests.cs

@@ -166,7 +166,7 @@ namespace Microsoft.Coyote.BugFinding.Tests
                 await task1;
                 AssertSharedEntryValue(entry, 5);
             },
-            configuration: this.GetConfiguration().WithTestingIterations(500),
+            configuration: this.GetConfiguration().WithTestingIterations(1000),
             expectedError: "Value is 3 instead of 5.",
             replay: true);
         }

Tests/Tests.BugFinding/Threading/ThreadPoolTests.cs

@@ -80,7 +80,7 @@ namespace Microsoft.Coyote.BugFinding.Tests
             configuration: this.GetConfiguration().WithTestingIterations(10),
             errorChecker: (e) =>
             {
-                Assert.StartsWith("Unhandled exception. System.InvalidOperationException", e);
+                Assert.StartsWith("Unhandled exception 'System.InvalidOperationException'", e);
             },
             replay: true);
         }
@@ -154,7 +154,7 @@ namespace Microsoft.Coyote.BugFinding.Tests
             configuration: this.GetConfiguration().WithTestingIterations(10),
             errorChecker: (e) =>
             {
-                Assert.StartsWith("Unhandled exception. System.InvalidOperationException", e);
+                Assert.StartsWith("Unhandled exception 'System.InvalidOperationException'", e);
             },
             replay: true);
         }

global.json

@@ -1,5 +1,5 @@
 {
   "sdk": {
-    "version": "5.0.300"
+    "version": "5.0.301"
   }
 }