This tarball contains the code and data files that allow one to
reproduce the results from the submitted paper "Formal Specification and
Verification of Information Flow in Dynamic Architectures"

The contents of the tarball was tested on Ubuntu 14.04.5.

Quick start:
    1) build mcmt as explained under 'mcmt'
    2) build the translator as explained under 'parser'
    3) use the script ./check to translate and check models in
       ./models_paper, as explained under 'check'
    4) use ./tester/tester.py to automatically generate, translate
       and check models, as explained under 'tester'

All example commands are to be run from the tarball top-level directory.


Description of tarball contents
-------------------------------

check
    - BASH script which automates parsing and checking of models
    - Requires built translator ./parser/parse
    - Requires mcmt binary ./mcmt/mcmt
    - Example: $ ./check -src d -dst e <models_paper/network_safe_1_d_e

check_silent
    - Like check, but produces less output. Used for automated testing.

mcmt
    - Directory where the mcmt binary with name 'mcmt' is expected
    - Please obtain MCMT from http://users.mat.unimi.it/users/ghilardi/mcmt/
      and install it. This requires an older version of Yices from
      http://yices.csl.sri.com/old/download-yices1.html (refer to MCMT
      INSTALL instructions). Save the 'mcmt' binary to './mcmt/mcmt'.

models
    - Directory where generated models are stored.
    - Naming: 'model_size_s_d', where s and d are suggested source and
      destination components or sets. The model can be checked by:
      $ ./check -src s -dst d <models/model_size_a_b
    - mcmt.in contains the MCMT input code for the last MCMT input file
      obtained by translation

models_paper
    - Directory containing the models as used in the submitted paper.
    - Same naming and use as above.

parser
    - Directory containing the source code of the translator.
    - Building the translator requires flex, bison, gcc, glib-2.0,
      pkg-config, make (tested on Ubuntu 14.04.5).
    - Please build the translator ./parser/parse by executing:
      $ cd parser
      $ make
      $ cd ..
    - Please note that the translator is not well tested and has many
      undocumented limitations.

results
    - Directory where the results of automatic testing runs are stored.
    - Naming: model_{safe|unsafe}_size_s_d
    - Format: columns are:
        1) model name
        2) model size
        3) input component or set
        4) output component or set
        5) time in seconds taken for verification or TIMEOUT or EXIT
		   (EXIT signifies that MCMT has exited with an error, it happens
		    when the translated model is too large for MCMT to handle)
        6) result of verification: SAFE or UNSAFE
        7) max depth reached by MCMT
        8) number of nodes processed by MCMT
        9) number of deleted nodes
       10) number of calls to the SMT solver Yices
       11) max number of index variables used by MCMT

tester
    - Directory containing model generators and a testing script
    - Requires Python 3
    - Requires built translator ./parser/parse
    - Requires mcmt binary ./mcmt/mcmt
    - Usage: $ ./tester/tester.py model_name size_start size_end timeout
    	where model_name is one of:
        	1) converging_safe
        	2) converging_unsafe
       		3) messenger_safe
        	4) messenger_unsafe
        	5) network_safe
        	6) network_unsafe
        	7) ring_safe
        	8) ring_unsafe
        	9) sequence_safe
       	   10) sequence_unsafe
        size_start is a natural number specifying the start model size
        size_end is a natural number specifying the end model size
        timeout is a floating point number specifying the timeout in seconds
    - Example: $ ./tester/tester.py converging_safe 1 10 20.0
      This will generate, translate and model check model
      converging_safe for sizes n=1,2,...,10 with timeout of 20.0
      seconds. It will save the generated models to ./models and output
	  the results to both stdout and to a file in ./results.
    - This testing script and the generators were used for the
      experiments in the paper and can be used to reproduce the results.
