gopherator

Modelator's cousin for Golang

Instruction

git clone git@github.com/informalsystems/gopherator
cd gopherator
# Build modelator library (one time)
cargo build --release --manifest-path third_party/mbt/Cargo.toml
# Test all examples
go test -v ./examples/...

Example

Golang port of NumberSystem

# Build modelator library (if not built already)
cargo build --release --manifest-path third_party/mbt/Cargo.toml
# Test NumberSystem example
go test -v ./examples/numbersystem

Output

=== RUN   TestFixedExecutions
=== RUN   TestFixedExecutions/test_0
=== RUN   TestFixedExecutions/test_1
--- PASS: TestFixedExecutions (0.00s)
    --- PASS: TestFixedExecutions/test_0 (0.00s)
    --- PASS: TestFixedExecutions/test_1 (0.00s)
=== RUN   TestModelBased
2021/11/08 15:15:26 Generating traces using Modelator cgo-binding...
=== RUN   TestModelBased/[test:_AMaxBMaxTest,_trace:_0]
=== RUN   TestModelBased/[test:_AMaxBMinTest,_trace:_0]
=== RUN   TestModelBased/[test:_AMinBMaxTest,_trace:_0]
--- PASS: TestModelBased (2.79s)
    --- PASS: TestModelBased/[test:_AMaxBMaxTest,_trace:_0] (0.00s)
    --- PASS: TestModelBased/[test:_AMaxBMinTest,_trace:_0] (0.00s)
    --- PASS: TestModelBased/[test:_AMinBMaxTest,_trace:_0] (0.00s)
PASS
ok  	github.com/informalsystems/gopherator/examples/numbersystem	2.792s