Demo tool for Go concurrency analysis framework
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
cmd/demotool
examples
static
templates
webservice
.gitignore
Dockerfile
LICENSE
README.md

README.md

Demo tool for Go concurrency analysis framework

The basic tool consists of a runnable code editor (for use with playground package). Designed for 2-stage transformation of Go code to an intermediate format, then analysis with an external tool.

Tools support

Configuration and usage

Server side: HTTP handler

A webservice handler is defined in webservice/webservice.go, defined as name and an init function. InitFunc sets up the HTTP handler path (using the default http.HandleFunc).

type Handler struct {
    Name     string
    InitFunc func()
}

HTTP handlers can be loaded selectively by flags in the executable. By default, only Godel is loaded.

Client side: Javascript

Event handlers are set up in static/script.js as ajax calls, responses should be encoded as JSON object.

  • MiGo (v1 and v2)
    • Endpoint: '/migo.v1' and '/migo.v2'
    • Response: { 'MiGo': migo_output, 'time': execution_time, 'Error': error }
  • CFSM synthesis
    • Endpoint: '/cfsm'
    • Response: { 'CFSM': cfsm_output, 'time': execution_time, 'Error': error }
  • Gong
    • Endpoint: '/gong'
    • Response: { 'Gong': gong_output, 'time': execution_time, 'Error': error }
  • Godel checker
    • Endpoint: '/godel'
    • Response: { 'Godel': godel_output, 'time': execution_time, 'Error': error }