Project
tla-trace-arch
    A set of [mustache] templates extending [tla-trace-filter] -tool
    to create a self extracting achieve for API traces generated, when
    model checking formal models created by [tla-Sbuilder] -tool.
    Also includes Ruby classes to extract test cases from archive
    extract.
    Use case:
    Formal models, built using [tla-sbuilder], and model checked using
    [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.  A 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.
   
    Ref: 
    - https://github.com/jarjuk/tla-trace-filter
    - https://mustache.github.io/mustache.5.html
    - https://github.com/jarjuk/tla-sbuilder
    - http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023
2024
2025
 Development
Licenses
MIT
 Dependencies
Runtime
>= 0.0.6, ~> 0.0