Commit ccdaec67 authored by Etienne Renault's avatar Etienne Renault

README: more details

* Here.
parent 84d95b0a
Pipeline #16334 passed with stage
in 1 minute and 58 seconds
# go2pins: A model checking toolset for the Go programming language
# Go2Pins: Bridging the Gap between Model Checking and Software Verification
The why and the how of this project are explained in the June 2018 report,
available in the `doc/` folder.
Go2Pins is a Golang-to-Golang transpiler. Its main objective is to
bring verification techniques into the Golang realm.
## Usage
go2pins is itself a Go program. As such, you will need to have installed a
Go2Pins is itself a Go program. As such, you will need to have installed a
distribution of Go on your computer in order to build it.
The minimum recommended Go version is 1.12.
......@@ -15,38 +15,83 @@ Once you have cloned the repository:
cd go2pins
# Build go2pins
go build
# Build go2pins and run tests
make check
# Then, you can feed your program to go2pins
./go2pins my_program.go
./go2pins -o output tests/concurrent_fibonacci.go
# The output directory will contain all the files necessary to compile the
# shared library
# shared library respecting the PINS interface
cd output
# Then, to generate the state tree of your program and if you have
# use Spot's modelcheck utility in your PATH (in tests/ltsmin/modelcheck)
# Then, you can generate the state tree of your program.
# Note that this is only aivalable if you have Spot's modelcheck
# utility in your PATH (in <spot>/tests/ltsmin/modelcheck)
./go2pins-mc -display
# You can also perform LTL model checking by running either
./go2pins-mc '<some_ltl_formula>' --backend spot
./go2pins-mc '<some_ltl_formula>' -backend spot
# or if you have LTSmin backend installed
./go2pins-mc '<some_ltl_formula>' --backend ltsmin
./go2pins-mc '<some_ltl_formula>' -backend ltsmin
# Note that the LTL syntax may differ according to the various backend.
# Spot requires escaping while ltsmin refuses uppercase atomic propositions
# and requires spaces
# - Spot syntax: '[] "main_fibonacci_n==1"'
# - LTsmin syntax: '[] main_fibonacci_n == 1'
# The list of available commands is accessible through
./go2pins-mc -help
## Performances
You can replay the benchmark presented in the paper by simply running
make benchmark
Note that some part of this benchmark requires a lot of memory and can
then fail on your machine.
## LTLrec
A tool named `ltlrec` is provided when running `make`. This tool
implements the LTLrec sugaring detailled in the paper. For now,
this tool is external so that it can easily be used by other tools.
As a consequence, the equivalences must be specified by hand though
a JSON file. For instance:
./ltlrec 'F all("a") || all("b")' '{"a": ["a1", "a2"], "b": ["b1", "b2", "b3"]}'
will output
F ("a1" && "a2") || ("b1" && "b2" && "b3")
Our goal is to integrate this tool directly inside of the `output` directory.
## Limitations
* go2pins does not support Go's concurrency model. As such, channels aren't
* Only 32-bit integer value types are currently supported.
* All variables must be declared inside of a function.
* Recursion is not supported.
* 32-bit integer array are supported, but raw initialisation is
not fully supported, especially for local arrays
* Function calls are authorized for goroutines, nonetheless they will
be automatically considered as blackbox
* Unbounded channels are supported. But channels can only be declared
as global variables
Ensuring that the input file respect all these limitation is very painful.
We try to reject it correctly, but, a lot of corner cases are not covered.
Please be indulgent, and bug report.
These limitations are explored in more details in the June 2018 report.
## Architecture of the project
......@@ -59,6 +104,7 @@ These limitations are explored in more details in the June 2018 report.
* `tests/` contains example programs that can be fed into go2pins.
* `tools/` contains utility tools to inspect the AST of Go programs. They should
be built separately.
* `doc/` contains documentation about go2pins.
* `boilerplate/` contains all the boilerplate necessary to create a PINS shared
library with cgo.
* `cspinfo` information about concurrency
* `benchs` the benchmark of the paper
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment