Merged PR 3020: new logger with log verbosity levels

Make RewritingOptions settable and add a Log option.  Also moved TextWriter to a new ILogger interface so that warnings and errors can be tracked through the whole stack.  This provides a nice feature, which is you can now filter the verbose Actor log output to only show errors like this:
```
coyote test MyActorTest.dll --verbosity minimal
```
and the console output will only show any errors found, same for warnings.  Only if you ask for --verbosity info will you get the full verbose log printed to the screen.

Also when this is published I can redirect [LogWriter.cs](https://github.com/microsoft/coyote-samples/blob/master/Common/LogWriter.cs) in our Samples to use this new interface.

Scripts/build.ps1

@@ -13,7 +13,7 @@ Write-Comment -prefix "." -text "Building Coyote" -color "yellow"
 $dotnet = "dotnet"
 $dotnet_path = FindDotNet($dotnet)
 $version31 = FindInstalledDotNetSdk -dotnet_path $dotnet_path -major "3.1" -minor 0
-$sdk_version = FindDotNetSdk($dotnet_path);
+$sdk_version = FindDotNetSdk -dotnet_path $dotnet_path
 
 if ($null -eq $sdk_version) {
     Write-Error "The global.json file is pointing to version '$sdk_version' but no matching version was found."

Source/Core/Actors/Actor.cs

@@ -5,7 +5,6 @@ using System;
 using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.Globalization;
-using System.IO;
 using System.Linq;
 using System.Reflection;
 using System.Runtime.CompilerServices;
@@ -97,7 +96,7 @@ namespace Microsoft.Coyote.Actors
         internal bool IsDefaultHandlerAvailable { get; private set; }
 
         /// <summary>
-        /// An optional `EventGroup` associated with the current event being handled.
+        /// An optional <see cref="EventGroup"/> associated with the current event being handled.
         /// This is an optional argument provided to CreateActor or SendEvent.
         /// </summary>
         public EventGroup CurrentEventGroup
@@ -118,12 +117,13 @@ namespace Microsoft.Coyote.Actors
         }
 
         /// <summary>
-        /// The installed runtime logger.
+        /// The installed runtime logger as an <see cref="ILogger"/>.  If you need a TextWriter
+        /// then use Logger.TextWriter.
         /// </summary>
         /// <remarks>
         /// See <see href="/coyote/learn/core/logging" >Logging</see> for more information.
         /// </remarks>
-        protected TextWriter Logger => this.Runtime.Logger;
+        protected ILogger Logger => this.Runtime.Logger;
 
         /// <summary>
         /// User-defined hashed state of the actor. Override to improve the

Source/Core/Actors/ActorRuntime.cs

@@ -10,6 +10,7 @@ using System.Reflection;
 using System.Runtime.CompilerServices;
 using System.Threading.Tasks;
 using Microsoft.Coyote.Actors.Timers;
+using Microsoft.Coyote.IO;
 using Microsoft.Coyote.Runtime;
 using Monitor = Microsoft.Coyote.Specifications.Monitor;
 
@@ -34,7 +35,11 @@ namespace Microsoft.Coyote.Actors
         /// Used to log text messages. Use <see cref="ICoyoteRuntime.SetLogger"/>
         /// to replace the logger with a custom one.
         /// </summary>
-        public override TextWriter Logger => this.LogWriter.Logger;
+        public override ILogger Logger
+        {
+            get { return this.LogWriter.Logger; }
+            set { using var v = this.LogWriter.SetLogger(value); }
+        }
 
         /// <summary>
         /// Callback that is fired when a Coyote event is dropped. This happens when
@@ -651,7 +656,17 @@ namespace Microsoft.Coyote.Actors
         internal void TryHandleDroppedEvent(Event e, ActorId id) => this.OnEventDropped?.Invoke(e, id);
 
         /// <inheritdoc/>
-        public override TextWriter SetLogger(TextWriter logger) => this.LogWriter.SetLogger(logger);
+        [Obsolete("Please set the Logger property directory instead of calling this method.")]
+        public override TextWriter SetLogger(TextWriter logger)
+        {
+            var result = this.LogWriter.SetLogger(new TextWriterLogger(logger));
+            if (result != null)
+            {
+                return result.TextWriter;
+            }
+
+            return null;
+        }
 
         /// <summary>
         /// Use this method to register an <see cref="IActorRuntimeLog"/>.

Source/Core/Actors/Logging/ActorRuntimeLogTextFormatter.cs

@@ -2,7 +2,6 @@
 // Licensed under the MIT License.
 
 using System;
-using System.IO;
 using System.Threading.Tasks;
 using Microsoft.Coyote.Actors.Timers;
 using Microsoft.Coyote.IO;
@@ -18,9 +17,13 @@ namespace Microsoft.Coyote.Actors
     public class ActorRuntimeLogTextFormatter : IActorRuntimeLog
     {
         /// <summary>
-        /// Get or set the TextWriter to write to.
+        /// Get or set the <see cref="ILogger"/> interface to the logger.
         /// </summary>
-        public TextWriter Logger { get; set; }
+        /// <remarks>
+        /// If you want Coyote to log to an existing TextWriter, then use the <see cref="TextWriterLogger"/> object
+        /// but that will have a minor performance overhead, so it is better to use <see cref="ILogger"/> directly.
+        /// </remarks>
+        public ILogger Logger { get; set; }
 
         /// <summary>
         /// Initializes a new instance of the <see cref="ActorRuntimeLogTextFormatter"/> class.
@@ -33,7 +36,7 @@ namespace Microsoft.Coyote.Actors
         /// <inheritdoc/>
         public virtual void OnAssertionFailure(string error)
         {
-            this.Logger.WriteLine(error);
+            this.Logger.WriteLine(LogSeverity.Error, error);
         }
 
         /// <inheritdoc/>
@@ -131,7 +134,7 @@ namespace Microsoft.Coyote.Actors
                 text = $"<ExceptionLog> {id} running action '{actionName}' in state '{stateName}' chose to handle exception '{ex.GetType().Name}'.";
             }
 
-            this.Logger.WriteLine(text);
+            this.Logger.WriteLine(LogSeverity.Warning, text);
         }
 
         /// <inheritdoc/>
@@ -147,7 +150,7 @@ namespace Microsoft.Coyote.Actors
                 text = $"<ExceptionLog> {id} running action '{actionName}' in state '{stateName}' threw exception '{ex.GetType().Name}'.";
             }
 
-            this.Logger.WriteLine(text);
+            this.Logger.WriteLine(LogSeverity.Warning, text);
         }
 
         /// <inheritdoc/>
@@ -225,6 +228,7 @@ namespace Microsoft.Coyote.Actors
         /// <inheritdoc/>
         public virtual void OnMonitorError(string monitorType, string stateName, bool? isInHotState)
         {
+            this.Logger.WriteLine(LogSeverity.Error, $"<MonitorLog> {monitorType} found an error in state {stateName}.");
         }
 
         /// <inheritdoc/>

Source/Core/Actors/Logging/LogWriter.cs

@@ -24,7 +24,12 @@ namespace Microsoft.Coyote.Actors
         /// <summary>
         /// Used to log messages.
         /// </summary>
-        internal TextWriter Logger { get; private set; }
+        internal ILogger Logger { get; private set; }
+
+        /// <summary>
+        /// The log level to report.
+        /// </summary>
+        private LogSeverity LogLevel { get; set; }
 
         /// <summary>
         /// Initializes a new instance of the <see cref="LogWriter"/> class.
@@ -33,13 +38,15 @@ namespace Microsoft.Coyote.Actors
         {
             this.Logs = new HashSet<IActorRuntimeLog>();
 
+            this.LogLevel = configuration.LogLevel;
+
             if (configuration.IsVerbose)
             {
                 this.GetOrCreateTextLog();
             }
             else
             {
-                this.Logger = TextWriter.Null;
+                this.Logger = new NullLogger();
             }
         }
 
@@ -599,14 +606,14 @@ namespace Microsoft.Coyote.Actors
             this.Logs.OfType<TActorRuntimeLog>();
 
         /// <summary>
-        /// Use this method to override the default <see cref="TextWriter"/> for logging messages.
+        /// Use this method to override the default <see cref="ILogger"/> for logging messages.
         /// </summary>
-        internal TextWriter SetLogger(TextWriter logger)
+        internal ILogger SetLogger(ILogger logger)
         {
             var prevLogger = this.Logger;
             if (logger == null)
             {
-                this.Logger = TextWriter.Null;
+                this.Logger = new NullLogger();
 
                 var textLog = this.GetLogsOfType<ActorRuntimeLogTextFormatter>().FirstOrDefault();
                 if (textLog != null)
@@ -633,7 +640,7 @@ namespace Microsoft.Coyote.Actors
             {
                 if (this.Logger == null)
                 {
-                    this.Logger = new ConsoleLogger();
+                    this.Logger = new ConsoleLogger() { LogLevel = this.LogLevel };
                 }
 
                 textLog = new ActorRuntimeLogTextFormatter

Source/Core/Configuration.cs

@@ -4,6 +4,7 @@
 using System;
 using System.Collections.Generic;
 using System.Runtime.Serialization;
+using Microsoft.Coyote.IO;
 
 namespace Microsoft.Coyote
 {
@@ -197,6 +198,12 @@ namespace Microsoft.Coyote
         [DataMember]
         public bool IsVerbose { get; internal set; }
 
+        /// <summary>
+        /// The level of detail to provide in verbose logging.
+        /// </summary>
+        [DataMember]
+        public LogSeverity LogLevel { get; internal set; }
+
         /// <summary>
         /// Enables code coverage reporting of a Coyote program.
         /// </summary>
@@ -371,6 +378,7 @@ namespace Microsoft.Coyote
             this.DebugActivityCoverage = false;
 
             this.IsVerbose = false;
+            this.LogLevel = LogSeverity.Informational;
             this.EnableDebugging = false;
 
             this.AdditionalCodeCoverageAssemblies = new Dictionary<string, bool>();
@@ -536,9 +544,11 @@ namespace Microsoft.Coyote
         /// Updates the configuration with verbose output enabled or disabled.
         /// </summary>
         /// <param name="isVerbose">If true, then messages are logged.</param>
-        public Configuration WithVerbosityEnabled(bool isVerbose = true)
+        /// <param name="logLevel">The level of detail to provide in verbose logging.</param>
+        public Configuration WithVerbosityEnabled(bool isVerbose = true, LogSeverity logLevel = LogSeverity.Informational)
         {
             this.IsVerbose = isVerbose;
+            this.LogLevel = logLevel;
             return this;
         }
 

Source/Core/IO/ErrorReporter.cs

@@ -1,57 +0,0 @@
-// Copyright (c) Microsoft Corporation.
-// Licensed under the MIT License.
-
-using System;
-using System.IO;
-
-namespace Microsoft.Coyote.IO
-{
-    /// <summary>
-    /// Reports errors and warnings to the user.
-    /// </summary>
-    internal sealed class ErrorReporter
-    {
-        /// <summary>
-        /// Configuration.
-        /// </summary>
-        private readonly Configuration Configuration;
-
-        /// <summary>
-        /// The installed logger.
-        /// </summary>
-        internal TextWriter Logger { get; set; }
-
-        /// <summary>
-        /// Initializes a new instance of the <see cref="ErrorReporter"/> class.
-        /// </summary>
-        internal ErrorReporter(Configuration configuration, TextWriter logger)
-        {
-            this.Configuration = configuration;
-            this.Logger = logger ?? new ConsoleLogger();
-        }
-
-        /// <summary>
-        /// Reports an error, followed by the current line terminator.
-        /// </summary>
-        public void WriteErrorLine(string value)
-        {
-            this.Write("Error: " + value, ConsoleColor.Red);
-            this.Logger.WriteLine(string.Empty);
-        }
-
-        /// <summary>
-        /// Writes the specified string value.
-        /// </summary>
-        private void Write(string value, ConsoleColor color)
-        {
-            if (this.Configuration.EnableColoredConsoleOutput)
-            {
-                Error.Write(this.Logger, color, value);
-            }
-            else
-            {
-                this.Logger.Write(value);
-            }
-        }
-    }
-}

Source/Core/IO/Logging/ConsoleLogger.cs

@@ -13,7 +13,7 @@ namespace Microsoft.Coyote.IO
     /// <remarks>
     /// See <see href="/coyote/learn/core/logging" >Logging</see> for more information.
     /// </remarks>
-    public sealed class ConsoleLogger : TextWriter
+    public sealed class ConsoleLogger : TextWriter, ILogger
     {
         /// <summary>
         /// Initializes a new instance of the <see cref="ConsoleLogger"/> class.
@@ -22,6 +22,9 @@ namespace Microsoft.Coyote.IO
         {
         }
 
+        /// <inheritdoc/>
+        public TextWriter TextWriter => this;
+
         /// <summary>
         /// When overridden in a derived class, returns the character encoding in which the
         /// output is written.
@@ -29,53 +32,115 @@ namespace Microsoft.Coyote.IO
         public override Encoding Encoding => Console.OutputEncoding;
 
         /// <summary>
-        /// Writes the specified Unicode character value to the standard output stream.
+        /// The level of detail to report.
         /// </summary>
-        /// <param name="value">The Unicode character.</param>
-        public override void Write(char value)
-        {
-            Console.Write(value);
-        }
+        public LogSeverity LogLevel { get; set; }
 
-        /// <summary>
-        /// Writes the specified string value.
-        /// </summary>
+        /// <inheritdoc/>
         public override void Write(string value)
         {
-            Console.Write(value);
+            this.Write(LogSeverity.Informational, value);
         }
 
-        /// <summary>
-        /// Writes a string followed by a line terminator to the text string or stream.
-        /// </summary>
-        /// <param name="value">The string to write.</param>
+        /// <inheritdoc/>
+        public void Write(LogSeverity severity, string value)
+        {
+            switch (severity)
+            {
+                case LogSeverity.Informational:
+                    if (this.LogLevel <= LogSeverity.Informational)
+                    {
+                        Console.Write(value);
+                    }
+
+                    break;
+                case LogSeverity.Warning:
+                    if (this.LogLevel <= LogSeverity.Warning)
+                    {
+                        Error.Write(Console.Out, ConsoleColor.Yellow, value);
+                    }
+
+                    break;
+                case LogSeverity.Error:
+                    if (this.LogLevel <= LogSeverity.Error)
+                    {
+                        Error.Write(Console.Out, ConsoleColor.Red, value);
+                    }
+
+                    break;
+
+                case LogSeverity.Important:
+                    Console.Write(value);
+                    break;
+
+                default:
+                    break;
+            }
+        }
+
+        /// <inheritdoc/>
+        public void Write(LogSeverity severity, string format, params object[] args)
+        {
+            string value = string.Format(format, args);
+            this.Write(severity, value);
+        }
+
+        /// <inheritdoc/>
         public override void WriteLine(string value)
         {
-            Console.WriteLine(value);
+            this.WriteLine(LogSeverity.Informational, value);
         }
 
-        /// <summary>
-        /// Reports an error, followed by the current line terminator.
-        /// </summary>
-        /// <param name="value">The string to write.</param>
-#pragma warning disable CA1822 // Mark members as static
-        public void WriteErrorLine(string value)
-#pragma warning restore CA1822 // Mark members as static
+        /// <inheritdoc/>
+        public override void WriteLine(string format, params object[] args)
         {
-            Error.Write(Console.Out, ConsoleColor.Red, value);
-            Console.WriteLine();
+            string value = string.Format(format, args);
+            this.WriteLine(LogSeverity.Informational, value);
         }
 
-        /// <summary>
-        /// Reports an warning, followed by the current line terminator.
-        /// </summary>
-        /// <param name="value">The string to write.</param>
-#pragma warning disable CA1822 // Mark members as static
-        public void WriteWarningLine(string value)
-#pragma warning restore CA1822 // Mark members as static
+        /// <inheritdoc/>
+        public void WriteLine(LogSeverity severity, string value)
         {
-            Error.Write(Console.Out, ConsoleColor.Yellow, value);
-            Console.WriteLine();
+            switch (severity)
+            {
+                case LogSeverity.Informational:
+                    if (this.LogLevel <= LogSeverity.Informational)
+                    {
+                        Console.WriteLine(value);
+                    }
+
+                    break;
+                case LogSeverity.Warning:
+                    if (this.LogLevel <= LogSeverity.Warning)
+                    {
+                        Error.Write(Console.Out, ConsoleColor.Yellow, value);
+                        Console.WriteLine();
+                    }
+
+                    break;
+                case LogSeverity.Error:
+                    if (this.LogLevel <= LogSeverity.Error)
+                    {
+                        Error.Write(Console.Out, ConsoleColor.Red, value);
+                        Console.WriteLine();
+                    }
+
+                    break;
+
+                case LogSeverity.Important:
+                    Console.WriteLine(value);
+                    break;
+
+                default:
+                    break;
+            }
+        }
+
+        /// <inheritdoc/>
+        public void WriteLine(LogSeverity severity, string format, params object[] args)
+        {
+            string value = string.Format(format, args);
+            this.WriteLine(severity, value);
         }
     }
 }

Source/Core/IO/Logging/ILogger.cs

@@ -0,0 +1,76 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.IO;
+
+namespace Microsoft.Coyote.IO
+{
+    /// <summary>
+    /// A logger is used to capture messages, warnings and errors.
+    /// </summary>
+    public interface ILogger : IDisposable
+    {
+        /// <summary>
+        /// This property provides a TextWriter that implements ILogger which is handy if you
+        /// have existing code that requires a TextWriter.
+        /// </summary>
+        public TextWriter TextWriter { get; }
+
+        /// <summary>
+        /// Writes an informational string to the log.
+        /// </summary>
+        /// <param name="value">The string to write.</param>
+        public void Write(string value);
+
+        /// <summary>
+        /// Writes an informational string to the log.
+        /// </summary>
+        /// <param name="format">The string format to write.</param>
+        /// <param name="args">The arguments needed to format the string.</param>
+        public void Write(string format, params object[] args);
+
+        /// <summary>
+        /// Writes a string to the log.
+        /// </summary>
+        /// <param name="severity">The severity of the issue being logged.</param>
+        /// <param name="value">The string to write.</param>
+        public void Write(LogSeverity severity, string value);
+
+        /// <summary>
+        /// Writes a string to the log.
+        /// </summary>
+        /// <param name="severity">The severity of the issue being logged.</param>
+        /// <param name="format">The string format to write.</param>
+        /// <param name="args">The arguments needed to format the string.</param>
+        public void Write(LogSeverity severity, string format, params object[] args);
+
+        /// <summary>
+        /// Writes an informational string to the log.
+        /// </summary>
+        /// <param name="value">The string to write.</param>
+        public void WriteLine(string value);
+
+        /// <summary>
+        /// Writes an informational string to the log.
+        /// </summary>
+        /// <param name="format">The string format to write.</param>
+        /// <param name="args">The arguments needed to format the string.</param>
+        public void WriteLine(string format, params object[] args);
+
+        /// <summary>
+        /// Writes a string followed by a line terminator to the text string or stream.
+        /// </summary>
+        /// <param name="severity">The severity of the issue being logged.</param>
+        /// <param name="value">The string to write.</param>
+        public void WriteLine(LogSeverity severity, string value);
+
+        /// <summary>
+        /// Writes a string followed by a line terminator to the text string or stream.
+        /// </summary>
+        /// <param name="severity">The severity of the issue being logged.</param>
+        /// <param name="format">The string format to write.</param>
+        /// <param name="args">The arguments needed to format the string.</param>
+        public void WriteLine(LogSeverity severity, string format, params object[] args);
+    }
+}

Source/Core/IO/Logging/InMemoryLogger.cs

@@ -14,7 +14,7 @@ namespace Microsoft.Coyote.IO
     /// <remarks>
     /// See <see href="/coyote/learn/core/logging" >Logging</see> for more information.
     /// </remarks>
-    public sealed class InMemoryLogger : TextWriter
+    public sealed class InMemoryLogger : TextWriter, ILogger
     {
         /// <summary>
         /// Underlying string builder.
@@ -29,7 +29,10 @@ namespace Microsoft.Coyote.IO
         /// <summary>
         /// Optional logger provided by the user to delegate logging to.
         /// </summary>
-        internal TextWriter UserLogger { get; set; }
+        internal ILogger UserLogger { get; set; }
+
+        /// <inheritdoc/>
+        public TextWriter TextWriter => this;
 
         /// <summary>
         /// When overridden in a derived class, returns the character encoding in which the
@@ -46,33 +49,14 @@ namespace Microsoft.Coyote.IO
             this.Lock = new object();
         }
 
-        /// <summary>
-        /// Writes the specified Unicode character value to the standard output stream.
-        /// </summary>
-        /// <param name="value">The Unicode character.</param>
-        public override void Write(char value)
-        {
-            try
-            {
-                lock (this.Lock)
-                {
-                    this.Builder.Append(value);
-                    if (this.UserLogger != null)
-                    {
-                        this.UserLogger.WriteLine(value);
-                    }
-                }
-            }
-            catch (ObjectDisposedException)
-            {
-                // The writer was disposed.
-            }
-        }
-
-        /// <summary>
-        /// Writes the specified string value.
-        /// </summary>
+        /// <inheritdoc/>
         public override void Write(string value)
+        {
+            this.Write(LogSeverity.Informational, value);
+        }
+
+        /// <inheritdoc/>
+        public void Write(LogSeverity severity, string value)
         {
             try
             {
@@ -81,7 +65,7 @@ namespace Microsoft.Coyote.IO
                     this.Builder.Append(value);
                     if (this.UserLogger != null)
                     {
-                        this.UserLogger.WriteLine(value);
+                        this.UserLogger.Write(severity, value);
                     }
                 }
             }
@@ -91,11 +75,21 @@ namespace Microsoft.Coyote.IO
             }
         }
 
-        /// <summary>
-        /// Writes a string followed by a line terminator to the text string or stream.
-        /// </summary>
-        /// <param name="value">The string to write.</param>
+        /// <inheritdoc/>
+        public void Write(LogSeverity severity, string format, params object[] args)
+        {
+            string msg = string.Format(format, args);
+            this.Write(severity, msg);
+        }
+
+        /// <inheritdoc/>
         public override void WriteLine(string value)
+        {
+            this.WriteLine(LogSeverity.Informational, value);
+        }
+
+        /// <inheritdoc/>
+        public void WriteLine(LogSeverity severity, string value)
         {
             try
             {
@@ -104,7 +98,7 @@ namespace Microsoft.Coyote.IO
                     this.Builder.AppendLine(value);
                     if (this.UserLogger != null)
                     {
-                        this.UserLogger.WriteLine(value);
+                        this.UserLogger.WriteLine(severity, value);
                     }
                 }
             }
@@ -114,6 +108,13 @@ namespace Microsoft.Coyote.IO
             }
         }
 
