Microsoft.Coyote assembly

Microsoft.Coyote namespace

public type description
class Configuration The Coyote runtime and testing configuration.
abstract class Event Abstract class representing an event.

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.
enum DequeueStatus The status returned as the result of an Actor dequeue operation.
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.Coverage namespace

public type description
class CoverageInfo Class for storing actor 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.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.IO namespace

public type description
class ConsoleLogger Logger that writes text to the console.
interface ILogger A logger is used to capture messages, warnings and errors.
class InMemoryLogger Thread safe logger that writes text to an in-memory buffer. The buffered text can be extracted using the ToString() method.
enum LogSeverity Flag indicating the type of logging information being provided to the ILogger.
class TextWriterLogger Bridges custom user provided TextWriter logger so it can be passed into Coyote via the ILogger interface.

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 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.