tla-sbuilder-trace - Post process trace output from model checking sbuilder formal models

Command line filter for processing TLA+ Tools trace output resulting from model checking TLA+ language specification code generated using sbuilder -tool.

The tool implements two commands

  • add-links : for adding links pointing 1) to TLA+ language specification code and 2) to source code translated by sbuilder tool

  • api-calls : for interpreting transitions in trace output as interface calls on sbuilder source code translated by sbuilder tool

Installation

To install tla-trace-filter GEM create a Gemfile -file with the content

source "https://rubygems.org"
gem 'tla-trace-filter'

and run

bundle install

Usage

To add links to model checker trace output in file gen/tlc.out resulting from model checking TLA+ language specification code in file gen/setup1/tla/model.tla, and using YAML file gen/setup1/tla/interfaces.yaml to map transition names back to source code modules in directory solidity run:

bundle exec tla-trace-filter.rb add-links setup1

To embed links to trace output run:

bundle exec tla-trace-filter.rb add-links setup1 --embed

tla-trace-filter.rb api-calls

To create API calls run:

bundle exec tla-trace-filter.rb api-calls setup1

Getting help

Location of the files and directories can be changes using command line options. To get a list of available command and their options run:

bundle exec tla-trace-filter.rb help

Documentation

See Cucumber tests in GEM directory features.

For a demonstration of api-call-init -extension point refer to a blog entry.

api-call-init-extension point

tla-trace-filter.rb -tool uses mustache templates to produce output. Default templates used are located in GEM directory mustache. Command line option --mustache can override the location, where templates are searched for.

To show templates, used by the tool, issue the command

ls $(bundle show tla-trace-filter)/mustache

To get instructions, how to use api-call-init -extension point, issue the command:

cat $(bundle show tla-trace-filter)/mustache/api-call-init.mustache

Mustache output lambdas

Following lambda function are available in mustache template

  • {{#YAML_DUMP}}key{{/YAML_DUMP}} : dump context key as YAML, e.g. to dump beforeState, api_input, api_return or afterState for tla-trace-filter.rb api-calls -command

License

MIT