+        /// <inheritdoc/>
+        public void WriteLine(LogSeverity severity, string format, params object[] args)
+        {
+            string msg = string.Format(format, args);
+            this.WriteLine(severity, msg);
+        }
+
         /// <summary>
         /// Returns the logged text as a string.
         /// </summary>

Source/Core/IO/Logging/LogSeverity.cs

@@ -0,0 +1,31 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+namespace Microsoft.Coyote.IO
+{
+    /// <summary>
+    /// Flag indicating the type of logging information being provided to the <see cref="ILogger"/>.
+    /// </summary>
+    public enum LogSeverity
+    {
+        /// <summary>
+        /// General information about what is happening in the program.
+        /// </summary>
+        Informational,
+
+        /// <summary>
+        /// Warnings that something unusual is found and is being handled.
+        /// </summary>
+        Warning,
+
+        /// <summary>
+        /// Error is something unexpected that usually means program cannot proceed normally.
+        /// </summary>
+        Error,
+
+        /// <summary>
+        /// Output that is not an error or warning, but is important.
+        /// </summary>
+        Important
+    }
+}

Source/Core/IO/Logging/NullLogger.cs

@@ -0,0 +1,61 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System.IO;
+using System.Text;
+
+namespace Microsoft.Coyote.IO
+{
+    /// <inheritdoc/>
+    internal class NullLogger : TextWriter, ILogger
+    {
+        /// <inheritdoc/>
+        public TextWriter TextWriter => this;
+
+        /// <inheritdoc/>
+        public override void Write(string value)
+        {
+        }
+
+        /// <summary>
+        /// When overridden in a derived class, returns the character encoding in which the
+        /// output is written.
+        /// </summary>
+        public override Encoding Encoding => Encoding.Unicode;
+
+        /// <inheritdoc/>
+        public void Write(LogSeverity severity, string value)
+        {
+        }
+
+        /// <inheritdoc/>
+        public override void Write(string format, params object[] args)
+        {
+        }
+
+        /// <inheritdoc/>
+        public void Write(LogSeverity severity, string format, params object[] args)
+        {
+        }
+
+        /// <inheritdoc/>
+        public override void WriteLine(string value)
+        {
+        }
+
+        /// <inheritdoc/>
+        public override void WriteLine(string format, params object[] args)
+        {
+        }
+
+        /// <inheritdoc/>
+        public void WriteLine(LogSeverity severity, string value)
+        {
+        }
+
+        /// <inheritdoc/>
+        public void WriteLine(LogSeverity severity, string format, params object[] args)
+        {
+        }
+    }
+}

Source/Core/IO/Logging/TextWriterLogger.cs

@@ -0,0 +1,80 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System.IO;
+using System.Text;
+
+namespace Microsoft.Coyote.IO
+{
+    /// <summary>
+    /// Bridges custom user provided TextWriter logger so it can be passed into
+    /// Coyote via the <see cref="ILogger"/> interface.
+    /// </summary>
+    internal class TextWriterLogger : TextWriter, ILogger
+    {
+        private readonly TextWriter UserLogger;
+
+        /// <inheritdoc/>
+        public TextWriter TextWriter => this.UserLogger;
+
+        /// <summary>
+        /// Initializes a new instance of the <see cref="TextWriterLogger"/> class.
+        /// </summary>
+        /// <param name="userLogger">The TextWriter to delegate to.</param>
+        public TextWriterLogger(TextWriter userLogger)
+        {
+            this.UserLogger = userLogger;
+        }
+
+        /// <inheritdoc/>
+        public override Encoding Encoding => this.UserLogger.Encoding;
+
+        /// <inheritdoc/>
+        public override void Write(string message)
+        {
+            this.UserLogger.Write(message);
+        }
+
+        /// <inheritdoc/>
+        public override void Write(string format, object[] args)
+        {
+            this.UserLogger.Write(format, args);
+        }
+
+        /// <inheritdoc/>
+        public void Write(LogSeverity severity, string value)
+        {
+            this.Write(value);
+        }
+
+        /// <inheritdoc/>
+        public void Write(LogSeverity severity, string format, params object[] args)
+        {
+            this.Write(format, args);
+        }
+
+        /// <inheritdoc/>
+        public override void WriteLine(string message)
+        {
+            this.UserLogger.WriteLine(message);
+        }
+
+        /// <inheritdoc/>
+        public override void WriteLine(string format, object[] args)
+        {
+            this.UserLogger.WriteLine(format, args);
+        }
+
+        /// <inheritdoc/>
+        public void WriteLine(LogSeverity severity, string value)
+        {
+            this.UserLogger.WriteLine(value);
+        }
+
+        /// <inheritdoc/>
+        public void WriteLine(LogSeverity severity, string format, params object[] args)
+        {
+            this.WriteLine(format, args);
+        }
+    }
+}

Source/Core/Runtime/CoyoteRuntime.cs

@@ -7,6 +7,7 @@ using System.Globalization;
 using System.IO;
 using System.Threading;
 using System.Threading.Tasks;
+using Microsoft.Coyote.IO;
 using Monitor = Microsoft.Coyote.Specifications.Monitor;
 
 namespace Microsoft.Coyote.Runtime
@@ -80,11 +81,8 @@ namespace Microsoft.Coyote.Runtime
         /// </summary>
         protected internal volatile bool IsRunning;
 
-        /// <summary>
-        /// Used to log text messages. Use <see cref="SetLogger"/>
-        /// to replace the logger with a custom one.
-        /// </summary>
-        public abstract TextWriter Logger { get; }
+        /// <inheritdoc/>
+        public abstract ILogger Logger { get; set; }
 
         /// <summary>
         /// Callback that is fired when the Coyote program throws an exception which includes failed assertions.
@@ -258,10 +256,9 @@ namespace Microsoft.Coyote.Runtime
         /// </summary>
         internal static void AssignAsyncControlFlowRuntime(CoyoteRuntime runtime) => AsyncLocalInstance.Value = runtime;
 
-        /// <summary>
-        /// Use this method to override the default <see cref="TextWriter"/> for logging messages.
-        /// </summary>
-        public abstract TextWriter SetLogger(TextWriter logger);
+        /// <inheritdoc/>
+        [Obsolete("Please set the Logger property directory instead of calling this method.")]
+        public abstract TextWriter SetLogger(TextWriter writer);
 
         /// <summary>
         /// Raises the <see cref="OnFailure"/> event with the specified <see cref="Exception"/>.

Source/Core/Runtime/ICoyoteRuntime.cs

@@ -3,6 +3,7 @@
 
 using System;
 using System.IO;
+using Microsoft.Coyote.IO;
 using Microsoft.Coyote.Specifications;
 
 namespace Microsoft.Coyote.Runtime
@@ -13,13 +14,12 @@ namespace Microsoft.Coyote.Runtime
     public interface ICoyoteRuntime : IDisposable
     {
         /// <summary>
-        /// Used to log messages. Use <see cref="SetLogger"/>
-        /// to replace the logger with a custom one.
+        /// Get or set the  <see cref="ILogger"/> used to log messages.
         /// </summary>
         /// <remarks>
         /// See <see href="/coyote/learn/core/logging" >Logging</see> for more information.
         /// </remarks>
-        TextWriter Logger { get; }
+        ILogger Logger { get; set; }
 
         /// <summary>
         /// Callback that is fired when the runtime throws an exception which includes failed assertions.
@@ -120,11 +120,17 @@ namespace Microsoft.Coyote.Runtime
         void Assert(bool predicate, string s, params object[] args);
 
         /// <summary>
-        /// Use this method to override the default <see cref="TextWriter"/> for logging messages.
+        /// The old way of setting the <see cref="Logger"/> property.
         /// </summary>
-        /// <param name="logger">The logger to install.</param>
+        /// <remarks>
+        /// The new way is to just set the Logger property to an <see cref="ILogger"/> object.
+        /// This method is only here for compatibility and has a minor perf impact as it has to
+        /// wrap the writer in an object that implements the <see cref="ILogger"/> interface.
+        /// </remarks>
+        /// <param name="writer">The writer to use for logging.</param>
         /// <returns>The previously installed logger.</returns>
-        TextWriter SetLogger(TextWriter logger);
+        [Obsolete("Please set the Logger property directory instead of calling this method.")]
+        TextWriter SetLogger(TextWriter writer);
 
         /// <summary>
         /// Terminates the runtime and notifies each active actor to halt execution.

Source/Core/Specifications/Monitors/Monitor.cs

@@ -4,12 +4,12 @@
 using System;
 using System.Collections.Concurrent;
 using System.Collections.Generic;
-using System.IO;
 using System.Linq;
 using System.Linq.Expressions;
 using System.Reflection;
 using System.Threading.Tasks;
 using Microsoft.Coyote.Actors;
+using Microsoft.Coyote.IO;
 
 namespace Microsoft.Coyote.Specifications
 {
@@ -96,7 +96,7 @@ namespace Microsoft.Coyote.Specifications
         /// <remarks>
         /// See <see href="/coyote/learn/core/logging" >Logging</see> for more information.
         /// </remarks>
-        protected TextWriter Logger => this.Runtime.Logger;
+        protected ILogger Logger => this.Runtime.Logger;
 
         /// <summary>
         /// Gets the current state.

Source/Core/SystematicTesting/Strategies/Special/InteractiveStrategy.cs

@@ -22,7 +22,7 @@ namespace Microsoft.Coyote.SystematicTesting.Strategies
         /// <summary>
         /// The installed logger.
         /// </summary>
-        private readonly TextWriter Logger;
+        private readonly ILogger Logger;
 
         /// <summary>
         /// The input cache.
@@ -37,7 +37,7 @@ namespace Microsoft.Coyote.SystematicTesting.Strategies
         /// <summary>
         /// Initializes a new instance of the <see cref="InteractiveStrategy"/> class.
         /// </summary>
-        public InteractiveStrategy(Configuration configuration, TextWriter logger)
+        public InteractiveStrategy(Configuration configuration, ILogger logger)
         {
             this.Logger = logger ?? new ConsoleLogger();
             this.Configuration = configuration;
@@ -131,20 +131,20 @@ namespace Microsoft.Coyote.SystematicTesting.Strategies
                         var idx = Convert.ToInt32(input);
                         if (idx < 0)
                         {
-                            this.Logger.WriteLine(">> Expected positive integer, please retry ...");
+                            this.Logger.WriteLine(LogSeverity.Warning, ">> Expected positive integer, please retry ...");
                             continue;
                         }
 
                         next = enabledOps[idx];
                         if (next is null)
                         {
-                            this.Logger.WriteLine(">> Unexpected id, please retry ...");
+                            this.Logger.WriteLine(LogSeverity.Warning, ">> Unexpected id, please retry ...");
                             continue;
                         }
                     }
                     catch (FormatException)
                     {
-                        this.Logger.WriteLine(">> Wrong format, please retry ...");
+                        this.Logger.WriteLine(LogSeverity.Warning, ">> Wrong format, please retry ...");
                         continue;
                     }
                 }
@@ -217,7 +217,7 @@ namespace Microsoft.Coyote.SystematicTesting.Strategies
                     }
                     catch (FormatException)
                     {
-                        this.Logger.WriteLine(">> Wrong format, please retry ...");
+                        this.Logger.WriteLine(LogSeverity.Warning, ">> Wrong format, please retry ...");
                         continue;
                     }
                 }
@@ -286,7 +286,7 @@ namespace Microsoft.Coyote.SystematicTesting.Strategies
                     }
                     catch (FormatException)
                     {
-                        this.Logger.WriteLine(">> Wrong format, please retry ...");
+                        this.Logger.WriteLine(LogSeverity.Warning, ">> Wrong format, please retry ...");
                         continue;
                     }
                 }
@@ -343,7 +343,7 @@ namespace Microsoft.Coyote.SystematicTesting.Strategies
                 var steps = Convert.ToInt32(Console.ReadLine());
                 if (steps < 0)
                 {
-                    this.Logger.WriteLine(">> Expected positive integer, please retry ...");
+                    this.Logger.WriteLine(LogSeverity.Warning, ">> Expected positive integer, please retry ...");
                     result = false;
                 }
 
@@ -351,7 +351,7 @@ namespace Microsoft.Coyote.SystematicTesting.Strategies
             }
             catch (FormatException)
             {
-                this.Logger.WriteLine(">> Wrong format, please retry ...");
+                this.Logger.WriteLine(LogSeverity.Warning, ">> Wrong format, please retry ...");
                 result = false;
             }
 
@@ -372,7 +372,7 @@ namespace Microsoft.Coyote.SystematicTesting.Strategies
                 var steps = Convert.ToInt32(Console.ReadLine());
                 if (steps < this.ExploredSteps)
                 {
-                    this.Logger.WriteLine(">> Expected integer greater than " +
+                    this.Logger.WriteLine(LogSeverity.Warning, ">> Expected integer greater than " +
                         $"{this.ExploredSteps}, please retry ...");
                     result = false;
                 }
@@ -381,7 +381,7 @@ namespace Microsoft.Coyote.SystematicTesting.Strategies
             }
             catch (FormatException)
             {
-                this.Logger.WriteLine(">> Wrong format, please retry ...");
+                this.Logger.WriteLine(LogSeverity.Warning, " >> Wrong format, please retry ...");
                 result = false;
             }
 

Source/Core/SystematicTesting/TaskController.cs

@@ -1071,14 +1071,14 @@ namespace Microsoft.Coyote.SystematicTesting
         /// </summary>
         private void ReportThrownException(Exception exception)
         {
-            if (!(exception is ExecutionCanceledException))
+            if (!(exception is ExecutionCanceledException) && !(exception is TaskCanceledException) && !(exception is OperationCanceledException))
             {
                 string message = string.Format(CultureInfo.InvariantCulture,
                     $"Exception '{exception.GetType()}' was thrown in task '{Task.CurrentId}', " +
                     $"'{exception.Source}':\n" +
                     $"   {exception.Message}\n" +
                     $"The stack trace is:\n{exception.StackTrace}");
-                this.Runtime.Logger.WriteLine($"<ExceptionLog> {message}");
+                this.Runtime.Logger.WriteLine(IO.LogSeverity.Warning, $"<ExceptionLog> {message}");
             }
         }
 

Source/Test/Rewriting/AssemblyRewriter.cs

@@ -54,13 +54,13 @@ namespace Microsoft.Coyote.Rewriting
 
         private readonly string[] DefaultDisallowedList = new string[]
         {
-            @"Newtonsoft\.Json",
+            @"Newtonsoft\.Json\.dll",
             @"Microsoft\.Coyote\.dll",
             @"Microsoft\.Coyote.Test\.dll",
             @"Microsoft\.VisualStudio\.TestPlatform.*",
             @"Microsoft\.TestPlatform.*",
-            @"System\.Private\.CoreLib",
-            @"mscorlib"
+            @"System\.Private\.CoreLib\.dll",
+            @"mscorlib\.dll"
         };
 
         /// <summary>
@@ -76,7 +76,7 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// The output log.
         /// </summary>
-        private readonly ConsoleLogger Log;
+        private readonly ILogger Log;
 
         /// <summary>
         /// List of assemblies to be rewritten.
