Formal Modeling

1 Instructions to Install Formal Modeling Environment

Components installed:

  • Ruby GEM tla-sbuilder for Sbuilder-tool to create runnable formal models in TLA+language
  • TLA+Tools model checker to verify formal model created by Sbuilder -tool
  • Ruby GEM tla-trace-arch to create self extracting archives for API Traces created, when model checking formal models generated by Sduilder

Following commands are execture within directory 02-formal-modeling

1.2 Create Gemfile

Configure Gemfile 

source "https://rubygems.org"
gem "tla-sbuilder", "=0.3.9"       # ,  :path => "../../tla-sbuilder"
gem "tla-trace-arch", "=0.1.1"     # ,  :path => "../../tla-trace-arch"
# comment out the paths!!

1.3 Run bundle install to install GEMS

bundle install

1.4 Install TLA+tools tla2tools.jar

Download TLA+ Tools distribution package tla2tools.jar to a local java -directory 

mkdir java
wget https://tla.msr-inria.inria.fr/tlatoolbox/dist/tla2tools.jar -O java/tla2tools.jar

TLA+tool versions used to create this document are 

pcal.trans Version 1.8 of 18 Aug 2015

for TLA+tools pcal translator, and 

TLC2 Version 2.12 of 29 January 2018 (rev: 2cf4197)

for TLA+tools TLC model checker.

1.5 Initialize tla-sbuilder directory structure

Command 

bundle exec  sbuilder.rb init

creates directory structure used by sbuilder

1.6 Validate sbuilder installation and ouput sbuilder version information

Run 

bundle exec sbuilder.rb version

to validate Sbuilder installation and ouput sbuilder version information: 

sbuilder.rb - 0.3.9

1.7 Create directory tla

Create a directory tla, which will later be used to store modeling snippets of the formal model: 

# create directory - if it does not exist
[ -d tla ] || mkdir tla

1.8 Versions used

  • TLA+tools:
    • java version: =java version "1.8.0161"=
    • pcal version pcal.trans Version 1.8 of 18 Aug 2015
    • TLC version TLC2 Version 2.12 of 29 January 2018 (rev: 2cf4197)
  • Sbuilder Tools Set
    • Ruby language envrionment : ruby 2.3.1p112 (2016-04-26 revision 54768) [x86_64-linux]
    • tla-sbuilder GEM create TLA+ language formal model: =sbuilder.rb - 0.3.9 =
    • tla-parser-s GEM parse TLA+ language: = * tla-parser-s (0.2.5)=
    • tla-trace-filter GEM parse TLA+tools log: = * tla-trace-filter (0.0.6)=
    • tla-trace-arch GEM create self extracting archive = * tla-trace-arch (0.1.1)=