# Model checker (Prototype)

Prototype of three explicit state model checker for Scala-Futures, [ZIO](https://zio.dev) and a subset of [akka typed](https://doc.akka.io/docs/akka/current/typed/index.html).

*Why?* Model checking allows to tests for race conditions and similar problems that arise in concurrent programs.
Something that is notorious difficult with normal tests.
This projects enables the power of model checking for Scala programs.

See the examples in tests:
* [Scala future](https://github.com/Jentsch/modelchecker/tree/master/futures/src/test/scala/berlin/jentsch/modelchecker/futures/example)
* [ZIO](https://github.com/Jentsch/modelchecker/tree/master/zio/src/test/scala/zio/modelchecker/example)
* [akka-typed](https://github.com/Jentsch/modelchecker/tree/master/akka/src/test/scala/berlin/jentsch/modelchecker/akka/example)

## Features

* finds race conditions
* produces trace to debug errors
* works on multiple JDK versions
* nice DSL to express advanced concepts
* finds bugs in non terminating programs (akka only)

Known limitations:

* relies upon the assumption that the tested program don't invoke more side effects than expected

## Install

Currently this project isn't publish on maven central or any other repository.
So you need to build it your self.

To publish it locally on your machine run `sbt +publishLocal`.
Add the following lines to your project:

```sbt
libraryDependencies ++= Seq(
  "jentsch.berlin" %% "modelchecker-futures" % "0.1.0-SNAPSHOT" % Test,
  "jentsch.berlin" %% "modelchecker-zio" % "0.1.0-SNAPSHOT" % Test,
  "jentsch.berlin" %% "modelchecker-akka" % "0.1.0-SNAPSHOT" % Test
)
```

This will enable all three model checkers in the tests of your project.
If you would prefer this on maven central, feel free to create a PR - until now this wasn't necessary for this prototype.

## Development

[![Build Status](https://travis-ci.org/Jentsch/modelchecker.svg?branch=master)](https://travis-ci.org/Jentsch/modelchecker)

This [sbt](https://www.scala-sbt.org/) project is separated into six sub projects:

* *futures* contains a model checker for scala Futures and their ExecutionContext
* *zio* contains a model checker for zio
* *akka* contains a model checker for Akka
* *core* contains shared functionality of futures, akka, and zio project
* *benchmarks* helps to justify performance sensitive decisions
* *jpf* helps to compare this project to [Java Pathfinder](https://github.com/javapathfinder/jpf-core)

IntelliJ and [Metals](https://scalameta.org/metals/) should be able to pick up the sbt configuration of the project.

### Tests

Use `sbt test` to execute all tests.

This project has three different kinds of tests.

#### Doc-Examples

Notice that example code snippets from scaladoc with [sbt-example](https://github.com/ThoughtWorksInc/sbt-example) are used to test functionality.
For those tests `ScalaTest with Matchers` is used.

An example:

```scala
/**
  * @example My little object. 
  * {{{
  *   MyObject.x should be(1)
  * }}}
  */
object MyObject {
  val x = 1
}
```

#### Regression tests

In some cases the behaviour of the system isn't covered by the doc-examples and a bug occure.
For such cases a regular test in `<sub-project>/test/scala/...` describes the correct behaviour.

####

Additionally some uses cases are also part of the test suite and live under `<sub-project>/test/scala/.../example/`.

## Documentation

The main source of information is currently the api-documentation generated by scaladoc and the above mentioned examples in test.

## Alternatives

The many more model checker out there.
As far as I'm aware only the [Java Pathfinder](https://github.com/javapathfinder/jpf-core) can consume Java-Programs.