Formal models, built using [[https://github.com/jarjuk/tla-sbuilder][tla-sbuilder]], and model checked using [[http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html][TLA+tools]], can generate /API Traces/, which represent end-to-end scenarios executing across system services in the formal model. An API Trace is composed of steps, with each step giving 1) a (formal) system state before the API call, 2) the API call exercised together with (formal model) value bindings of request parameters, 3) API response returned, and 4) the (formal) system state after the API call. An API Trace can be mapped to /Unit Tests/ on implementation with each Unit Test corresponding a step in the API Trace. After executing each of the individual Unit Tests, the aggregate result can be interpreted as an execution of a "virtual" System Test - considerably easier than managing the execution a System Test as a single unit.

The purpose of =tla-trace-arch= GEM is create a self extracting archive, which can be safely distributed to system service developers for extracting API Trace Steps to create unit tests for the service being developed by the developer.

** Features

Notice: Unchecked boxes have not yet been implemented.

Ref also [[https://cucumber.io/][Cucumber]] tests in directory [[./features][features]].

** Installation

Create GEM file with the content

#+BEGIN_SRC ruby :eval no :exports code source "https://rubygems.org" gem "tla-trace-arch" #+END_SRC

and run

#+BEGIN_SRC sh :eval no :results output bundle install #+END_SRC

** Usage

For a complete example, starting with installation of sbuilder- tool and creating a formal model, refer to [[./test-trace.org][test-trace.org]].

*** Create Archive

=tla-trace-filter= uses TLA+tools model checker log output and a YAML file mapping model checker log output to application interfaces.

For example, generating a formal model using =sbuilder= for =setup1= with the command

#+name: sbuilder-gen #+BEGIN_SRC sh :eval no :results output :exports code bundle exec sbuilder.rb generate setup1 #+END_SRC

creates a YAML file =gen/$SETUP/tla/interfaces.yaml=, which allows =tla-trace-filter= to map model checker log output to application interfaces.

Using the commands below to model check the formal model, generated by sbuilder, creates a file =gen/$SETUP/tlc.out=.

#+BEGIN_SRC sh :eval no :results output :exports code (SETUP=setup1;export TLATOOLS_JAR=$(pwd)/java/tla2tools.jar; cd gen/$SETUP/tla && java -cp $TLATOOLS_JAR pcal.trans model) (SETUP=setup1;export TLATOOLS_JAR=$(pwd)/java/tla2tools.jar; cd gen/$SETUP/tla && java -cp $TLATOOLS_JAR tlc2.TLC possible_bank_executed | tee ../tlc.out ) #+END_SRC

If the model checker finds a violation of property, it outputs a trace of states leading to state violating the property. API calls leading to the error state can be inspected with the command

#+BEGIN_SRC sh :eval no :results output :exports both export SETUP=setup1; bundle exec tla-trace-filter.rb api-calls $SETUP --src-dir . --solc-line #+END_SRC

and an self extracting archive created with the command:

#+name: api-arch #+BEGIN_SRC sh :eval no :results output export SETUP=setup1; bundle exec tla-trace-filter.rb api-calls $SETUP --src-dir . --solc-line --mustache tla-trace-arch | tee arch.sh chmod +x arch.sh #+END_SRC

*** Using the Archive

To show instructions for using the archive run

#+name: exe-arch #+Begin_SRC sh :eval no :results output :exports both ./arch.sh #+END_SRC

and observe

#+RESULTS: exe-arch #+begin_example

Self extracting archive created on 2017-12-27 10:05:15 by jj@horsti

$ usage ./arch.sh [options] cmd

cmd:
- step STEP              : extract files for STEP#
- interface INTERFACE    : extract files for INTERFACE
- list [INTERFACE]       : list steps matching INTERFACE, all if not given

options:
--dir DIR | -d DIR       : extract into directory DIR=tmp
--help                   : output this message
--awk-debug              : output debug message from awk extract

Notice 1: STEP and INTERFACE parameters are treated as regexps,
and regexp special characters must be escaped with backslash
character.

Notice 2: Backslash characters must also be escaped. In effect,
use double backslash characters for escaping.

#+end_example

To extract files in the archive =arch.sh= for API trace step =1= into an existing directory =tmp= run

#+BEGIN_SRC sh :eval no ./arch.sh --dir tmp step 1 #+END_SRC

*** Iterate extracted archive files in Ruby

Files extracted from an archive can be iterated and parsed using APIs in =tla_trace_arch= GEM.

#+BEGIN_SRC ruby :eval no require 'tla_trace_arch' require 'set'

Iterate api-steps for 'interface' extracted into directory 'ARGV[0]'

Sbuilder::TlaTraceArch::ReadArchiveFile.iterateApiTraceSteps( ARGV[0], interface ) do |sha1,apiTraceStep|

parse YAML data && output

puts "sha1 : #{sha1} = #{apiTraceStep["00-step"]["sha1"]} step=#{apiTraceStep["00-step"]["step"]} interface=#{apiTraceStep["00-step"]["interface"]}" puts "beforeState #{apiTraceStep["01-inp"]}" puts "api_input #{apiTraceStep["02-api"]}" puts "api_return #{apiTraceStep["03-ret"]}" puts "afterState #{apiTraceStep["04-out"]}" end

#+END_SRC

** Extension point =api-call-init=

These templates work with [[https://github.com/jarjuk/tla-trace-filter#api-call-init-extension-point][api-call-init extension point]] allowing to create interface specific archive content.

** License

MIT

FAQs

What is tla-trace-arch?

Is tla-trace-arch well maintained?

Package last updated on 02 Feb 2018

Did you know?

Socket for GitHub automatically highlights issues in each pull request and monitors the health of all your open source dependencies. Discover the contents of your packages and block harmful activity before you install or update your dependencies.

Install