Formal Modeling

• List setups
• Generate Formal Model for setup setup_companyRegistered
• Check Correctness of Formal Model in setup setup_companyRegistered
• Generatetate API Trace for Possibility Operator isCompanyRegistered
• Generate APItrace for Possibility Operator isCompanyRegisteredFails
• Distribute setup export SETUP=setup_companyRegistered achieve
• Versions used

Command

bundle exec  sbuilder.rb list setups

shows setups configured in cnf/sbuider.yaml

Running

(SETUP=setup_companyRegistered;  bundle exec  sbuilder.rb generate $SETUP)

outputs sbuilder translation log

generate setup: setup_companyRegistered
Unmustache  src/ --> cache/unmustache - start
Unmustache  src/ --> cache/unmustache - done
Parse snippet from repository cache/unmustache - start
 Initialize parserResolver context symbols
   4 TLA+ symbols
   6 SBuilder symbols
   3 model symbols
 Initialize parserResolver context symbols - done

Parse snippet from repository cache/unmustache - done: parsed 0 snippets

and creates TLA-files for setup setup_companyRegistered into the directory gen/$SETUP/tla:

gen/setup_companyRegistered/tla/config.tla
gen/setup_companyRegistered/tla/model.tla
gen/setup_companyRegistered/tla/possible_isCompanyRegisteredFails.tla
gen/setup_companyRegistered/tla/possible_isCompanyRegistered.tla
gen/setup_companyRegistered/tla/setup.tla

Model check formal model in file gen/setup_companyRegistered/tla/model.tla using TLA configuration gen/setup_companyRegistered/tla/setup.tla,

export SETUP=setup_companyRegistered; 
export TLATOOLS_JAR=$(pwd)/java/tla2tools.jar; 
cd gen/$SETUP/tla 
(java -cp $TLATOOLS_JAR pcal.trans model && \
 java -cp $TLATOOLS_JAR tlc2.TLC setup | tee ../tlc.out ) \
   | grep 'No error has been found.'

and observe output No error has been found:

Model checking completed. No error has been found.

Run model checking for possibility operator isCompanyRegistered in setup setup_companyRegistered using the same formal model in file gen/setup_companyRegistered/tla/model.tla, which was checked for correctness above.

# config env
export SETUP=setup_companyRegistered; 
export POSSIBILITY=isCompanyRegistered; 
export TLATOOLS_JAR=$(pwd)/java/tla2tools.jar
# model check && collect log && expect correct message
(cd gen/$SETUP/tla &&  \
   java -cp $TLATOOLS_JAR pcal.trans model && \
   java -cp $TLATOOLS_JAR tlc2.TLC possible_${POSSIBILITY} | \
   tee ../tlc_${POSSIBILITY}.out ) \
   | grep "Invariant possible_$POSSIBILITY is violated."

In the output, observe message Invariant possible_isCompanyRegistered is violated confirming that state given by the possibility operator has been observed in the state space generated for the formal model.

Error: Invariant possible_isCompanyRegistered is violated.

Create executable self extracting archive for the Model Checker Error Log, which was created when running the model checker with POSSIBLITY = isCompanyRegistered:

export SETUP=setup_companyRegistered;  
export export POSSIBILITY=isCompanyRegistered; 
ls -l gen/$SETUP/tlc_${POSSIBILITY}.out
bundle exec  tla-trace-filter.rb api-calls $SETUP \
      gen/$SETUP/tlc_${POSSIBILITY}.out \
      --mustache tla-trace-arch \
      > gen/$SETUP/arch_${POSSIBILITY}.sh
chmod +x gen/$SETUP/arch_${POSSIBILITY}.sh
gen/$SETUP/arch_${POSSIBILITY}.sh -d tmp list 2>&1
ls -l gen/$SETUP/arch_${POSSIBILITY}.sh

Output for the commands above show

-rw-rw-r-- 1 jj jj 5351 helmi  8 15:57 gen/setup_companyRegistered/tlc_isCompanyRegistered.out

Self create by jj@horsti

.. Checking SHA1 of gen/setup_companyRegistered/arch_isCompanyRegistered.sh
.. Archive SHA1 ok
.. list step=, interface=
Step 1 interface /registerCompany(post)
-rwxrwxr-x 1 jj jj 10418 helmi  8 15:57 gen/setup_companyRegistered/arch_isCompanyRegistered.sh

Check possibility isCompanyRegisteredFails in setup setup_companyRegistered:

# config env
export SETUP=setup_companyRegistered; 
export POSSIBILITY=isCompanyRegisteredFails; 
export TLATOOLS_JAR=$(pwd)/java/tla2tools.jar
# model check && collect log && expect correct message
(cd gen/$SETUP/tla &&  \
    java -cp $TLATOOLS_JAR pcal.trans model && \
    java -cp $TLATOOLS_JAR tlc2.TLC possible_${POSSIBILITY} \
    | tee ../tlc_${POSSIBILITY}.out \
) \
   | grep "Invariant possible_$POSSIBILITY is violated."

and observe confirmation in the output:

Error: Invariant possible_isCompanyRegisteredFails is violated.

Issue the following commands to create an executable archive file gen/$SETUP/arch_${POSSIBILITY}.sh

export SETUP=setup_companyRegistered; 
export POSSIBILITY=isCompanyRegisteredFails; 
ls -l gen/$SETUP/tlc_${POSSIBILITY}.out
bundle exec  \
     tla-trace-filter.rb api-calls $SETUP gen/$SETUP/tlc_${POSSIBILITY}.out \
        --mustache tla-trace-arch \
        > gen/$SETUP/arch_${POSSIBILITY}.sh; 
chmod +x gen/$SETUP/arch_${POSSIBILITY}.sh; 
gen/$SETUP/arch_${POSSIBILITY}.sh -d tmp list 2>&1
ls -l gen/$SETUP/arch_${POSSIBILITY}.sh

and observe the output

-rw-rw-r-- 1 jj jj 4944 helmi  8 15:57 gen/setup_companyRegistered/tlc_isCompanyRegisteredFails.out

Self create by jj@horsti

.. Checking SHA1 of gen/setup_companyRegistered/arch_isCompanyRegisteredFails.sh
.. Archive SHA1 ok
.. list step=, interface=
Step 1 interface /registerCompany(post)
-rwxrwxr-x 1 jj jj 10034 helmi  8 15:57 gen/setup_companyRegistered/arch_isCompanyRegisteredFails.sh

Copy archive files gen/$SETUP/arch_*.sh the to staging directory ../stage

Issue the commands and

export SETUP=setup_companyRegistered
cp gen/$SETUP/arch_*.sh ../stage
ls -l  ../stage/arch_*.sh

and observe files being copied to ../stage -directory:

-rwxrwxr-x 1 jj jj 10034 helmi  8 15:57 ../stage/arch_isCompanyRegisteredFails.sh
-rwxrwxr-x 1 jj jj 10418 helmi  8 15:57 ../stage/arch_isCompanyRegistered.sh

• TLA+tools:
  • java version: =java version "1.8.0₁₆₁"=
  • 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)=