Microsoft.Coyote assembly

Microsoft.Coyote namespace

public type description
class Configuration The Coyote project configurations.
abstract class Event Abstract class representing an event.
class ExecutionCanceledException Exception that is thrown upon cancellation of testing execution by the runtime.
class RuntimeException An exception that is thrown by the Coyote runtime.

Microsoft.Coyote.Actors namespace

public type description
abstract class Actor Type that implements an actor. Inherit from this class to declare a custom actor.
class ActorId Unique actor id.
class ActorRuntimeLogTextFormatter This class implements IActorRuntimeLog and generates output in a a human readable text format.
class AwaitableEventGroup<T> An object representing an awaitable long running context involving one or more actors. An AwaitableEventGroup can be provided as an optional argument in CreateActor and SendEvent. If a null AwaitableEventGroup is passed then the EventGroup is inherited from the sender or target actors (based on which ever one has a CurrentEventGroup). In this way an AwaitableEventGroup is automatically communicated to all actors involved in completing some larger operation. Each actor involved can find the AwaitableEventGroup using their CurrentEventGroup property.
class DefaultEvent A default event that is generated by the runtime when no user-defined event is dequeued or received.
class EventGroup An object representing a long running context involving one or more actors. An EventGroup can be provided as an optional argument in CreateActor and SendEvent. If a null EventGroup is passed then the EventGroup is inherited from the sender or target actors (based on which ever one has a CurrentEventGroup). In this way an EventGroup is automatically communicated to all actors involved in completing some larger operation. Each actor involved can find the EventGroup using their CurrentEventGroup property.
class HaltEvent The halt event.
interface IActorRuntime Interface that exposes runtime methods for creating and executing actors.
interface IActorRuntimeLog Interface that allows an external module to track what is happening in the IActorRuntime.
delegate OnEventDroppedHandler Handles the OnEventDropped event.
enum OnExceptionOutcome The outcome when an Actor throws an exception.
static class RuntimeFactory Provides methods for creating a IActorRuntime runtime.
class SendOptions Represents a send event configuration that is used during testing.
abstract class StateMachine Type that implements a state machine actor. Inherit from this class to declare a custom actor with states, state transitions and event handlers.
class UnhandledEventException Signals that an Actor received an unhandled event.
class WildCardEvent The wild card event.

Microsoft.Coyote.Actors.SharedObjects namespace

public type description
class SharedCounter A thread-safe counter that can be shared in-memory by actors.
class SharedDictionary<TKey,TValue> A thread-safe dictionary that can be shared in-memory by actors.
static class SharedDictionary A thread-safe dictionary that can be shared in-memory by actors.
class SharedRegister<T> A thread-safe register that can be shared in-memory by actors.
static class SharedRegister A thread-safe register that can be shared in-memory by actors.

Microsoft.Coyote.Actors.Timers namespace

public type description
class TimerElapsedEvent Defines a timer elapsed event that is sent from a timer to the actor that owns the timer.
class TimerInfo Stores information about a timer that can send timeout events to its owner actor.

Microsoft.Coyote.Coverage namespace

public type description
class ActorRuntimeLogGraphBuilder Implements the IActorRuntimeLog and builds a directed graph from the recorded events and state transitions.
class CoverageInfo Class for storing coverage-specific data across multiple testing iterations.
class EventCoverage This class maintains information about events received and sent from each state of each actor.
class Graph A directed graph made up of Nodes and Links.
class GraphLink A Link represents a directed graph connection between two Nodes.
class GraphNode A Node of a Graph.
class GraphObject A Node of a Graph.

Microsoft.Coyote.IO namespace

public type description
class ConsoleLogger Logger that writes text to the console.
class InMemoryLogger Thread safe logger that writes text to an in-memory buffer. The buffered text can be extracted using the ToString() method.

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
interface ICoyoteRuntime Interface that exposes base runtime methods for Coyote.
delegate OnFailureHandler Handles the OnFailure event.
static class RuntimeFactory Provides methods for creating a ICoyoteRuntime 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.

Microsoft.Coyote.SystematicTesting.Interception namespace

public type description
static class ControlledTask<TResult> Provides methods for creating generic tasks that can be controlled during testing.

Microsoft.Coyote.Tasks namespace

public type description
class AsyncLock A non-reentrant mutual exclusion lock that can be acquired asynchronously in a first-in first-out order. During testing, the lock is automatically replaced with a controlled mocked version.
class Semaphore A semaphore that limits the number of tasks that can access a resource. During testing, the semaphore is automatically replaced with a controlled mocked version.
class SynchronizedBlock Provides a mechanism that synchronizes access to objects. It is implemented as a thin wrapper on Monitor. During testing, the implementation is automatically replaced with a controlled mocked version. It can be used as a replacement of the lock keyword to allow systematic testing.
class Task<TResult> Represents an asynchronous operation that can return a value. Each Task is a thin wrapper over Task and each call simply invokes the wrapped task. During testing, a Task is controlled by the runtime and systematically interleaved with other asynchronous operations to find bugs.
class Task Represents an asynchronous operation. Each Task is a thin wrapper over Task and each call simply invokes the wrapped task. During testing, a Task is controlled by the runtime and systematically interleaved with other asynchronous operations to find bugs.
class TaskCompletionSource<TResult> Represents the producer side of a task unbound to a delegate, providing access to the consumer side through the Task property.
static class TaskCompletionSource Represents the producer side of a task unbound to a delegate, providing access to the consumer side through the Task property.
static class TaskExtensions Extension methods for Task and Task objects.