Compiling LTSMin

S# includes its own [model checker](Model Checking) and also supports LTSMin. LTSMin, however, is not built-into S# and has to be downloaded and compiled separately as follows:

1. Clone LTSMin: git clone https://github.com/utwente-fmt/ltsmin

2. Switch to the commit for version 2.1: git checkout ba6db31; newer versions are not supported.

3. Install the latest 64-bit version of cygwin.

4. Open a cygwin console, go to the directory containing the LTSMin repository, and run the following commands:

$ ./configure --disable-dependency-tracking LDFLAGS=-Wl,--export-all-symbols
$ make

5. Add the path to the compiled file pins2lts-seq.exe to your system path:

   1. In the start menu, search for "edit system variables" to open the advanced system properties dialog.

   2. Click on "Environment Variables".

   3. In the section "System Variables", search for the "Path" entry and click "Edit".

   4. Add a ; at the end of the "Variable value" line and append the full path (excluding the file name) to the compiled pins2lts-seq.exe.

6. Make sure the following cygwin DLLs are in a directory included in your system path as well: cyggcc_s-seh-1.dll, cygiconv-2.dll, cygintl-8.dll, cygpopt-0.dll, cygstdc++-6.dll, cygstdc++-6.dll, cygwin1.dll, and cygz.dll.

If you follow these instructions, S# should be able to use LTSMin for model checking as shown in the example below. If S# still cannot find LTSMin, check if your paths are wrong; you might also have to restart your system.

var model = // ...

var ltsmin = new LtsMin();
var result = ltsmin.CheckInvariant(model, true);

if (result.FormulaHolds)
   Console.WriteLine($"Formula holds.");

Note, however, that S#'s LTSMin integration does not support counter examples. For the full list of limitations, see the [model checking page](Model Checking).