@@ -91,7 +91,7 @@ namespace Microsoft.Coyote.Rewriting
         private AssemblyRewriter(Configuration configuration, RewritingOptions options)
         {
             this.Configuration = configuration;
-            this.Log = new ConsoleLogger();
+            this.Log = options.Log ?? new ConsoleLogger() { LogLevel = options.LogLevel };
             this.Options = options;
             this.RewrittenAssemblies = new Dictionary<string, AssemblyNameDefinition>();
             var userList = options.DisallowedAssemblies ?? Array.Empty<string>();
@@ -145,7 +145,7 @@ namespace Microsoft.Coyote.Rewriting
                 // Expand to include all .dll files in AssemblyPaths.
                 foreach (var file in Directory.GetFiles(this.Options.AssembliesDirectory, "*.dll"))
                 {
-                    if (this.IsDisallowed(Path.GetFileNameWithoutExtension(file)))
+                    if (this.IsDisallowed(Path.GetFileName(file)))
                     {
                         this.Options.AssemblyPaths.Add(file);
                     }
@@ -172,6 +172,21 @@ namespace Microsoft.Coyote.Rewriting
         /// </summary>
         public static void Rewrite(Configuration configuration, RewritingOptions options)
         {
+            if (string.IsNullOrEmpty(options.AssembliesDirectory))
+            {
+                throw new Exception("Please provide RewritingOptions.AssembliesDirectory");
+            }
+
+            if (string.IsNullOrEmpty(options.OutputDirectory))
+            {
+                throw new Exception("Please provide RewritingOptions.OutputDirectory");
+            }
+
+            if (options.AssemblyPaths == null || options.AssemblyPaths.Count == 0)
+            {
+                throw new Exception("Please provide RewritingOptions.AssemblyPaths");
+            }
+
             var binaryRewriter = new AssemblyRewriter(configuration, options);
             binaryRewriter.Rewrite();
         }
@@ -204,11 +219,11 @@ namespace Microsoft.Coyote.Rewriting
                 {
                     if (ex is AggregateException ae && ae.InnerException != null)
                     {
-                        this.Log.WriteErrorLine(ae.InnerException.Message);
+                        this.Log.WriteLine(LogSeverity.Error, ae.InnerException.Message);
                     }
                     else
                     {
-                        this.Log.WriteErrorLine(ex.Message);
+                        this.Log.WriteLine(LogSeverity.Error, ex.Message);
                     }
 
                     errors++;
@@ -262,7 +277,7 @@ namespace Microsoft.Coyote.Rewriting
                 if (IsAssemblyRewritten(assembly))
                 {
                     // The assembly has been already rewritten by this version of Coyote, so skip it.
-                    this.Log.WriteWarningLine($"..... Skipping assembly (reason: already rewritten by Coyote v{GetAssemblyRewritterVersion()})");
+                    this.Log.WriteLine(LogSeverity.Warning, $"..... Skipping assembly (reason: already rewritten by Coyote v{GetAssemblyRewritterVersion()})");
                     return;
                 }
 
@@ -332,7 +347,7 @@ namespace Microsoft.Coyote.Rewriting
                     }
 
                     await Task.Delay(100);
-                    this.Log.WriteLine($"... Retrying write to {targetFile}");
+                    this.Log.WriteLine(LogSeverity.Warning, $"... Retrying write to {targetFile}");
                 }
             }
         }
@@ -366,8 +381,8 @@ namespace Microsoft.Coyote.Rewriting
             {
                 foreach (var ar in module.AssemblyReferences)
                 {
-                    var name = ar.Name;
-                    var localName = Path.Combine(assemblyDir, name + ".dll");
+                    var name = ar.Name + ".dll";
+                    var localName = Path.Combine(assemblyDir, name);
                     if (!this.IsDisallowed(name) &&
                         File.Exists(localName) && !this.Pending.Contains(localName))
                     {
@@ -564,7 +579,7 @@ namespace Microsoft.Coyote.Rewriting
         /// </summary>
         private AssemblyDefinition OnResolveAssemblyFailure(object sender, AssemblyNameReference reference)
         {
-            this.Log.WriteErrorLine("Error resolving assembly: " + reference.FullName);
+            this.Log.WriteLine(LogSeverity.Warning, "Error resolving assembly: " + reference.FullName);
             return null;
         }
     }

Source/Test/Rewriting/RewritingOptions.cs

@@ -22,20 +22,20 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// The directory containing the assemblies to rewrite.
         /// </summary>
-        public string AssembliesDirectory { get; internal set; }
+        public string AssembliesDirectory { get; set; }
 
         /// <summary>
         /// The output directory where rewritten assemblies are placed.
         /// If this is the same as the <see cref="AssembliesDirectory"/> then
         /// the rewritten assemblies will replace the original assemblies.
         /// </summary>
-        public string OutputDirectory { get; internal set; }
+        public string OutputDirectory { get; set; }
 
         /// <summary>
         /// The file names of the assemblies to rewrite.  If this list is empty then it will
         /// rewrite all assemblies in the <see cref="AssembliesDirectory"/>.
         /// </summary>
-        public HashSet<string> AssemblyPaths { get; internal set; }
+        public HashSet<string> AssemblyPaths { get; set; }
 
         /// <summary>
         /// The regular expressions used to match against assembly names to determine which assemblies
@@ -50,7 +50,7 @@ namespace Microsoft.Coyote.Rewriting
         /// System\.Private\.CoreLib
         /// mscorlib.
         /// </remarks>
-        public IList<string> DisallowedAssemblies { get; internal set; }
+        public IList<string> DisallowedAssemblies { get; set; }
 
         /// <summary>
         /// True if the input assemblies are being replaced by the rewritten ones.
@@ -65,12 +65,22 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Path of strong name key to use for signing rewritten assemblies.
         /// </summary>
-        public string StrongNameKeyFile { get; internal set; }
+        public string StrongNameKeyFile { get; set; }
 
         /// <summary>
         /// Whether to also rewrite dependent assemblies that are found in the same location.
         /// </summary>
-        public bool IsRewritingDependencies { get; internal set; }
+        public bool IsRewritingDependencies { get; set; }
+
+        /// <summary>
+        /// Log output from rewriter (default is Console output).
+        /// </summary>
+        public ILogger Log { get; set; }
+
+        /// <summary>
+        /// The amount of log output to produce.
+        /// </summary>
+        public LogSeverity LogLevel { get; set; }
 
         /// <summary>
         /// True if rewriting of unit test methods is enabled, else false.
@@ -107,13 +117,6 @@ namespace Microsoft.Coyote.Rewriting
             }
         }
 
-        /// <summary>
-        /// Initializes a new instance of the <see cref="RewritingOptions"/> class.
-        /// </summary>
-        internal RewritingOptions()
-        {
-        }
-
         /// <summary>
         /// Parses the <see cref="RewritingOptions"/> from the specified JSON configuration file.
         /// </summary>

Source/Test/Rewriting/Transforms/AssemblyTransform.cs

@@ -20,12 +20,12 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Console output writer.
         /// </summary>
-        protected readonly ConsoleLogger Log;
+        protected readonly ILogger Log;
 
         /// <summary>
         /// Initializes a new instance of the <see cref="AssemblyTransform"/> class.
         /// </summary>
-        protected AssemblyTransform(ConsoleLogger log)
+        protected AssemblyTransform(ILogger log)
         {
             this.Log = log;
         }
@@ -382,7 +382,7 @@ namespace Microsoft.Coyote.Rewriting
             resolved = method.Resolve();
             if (resolved is null)
             {
-                this.Log.WriteWarningLine($"Unable to resolve '{method.FullName}' method. The method is either unsupported by Coyote, " +
+                this.Log.WriteLine(LogSeverity.Warning, $"Unable to resolve '{method.FullName}' method. The method is either unsupported by Coyote, " +
                     "or a user-defined extension method, or the .NET platform of Coyote and the target assembly do not match.");
                 return false;
             }

Source/Test/Rewriting/Transforms/ExceptionFilterTransform.cs

@@ -32,7 +32,7 @@ namespace Microsoft.Coyote.Rewriting
         /// </summary>
         private bool ModifiedHandlers;
 
-        internal ExceptionFilterTransform(ConsoleLogger log)
+        internal ExceptionFilterTransform(ILogger log)
 
             : base(log)
         {

Source/Test/Rewriting/Transforms/MSTestTransform.cs

@@ -27,7 +27,7 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="MSTestTransform"/> class.
         /// </summary>
-        internal MSTestTransform(Configuration configuration, ConsoleLogger log)
+        internal MSTestTransform(Configuration configuration, ILogger log)
             : base(log)
         {
             this.Configuration = configuration;

Source/Test/Rewriting/Transforms/MonitorTransform.cs

@@ -38,7 +38,7 @@ namespace Microsoft.Coyote.Rewriting
 
         private const string MonitorClassName = "System.Threading.Monitor";
 
-        internal MonitorTransform(ConsoleLogger log)
+        internal MonitorTransform(ILogger log)
             : base(log)
         {
         }

Source/Test/Rewriting/Transforms/TaskTransform.cs

@@ -44,7 +44,7 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="TaskTransform"/> class.
         /// </summary>
-        internal TaskTransform(ConsoleLogger log)
+        internal TaskTransform(ILogger log)
             : base(log)
         {
             this.RewrittenMethodCache = new Dictionary<string, MethodReference>();

Source/Test/Rewriting/Transforms/ThreadTransform.cs

@@ -38,7 +38,7 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="ThreadTransform"/> class.
         /// </summary>
-        internal ThreadTransform(ConsoleLogger log)
+        internal ThreadTransform(ILogger log)
             : base(log)
         {
         }

Source/Test/SystematicTesting/TestingEngine.cs

@@ -64,23 +64,18 @@ namespace Microsoft.Coyote.SystematicTesting
         /// </summary>
         private readonly IRandomValueGenerator RandomValueGenerator;
 
-        /// <summary>
-        /// The error reporter.
-        /// </summary>
-        private readonly ErrorReporter ErrorReporter;
-
         /// <summary>
         /// The installed logger.
         /// </summary>
         /// <remarks>
         /// See <see href="/coyote/learn/core/logging" >Logging</see> for more information.
         /// </remarks>
-        private TextWriter Logger;
+        private ILogger Log;
 
         /// <summary>
         /// The default logger that is used during testing.
         /// </summary>
-        private readonly TextWriter DefaultLogger;
+        private readonly ILogger DefaultLogger;
 
         /// <summary>
         /// The profiler.
@@ -230,9 +225,8 @@ namespace Microsoft.Coyote.SystematicTesting
             this.Configuration = configuration;
             this.TestMethodInfo = testMethodInfo;
 
-            this.DefaultLogger = new ConsoleLogger();
+            this.DefaultLogger = new ConsoleLogger() { LogLevel = configuration.LogLevel };
             this.Logger = this.DefaultLogger;
-            this.ErrorReporter = new ErrorReporter(configuration, this.Logger);
             this.Profiler = new Profiler();
 
             this.PerIterationCallbacks = new HashSet<Action<uint>>();
@@ -354,7 +348,7 @@ namespace Microsoft.Coyote.SystematicTesting
             {
                 if (this.CancellationTokenSource.IsCancellationRequested)
                 {
-                    this.Logger.WriteLine($"... Task {this.Configuration.TestingProcessId} timed out.");
+                    this.Logger.WriteLine(LogSeverity.Warning, $"... Task {this.Configuration.TestingProcessId} timed out.");
                 }
             }
             catch (AggregateException aex)
@@ -390,7 +384,7 @@ namespace Microsoft.Coyote.SystematicTesting
             }
             catch (Exception ex)
             {
-                this.Logger.WriteLine($"... Task {this.Configuration.TestingProcessId} failed due to an internal error: {ex}");
+                this.Logger.WriteLine(LogSeverity.Error, $"... Task {this.Configuration.TestingProcessId} failed due to an internal error: {ex}");
                 this.TestReport.InternalErrors.Add(ex.ToString());
             }
             finally
@@ -423,12 +417,12 @@ namespace Microsoft.Coyote.SystematicTesting
                 options = $" (seed:{this.RandomValueGenerator.Seed})";
             }
 
-            this.Logger.WriteLine($"... Task {this.Configuration.TestingProcessId} is " +
+            this.Logger.WriteLine(LogSeverity.Important, $"... Task {this.Configuration.TestingProcessId} is " +
                 $"using '{this.Configuration.SchedulingStrategy}' strategy{options}.");
 
             if (this.Configuration.EnableTelemetry)
             {
-                this.Logger.WriteLine($"... Telemetry is enabled, see {LearnAboutTelemetryUrl}.");
+                this.Logger.WriteLine(LogSeverity.Important, $"... Telemetry is enabled, see {LearnAboutTelemetryUrl}.");
             }
 
             return new Task(() =>
@@ -512,7 +506,7 @@ namespace Microsoft.Coyote.SystematicTesting
 
             if (!this.IsReplayModeEnabled && this.ShouldPrintIteration(iteration + 1))
             {
-                this.Logger.WriteLine($"..... Iteration #{iteration + 1}");
+                this.Logger.WriteLine(LogSeverity.Important, $"..... Iteration #{iteration + 1}");
 
                 // Flush when logging to console.
                 if (this.Logger is ConsoleLogger)
@@ -547,7 +541,7 @@ namespace Microsoft.Coyote.SystematicTesting
                         runtimeLogger.UserLogger = this.Logger;
                     }
 
-                    runtime.SetLogger(runtimeLogger);
+                    runtime.Logger = runtimeLogger;
 
                     var writer = TextWriter.Null;
                     Console.SetOut(writer);
@@ -555,7 +549,7 @@ namespace Microsoft.Coyote.SystematicTesting
                 }
                 else if (this.Logger != this.DefaultLogger)
                 {
-                    runtime.SetLogger(this.Logger);
+                    runtime.Logger = this.Logger;
                 }
 
                 this.InitializeCustomLogging(runtime);
@@ -582,7 +576,7 @@ namespace Microsoft.Coyote.SystematicTesting
 
                 if (runtime.Scheduler.BugFound)
                 {
-                    this.ErrorReporter.WriteErrorLine(runtime.Scheduler.BugReport);
+                    this.Logger.WriteLine(LogSeverity.Error, runtime.Scheduler.BugReport);
                 }
 
                 runtime.LogWriter.LogCompletion();
@@ -617,7 +611,7 @@ namespace Microsoft.Coyote.SystematicTesting
 
                 if (!this.IsReplayModeEnabled && this.Configuration.PerformFullExploration && runtime.Scheduler.BugFound)
                 {
-                    this.Logger.WriteLine($"..... Iteration #{iteration + 1} " +
+                    this.Logger.WriteLine(LogSeverity.Important, $"..... Iteration #{iteration + 1} " +
                         $"triggered bug #{this.TestReport.NumOfFoundBugs} " +
                         $"[task-{this.Configuration.TestingProcessId}]");
                 }
@@ -699,7 +693,7 @@ namespace Microsoft.Coyote.SystematicTesting
                 if (!string.IsNullOrEmpty(this.ReadableTrace))
                 {
                     string readableTracePath = Path.Combine(directory, file + "_" + index + ".txt");
-                    this.Logger.WriteLine($"..... Writing {readableTracePath}");
+                    this.Logger.WriteLine(LogSeverity.Important, $"..... Writing {readableTracePath}");
                     File.WriteAllText(readableTracePath, this.ReadableTrace);
                     yield return readableTracePath;
                 }
@@ -708,7 +702,7 @@ namespace Microsoft.Coyote.SystematicTesting
             if (this.Configuration.IsXmlLogEnabled)
             {
                 string xmlPath = Path.Combine(directory, file + "_" + index + ".trace.xml");
-                this.Logger.WriteLine($"..... Writing {xmlPath}");
+                this.Logger.WriteLine(LogSeverity.Important, $"..... Writing {xmlPath}");
                 File.WriteAllText(xmlPath, this.XmlLog.ToString());
                 yield return xmlPath;
             }
@@ -717,7 +711,7 @@ namespace Microsoft.Coyote.SystematicTesting
             {
                 string graphPath = Path.Combine(directory, file + "_" + index + ".dgml");
                 this.Graph.SaveDgml(graphPath, true);
-                this.Logger.WriteLine($"..... Writing {graphPath}");
+                this.Logger.WriteLine(LogSeverity.Important, $"..... Writing {graphPath}");
                 yield return graphPath;
             }
 
@@ -727,13 +721,13 @@ namespace Microsoft.Coyote.SystematicTesting
                 if (!string.IsNullOrEmpty(this.ReproducableTrace))
                 {
                     string reproTracePath = Path.Combine(directory, file + "_" + index + ".schedule");
-                    this.Logger.WriteLine($"..... Writing {reproTracePath}");
+                    this.Logger.WriteLine(LogSeverity.Important, $"..... Writing {reproTracePath}");
                     File.WriteAllText(reproTracePath, this.ReproducableTrace);
                     yield return reproTracePath;
                 }
             }
 
-            this.Logger.WriteLine($"... Elapsed {this.Profiler.Results()} sec.");
+            this.Logger.WriteLine(LogSeverity.Important, $"... Elapsed {this.Profiler.Results()} sec.");
         }
 
         /// <summary>
@@ -815,7 +809,7 @@ namespace Microsoft.Coyote.SystematicTesting
             }
             catch (Exception ex)
             {
-                this.Logger.WriteLine(ex.Message);
+                this.Logger.WriteLine(LogSeverity.Error, ex.Message);
             }
 
             return null;
@@ -1011,29 +1005,60 @@ namespace Microsoft.Coyote.SystematicTesting
         public bool IsTestRewritten() => AssemblyRewriter.IsAssemblyRewritten(this.TestMethodInfo.Assembly);
 
         /// <summary>
-        /// Installs the specified <see cref="TextWriter"/>.
+        /// Get or set the <see cref="ILogger"/> used to log messages during testing.
         /// </summary>
-        /// <param name="logger">The logger to install.</param>
-        /// <returns>The previously installed logger.</returns>
-        public TextWriter SetLogger(TextWriter logger)
+        /// <remarks>
+        /// See <see href="/coyote/learn/core/logging" >Logging</see> for more information.
+        /// </remarks>
+        public ILogger Logger
         {
-            TextWriter oldLoger = null;
-            if (this.Logger != this.DefaultLogger)
+            get
             {
-                oldLoger = this.Logger;
+                return this.Log;
             }
 
-            if (logger is null)
+            set
             {
-                this.Logger = TextWriter.Null;
+                var old = this.Log;
+                if (value is null)
+                {
+                    this.Log = new NullLogger();
+                }
+                else
+                {
+                    this.Log = value;
+                }
+
+                using var v = old;
             }
-            else
+        }
+
+        /// <summary>
+        /// Teh old way of installing a TextWriter for logging.
+        /// </summary>
+        /// <remarks>
+        /// This writer will be wrapped in an object that implements the <see cref="ILogger"/> interface which
+        /// will have a minor performance overhead, so it is better to set the <see cref="Logger"/> property instead.
+        /// </remarks>
+        /// <param name="writer">The writer to use for logging.</param>
+        /// <returns>The previously installed logger.</returns>
+        [Obsolete("Use the new ILogger version of SetLogger")]
+        public TextWriter SetLogger(TextWriter writer)
+        {
+            ILogger oldLogger = this.Logger;
+            if (oldLogger == this.DefaultLogger)
             {
-                this.Logger = logger;
+                oldLogger = null;
             }
 
-            this.ErrorReporter.Logger = logger;
-            return oldLoger;
+            this.Logger = new TextWriterLogger(writer);
+
+            if (oldLogger != null)
+            {
+                return oldLogger.TextWriter;
+            }
+
+            return null;
         }
     }
 }

