A fault-aware model checker for message passing systems
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
lang
test
.gitignore
README.md
sandal.go

README.md

Sandal

Sandal is a fault-aware model checker for message passing systems.

Install

Sandal follows Go's standard package structure. The following command will install Sandal compiler to $GOPATH/bin:

$ go get github.com/draftcode/sandal

In addition to Sandal compiler, you need to install NuSMV to model-check a converted model that the compiler outputs.

Usage

Sandal compiler converts a model written in Sandal into a NuSMV module, and write it to STDOUT. For example, the following command will convert your Sandal model to a NuSMV module and execute NuSMV:

$ sandal your_model.sandal | nusmv