Microsoft.Coyote assembly

Microsoft.Coyote namespace

public type description
class Configuration The Coyote runtime and testing configuration.

Microsoft.Coyote.Coverage namespace

public type description
class CoverageGraph A directed graph made up of Node and Link objects.
class CoverageInfo Class for storing coverage-specific data across multiple testing iterations.
class MonitorEventCoverage This class maintains information about events received in each state of each specification monitor.

Microsoft.Coyote.Logging namespace

public type description
interface ILogger A logger is used to capture messages, warnings and errors.
enum LogSeverity The severity of the log message being provided to the ILogger.
class MemoryLogger Logger that writes all messages to memory.
class TextWriterLogger Logger that writes to the specified TextWriter.
enum VerbosityLevel The level of verbosity used during logging.

Microsoft.Coyote.Random namespace

public type description
class Generator Represents a pseudo-random value generator, which is an algorithm that produces a sequence of values that meet certain statistical requirements for randomness. During systematic testing, the generation of random values is controlled, which allows the runtime to explore combinations of choices to find bugs.

Microsoft.Coyote.Runtime namespace

public type description
class AssertionFailureException The exception that is thrown by the Coyote runtime upon assertion failure.
interface ICoyoteRuntime Interface that exposes base runtime methods for Coyote.
interface IOperationBuilder Interface of a controlled operation builder.
interface IRuntimeExtension Interface for a Coyote runtime extension.
interface IRuntimeLog Interface that allows an external module to track what is happening in the ICoyoteRuntime.
delegate OnFailureHandler Handles the OnFailure event.
static class Operation Provides a set of static methods for instrumenting concurrency primitives that can then be controlled during testing.
class RuntimeException An exception that is thrown by the Coyote runtime.
class RuntimeLogTextFormatter This class implements IRuntimeLog and generates output in a a human readable text format.
static class RuntimeProvider Provides methods for creating or accessing a ICoyoteRuntime runtime.
static class SchedulingPoint Provides a set of static methods for declaring points in the execution where interleavings between operations should be explored during testing.
static class TaskServices Provides methods for interacting with tasks using the runtime.

Microsoft.Coyote.Specifications namespace

public type description
abstract class Monitor Abstract class representing a specification monitor.
static class Specification Provides static methods that are useful for writing specifications and interacting with the systematic testing engine.