1. Files:
=========

. startup-skel.sal
is a skeleton model for simulations with a faulty node.

. run.sh
is a shell-script that instantiates the skeleton model with
concrete values for the parameters.

traces(dir)
this directory contains the test runs generated by run.sh


2. Lemmas:
==========

. safety, safety_2
safety lemmas

. startuptime
the timeliness lemma


3. Execution Instruction:
=========================

run the shell-script "run.sh"