FiniteModelChecker 1.0.1

A finite model checking framework for C# code

Install-Package FiniteModelChecker -Version 1.0.1
dotnet add package FiniteModelChecker --version 1.0.1
<PackageReference Include="FiniteModelChecker" Version="1.0.1" />
For projects that support PackageReference, copy this XML node into the project file to reference the package.
paket add FiniteModelChecker --version 1.0.1
The NuGet Team does not provide support for this client. Please contact its maintainers for support.
#r "nuget: FiniteModelChecker, 1.0.1"
#r directive can be used in F# Interactive, C# scripting and .NET Interactive. Copy this into the interactive tool or source code of the script to reference the package.
// Install FiniteModelChecker as a Cake Addin
#addin nuget:?package=FiniteModelChecker&version=1.0.1

// Install FiniteModelChecker as a Cake Tool
#tool nuget:?package=FiniteModelChecker&version=1.0.1
The NuGet Team does not provide support for this client. Please contact its maintainers for support.

Finite Model Checker

This is a finite model checker for C#. Use it to exhaustively explore all possible sequences of operations against your codebase. Instead of arduously writing unit tests to perform a small series of operations, just define the set of all possible operations and let this library get to work! Example use cases:

  • Exhaustively test your custom data structure against reads and writes
  • Effectively explore the state space of your concurrency control code
  • Simulate events in a multi-replica mockup of your system

Forked from Azure/RingMaster; I wrote this tool at Microsoft to test some particularly tricky serialization code for reducing memory usage.

NuGet package: https://www.nuget.org/packages/FiniteModelChecker/

The assemblies distributed in the NuGet package are compiled against .NET Standard 1.0, which means your project must be using .NET Framework 4.5+ or .NET Core 1.0+ to reference them (see here for more details).

Build & Test

  1. Install .NET Core
  2. Clone the repo
  3. To build, run dotnet build from the root of the repo
  4. To test, run dotnet test from the FiniteModelChecker.Tests directory
  5. To package, run dotnet pack -c release

Usage

In order to model-check your code, you must define the following:

  • The set of initial states
  • The set of possible state transitions
  • The set of safety invariants: things which you want to always be true

The model-checker will then perform a breadth-first search from your initial states using the state transitions, checking the invariants in each state and reporting a full error trace if an invariant fails to hold. This means your model must generate only a finite number of states, as otherwise the model-checker will run forever.

For a simple example, you can see an implementation of the water jugs puzzle from Die Hard 3 in the Tests directory.

Finite Model Checker

This is a finite model checker for C#. Use it to exhaustively explore all possible sequences of operations against your codebase. Instead of arduously writing unit tests to perform a small series of operations, just define the set of all possible operations and let this library get to work! Example use cases:

  • Exhaustively test your custom data structure against reads and writes
  • Effectively explore the state space of your concurrency control code
  • Simulate events in a multi-replica mockup of your system

Forked from Azure/RingMaster; I wrote this tool at Microsoft to test some particularly tricky serialization code for reducing memory usage.

NuGet package: https://www.nuget.org/packages/FiniteModelChecker/

The assemblies distributed in the NuGet package are compiled against .NET Standard 1.0, which means your project must be using .NET Framework 4.5+ or .NET Core 1.0+ to reference them (see here for more details).

Build & Test

  1. Install .NET Core
  2. Clone the repo
  3. To build, run dotnet build from the root of the repo
  4. To test, run dotnet test from the FiniteModelChecker.Tests directory
  5. To package, run dotnet pack -c release

Usage

In order to model-check your code, you must define the following:

  • The set of initial states
  • The set of possible state transitions
  • The set of safety invariants: things which you want to always be true

The model-checker will then perform a breadth-first search from your initial states using the state transitions, checking the invariants in each state and reporting a full error trace if an invariant fails to hold. This means your model must generate only a finite number of states, as otherwise the model-checker will run forever.

For a simple example, you can see an implementation of the water jugs puzzle from Die Hard 3 in the Tests directory.

NuGet packages

This package is not used by any NuGet packages.

GitHub repositories

This package is not used by any popular GitHub repositories.

Version History

Version Downloads Last updated
1.0.1 1,809 8/22/2018
1.0.0 450 8/20/2018