Tests/Production.Tests/Actors/EventQueues/MockActorManager.cs

@@ -6,6 +6,7 @@ using System.Collections.Generic;
 using System.IO;
 using System.Linq;
 using Microsoft.Coyote.Actors;
+using Microsoft.Coyote.IO;
 
 namespace Microsoft.Coyote.Production.Tests.Actors
 {
@@ -21,7 +22,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
             DropEvent
         }
 
-        private readonly TextWriter Logger;
+        private readonly ILogger Logger;
         private readonly Action<Notification, Event, EventInfo> Notify;
         private readonly Type[] IgnoredEvents;
         private readonly Type[] DeferredEvents;
@@ -31,7 +32,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
 
         public EventGroup CurrentEventGroup { get; set; }
 
-        internal MockActorManager(TextWriter logger, Action<Notification, Event, EventInfo> notify,
+        internal MockActorManager(ILogger logger, Action<Notification, Event, EventInfo> notify,
             Type[] ignoredEvents = null, Type[] deferredEvents = null, bool isDefaultHandlerInstalled = false)
         {
             this.Logger = logger;

Tests/Production.Tests/Actors/Logging/CustomActorRuntimeLogTests.cs

@@ -4,6 +4,7 @@
 using System.IO;
 using Microsoft.Coyote.Actors;
 using Microsoft.Coyote.Coverage;
+using Microsoft.Coyote.IO;
 using Microsoft.Coyote.Specifications;
 using Microsoft.Coyote.Tasks;
 using Microsoft.Coyote.Tests.Common;
@@ -134,7 +135,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
             {
                 using (CustomLogger logger = new CustomLogger())
                 {
-                    runtime.SetLogger(logger);
+                    runtime.Logger = logger;
                     var tcs = TaskCompletionSource.Create<bool>();
                     runtime.RegisterMonitor<TestMonitor>();
                     runtime.Monitor<TestMonitor>(new SetupEvent(tcs));
@@ -182,7 +183,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
             {
                 using (CustomLogger logger = new CustomLogger())
                 {
-                    runtime.SetLogger(logger);
+                    runtime.Logger = logger;
                     var tcs = TaskCompletionSource.Create<bool>();
                     runtime.RegisterMonitor<TestMonitor>();
                     runtime.Monitor<TestMonitor>(new SetupEvent(tcs));
@@ -232,13 +233,13 @@ namespace Microsoft.Coyote.Production.Tests.Actors
             Configuration config = Configuration.Create();
             this.Test(async runtime =>
             {
-                runtime.SetLogger(TextWriter.Null);
+                runtime.Logger = new NullLogger();
                 var tcs = TaskCompletionSource.Create<bool>();
                 runtime.RegisterMonitor<TestMonitor>();
                 runtime.Monitor<TestMonitor>(new SetupEvent(tcs));
                 runtime.CreateActor(typeof(M));
                 await this.WaitAsync(tcs.Task);
-                Assert.Equal("System.IO.TextWriter+NullTextWriter", runtime.Logger.ToString());
+                Assert.Equal("Microsoft.Coyote.IO.NullLogger", runtime.Logger.ToString());
             }, config);
         }
 
@@ -251,10 +252,10 @@ namespace Microsoft.Coyote.Production.Tests.Actors
                 var tcs = TaskCompletionSource.Create<bool>();
                 runtime.RegisterMonitor<TestMonitor>();
                 runtime.Monitor<TestMonitor>(new SetupEvent(tcs));
-                runtime.SetLogger(null);
+                runtime.Logger = null;
                 runtime.CreateActor(typeof(M));
                 await this.WaitAsync(tcs.Task);
-                Assert.Equal("System.IO.TextWriter+NullTextWriter", runtime.Logger.ToString());
+                Assert.Equal("Microsoft.Coyote.IO.NullLogger", runtime.Logger.ToString());
             }, config);
         }
 
@@ -268,7 +269,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
                 runtime.RegisterMonitor<TestMonitor>();
                 runtime.Monitor<TestMonitor>(new SetupEvent(tcs));
                 runtime.RegisterMonitor<S>();
-                runtime.SetLogger(null);
+                runtime.Logger = null;
 
                 var logger = new CustomActorRuntimeLog();
                 runtime.RegisterLog(logger);
@@ -383,7 +384,7 @@ StateTransition";
             {
                 using (CustomLogger logger = new CustomLogger())
                 {
-                    runtime.SetLogger(logger);
+                    runtime.Logger = logger;
 
                     var graphBuilder = new ActorRuntimeLogGraphBuilder(false);
 
@@ -419,7 +420,7 @@ StateTransition";
             {
                 using (CustomLogger logger = new CustomLogger())
                 {
-                    runtime.SetLogger(logger);
+                    runtime.Logger = logger;
 
                     var graphBuilder = new ActorRuntimeLogGraphBuilder(false)
                     {

Tests/Production.Tests/Actors/Timers/TimerTests.cs

@@ -4,6 +4,7 @@
 using System;
 using Microsoft.Coyote.Actors;
 using Microsoft.Coyote.Actors.Timers;
+using Microsoft.Coyote.IO;
 using Microsoft.Coyote.Tasks;
 using Xunit;
 using Xunit.Abstractions;
@@ -227,7 +228,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
                 }
                 catch (AssertionFailureException ex)
                 {
-                    this.Logger.WriteLine(ex.Message);
+                    this.Logger.WriteLine(LogSeverity.Error, ex.Message);
                     tcs.SetResult(true);
                     this.RaiseHaltEvent();
                     return;
@@ -268,7 +269,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
                 }
                 catch (AssertionFailureException ex)
                 {
-                    this.Logger.WriteLine(ex.Message);
+                    this.Logger.WriteLine(LogSeverity.Error, ex.Message);
                     tcs.SetResult(true);
                     this.RaiseHaltEvent();
                     return;
@@ -341,7 +342,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
                 }
                 catch (AssertionFailureException ex)
                 {
-                    this.Logger.WriteLine(ex.Message);
+                    this.Logger.WriteLine(LogSeverity.Error, ex.Message);
                     ce.Tcs.SetResult(expectError == true);
                     this.RaiseHaltEvent();
                 }
@@ -355,7 +356,7 @@ namespace Microsoft.Coyote.Production.Tests.Actors
                 }
                 else
                 {
-                    this.Logger.WriteLine("Unexpected event type {0}", e.GetType().FullName);
+                    this.Logger.WriteLine(LogSeverity.Error, "Unexpected event type {0}", e.GetType().FullName);
                     this.Config.Tcs.SetResult(false);
                 }
 

Tests/Production.Tests/Tasks/Logging/CustomTaskLogTests.cs

@@ -25,7 +25,7 @@ namespace Microsoft.Coyote.Production.Tests.Tasks
             Configuration config = Configuration.Create().WithVerbosityEnabled();
 
             ICoyoteRuntime runtime = RuntimeFactory.Create(config);
-            runtime.SetLogger(logger);
+            runtime.Logger = logger;
 
             Generator generator = Generator.Create();
 

Tests/SystematicTesting.Tests/Tasks/Logging/CustomTaskLogTests.cs

@@ -8,6 +8,7 @@ using System.Threading.Tasks;
 #else
 using Microsoft.Coyote.Tasks;
 #endif
+using Microsoft.Coyote.IO;
 using Microsoft.Coyote.Runtime;
 using Microsoft.Coyote.Specifications;
 using Microsoft.Coyote.SystematicTesting;
@@ -31,7 +32,7 @@ namespace Microsoft.Coyote.Production.Tests.Tasks
         [Fact(Timeout = 5000)]
         public void TestCustomLogger()
         {
-            StringWriter log = new StringWriter();
+            InMemoryLogger log = new InMemoryLogger();
 
             var config = Configuration.Create().WithVerbosityEnabled().WithTestingIterations(3);
             TestingEngine engine = TestingEngine.Create(config, (ICoyoteRuntime runtime) =>
@@ -39,7 +40,7 @@ namespace Microsoft.Coyote.Production.Tests.Tasks
                 runtime.Logger.WriteLine("Hi mom!");
             });
 
-            engine.SetLogger(log);
+            engine.Logger = log;
             engine.Run();
 
             var result = log.ToString();

Tests/Tests.Common/BaseTest.cs

@@ -9,6 +9,7 @@ using System.Text;
 using System.Threading.Tasks;
 using Microsoft.Coyote.Actors;
 using Microsoft.Coyote.Coverage;
+using Microsoft.Coyote.IO;
 using Microsoft.Coyote.SystematicTesting;
 using Microsoft.Coyote.SystematicTesting.Strategies;
 using Xunit;
@@ -97,16 +98,7 @@ namespace Microsoft.Coyote.Tests.Common
         private TestingEngine InternalTest(Delegate test, Configuration configuration)
         {
             configuration = configuration ?? GetConfiguration();
-
-            TextWriter logger;
-            if (configuration.IsVerbose)
-            {
-                logger = new TestOutputLogger(this.TestOutput, true);
-            }
-            else
-            {
-                logger = TextWriter.Null;
-            }
+            ILogger logger = this.GetLogger(configuration);
 
             TestingEngine engine = null;
 
@@ -287,16 +279,7 @@ namespace Microsoft.Coyote.Tests.Common
         private void TestWithErrors(Delegate test, Configuration configuration, TestErrorChecker errorChecker, bool replay)
         {
             configuration = configuration ?? GetConfiguration();
-
-            TextWriter logger;
-            if (configuration.IsVerbose)
-            {
-                logger = new TestOutputLogger(this.TestOutput, true);
-            }
-            else
-            {
-                logger = TextWriter.Null;
-            }
+            ILogger logger = this.GetLogger(configuration);
 
             try
             {
@@ -387,15 +370,7 @@ namespace Microsoft.Coyote.Tests.Common
             Assert.True(exceptionType.IsSubclassOf(typeof(Exception)), "Please configure the test correctly. " +
                 $"Type '{exceptionType}' is not an exception type.");
 
-            TextWriter logger;
-            if (configuration.IsVerbose)
-            {
-                logger = new TestOutputLogger(this.TestOutput, true);
-            }
-            else
-            {
-                logger = TextWriter.Null;
-            }
+            ILogger logger = this.GetLogger(configuration);
 
             try
             {
@@ -429,21 +404,13 @@ namespace Microsoft.Coyote.Tests.Common
         {
             configuration = configuration ?? GetConfiguration();
 
-            TextWriter logger;
-            if (configuration.IsVerbose)
-            {
-                logger = new TestOutputLogger(this.TestOutput, true);
-            }
-            else
-            {
-                logger = TextWriter.Null;
-            }
+            ILogger logger = this.GetLogger(configuration);
 
             try
             {
                 configuration.IsMonitoringEnabledInInProduction = true;
                 var runtime = RuntimeFactory.Create(configuration);
-                runtime.SetLogger(logger);
+                runtime.Logger = logger;
                 for (int i = 0; i < configuration.TestingIterations; i++)
                 {
                     test(runtime);
@@ -466,21 +433,13 @@ namespace Microsoft.Coyote.Tests.Common
             uint iterations = Math.Max(1, configuration.TestingIterations);
             for (int i = 0; i < iterations; i++)
             {
-                TextWriter logger;
-                if (configuration.IsVerbose)
-                {
-                    logger = new TestOutputLogger(this.TestOutput, true);
-                }
-                else
-                {
-                    logger = TextWriter.Null;
-                }
+                ILogger logger = this.GetLogger(configuration);
 
                 try
                 {
                     configuration.IsMonitoringEnabledInInProduction = true;
                     var runtime = RuntimeFactory.Create(configuration);
-                    runtime.SetLogger(logger);
+                    runtime.Logger = logger;
 
                     var errorTask = new TaskCompletionSource<Exception>();
                     if (handleFailures)
@@ -553,15 +512,7 @@ namespace Microsoft.Coyote.Tests.Common
             configuration = configuration ?? GetConfiguration();
 
             string errorMessage = string.Empty;
-            TextWriter logger;
-            if (configuration.IsVerbose)
-            {
-                logger = new TestOutputLogger(this.TestOutput, true);
-            }
-            else
-            {
-                logger = TextWriter.Null;
-            }
+            ILogger logger = this.GetLogger(configuration);
 
             try
             {
@@ -573,7 +524,7 @@ namespace Microsoft.Coyote.Tests.Common
                     errorTask.TrySetResult(e);
                 };
 
-                runtime.SetLogger(logger);
+                runtime.Logger = logger;
                 for (int i = 0; i < configuration.TestingIterations; i++)
                 {
                     test(runtime);
@@ -606,15 +557,7 @@ namespace Microsoft.Coyote.Tests.Common
             configuration = configuration ?? GetConfiguration();
 
             string errorMessage = string.Empty;
-            TextWriter logger;
-            if (configuration.IsVerbose)
-            {
-                logger = new TestOutputLogger(this.TestOutput, true);
-            }
-            else
-            {
-                logger = TextWriter.Null;
-            }
+            ILogger logger = this.GetLogger(configuration);
 
             try
             {
@@ -626,7 +569,7 @@ namespace Microsoft.Coyote.Tests.Common
                     errorCompletion.TrySetResult(e);
                 };
 
-                runtime.SetLogger(logger);
+                runtime.Logger = logger;
                 for (int i = 0; i < configuration.TestingIterations; i++)
                 {
                     await test(runtime);
@@ -663,15 +606,7 @@ namespace Microsoft.Coyote.Tests.Common
             Assert.True(exceptionType.IsSubclassOf(typeof(Exception)), "Please configure the test correctly. " +
                 $"Type '{exceptionType}' is not an exception type.");
 
-            TextWriter logger;
-            if (configuration.IsVerbose)
-            {
-                logger = new TestOutputLogger(this.TestOutput, true);
-            }
-            else
-            {
-                logger = TextWriter.Null;
-            }
+            ILogger logger = this.GetLogger(configuration);
 
             try
             {
@@ -682,7 +617,7 @@ namespace Microsoft.Coyote.Tests.Common
                 {
                     errorCompletion.TrySetResult(e);
                 };
-                runtime.SetLogger(logger);
+                runtime.Logger = logger;
                 for (int i = 0; i < configuration.TestingIterations; i++)
                 {
                     test(runtime);
@@ -719,15 +654,7 @@ namespace Microsoft.Coyote.Tests.Common
             Assert.True(exceptionType.IsSubclassOf(typeof(Exception)), "Please configure the test correctly. " +
                 $"Type '{exceptionType}' is not an exception type.");
 
-            TextWriter logger;
-            if (configuration.IsVerbose)
-            {
-                logger = new TestOutputLogger(this.TestOutput, true);
-            }
-            else
-            {
-                logger = TextWriter.Null;
-            }
+            ILogger logger = this.GetLogger(configuration);
 
             try
             {
@@ -738,7 +665,7 @@ namespace Microsoft.Coyote.Tests.Common
                 {
                     errorCompletion.TrySetResult(e);
                 };
-                runtime.SetLogger(logger);
+                runtime.Logger = logger;
                 for (int i = 0; i < configuration.TestingIterations; i++)
                 {
                     test();
@@ -775,15 +702,7 @@ namespace Microsoft.Coyote.Tests.Common
             Assert.True(exceptionType.IsSubclassOf(typeof(Exception)), "Please configure the test correctly. " +
                 $"Type '{exceptionType}' is not an exception type.");
 
-            TextWriter logger;
-            if (configuration.IsVerbose)
-            {
-                logger = new TestOutputLogger(this.TestOutput, true);
-            }
-            else
-            {
-                logger = TextWriter.Null;
-            }
+            ILogger logger = this.GetLogger(configuration);
 
             try
             {
@@ -795,7 +714,7 @@ namespace Microsoft.Coyote.Tests.Common
                     errorCompletion.TrySetResult(e);
                 };
 
-                runtime.SetLogger(logger);
+                runtime.Logger = logger;
                 for (int i = 0; i < configuration.TestingIterations; i++)
                 {
                     await test(runtime);
@@ -833,15 +752,7 @@ namespace Microsoft.Coyote.Tests.Common
             Assert.True(exceptionType.IsSubclassOf(typeof(Exception)), "Please configure the test correctly. " +
                 $"Type '{exceptionType}' is not an exception type.");
 
-            TextWriter logger;
-            if (configuration.IsVerbose)
-            {
-                logger = new TestOutputLogger(this.TestOutput, true);
-            }
-            else
-            {
-                logger = TextWriter.Null;
-            }
+            ILogger logger = this.GetLogger(configuration);
 
             try
             {
@@ -853,7 +764,7 @@ namespace Microsoft.Coyote.Tests.Common
                     errorCompletion.TrySetResult(e);
                 };
 
-                runtime.SetLogger(logger);
+                runtime.Logger = logger;
                 for (int i = 0; i < configuration.TestingIterations; i++)
                 {
                     await test();
@@ -882,6 +793,21 @@ namespace Microsoft.Coyote.Tests.Common
             Assert.True(actualException.GetType() == exceptionType, actualException.Message + "\n" + actualException.StackTrace);
         }
 
+        private ILogger GetLogger(Configuration configuration)
+        {
+            ILogger logger;
+            if (configuration.IsVerbose)
+            {
+                logger = new TestOutputLogger(this.TestOutput, true);
+            }
+            else
+            {
+                logger = new NullLogger();
+            }
+
+            return logger;
+        }
+
         private static int GetExceptionTimeout(int millisecondsDelay = 5000)
         {
             if (Debugger.IsAttached)
@@ -946,10 +872,10 @@ namespace Microsoft.Coyote.Tests.Common
             return await task;
         }
 
-        private static TestingEngine RunTest(Delegate test, Configuration configuration, TextWriter logger)
+        private static TestingEngine RunTest(Delegate test, Configuration configuration, ILogger logger)
         {
             var engine = new TestingEngine(configuration, test);
-            engine.SetLogger(logger);
+            engine.Logger = logger;
             engine.Run();
             return engine;
         }

Tests/Tests.Common/Logging/CustomLogger.cs

@@ -3,10 +3,11 @@
 
 using System.IO;
 using System.Text;
+using Microsoft.Coyote.IO;
 
 namespace Microsoft.Coyote.Tests.Common
 {
-    public class CustomLogger : TextWriter
+    public class CustomLogger : TextWriter, ILogger
     {
         private StringBuilder StringBuilder;
 
@@ -15,28 +16,13 @@ namespace Microsoft.Coyote.Tests.Common
             this.StringBuilder = new StringBuilder();
         }
 
-        /// <summary>
-        /// When overridden in a derived class, returns the character encoding in which the
-        /// output is written.
-        /// </summary>
+        /// <inheritdoc/>
+        public TextWriter TextWriter => this;
+
+        /// <inheritdoc/>
         public override Encoding Encoding => Encoding.Unicode;
 
-        public override void Write(string value)
-        {
-            if (this.StringBuilder != null)
-            {
-                this.StringBuilder.Append(value);
-            }
-        }
-
-        public override void WriteLine(string value)
-        {
-            if (this.StringBuilder != null)
-            {
-                this.StringBuilder.AppendLine(value);
-            }
-        }
-
+        /// <inheritdoc/>
         public override string ToString()
         {
             if (this.StringBuilder != null)
@@ -47,6 +33,67 @@ namespace Microsoft.Coyote.Tests.Common
             return string.Empty;
         }
 
+        /// <inheritdoc/>
+        public override void Write(string value)
+        {
+            this.Write(LogSeverity.Informational, value);
+        }
+
+        /// <inheritdoc/>
+        public override void Write(string format, params object[] args)
+        {
+            this.Write(LogSeverity.Informational, string.Format(format, args));
+        }
+
+        /// <inheritdoc/>
+        public void Write(LogSeverity severity, string value)
+        {
+            if (this.StringBuilder != null)
+            {
+                this.StringBuilder.Append(value);
+            }
+        }
+
+        /// <inheritdoc/>
+        public void Write(LogSeverity severity, string format, params object[] args)
+        {
+            if (this.StringBuilder != null)
+            {
+                this.StringBuilder.Append(string.Format(format, args));
+            }
+        }
+
+        /// <inheritdoc/>
+        public override void WriteLine(string value)
+        {
+            this.WriteLine(LogSeverity.Informational, value);
+        }
+
+        /// <inheritdoc/>
+        public override void WriteLine(string format, params object[] args)
+        {
+            this.WriteLine(LogSeverity.Informational, string.Format(format, args));
+        }
+
+        /// <inheritdoc/>
+        public void WriteLine(LogSeverity severity, string value)
+        {
+            if (this.StringBuilder != null)
+            {
+                this.StringBuilder.AppendLine(value);
+            }
+        }
+
+        /// <inheritdoc/>
+        public void WriteLine(LogSeverity severity, string format, params object[] args)
+        {
+            if (this.StringBuilder != null)
+            {
+                this.StringBuilder.AppendLine(string.Format(format, args));
+            }
+        }
+
+        /// <inheritdoc/>
         protected override void Dispose(bool disposing)
         {
             if (disposing)
@@ -54,8 +101,6 @@ namespace Microsoft.Coyote.Tests.Common
                 this.StringBuilder.Clear();
                 this.StringBuilder = null;
             }
-
-            base.Dispose(disposing);
         }
     }
 }

Tests/Tests.Common/TestConsoleLogger.cs

@@ -1,157 +0,0 @@
-// Copyright (c) Microsoft Corporation.
-// Licensed under the MIT License.
-
-using System;
-using System.IO;
-using System.Text;
-using Xunit.Abstractions;
-
-namespace Microsoft.Coyote.Tests.Common
-{
-    /// <summary>
-    /// Logger that writes to the console.
-    /// </summary>
-    public sealed class TestConsoleLogger : TextWriter, ITestOutputHelper
-    {
-        /// <summary>
-        /// If true, then messages are logged. The default value is false.
-        /// </summary>
-        public bool IsVerbose { get; set; } = false;
-
-        /// <summary>
-        /// Initializes a new instance of the <see cref="TestConsoleLogger"/> class.
-        /// </summary>
-        /// <param name="isVerbose">If true, then messages are logged.</param>
-        public TestConsoleLogger(bool isVerbose)
-        {
-            this.IsVerbose = isVerbose;
-        }
-
-        /// <summary>
-        /// When overridden in a derived class, returns the character encoding in which the
-        /// output is written.
-        /// </summary>
-        public override Encoding Encoding => Console.OutputEncoding;
-
-        /// <summary>
-        /// Writes the specified string value.
-        /// </summary>
-        /// <param name="value">Text.</param>
-        public override void Write(string value)
-        {
-            if (this.IsVerbose)
-            {
-                Console.Write(value);
-            }
-        }
-
-        /// <summary>
-        /// Writes the text representation of the specified argument.
-        /// </summary>
-        public override void Write(string format, object arg0)
-        {
-            if (this.IsVerbose)
-            {
-                Console.Write(format, arg0?.ToString());
-            }
-        }
-
-        /// <summary>
-        /// Writes the text representation of the specified arguments.
-        /// </summary>
-        public override void Write(string format, object arg0, object arg1)
-        {
-            if (this.IsVerbose)
-            {
-                Console.Write(format, arg0?.ToString(), arg1?.ToString());
-            }
-        }
-
-        /// <summary>
-        /// Writes the text representation of the specified arguments.
-        /// </summary>
-        public override void Write(string format, object arg0, object arg1, object arg2)
-        {
-            if (this.IsVerbose)
-            {
-                Console.Write(format, arg0?.ToString(), arg1?.ToString(), arg2?.ToString());
-            }
-        }
-
-        /// <summary>
-        /// Writes the text representation of the specified array of objects.
-        /// </summary>
-        /// <param name="format">Text.</param>
-        /// <param name="args">Arguments.</param>
-        public override void Write(string format, params object[] args)
-        {
-            if (this.IsVerbose)
-            {
-                Console.Write(format, args);
-            }
-        }
-
-        /// <summary>
-        /// Writes the specified string value, followed by the
-        /// current line terminator.
-        /// </summary>
-        /// <param name="value">Text.</param>
-        public override void WriteLine(string value)
-        {
-            if (this.IsVerbose)
-            {
-                Console.WriteLine(value);
-            }
-        }
-
-        /// <summary>
-        /// Writes the text representation of the specified argument, followed by the
-        /// current line terminator.
-        /// </summary>
-        public override void WriteLine(string format, object arg0)
-        {
-            if (this.IsVerbose)
-            {
-                Console.WriteLine(format, arg0?.ToString());
-            }
-        }
-
-        /// <summary>
-        /// Writes the text representation of the specified arguments, followed by the
-        /// current line terminator.
-        /// </summary>
-        public override void WriteLine(string format, object arg0, object arg1)
-        {
-            if (this.IsVerbose)
-            {
-                Console.WriteLine(format, arg0?.ToString(), arg1?.ToString());
-            }
-        }
-
-        /// <summary>
-        /// Writes the text representation of the specified arguments, followed by the
-        /// current line terminator.
-        /// </summary>
-        public override void WriteLine(string format, object arg0, object arg1, object arg2)
-        {
-            if (this.IsVerbose)
-            {
-                Console.WriteLine(format, arg0?.ToString(), arg1?.ToString(), arg2?.ToString());
-            }
-        }
-
-        /// <summary>
-        /// Writes the text representation of the specified array of objects,
-        /// followed by the current line terminator.
-        /// </summary>
-        /// <param name="format">Text.</param>
-        /// <param name="args">Arguments.</param>
-        public override void WriteLine(string format, params object[] args)
-        {
-            if (this.IsVerbose)
-            {
-                Console.WriteLine(format, args);
-            }
-        }
-    }
-}

Tests/Tests.Common/TestOutputLogger.cs

@@ -2,7 +2,9 @@
 // Licensed under the MIT License.
 
 using System.IO;
+using System.Runtime.CompilerServices;
 using System.Text;
+using Microsoft.Coyote.IO;
 using Xunit.Abstractions;
 
 namespace Microsoft.Coyote.Tests.Common
@@ -10,22 +12,27 @@ namespace Microsoft.Coyote.Tests.Common
     /// <summary>
     /// Logger that writes to the test output.
     /// </summary>
-    public sealed class TestOutputLogger : TextWriter
+    public sealed class TestOutputLogger : TextWriter, ILogger
     {
         /// <summary>
         /// Underlying test output.
         /// </summary>
         private readonly ITestOutputHelper TestOutput;
 
+        /// <summary>
+        /// Saved current line since ITestOutputHelper provides no "Write" method.
+        /// </summary>
+        private readonly StringBuilder Line = new StringBuilder();
+
         /// <summary>
         /// False means don't write anything.
         /// </summary>
         public bool IsVerbose { get; set; }
 
-        /// <summary>
-        /// When overridden in a derived class, returns the character encoding in which the
-        /// output is written.
-        /// </summary>
+        /// <inheritdoc/>
+        public TextWriter TextWriter => this;
+
+        /// <inheritdoc/>
         public override Encoding Encoding => Encoding.Unicode;
 
         /// <summary>
@@ -39,23 +46,74 @@ namespace Microsoft.Coyote.Tests.Common
             this.IsVerbose = isVerbose;
         }
 
-        /// <summary>
-        /// Writes the specified string value.
-        /// </summary>
+        /// <inheritdoc/>
         public override void Write(string value)
+        {
+            this.Write(LogSeverity.Informational, value);
+        }
+
+        /// <inheritdoc/>
+        public override void Write(string format, params object[] args)
+        {
+            this.Write(LogSeverity.Informational, string.Format(format, args));
+        }
+
+        public void Write(LogSeverity severity, string value)
         {
             if (this.IsVerbose)
             {
+                this.Line.Append(value);
+            }
+        }
+
+        /// <inheritdoc/>
+        public void Write(LogSeverity severity, string format, params object[] args)
+        {
+            this.Write(severity, string.Format(format, args));
+        }
+
+        /// <inheritdoc/>
+        public override void WriteLine(string value)
+        {
+            this.WriteLine(LogSeverity.Informational, value);
+        }
+
+        /// <inheritdoc/>
+        public override void WriteLine(string format, params object[] args)
+        {
+            this.Write(LogSeverity.Informational, string.Format(format, args));
+        }
+
+        /// <inheritdoc/>
+        public void WriteLine(LogSeverity severity, string value)
+        {
+            if (this.IsVerbose)
+            {
+                this.FlushLine();
                 this.TestOutput.WriteLine(value);
             }
         }
 
-        /// <summary>
-        /// Returns the logged text as a string.
-        /// </summary>
-        public override string ToString()
+        /// <inheritdoc/>
+        public void WriteLine(LogSeverity severity, string format, params object[] args)
         {
-            return this.TestOutput.ToString();
+            this.WriteLine(severity, string.Format(format, args));
+        }
+
+        /// <inheritdoc/>
+        protected override void Dispose(bool disposing)
+        {
+            base.Dispose(disposing);
+            this.FlushLine();
+        }
+
+        private void FlushLine()
+        {
+            if (this.Line.Length > 0)
+            {
+                this.TestOutput.WriteLine(this.Line.ToString());
+                this.Line.Length = 0;
+            }
         }
     }
 }

Tools/Coyote/Utilities/CommandLineArgumentParser.cs

@@ -96,6 +96,11 @@ namespace Microsoft.Coyote.Utilities
         /// </summary>
         public object Value;
 
+        /// <summary>
+        /// The default value to use if no value provided.
+        /// </summary>
+        public string DefaultValue;
+
         /// <summary>
         /// This is the print help option.
         /// </summary>
@@ -270,6 +275,7 @@ namespace Microsoft.Coyote.Utilities
                 DataType = this.DataType,
                 Description = this.Description,
                 IsRequired = this.IsRequired,
+                DefaultValue = this.DefaultValue,
                 Group = this.Group,
                 IsHidden = this.IsHidden,
                 AllowedValues = this.AllowedValues,
@@ -344,6 +350,14 @@ namespace Microsoft.Coyote.Utilities
             newList[i] = (T)value2;
             return newList;
         }
+
+        internal void CheckDefaultValue()
+        {
+            if (this.Value == null && !string.IsNullOrEmpty(this.DefaultValue))
+            {
+                this.AddParsedValue(this.DefaultValue);
+            }
+        }
     }
 
     /// <summary>
@@ -415,15 +429,16 @@ namespace Microsoft.Coyote.Utilities
         /// <param name="dataType">Optional datatype (default string). Supported datatypes are primitive types
         /// only (e.g. int, float, string, bool).</param>
         /// <param name="required">Whether the argument is required or not.</param>
+        /// <param name="defaultValue">The default value to use if no value is provided.</param>
         /// <returns>The new <see cref="CommandLineArgument"/> object.</returns>
-        public CommandLineArgument AddArgument(string longName, string shortName, string description = null, Type dataType = null, bool required = false)
+        public CommandLineArgument AddArgument(string longName, string shortName, string description = null, Type dataType = null, bool required = false, string defaultValue = null)
         {
             if (dataType == null)
             {
                 dataType = typeof(string);
             }
 
-            var argument = this.Parser.AddArgument(longName, shortName, description, dataType, required);
+            var argument = this.Parser.AddArgument(longName, shortName, description, dataType, required, defaultValue);
             argument.IsHidden = this.IsHidden;
             argument.Group = this.Name;
             return argument;
@@ -537,8 +552,9 @@ namespace Microsoft.Coyote.Utilities
         /// <param name="dataType">Optional datatype (default string). Supported datatypes are primitive types
         /// only (e.g. int, float, string, bool).</param>
         /// <param name="required">Whether argument is required.</param>
+        /// <param name="defaultValue">The default value to use if no value is provided.</param>
         /// <returns>The new option or throws <see cref="System.Data.DuplicateNameException"/>.</returns>
-        public CommandLineArgument AddArgument(string longName, string shortName, string description = null, Type dataType = null, bool required = false)
+        public CommandLineArgument AddArgument(string longName, string shortName, string description = null, Type dataType = null, bool required = false, string defaultValue = null)
         {
             if (this.Arguments.TryGetValue(longName, out CommandLineArgument argument))
             {
@@ -561,6 +577,7 @@ namespace Microsoft.Coyote.Utilities
                 DataType = dataType,
                 Description = description,
                 IsRequired = required,
+                DefaultValue = defaultValue
             };
             this.Arguments[longName] = argument;
             this.LongNames.Add(longName);
@@ -646,12 +663,14 @@ namespace Microsoft.Coyote.Utilities
                 {
                     if (arg.StartsWith("--"))
                     {
+                        current?.CheckDefaultValue();
                         var name = arg.Substring(2);
                         current = null;
                         this.Arguments.TryGetValue(name, out current);
                     }
                     else if (arg.StartsWith("-"))
                     {
+                        current?.CheckDefaultValue();
                         current = null;
                         var name = arg.Substring(1);
                         // Note that "/" is not supported as an argument delimiter because it conflicts with unix file paths.
@@ -721,6 +740,8 @@ namespace Microsoft.Coyote.Utilities
                 }
             }
 
+            current?.CheckDefaultValue();
+
             foreach (var arg in this.Arguments.Values)
             {
                 if (this.IsRequired(arg) && !(from r in result where r.LongName == arg.LongName select r).Any())
@@ -738,7 +759,7 @@ namespace Microsoft.Coyote.Utilities
 
             foreach (var arg in result)
             {
-                if (!arg.IsPositional && arg.Value == null && arg.DataType != typeof(bool) && !arg.AllowedValues.Contains(string.Empty))
+                if (!arg.IsPositional && arg.Value == null && string.IsNullOrEmpty(arg.DefaultValue) && arg.DataType != typeof(bool) && !arg.AllowedValues.Contains(string.Empty))
                 {
                     throw new CommandLineException(string.Format("Missing value for argument: '--{0}'", arg.LongName), result);
                 }

Tools/Coyote/Utilities/CommandLineOptions.cs

@@ -3,6 +3,7 @@
 
 using System;
 using System.Collections.Generic;
+using System.ComponentModel;
 using System.IO;
 using System.Linq;
 using System.Net;
@@ -34,7 +35,8 @@ namespace Microsoft.Coyote.Utilities
             basicGroup.AddArgument("method", "m", "Suffix of the test method to execute");
             basicGroup.AddArgument("timeout", "t", "Timeout in seconds (disabled by default)", typeof(uint));
             basicGroup.AddArgument("outdir", "o", "Dump output to directory x (absolute path or relative to current directory");
-            basicGroup.AddArgument("verbose", "v", "Enable verbose log output during testing", typeof(bool));
+            var verbosityArg = basicGroup.AddArgument("verbosity", "v", "Enable verbose log output during testing providing the level of logging you want to see: quiet, minimal, normal, detailed.  Using -v with no argument defaults to 'detailed'", typeof(string), defaultValue: "detailed");
+            verbosityArg.AllowedValues = new List<string>(new string[] { "quiet", "minimal", "normal", "detailed" });
             basicGroup.AddArgument("debug", "d", "Enable debugging", typeof(bool)).IsHidden = true;
             basicGroup.AddArgument("break", "b", "Attaches the debugger and also adds a breakpoint when an assertion fails (disabled during parallel testing)", typeof(bool));
             basicGroup.AddArgument("version", null, "Show tool version", typeof(bool));
@@ -162,12 +164,32 @@ You can provide one or two unsigned integer values", typeof(uint)).IsMultiValue
                 case "outdir":
                     configuration.OutputFilePath = (string)option.Value;
                     break;
-                case "verbose":
-                    configuration.IsVerbose = true;
-                    break;
                 case "debug":
                     configuration.EnableDebugging = true;
                     Debug.IsEnabled = true;
+                    break;
+                case "verbosity":
+                    configuration.IsVerbose = true;
+                    string verbosity = (string)option.Value;
+                    switch (verbosity)
+                    {
+                        case "quiet":
+                            configuration.IsVerbose = false;
+                            break;
+                        case "detailed":
+                            configuration.LogLevel = options.LogLevel = LogSeverity.Informational;
+                            break;
+                        case "normal":
+                            configuration.LogLevel = options.LogLevel = LogSeverity.Warning;
+                            break;
+                        case "minimal":
+                            configuration.LogLevel = options.LogLevel = LogSeverity.Error;
+                            break;
+                        default:
+                            Error.ReportAndExit($"Please give a valid value for 'verbosity' must be one of 'errors', 'warnings', or 'info', but found {verbosity}.");
+                            break;
+                    }
+
                     break;
                 case "timeout":
                     configuration.Timeout = (int)(uint)option.Value;

docs/_data/sidebar-learn.yml

@@ -169,6 +169,8 @@ learn-toc:
           link: /learn/ref/Microsoft.Coyote/Configuration/LivenessTemperatureThreshold
         - name: IsVerbose
           link: /learn/ref/Microsoft.Coyote/Configuration/IsVerbose
+        - name: LogLevel
+          link: /learn/ref/Microsoft.Coyote/Configuration/LogLevel
         - name: ReportActivityCoverage
           link: /learn/ref/Microsoft.Coyote/Configuration/ReportActivityCoverage
         - name: IsDgmlGraphEnabled
@@ -849,14 +851,23 @@ learn-toc:
           link: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/Write
         - name: WriteLine
           link: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/WriteLine
-        - name: WriteErrorLine
-          link: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/WriteErrorLine
-        - name: WriteWarningLine
-          link: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/WriteWarningLine
         - name: ConsoleLogger
           link: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/ConsoleLogger
+        - name: TextWriter
+          link: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/TextWriter
         - name: Encoding
           link: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/Encoding
+        - name: LogLevel
+          link: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/LogLevel
+      - name: ILogger
+        link: /learn/ref/Microsoft.Coyote.IO/ILoggerType
+        subfolderitems:
+        - name: Write
+          link: /learn/ref/Microsoft.Coyote.IO/ILogger/Write
+        - name: WriteLine
+          link: /learn/ref/Microsoft.Coyote.IO/ILogger/WriteLine
+        - name: TextWriter
+          link: /learn/ref/Microsoft.Coyote.IO/ILogger/TextWriter
       - name: InMemoryLogger
         link: /learn/ref/Microsoft.Coyote.IO/InMemoryLoggerType
         subfolderitems:
@@ -868,8 +879,12 @@ learn-toc:
           link: /learn/ref/Microsoft.Coyote.IO/InMemoryLogger/ToString
         - name: InMemoryLogger
           link: /learn/ref/Microsoft.Coyote.IO/InMemoryLogger/InMemoryLogger
+        - name: TextWriter
+          link: /learn/ref/Microsoft.Coyote.IO/InMemoryLogger/TextWriter
         - name: Encoding
           link: /learn/ref/Microsoft.Coyote.IO/InMemoryLogger/Encoding
+      - name: LogSeverity
+        link: /learn/ref/Microsoft.Coyote.IO/LogSeverityType
     - name: Microsoft.Coyote.Random
       link: /learn/ref/MicrosoftCoyoteRandomNamespace
       subfolderitems:
@@ -898,8 +913,6 @@ learn-toc:
           link: /learn/ref/Microsoft.Coyote.Runtime/ICoyoteRuntime/RandomInteger
         - name: Assert
           link: /learn/ref/Microsoft.Coyote.Runtime/ICoyoteRuntime/Assert
-        - name: SetLogger
-          link: /learn/ref/Microsoft.Coyote.Runtime/ICoyoteRuntime/SetLogger
         - name: Stop
           link: /learn/ref/Microsoft.Coyote.Runtime/ICoyoteRuntime/Stop
         - name: Logger
@@ -1178,6 +1191,8 @@ learn-toc:
         subfolderitems:
         - name: ParseFromJSON
           link: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/ParseFromJSON
+        - name: RewritingOptions
+          link: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/RewritingOptions
         - name: AssembliesDirectory
           link: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssembliesDirectory
         - name: OutputDirectory
@@ -1190,6 +1205,10 @@ learn-toc:
           link: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/StrongNameKeyFile
         - name: IsRewritingDependencies
           link: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingDependencies
+        - name: Log
+          link: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/Log
+        - name: LogLevel
+          link: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/LogLevel
         - name: IsRewritingUnitTests
           link: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingUnitTests
         - name: IsRewritingThreads
@@ -1236,14 +1255,14 @@ learn-toc:
           link: /learn/ref/Microsoft.Coyote.SystematicTesting/TestingEngine/RegisterPerIterationCallBack
         - name: IsTestRewritten
           link: /learn/ref/Microsoft.Coyote.SystematicTesting/TestingEngine/IsTestRewritten
-        - name: SetLogger
-          link: /learn/ref/Microsoft.Coyote.SystematicTesting/TestingEngine/SetLogger
         - name: TestReport
           link: /learn/ref/Microsoft.Coyote.SystematicTesting/TestingEngine/TestReport
         - name: ReadableTrace
           link: /learn/ref/Microsoft.Coyote.SystematicTesting/TestingEngine/ReadableTrace
         - name: ReproducableTrace
           link: /learn/ref/Microsoft.Coyote.SystematicTesting/TestingEngine/ReproducableTrace
+        - name: Logger
+          link: /learn/ref/Microsoft.Coyote.SystematicTesting/TestingEngine/Logger
       - name: TestReport
         link: /learn/ref/Microsoft.Coyote.SystematicTesting/TestReportType
         subfolderitems:

docs/_learn/core/logging.md

@@ -7,7 +7,7 @@ permalink: /learn/core/logging
 
 ## Logging
 
-The Coyote runtime provides a `System.IO.TextWriter` for logging so that your program output can be
+The Coyote runtime provides a `Microsoft.Coyote.IO.ILogger` interface for logging so that your program output can be
 captured and included in `coyote` test tool output logs.  A default `Logger` is provided and can be
 accessed like this:
 
@@ -17,36 +17,81 @@ accessed like this:
 | `Actor` based program | `Microsoft.Coyote.Runtime.RuntimeFactory.Create().Logger` <br/> `Actor.Logger`, `StateMachine.Logger`, `Monitor.Logger` |
 
 The default `Logger` is a `ConsoleLogger` which is used to write output to the `System.Console`.
-You can provide your own implementation of `System.IO.TextWriter` by calling the `SetLogger` method on the
+You can provide your own implementation of `Microsoft.Coyote.IO.ILogger` by setting the `Logger` property on the
 `ICoyoteRuntime` or `IActorRuntime`.
 
 The `IActorRuntime` also provides a higher level logging interface called [`IActorRuntimeLog`](/coyote/learn/core/logging#iactorruntimelog) for
 logging `Actor` and `StateMachine` activity.
 
-## Example of custom TextWriter
+## Example of custom ILogger
 
 It is possible to replace the default logger with a custom one. The following example captures all log output in a `StringBuilder`:
 
 ```c#
-public class CustomLogger : TextWriter
+public class CustomLogger : ILogger
 {
     private StringBuilder StringBuilder;
 
+    public TextWriter TextWriter => throw new NotImplementedException();
+
     public CustomLogger()
     {
         this.StringBuilder = new StringBuilder();
     }
 
-    public override Encoding Encoding => Encoding.Unicode;
-
-    public override void Write(string value)
+    public void Write(string value)
     {
-        this.StringBuilder.Append(value);
+        this.Write(LogSeverity.Informational, value);
     }
 
-    public override void WriteLine(string value)
+    public void WriteLine(string value)
     {
-        this.StringBuilder.AppendLine(value);
+        this.WriteLine(LogSeverity.Informational, value);
+    }
+
+    public void Write(string format, params object[] args)
+    {
+        this.Write(LogSeverity.Informational, format, args);
+    }
+
+    public void WriteLine(string format, params object[] args)
+    {
+        this.WriteLine(LogSeverity.Informational, format, args);
+    }
+
+    public void Write(LogSeverity severity, string format, object[] args)
+    {
+        this.Write(severity, string.Format(format, args));
+    }
+
+    public void WriteLine(LogSeverity severity, string format, object[] args)
+    {
+        this.WriteLine(severity, string.Format(format, args));
+    }
+
+    public void Write(LogSeverity severity, string value)
+    {
+        switch (severity)
+        {
+            case LogSeverity.Informational:
+                this.StringBuilder.Append("<info>" + value);
+                break;
+            case LogSeverity.Warning:
+                this.StringBuilder.Append("<warning>" + value);
+                break;
+            case LogSeverity.Error:
+                this.StringBuilder.Append("<error>" + value);
+                break;
+            case LogSeverity.Important:
+                this.StringBuilder.Append("<important>" + value);
+                break;
+        }
+    }
+
+    public void WriteLine(LogSeverity severity, string value)
+    {
+        this.Write(severity, value);
+        this.StringBuilder.AppendLine();
     }
 
     public override string ToString()
@@ -54,15 +99,9 @@ public class CustomLogger : TextWriter
         return this.StringBuilder.ToString();
     }
 
-    protected override void Dispose(bool disposing)
+    public void Dispose()
     {
-        if (disposing)
-        {
-            this.StringBuilder.Clear();
-            this.StringBuilder = null;
-        }
-
-        base.Dispose(disposing);
+        // todo      
     }
 }
 ```
@@ -70,20 +109,23 @@ public class CustomLogger : TextWriter
 To replace the default logger, call the following `IActorRuntime` method:
 
 ```c#
-using (var oldLogger = runtime.SetLogger(new CustomLogger()))
-{
-  // disposes the old logger.
-}
+runtime.Logger = new CustomLogger();
 ```
 
 The above method replaces the previously installed logger with the specified one and returns the
 previously installed logger.
 
-Note that `SetLogger` does not `Dispose` the previously installed logger. This allows the logger to
-be accessed and used after being removed from the Coyote runtime, so it is your responsibility to
-call Dispose, which can be done with a `using` block.
+Note that the old `Logger` might be disposable, so if you care about disposing the old logger at
+the same time you may need to write this instead:
 
-You could write a custom `Logger` to intercept all logging messages and send them to an Azure Log
+```c#
+using (var oldLogger = runtime.Logger) 
+{
+   runtime.Logger = new CustomLogger();
+}
+```
+
+You could write a custom `ILogger` to intercept all logging messages and send them to an Azure Log
 table, or over a TCP socket.
 
 ## IActorRuntimeLog
@@ -100,13 +142,13 @@ graph representing all activities that happened during the execution of your act
 coverage](../tools/coverage) for an example graph output. The `coyote` test tool sets this up for
 you when you specify `--graph` or `--coverage activity` command line options.
 
-The `--verbose` command line option can also affect the default logging behavior. When `--verbose`
-is specified all log output is written to the `System.Console`. This can result in a lot of output
-especially if the test is performing many iterations. It is usually more useful to only capture the
-output of the one failing iteration in a given test run and this is done by the testing runtime
-automatically when `--verbose` is not set. In the latter case, all logging is redirected into an
-`NullTextWriter` and only when a bug is found is the iteration run again with your real log writers
-activated to capture the full log for that iteration.
+The `--verbosity` command line option can also affect the default logging behavior. When
+`--verbosity` is specified all log output is written to the `System.Console` by default, but you
+can specify different levels of output using `--verbosity quiet` to get no output, `--verbosity
+minimal` to see only error messages and `--verbosity normal` to get errors and warnings. This can
+produce a lot of output especially if you run many testing iterations. It is usually more useful to
+only capture the output of the one failing iteration in a log file and this is done automatically
+by the testing runtime when `--verbosity` is not specified.
 
 See [IActorRuntimeLog API documentation](/coyote/learn/ref/Microsoft.Coyote.Actors/IActorRuntimeLogType).
 

docs/_learn/ref/Microsoft.Coyote.Actors/Actor/CurrentEventGroup.md

@@ -6,7 +6,7 @@ permalink: /learn/ref/Microsoft.Coyote.Actors/Actor/CurrentEventGroup
 ---
 # Actor.CurrentEventGroup property
 
-An optional `EventGroup` associated with the current event being handled. This is an optional argument provided to CreateActor or SendEvent.
+An optional [`EventGroup`](../EventGroupType) associated with the current event being handled. This is an optional argument provided to CreateActor or SendEvent.
 
 ```csharp
 public EventGroup CurrentEventGroup { get; set; }

docs/_learn/ref/Microsoft.Coyote.Actors/Actor/Logger.md

@@ -6,10 +6,10 @@ permalink: /learn/ref/Microsoft.Coyote.Actors/Actor/Logger
 ---
 # Actor.Logger property
 
-The installed runtime logger.
+The installed runtime logger as an [`ILogger`](../../Microsoft.Coyote.IO/ILoggerType). If you need a TextWriter then use Logger.TextWriter.
 
 ```csharp
-protected TextWriter Logger { get; }
+protected ILogger Logger { get; }
 ```
 
 ## Remarks
@@ -18,6 +18,7 @@ See [Logging](/coyote/learn/core/logging) for more information.
 
 ## See Also
 
+* interface [ILogger](../../Microsoft.Coyote.IO/ILoggerType)
 * class [Actor](../ActorType)
 * namespace [Microsoft.Coyote.Actors](../ActorType)
 * assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)

docs/_learn/ref/Microsoft.Coyote.Actors/ActorRuntimeLogTextFormatter/Logger.md

@@ -6,14 +6,19 @@ permalink: /learn/ref/Microsoft.Coyote.Actors/ActorRuntimeLogTextFormatter/Logge
 ---
 # ActorRuntimeLogTextFormatter.Logger property
 
-Get or set the TextWriter to write to.
+Get or set the [`ILogger`](../../Microsoft.Coyote.IO/ILoggerType) interface to the logger.
 
 ```csharp
-public TextWriter Logger { get; set; }
+public ILogger Logger { get; set; }
 ```
 
+## Remarks
+
+If you want Coyote to log to an existing TextWriter, then use the TextWriterLogger object but that will have a minor performance overhead, so it is better to use [`ILogger`](../../Microsoft.Coyote.IO/ILoggerType) directly.
+
 ## See Also
 
+* interface [ILogger](../../Microsoft.Coyote.IO/ILoggerType)
 * class [ActorRuntimeLogTextFormatter](../ActorRuntimeLogTextFormatterType)
 * namespace [Microsoft.Coyote.Actors](../ActorRuntimeLogTextFormatterType)
 * assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)

docs/_learn/ref/Microsoft.Coyote.Actors/ActorRuntimeLogTextFormatterType.md

@@ -17,7 +17,7 @@ public class ActorRuntimeLogTextFormatter : IActorRuntimeLog
 | name | description |
 | --- | --- |
 | [ActorRuntimeLogTextFormatter](ActorRuntimeLogTextFormatter/ActorRuntimeLogTextFormatter)() | Initializes a new instance of the [`ActorRuntimeLogTextFormatter`](ActorRuntimeLogTextFormatterType) class. |
-| [Logger](ActorRuntimeLogTextFormatter/Logger) { get; set; } | Get or set the TextWriter to write to. |
+| [Logger](ActorRuntimeLogTextFormatter/Logger) { get; set; } | Get or set the [`ILogger`](../Microsoft.Coyote.IO/ILoggerType) interface to the logger. |
 | virtual [OnAssertionFailure](ActorRuntimeLogTextFormatter/OnAssertionFailure)(…) | Invoked when the specified assertion failure has occurred. |
 | virtual [OnCompleted](ActorRuntimeLogTextFormatter/OnCompleted)() | Invoked when a log is complete (and is about to be closed). |
 | virtual [OnCreateActor](ActorRuntimeLogTextFormatter/OnCreateActor)(…) | Invoked when the specified actor has been created. |

docs/_learn/ref/Microsoft.Coyote.Actors/ActorType.md

@@ -16,7 +16,7 @@ public abstract class Actor
 
 | name | description |
 | --- | --- |
-| [CurrentEventGroup](Actor/CurrentEventGroup) { get; set; } | An optional `EventGroup` associated with the current event being handled. This is an optional argument provided to CreateActor or SendEvent. |
+| [CurrentEventGroup](Actor/CurrentEventGroup) { get; set; } | An optional [`EventGroup`](EventGroupType) associated with the current event being handled. This is an optional argument provided to CreateActor or SendEvent. |
 | override [Equals](Actor/Equals)(…) | Determines whether the specified object is equal to the current object. |
 | override [GetHashCode](Actor/GetHashCode)() | Returns the hash code for this instance. |
 | override [ToString](Actor/ToString)() | Returns a string that represents the current actor. |
@@ -28,7 +28,7 @@ public abstract class Actor
 | [Actor](Actor/Actor)() | Initializes a new instance of the [`Actor`](ActorType) class. |
 | virtual [HashedState](Actor/HashedState) { get; } | User-defined hashed state of the actor. Override to improve the accuracy of stateful techniques during testing. |
 | [Id](Actor/Id) { get; } | Unique id that identifies this actor. |
-| [Logger](Actor/Logger) { get; } | The installed runtime logger. |
+| [Logger](Actor/Logger) { get; } | The installed runtime logger as an [`ILogger`](../Microsoft.Coyote.IO/ILoggerType). If you need a TextWriter then use Logger.TextWriter. |
 | [Assert](Actor/Assert)(…) | Checks if the assertion holds, and if not, throws an AssertionFailureException exception. (5 methods) |
 | [CreateActor](Actor/CreateActor)(…) | Creates a new actor of the specified type and with the specified optional [`Event`](../Microsoft.Coyote/EventType). This [`Event`](../Microsoft.Coyote/EventType) can only be used to access its payload, and cannot be handled. (3 methods) |
 | [Monitor](Actor/Monitor)(…) | Invokes the specified monitor with the specified event. |

docs/_learn/ref/Microsoft.Coyote.IO/ConsoleLogger/LogLevel.md

@@ -1,23 +1,20 @@
 ---
 layout: reference
 section: learn
-title: WriteErrorLine
-permalink: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/WriteErrorLine
+title: LogLevel
+permalink: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/LogLevel
 ---
-# ConsoleLogger.WriteErrorLine method
+# ConsoleLogger.LogLevel property
 
-Reports an error, followed by the current line terminator.
+The level of detail to report.
 
 ```csharp
-public void WriteErrorLine(string value)
+public LogSeverity LogLevel { get; set; }
 ```
 
-| parameter | description |
-| --- | --- |
-| value | The string to write. |
-
 ## See Also
 
+* enum [LogSeverity](../LogSeverityType)
 * class [ConsoleLogger](../ConsoleLoggerType)
 * namespace [Microsoft.Coyote.IO](../ConsoleLoggerType)
 * assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)

docs/_learn/ref/Microsoft.Coyote.IO/ConsoleLogger/TextWriter.md

@@ -0,0 +1,21 @@
+---
+layout: reference
+section: learn
+title: TextWriter
+permalink: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/TextWriter
+---
+# ConsoleLogger.TextWriter property
+
+This property provides a TextWriter that implements ILogger which is handy if you have existing code that requires a TextWriter.
+
+```csharp
+public TextWriter TextWriter { get; }
+```
+
+## See Also
+
+* class [ConsoleLogger](../ConsoleLoggerType)
+* namespace [Microsoft.Coyote.IO](../ConsoleLoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->

docs/_learn/ref/Microsoft.Coyote.IO/ConsoleLogger/Write.md

@@ -4,17 +4,17 @@ section: learn
 title: Write
 permalink: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/Write
 ---
-# ConsoleLogger.Write method (1 of 2)
+# ConsoleLogger.Write method (1 of 3)
 
-Writes the specified Unicode character value to the standard output stream.
+Writes an informational string to the log.
 
 ```csharp
-public override void Write(char value)
+public override void Write(string value)
 ```
 
 | parameter | description |
 | --- | --- |
-| value | The Unicode character. |
+| value | The string to write. |
 
 ## See Also
 
@@ -24,16 +24,45 @@ public override void Write(char value)
 
 ---
 
-# ConsoleLogger.Write method (2 of 2)
+# ConsoleLogger.Write method (2 of 3)
 
-Writes the specified string value.
+Writes a string to the log.
 
 ```csharp
-public override void Write(string value)
+public void Write(LogSeverity severity, string value)
 ```
 
+| parameter | description |
+| --- | --- |
+| severity | The severity of the issue being logged. |
+| value | The string to write. |
+
 ## See Also
 
+* enum [LogSeverity](../LogSeverityType)
+* class [ConsoleLogger](../ConsoleLoggerType)
+* namespace [Microsoft.Coyote.IO](../ConsoleLoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+---
+
+# ConsoleLogger.Write method (3 of 3)
+
+Writes a string to the log.
+
+```csharp
+public void Write(LogSeverity severity, string format, params object[] args)
+```
+
+| parameter | description |
+| --- | --- |
+| severity | The severity of the issue being logged. |
+| format | The string format to write. |
+| args | The arguments needed to format the string. |
+
+## See Also
+
+* enum [LogSeverity](../LogSeverityType)
 * class [ConsoleLogger](../ConsoleLoggerType)
 * namespace [Microsoft.Coyote.IO](../ConsoleLoggerType)
 * assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)

docs/_learn/ref/Microsoft.Coyote.IO/ConsoleLogger/WriteLine.md

@@ -4,9 +4,9 @@ section: learn
 title: WriteLine
 permalink: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/WriteLine
 ---
-# ConsoleLogger.WriteLine method
+# ConsoleLogger.WriteLine method (1 of 4)
 
-Writes a string followed by a line terminator to the text string or stream.
+Writes an informational string to the log.
 
 ```csharp
 public override void WriteLine(string value)
@@ -22,4 +22,70 @@ public override void WriteLine(string value)
 * namespace [Microsoft.Coyote.IO](../ConsoleLoggerType)
 * assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
 
+---
+
+# ConsoleLogger.WriteLine method (2 of 4)
+
+Writes a string followed by a line terminator to the text string or stream.
+
+```csharp
+public void WriteLine(LogSeverity severity, string value)
+```
+
+| parameter | description |
+| --- | --- |
+| severity | The severity of the issue being logged. |
+| value | The string to write. |
+
+## See Also
+
+* enum [LogSeverity](../LogSeverityType)
+* class [ConsoleLogger](../ConsoleLoggerType)
+* namespace [Microsoft.Coyote.IO](../ConsoleLoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+---
+
+# ConsoleLogger.WriteLine method (3 of 4)
+
+Writes an informational string to the log.
+
+```csharp
+public override void WriteLine(string format, params object[] args)
+```
+
+| parameter | description |
+| --- | --- |
+| format | The string format to write. |
+| args | The arguments needed to format the string. |
+
+## See Also
+
+* class [ConsoleLogger](../ConsoleLoggerType)
+* namespace [Microsoft.Coyote.IO](../ConsoleLoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+---
+
+# ConsoleLogger.WriteLine method (4 of 4)
+
+Writes a string followed by a line terminator to the text string or stream.
+
+```csharp
+public void WriteLine(LogSeverity severity, string format, params object[] args)
+```
+
+| parameter | description |
+| --- | --- |
+| severity | The severity of the issue being logged. |
+| format | The string format to write. |
+| args | The arguments needed to format the string. |
+
+## See Also
+
+* enum [LogSeverity](../LogSeverityType)
+* class [ConsoleLogger](../ConsoleLoggerType)
+* namespace [Microsoft.Coyote.IO](../ConsoleLoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
 <!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->

docs/_learn/ref/Microsoft.Coyote.IO/ConsoleLogger/WriteWarningLine.md

@@ -1,25 +0,0 @@
----
-layout: reference
-section: learn
-title: WriteWarningLine
-permalink: /learn/ref/Microsoft.Coyote.IO/ConsoleLogger/WriteWarningLine
----
-# ConsoleLogger.WriteWarningLine method
-
-Reports an warning, followed by the current line terminator.
-
-```csharp
-public void WriteWarningLine(string value)
-```
-
-| parameter | description |
-| --- | --- |
-| value | The string to write. |
-
-## See Also
-
-* class [ConsoleLogger](../ConsoleLoggerType)
-* namespace [Microsoft.Coyote.IO](../ConsoleLoggerType)
-* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->

docs/_learn/ref/Microsoft.Coyote.IO/ConsoleLoggerType.md

@@ -9,7 +9,7 @@ permalink: /learn/ref/Microsoft.Coyote.IO/ConsoleLoggerType
 Logger that writes text to the console.
 
 ```csharp
-public sealed class ConsoleLogger : TextWriter
+public sealed class ConsoleLogger : TextWriter, ILogger
 ```
 
 ## Public Members
@@ -18,10 +18,12 @@ public sealed class ConsoleLogger : TextWriter
 | --- | --- |
 | [ConsoleLogger](ConsoleLogger/ConsoleLogger)() | Initializes a new instance of the [`ConsoleLogger`](ConsoleLoggerType) class. |
 | override [Encoding](ConsoleLogger/Encoding) { get; } | When overridden in a derived class, returns the character encoding in which the output is written. |
-| override [Write](ConsoleLogger/Write)(…) | Writes the specified Unicode character value to the standard output stream. (2 methods) |
-| [WriteErrorLine](ConsoleLogger/WriteErrorLine)(…) | Reports an error, followed by the current line terminator. |
-| override [WriteLine](ConsoleLogger/WriteLine)(…) | Writes a string followed by a line terminator to the text string or stream. |
-| [WriteWarningLine](ConsoleLogger/WriteWarningLine)(…) | Reports an warning, followed by the current line terminator. |
+| [LogLevel](ConsoleLogger/LogLevel) { get; set; } | The level of detail to report. |
+| [TextWriter](ConsoleLogger/TextWriter) { get; } | This property provides a TextWriter that implements ILogger which is handy if you have existing code that requires a TextWriter. |
+| override [Write](ConsoleLogger/Write)(…) | Writes an informational string to the log. |
+| [Write](ConsoleLogger/Write)(…) | Writes a string to the log. (2 methods) |
+| override [WriteLine](ConsoleLogger/WriteLine)(…) | Writes an informational string to the log. (2 methods) |
+| [WriteLine](ConsoleLogger/WriteLine)(…) | Writes a string followed by a line terminator to the text string or stream. (2 methods) |
 
 ## Remarks
 
@@ -29,6 +31,7 @@ See [Logging](/coyote/learn/core/logging) for more information.
 
 ## See Also
 
+* interface [ILogger](ILoggerType)
 * namespace [Microsoft.Coyote.IO](../MicrosoftCoyoteIONamespace)
 * assembly [Microsoft.Coyote](../MicrosoftCoyoteAssembly)
 

docs/_learn/ref/Microsoft.Coyote.IO/ILogger/TextWriter.md

@@ -0,0 +1,21 @@
+---
+layout: reference
+section: learn
+title: TextWriter
+permalink: /learn/ref/Microsoft.Coyote.IO/ILogger/TextWriter
+---
+# ILogger.TextWriter property
+
+This property provides a TextWriter that implements ILogger which is handy if you have existing code that requires a TextWriter.
+
+```csharp
+public TextWriter TextWriter { get; }
+```
+
+## See Also
+
+* interface [ILogger](../ILoggerType)
+* namespace [Microsoft.Coyote.IO](../ILoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->

docs/_learn/ref/Microsoft.Coyote.IO/ILogger/Write.md

@@ -0,0 +1,91 @@
+---
+layout: reference
+section: learn
+title: Write
+permalink: /learn/ref/Microsoft.Coyote.IO/ILogger/Write
+---
+# ILogger.Write method (1 of 4)
+
+Writes an informational string to the log.
+
+```csharp
+public void Write(string value)
+```
+
+| parameter | description |
+| --- | --- |
+| value | The string to write. |
+
+## See Also
+
+* interface [ILogger](../ILoggerType)
+* namespace [Microsoft.Coyote.IO](../ILoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+---
+
+# ILogger.Write method (2 of 4)
+
+Writes a string to the log.
+
+```csharp
+public void Write(LogSeverity severity, string value)
+```
+
+| parameter | description |
+| --- | --- |
+| severity | The severity of the issue being logged. |
+| value | The string to write. |
+
+## See Also
+
+* enum [LogSeverity](../LogSeverityType)
+* interface [ILogger](../ILoggerType)
+* namespace [Microsoft.Coyote.IO](../ILoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+---
+
+# ILogger.Write method (3 of 4)
+
+Writes an informational string to the log.
+
+```csharp
+public void Write(string format, params object[] args)
+```
+
+| parameter | description |
+| --- | --- |
+| format | The string format to write. |
+| args | The arguments needed to format the string. |
+
+## See Also
+
+* interface [ILogger](../ILoggerType)
+* namespace [Microsoft.Coyote.IO](../ILoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+---
+
+# ILogger.Write method (4 of 4)
+
+Writes a string to the log.
+
+```csharp
+public void Write(LogSeverity severity, string format, params object[] args)
+```
+
+| parameter | description |
+| --- | --- |
+| severity | The severity of the issue being logged. |
+| format | The string format to write. |
+| args | The arguments needed to format the string. |
+
+## See Also
+
+* enum [LogSeverity](../LogSeverityType)
+* interface [ILogger](../ILoggerType)
+* namespace [Microsoft.Coyote.IO](../ILoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->

docs/_learn/ref/Microsoft.Coyote.IO/ILogger/WriteLine.md

@@ -0,0 +1,91 @@
+---
+layout: reference
+section: learn
+title: WriteLine
+permalink: /learn/ref/Microsoft.Coyote.IO/ILogger/WriteLine
+---
+# ILogger.WriteLine method (1 of 4)
+
+Writes an informational string to the log.
+
+```csharp
+public void WriteLine(string value)
+```
+
+| parameter | description |
+| --- | --- |
+| value | The string to write. |
+
+## See Also
+
+* interface [ILogger](../ILoggerType)
+* namespace [Microsoft.Coyote.IO](../ILoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+---
+
+# ILogger.WriteLine method (2 of 4)
+
+Writes a string followed by a line terminator to the text string or stream.
+
+```csharp
+public void WriteLine(LogSeverity severity, string value)
+```
+
+| parameter | description |
+| --- | --- |
+| severity | The severity of the issue being logged. |
+| value | The string to write. |
+
+## See Also
+
+* enum [LogSeverity](../LogSeverityType)
+* interface [ILogger](../ILoggerType)
+* namespace [Microsoft.Coyote.IO](../ILoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+---
+
+# ILogger.WriteLine method (3 of 4)
+
+Writes an informational string to the log.
+
+```csharp
+public void WriteLine(string format, params object[] args)
+```
+
+| parameter | description |
+| --- | --- |
+| format | The string format to write. |
+| args | The arguments needed to format the string. |
+
+## See Also
+
+* interface [ILogger](../ILoggerType)
+* namespace [Microsoft.Coyote.IO](../ILoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+---
+
+# ILogger.WriteLine method (4 of 4)
+
+Writes a string followed by a line terminator to the text string or stream.
+
+```csharp
+public void WriteLine(LogSeverity severity, string format, params object[] args)
+```
+
+| parameter | description |
+| --- | --- |
+| severity | The severity of the issue being logged. |
+| format | The string format to write. |
+| args | The arguments needed to format the string. |
+
+## See Also
+
+* enum [LogSeverity](../LogSeverityType)
+* interface [ILogger](../ILoggerType)
+* namespace [Microsoft.Coyote.IO](../ILoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->

docs/_learn/ref/Microsoft.Coyote.IO/ILoggerType.md

@@ -0,0 +1,28 @@
+---
+layout: reference
+section: learn
+title: ILogger
+permalink: /learn/ref/Microsoft.Coyote.IO/ILoggerType
+---
+# ILogger interface
+
+A logger is used to capture messages, warnings and errors.
+
+```csharp
+public interface ILogger : IDisposable
+```
+
+## Members
+
+| name | description |
+| --- | --- |
+| [TextWriter](ILogger/TextWriter) { get; } | This property provides a TextWriter that implements ILogger which is handy if you have existing code that requires a TextWriter. |
+| [Write](ILogger/Write)(…) | Writes an informational string to the log. (4 methods) |
+| [WriteLine](ILogger/WriteLine)(…) | Writes an informational string to the log. (4 methods) |
+
+## See Also
+
+* namespace [Microsoft.Coyote.IO](../MicrosoftCoyoteIONamespace)
+* assembly [Microsoft.Coyote](../MicrosoftCoyoteAssembly)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->

docs/_learn/ref/Microsoft.Coyote.IO/InMemoryLogger/TextWriter.md

@@ -0,0 +1,21 @@
+---
+layout: reference
+section: learn
+title: TextWriter
+permalink: /learn/ref/Microsoft.Coyote.IO/InMemoryLogger/TextWriter
+---
+# InMemoryLogger.TextWriter property
+
+This property provides a TextWriter that implements ILogger which is handy if you have existing code that requires a TextWriter.
+
+```csharp
+public TextWriter TextWriter { get; }
+```
+
+## See Also
+
+* class [InMemoryLogger](../InMemoryLoggerType)
+* namespace [Microsoft.Coyote.IO](../InMemoryLoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->

docs/_learn/ref/Microsoft.Coyote.IO/InMemoryLogger/Write.md

@@ -4,17 +4,17 @@ section: learn
 title: Write
 permalink: /learn/ref/Microsoft.Coyote.IO/InMemoryLogger/Write
 ---
-# InMemoryLogger.Write method (1 of 2)
+# InMemoryLogger.Write method (1 of 3)
 
-Writes the specified Unicode character value to the standard output stream.
+Writes an informational string to the log.
 
 ```csharp
-public override void Write(char value)
+public override void Write(string value)
 ```
 
 | parameter | description |
 | --- | --- |
-| value | The Unicode character. |
+| value | The string to write. |
 
 ## See Also
 
@@ -24,16 +24,45 @@ public override void Write(char value)
 
 ---
 
-# InMemoryLogger.Write method (2 of 2)
+# InMemoryLogger.Write method (2 of 3)
 
-Writes the specified string value.
+Writes a string to the log.
 
 ```csharp
-public override void Write(string value)
+public void Write(LogSeverity severity, string value)
 ```
 
+| parameter | description |
+| --- | --- |
+| severity | The severity of the issue being logged. |
+| value | The string to write. |
+
 ## See Also
 
+* enum [LogSeverity](../LogSeverityType)
+* class [InMemoryLogger](../InMemoryLoggerType)
+* namespace [Microsoft.Coyote.IO](../InMemoryLoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+---
+
+# InMemoryLogger.Write method (3 of 3)
+
+Writes a string to the log.
+
+```csharp
+public void Write(LogSeverity severity, string format, params object[] args)
+```
+
+| parameter | description |
+| --- | --- |
+| severity | The severity of the issue being logged. |
+| format | The string format to write. |
+| args | The arguments needed to format the string. |
+
+## See Also
+
+* enum [LogSeverity](../LogSeverityType)
 * class [InMemoryLogger](../InMemoryLoggerType)
 * namespace [Microsoft.Coyote.IO](../InMemoryLoggerType)
 * assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)

docs/_learn/ref/Microsoft.Coyote.IO/InMemoryLogger/WriteLine.md

@@ -4,9 +4,9 @@ section: learn
 title: WriteLine
 permalink: /learn/ref/Microsoft.Coyote.IO/InMemoryLogger/WriteLine
 ---
-# InMemoryLogger.WriteLine method
+# InMemoryLogger.WriteLine method (1 of 3)
 
-Writes a string followed by a line terminator to the text string or stream.
+Writes an informational string to the log.
 
 ```csharp
 public override void WriteLine(string value)
@@ -22,4 +22,49 @@ public override void WriteLine(string value)
 * namespace [Microsoft.Coyote.IO](../InMemoryLoggerType)
 * assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
 
+---
+
+# InMemoryLogger.WriteLine method (2 of 3)
+
+Writes a string followed by a line terminator to the text string or stream.
+
+```csharp
+public void WriteLine(LogSeverity severity, string value)
+```
+
+| parameter | description |
+| --- | --- |
+| severity | The severity of the issue being logged. |
+| value | The string to write. |
+
+## See Also
+
+* enum [LogSeverity](../LogSeverityType)
+* class [InMemoryLogger](../InMemoryLoggerType)
+* namespace [Microsoft.Coyote.IO](../InMemoryLoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+---
+
+# InMemoryLogger.WriteLine method (3 of 3)
+
+Writes a string followed by a line terminator to the text string or stream.
+
+```csharp
+public void WriteLine(LogSeverity severity, string format, params object[] args)
+```
+
+| parameter | description |
+| --- | --- |
+| severity | The severity of the issue being logged. |
+| format | The string format to write. |
+| args | The arguments needed to format the string. |
+
+## See Also
+
+* enum [LogSeverity](../LogSeverityType)
+* class [InMemoryLogger](../InMemoryLoggerType)
+* namespace [Microsoft.Coyote.IO](../InMemoryLoggerType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
 <!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->

docs/_learn/ref/Microsoft.Coyote.IO/InMemoryLoggerType.md

@@ -9,7 +9,7 @@ permalink: /learn/ref/Microsoft.Coyote.IO/InMemoryLoggerType
 Thread safe logger that writes text to an in-memory buffer. The buffered text can be extracted using the ToString() method.
 
 ```csharp
-public sealed class InMemoryLogger : TextWriter
+public sealed class InMemoryLogger : TextWriter, ILogger
 ```
 
 ## Public Members
@@ -18,9 +18,12 @@ public sealed class InMemoryLogger : TextWriter
 | --- | --- |
 | [InMemoryLogger](InMemoryLogger/InMemoryLogger)() | Initializes a new instance of the [`InMemoryLogger`](InMemoryLoggerType) class. |
 | override [Encoding](InMemoryLogger/Encoding) { get; } | When overridden in a derived class, returns the character encoding in which the output is written. |
+| [TextWriter](InMemoryLogger/TextWriter) { get; } | This property provides a TextWriter that implements ILogger which is handy if you have existing code that requires a TextWriter. |
 | override [ToString](InMemoryLogger/ToString)() | Returns the logged text as a string. |
-| override [Write](InMemoryLogger/Write)(…) | Writes the specified Unicode character value to the standard output stream. (2 methods) |
-| override [WriteLine](InMemoryLogger/WriteLine)(…) | Writes a string followed by a line terminator to the text string or stream. |
+| override [Write](InMemoryLogger/Write)(…) | Writes an informational string to the log. |
+| [Write](InMemoryLogger/Write)(…) | Writes a string to the log. (2 methods) |
+| override [WriteLine](InMemoryLogger/WriteLine)(…) | Writes an informational string to the log. |
+| [WriteLine](InMemoryLogger/WriteLine)(…) | Writes a string followed by a line terminator to the text string or stream. (2 methods) |
 
 ## Remarks
 
@@ -28,6 +31,7 @@ See [Logging](/coyote/learn/core/logging) for more information.
 
 ## See Also
 
+* interface [ILogger](ILoggerType)
 * namespace [Microsoft.Coyote.IO](../MicrosoftCoyoteIONamespace)
 * assembly [Microsoft.Coyote](../MicrosoftCoyoteAssembly)
 

docs/_learn/ref/Microsoft.Coyote.IO/LogSeverityType.md

@@ -0,0 +1,29 @@
+---
+layout: reference
+section: learn
+title: LogSeverity
+permalink: /learn/ref/Microsoft.Coyote.IO/LogSeverityType
+---
+# LogSeverity enumeration
+
+Flag indicating the type of logging information being provided to the [`ILogger`](ILoggerType).
+
+```csharp
+public enum LogSeverity
+```
+
+## Values
+
+| name | value | description |
+| --- | --- | --- |
+| Informational | `0` | General information about what is happening in the program. |
+| Warning | `1` | Warnings that something unusual is found and is being handled. |
+| Error | `2` | Error is something unexpected that usually means program cannot proceed normally. |
+| Important | `3` | Output that is not an error or warning, but is important. |
+
+## See Also
+
+* namespace [Microsoft.Coyote.IO](../MicrosoftCoyoteIONamespace)
+* assembly [Microsoft.Coyote](../MicrosoftCoyoteAssembly)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->

docs/_learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssembliesDirectory.md

@@ -9,7 +9,7 @@ permalink: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssembliesDire
 The directory containing the assemblies to rewrite.
 
 ```csharp
-public string AssembliesDirectory { get; }
+public string AssembliesDirectory { get; set; }
 ```
 
 ## See Also

docs/_learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssemblyPaths.md

@@ -9,7 +9,7 @@ permalink: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssemblyPaths
 The file names of the assemblies to rewrite. If this list is empty then it will rewrite all assemblies in the [`AssembliesDirectory`](AssembliesDirectory).
 
 ```csharp
-public HashSet<string> AssemblyPaths { get; }
+public HashSet<string> AssemblyPaths { get; set; }
 ```
 
 ## See Also

docs/_learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/DisallowedAssemblies.md

@@ -9,7 +9,7 @@ permalink: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/DisallowedAsse
 The regular expressions used to match against assembly names to determine which assemblies to ignore when rewriting dependencies or a whole directory.
 
 ```csharp
-public IList<string> DisallowedAssemblies { get; }
+public IList<string> DisallowedAssemblies { get; set; }
 ```
 
 ## Remarks

docs/_learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingDependencies.md

@@ -9,7 +9,7 @@ permalink: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingDep
 Whether to also rewrite dependent assemblies that are found in the same location.
 
 ```csharp
-public bool IsRewritingDependencies { get; }
+public bool IsRewritingDependencies { get; set; }
 ```
 
 ## See Also

docs/_learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/Log.md

@@ -0,0 +1,21 @@
+---
+layout: reference
+section: learn
+title: Log
+permalink: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/Log
+---
+# RewritingOptions.Log property
+
+Log output from rewriter (default is Console output).
+
+```csharp
+public ILogger Log { get; set; }
+```
+
+## See Also
+
+* class [RewritingOptions](../RewritingOptionsType)
+* namespace [Microsoft.Coyote.Rewriting](../RewritingOptionsType)
+* assembly [Microsoft.Coyote.Test](../../MicrosoftCoyoteTestAssembly)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/_learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/LogLevel.md

@@ -0,0 +1,21 @@
+---
+layout: reference
+section: learn
+title: LogLevel
+permalink: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/LogLevel
+---
+# RewritingOptions.LogLevel property
+
+The amount of log output to produce.
+
+```csharp
+public LogSeverity LogLevel { get; set; }
+```
+
+## See Also
+
+* class [RewritingOptions](../RewritingOptionsType)
+* namespace [Microsoft.Coyote.Rewriting](../RewritingOptionsType)
+* assembly [Microsoft.Coyote.Test](../../MicrosoftCoyoteTestAssembly)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/_learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/OutputDirectory.md

@@ -9,7 +9,7 @@ permalink: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/OutputDirector
 The output directory where rewritten assemblies are placed. If this is the same as the [`AssembliesDirectory`](AssembliesDirectory) then the rewritten assemblies will replace the original assemblies.
 
 ```csharp
-public string OutputDirectory { get; }
+public string OutputDirectory { get; set; }
 ```
 
 ## See Also

docs/_learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/RewritingOptions.md

@@ -0,0 +1,21 @@
+---
+layout: reference
+section: learn
+title: RewritingOptions
+permalink: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/RewritingOptions
+---
+# RewritingOptions constructor
+
+The default constructor.
+
+```csharp
+public RewritingOptions()
+```
+
+## See Also
+
+* class [RewritingOptions](../RewritingOptionsType)
+* namespace [Microsoft.Coyote.Rewriting](../RewritingOptionsType)
+* assembly [Microsoft.Coyote.Test](../../MicrosoftCoyoteTestAssembly)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/_learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/StrongNameKeyFile.md

@@ -9,7 +9,7 @@ permalink: /learn/ref/Microsoft.Coyote.Rewriting/RewritingOptions/StrongNameKeyF
 Path of strong name key to use for signing rewritten assemblies.
 
 ```csharp
-public string StrongNameKeyFile { get; }
+public string StrongNameKeyFile { get; set; }
 ```
 
 ## See Also

docs/_learn/ref/Microsoft.Coyote.Rewriting/RewritingOptionsType.md

@@ -16,15 +16,18 @@ public class RewritingOptions
 
 | name | description |
 | --- | --- |
+| [RewritingOptions](RewritingOptions/RewritingOptions)() | The default constructor. |
 | static [ParseFromJSON](RewritingOptions/ParseFromJSON)(…) | Parses the [`RewritingOptions`](RewritingOptionsType) from the specified JSON configuration file. |
-| [AssembliesDirectory](RewritingOptions/AssembliesDirectory) { get; } | The directory containing the assemblies to rewrite. |
-| [AssemblyPaths](RewritingOptions/AssemblyPaths) { get; } | The file names of the assemblies to rewrite. If this list is empty then it will rewrite all assemblies in the [`AssembliesDirectory`](RewritingOptions/AssembliesDirectory). |
-| [DisallowedAssemblies](RewritingOptions/DisallowedAssemblies) { get; } | The regular expressions used to match against assembly names to determine which assemblies to ignore when rewriting dependencies or a whole directory. |
-| [IsRewritingDependencies](RewritingOptions/IsRewritingDependencies) { get; } | Whether to also rewrite dependent assemblies that are found in the same location. |
+| [AssembliesDirectory](RewritingOptions/AssembliesDirectory) { get; set; } | The directory containing the assemblies to rewrite. |
+| [AssemblyPaths](RewritingOptions/AssemblyPaths) { get; set; } | The file names of the assemblies to rewrite. If this list is empty then it will rewrite all assemblies in the [`AssembliesDirectory`](RewritingOptions/AssembliesDirectory). |
+| [DisallowedAssemblies](RewritingOptions/DisallowedAssemblies) { get; set; } | The regular expressions used to match against assembly names to determine which assemblies to ignore when rewriting dependencies or a whole directory. |
+| [IsRewritingDependencies](RewritingOptions/IsRewritingDependencies) { get; set; } | Whether to also rewrite dependent assemblies that are found in the same location. |
 | [IsRewritingThreads](RewritingOptions/IsRewritingThreads) { get; } | True if rewriting Threads as controlled tasks. |
 | [IsRewritingUnitTests](RewritingOptions/IsRewritingUnitTests) { get; } | True if rewriting of unit test methods is enabled, else false. |
-| [OutputDirectory](RewritingOptions/OutputDirectory) { get; } | The output directory where rewritten assemblies are placed. If this is the same as the [`AssembliesDirectory`](RewritingOptions/AssembliesDirectory) then the rewritten assemblies will replace the original assemblies. |
-| [StrongNameKeyFile](RewritingOptions/StrongNameKeyFile) { get; } | Path of strong name key to use for signing rewritten assemblies. |
+| [Log](RewritingOptions/Log) { get; set; } | Log output from rewriter (default is Console output). |
+| [LogLevel](RewritingOptions/LogLevel) { get; set; } | The amount of log output to produce. |
+| [OutputDirectory](RewritingOptions/OutputDirectory) { get; set; } | The output directory where rewritten assemblies are placed. If this is the same as the [`AssembliesDirectory`](RewritingOptions/AssembliesDirectory) then the rewritten assemblies will replace the original assemblies. |
+| [StrongNameKeyFile](RewritingOptions/StrongNameKeyFile) { get; set; } | Path of strong name key to use for signing rewritten assemblies. |
 
 ## Remarks
 

docs/_learn/ref/Microsoft.Coyote.Runtime/ICoyoteRuntime/Logger.md

@@ -6,10 +6,10 @@ permalink: /learn/ref/Microsoft.Coyote.Runtime/ICoyoteRuntime/Logger
 ---
 # ICoyoteRuntime.Logger property
 
-Used to log messages. Use [`SetLogger`](SetLogger) to replace the logger with a custom one.
+Get or set the [`ILogger`](../../Microsoft.Coyote.IO/ILoggerType) used to log messages.
 
 ```csharp
-public TextWriter Logger { get; }
+public ILogger Logger { get; set; }
 ```
 
 ## Remarks
@@ -18,6 +18,7 @@ See [Logging](/coyote/learn/core/logging) for more information.
 
 ## See Also
 
+* interface [ILogger](../../Microsoft.Coyote.IO/ILoggerType)
 * interface [ICoyoteRuntime](../ICoyoteRuntimeType)
 * namespace [Microsoft.Coyote.Runtime](../ICoyoteRuntimeType)
 * assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)

docs/_learn/ref/Microsoft.Coyote.Runtime/ICoyoteRuntime/SetLogger.md

@@ -1,29 +0,0 @@
----
-layout: reference
-section: learn
-title: SetLogger
-permalink: /learn/ref/Microsoft.Coyote.Runtime/ICoyoteRuntime/SetLogger
----
-# ICoyoteRuntime.SetLogger method
-
-Use this method to override the default TextWriter for logging messages.
-
-```csharp
-public TextWriter SetLogger(TextWriter logger)
-```
-
-| parameter | description |
-| --- | --- |
-| logger | The logger to install. |
-
-## Return Value
-
-The previously installed logger.
-
-## See Also
-
-* interface [ICoyoteRuntime](../ICoyoteRuntimeType)
-* namespace [Microsoft.Coyote.Runtime](../ICoyoteRuntimeType)
-* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->

docs/_learn/ref/Microsoft.Coyote.Runtime/ICoyoteRuntimeType.md

@@ -16,7 +16,7 @@ public interface ICoyoteRuntime : IDisposable
 
 | name | description |
 | --- | --- |
-| [Logger](ICoyoteRuntime/Logger) { get; } | Used to log messages. Use [`SetLogger`](ICoyoteRuntime/SetLogger) to replace the logger with a custom one. |
+| [Logger](ICoyoteRuntime/Logger) { get; set; } | Get or set the [`ILogger`](../Microsoft.Coyote.IO/ILoggerType) used to log messages. |
 | event [OnFailure](ICoyoteRuntime/OnFailure) | Callback that is fired when the runtime throws an exception which includes failed assertions. |
 | [Assert](ICoyoteRuntime/Assert)(…) | Checks if the assertion holds, and if not, throws an AssertionFailureException exception. (5 methods) |
 | [Monitor<T>](ICoyoteRuntime/Monitor)(…) | Invokes the specified monitor with the specified [`Event`](../Microsoft.Coyote/EventType). |
@@ -24,7 +24,6 @@ public interface ICoyoteRuntime : IDisposable
 | [RandomBoolean](ICoyoteRuntime/RandomBoolean)(…) | Returns a nondeterministic boolean choice, that can be controlled during analysis or testing. The value is used to generate a number in the range [0..maxValue), where 0 triggers true. |
 | [RandomInteger](ICoyoteRuntime/RandomInteger)(…) | Returns a nondeterministic integer choice, that can be controlled during analysis or testing. The value is used to generate an integer in the range [0..maxValue). |
 | [RegisterMonitor<T>](ICoyoteRuntime/RegisterMonitor)() | Registers a new specification monitor of the specified Type. |
-| [SetLogger](ICoyoteRuntime/SetLogger)(…) | Use this method to override the default TextWriter for logging messages. |
 | [Stop](ICoyoteRuntime/Stop)() | Terminates the runtime and notifies each active actor to halt execution. |
 
 ## See Also

docs/_learn/ref/Microsoft.Coyote.Specifications/Monitor/Logger.md

@@ -9,7 +9,7 @@ permalink: /learn/ref/Microsoft.Coyote.Specifications/Monitor/Logger
 The logger installed to the runtime.
 
 ```csharp
-protected TextWriter Logger { get; }
+protected ILogger Logger { get; }
 ```
 
 ## Remarks
@@ -18,6 +18,7 @@ See [Logging](/coyote/learn/core/logging) for more information.
 
 ## See Also
 
+* interface [ILogger](../../Microsoft.Coyote.IO/ILoggerType)
 * class [Monitor](../MonitorType)
 * namespace [Microsoft.Coyote.Specifications](../MonitorType)
 * assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)

docs/_learn/ref/Microsoft.Coyote.SystematicTesting/TestingEngine/Logger.md

@@ -1,24 +1,20 @@
 ---
 layout: reference
 section: learn
-title: SetLogger
-permalink: /learn/ref/Microsoft.Coyote.SystematicTesting/TestingEngine/SetLogger
+title: Logger
+permalink: /learn/ref/Microsoft.Coyote.SystematicTesting/TestingEngine/Logger
 ---
-# TestingEngine.SetLogger method
+# TestingEngine.Logger property
 
-Installs the specified TextWriter.
+Get or set the ILogger used to log messages during testing.
 
 ```csharp
-public TextWriter SetLogger(TextWriter logger)
+public ILogger Logger { get; set; }
 ```
 
-| parameter | description |
-| --- | --- |
-| logger | The logger to install. |
+## Remarks
 
-## Return Value
-
-The previously installed logger.
+See [Logging](/coyote/learn/core/logging) for more information.
 
 ## See Also
 

docs/_learn/ref/Microsoft.Coyote.SystematicTesting/TestingEngineType.md

@@ -17,6 +17,7 @@ public sealed class TestingEngine
 | name | description |
 | --- | --- |
 | static [Create](TestingEngine/Create)(…) | Creates a new systematic testing engine. (10 methods) |
+| [Logger](TestingEngine/Logger) { get; set; } | Get or set the ILogger used to log messages during testing. |
 | [ReadableTrace](TestingEngine/ReadableTrace) { get; } | The readable trace, if any. |
 | [ReproducableTrace](TestingEngine/ReproducableTrace) { get; } | The reproducable trace, if any. |
 | [TestReport](TestingEngine/TestReport) { get; set; } | Data structure containing information gathered during testing. |
@@ -25,7 +26,6 @@ public sealed class TestingEngine
 | [RegisterPerIterationCallBack](TestingEngine/RegisterPerIterationCallBack)(…) | Registers a callback to invoke at the end of each iteration. The callback takes as a parameter an integer representing the current iteration. |
 | [RethrowUnhandledException](TestingEngine/RethrowUnhandledException)() | If an iteration catches an unhandled exception then this method will rethrow that exception. |
 | [Run](TestingEngine/Run)() | Runs the testing engine. |
-| [SetLogger](TestingEngine/SetLogger)(…) | Installs the specified TextWriter. |
 | [Stop](TestingEngine/Stop)() | Stops the testing engine. |
 | [TryEmitTraces](TestingEngine/TryEmitTraces)(…) | Tries to emit the testing traces, if any. |
 

docs/_learn/ref/Microsoft.Coyote/Configuration/LogLevel.md

@@ -0,0 +1,22 @@
+---
+layout: reference
+section: learn
+title: LogLevel
+permalink: /learn/ref/Microsoft.Coyote/Configuration/LogLevel
+---
+# Configuration.LogLevel property
+
+The level of detail to provide in verbose logging.
+
+```csharp
+public LogSeverity LogLevel { get; }
+```
+
+## See Also
+
+* enum [LogSeverity](../../Microsoft.Coyote.IO/LogSeverityType)
+* class [Configuration](../ConfigurationType)
+* namespace [Microsoft.Coyote](../ConfigurationType)
+* assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->

docs/_learn/ref/Microsoft.Coyote/Configuration/WithVerbosityEnabled.md

@@ -9,15 +9,18 @@ permalink: /learn/ref/Microsoft.Coyote/Configuration/WithVerbosityEnabled
 Updates the configuration with verbose output enabled or disabled.
 
 ```csharp
-public Configuration WithVerbosityEnabled(bool isVerbose = true)
+public Configuration WithVerbosityEnabled(bool isVerbose = true, 
+    LogSeverity logLevel = LogSeverity.Informational)
 ```
 
 | parameter | description |
 | --- | --- |
 | isVerbose | If true, then messages are logged. |
+| logLevel | The level of detail to provide in verbose logging. |
 
 ## See Also
 
+* enum [LogSeverity](../../Microsoft.Coyote.IO/LogSeverityType)
 * class [Configuration](../ConfigurationType)
 * namespace [Microsoft.Coyote](../ConfigurationType)
 * assembly [Microsoft.Coyote](../../MicrosoftCoyoteAssembly)

docs/_learn/ref/Microsoft.Coyote/ConfigurationType.md

@@ -21,6 +21,7 @@ public class Configuration
 | [IsVerbose](Configuration/IsVerbose) { get; } | If true, then messages are logged. |
 | [IsXmlLogEnabled](Configuration/IsXmlLogEnabled) { get; } | Produce an XML formatted runtime log file. |
 | [LivenessTemperatureThreshold](Configuration/LivenessTemperatureThreshold) { get; } | The liveness temperature threshold. If it is 0 then it is disabled. By default this value is assigned to [`MaxFairSchedulingSteps`](Configuration/MaxFairSchedulingSteps) / 2. |
+| [LogLevel](Configuration/LogLevel) { get; } | The level of detail to provide in verbose logging. |
 | [MaxFairSchedulingSteps](Configuration/MaxFairSchedulingSteps) { get; } | The maximum scheduling steps to explore for fair schedulers. By default this is set to 100,000 steps. |
 | [MaxUnfairSchedulingSteps](Configuration/MaxUnfairSchedulingSteps) { get; } | The maximum scheduling steps to explore for unfair schedulers. By default this is set to 10,000 steps. |
 | [RandomGeneratorSeed](Configuration/RandomGeneratorSeed) { get; } | Custom seed to be used by the random value generator. By default, this value is null indicating that no seed has been set. |

docs/_learn/ref/MicrosoftCoyoteAssembly.md

@@ -70,7 +70,9 @@ permalink: /learn/ref/MicrosoftCoyoteAssembly
 | public type | description |
 | --- | --- |
 | class [ConsoleLogger](Microsoft.Coyote.IO/ConsoleLoggerType) | Logger that writes text to the console. |
+| interface [ILogger](Microsoft.Coyote.IO/ILoggerType) | A logger is used to capture messages, warnings and errors. |
 | class [InMemoryLogger](Microsoft.Coyote.IO/InMemoryLoggerType) | Thread safe logger that writes text to an in-memory buffer. The buffered text can be extracted using the ToString() method. |
+| enum [LogSeverity](Microsoft.Coyote.IO/LogSeverityType) | Flag indicating the type of logging information being provided to the [`ILogger`](Microsoft.Coyote.IO/ILoggerType). |
 
 ## Microsoft.Coyote.Random namespace
 

docs/_learn/ref/MicrosoftCoyoteIONamespace.md

@@ -9,6 +9,8 @@ permalink: /learn/ref/MicrosoftCoyoteIONamespace
 | public type | description |
 | --- | --- |
 | class [ConsoleLogger](Microsoft.Coyote.IO/ConsoleLoggerType) | Logger that writes text to the console. |
+| interface [ILogger](Microsoft.Coyote.IO/ILoggerType) | A logger is used to capture messages, warnings and errors. |
 | class [InMemoryLogger](Microsoft.Coyote.IO/InMemoryLoggerType) | Thread safe logger that writes text to an in-memory buffer. The buffered text can be extracted using the ToString() method. |
+| enum [LogSeverity](Microsoft.Coyote.IO/LogSeverityType) | Flag indicating the type of logging information being provided to the [`ILogger`](Microsoft.Coyote.IO/ILoggerType). |
 
 <!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.dll -->