tla-trace-arch

• =tla-trace-arch= - Create a self extracting archive for Sbuilder API trace

A set of [[https://mustache.github.io/mustache.5.html][mustache]] templates extending [[https://github.com/jarjuk/tla-trace-filter][tla-trace-filter]] -tool to create a self extracting achieve for API traces generated, when [[http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html][model checking]] formal models created by [[https://github.com/jarjuk/tla-sbuilder][Sbuilder]] -tool. Includes also APIs for iterating files extracted from the archive.

** Use case

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

• Archive meta data
  • SHA1 hash to guarantee achieve integrity
  • Archive creation time stamp, hostname and userid
  • Name of property generating API Trace
• Content of Api Trace step in the archive
  • Before state
  • Name of interface operation and parameter values
  • Return values and return status
  • After state
  • Defaults YAML dump for =beforeState=, =ap_input=, =api_return=, =afterState=
• Archive commands
  • Help
  • List steps
  • Extract by step number
  • Extract by interface name
• Name of extracted file
  • File name pattern -<inp|api|ret|out>-.
• Archive extract options
  • Define target directory for achieve extract
• API to acess the extracted files
  • =Sbuilder::TlaTraceArch::IterateArchiveFiles.iteratateTestCases=
  • =Sbuilder::TlaTraceArch::ExtractArchiveFile.parserTestCaseFile=
• Extension points
  • Control content of Api Trace Step elements per interface name

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