FiniteModelChecker 1.0.1
A finite model checking framework for C# code
InstallPackage FiniteModelChecker Version 1.0.1
dotnet add package FiniteModelChecker version 1.0.1
<PackageReference Include="FiniteModelChecker" Version="1.0.1" />
paket add FiniteModelChecker version 1.0.1
#r "nuget: FiniteModelChecker, 1.0.1"
// 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
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 multireplica 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
 Install .NET Core
 Clone the repo
 To build, run
dotnet build
from the root of the repo  To test, run
dotnet test
from the FiniteModelChecker.Tests directory  To package, run
dotnet pack c release
Usage
In order to modelcheck 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 modelchecker will then perform a breadthfirst 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 modelchecker 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 multireplica 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
 Install .NET Core
 Clone the repo
 To build, run
dotnet build
from the root of the repo  To test, run
dotnet test
from the FiniteModelChecker.Tests directory  To package, run
dotnet pack c release
Usage
In order to modelcheck 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 modelchecker will then perform a breadthfirst 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 modelchecker 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.
Dependencies

.NETStandard 1.0
 NETStandard.Library (>= 1.6.1)
Used By
NuGet packages
This package is not used by any NuGet packages.
GitHub repositories
This package is not used by any popular GitHub repositories.