From 4a1898db928180d7556868f1e8e9725ae2bfbcbb Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Tue, 23 Apr 2013 23:53:26 +0200
Subject: [PATCH] src/regression-tests: Consistent regression testing.

There is now a script

  src/regression-tests/regression-test.py

that should in the future be the default for running regression tests
instead of the ad-hoc approach we are currently using. The goal is to
ultimately have more reliable and consistent regression testing.

The script takes as input "tests.txt" and tries to perform tests from
that. This is effectively a collection of inputs to the scyther-linux
binary. The results are writting to the 'results' directory, as
test-X.out and test-X.err, where those correspond to stdout and stderr,
respectively. Additionally, a measurement of wall-clock time in seconds
is written to test-X.time.

For now, we are using the timer to ensure all tests terminate. It would
be nicer to use a less environment-dependent way of enforcing
termination.
---
 src/regression-tests/Makefile                 |   5 +
 src/regression-tests/regression-test.py       | 140 ++++++++
 ...ocols-Demo-ns3.spdl --timer=60 --plain.err |   0
 ...ocols-Demo-ns3.spdl --timer=60 --plain.out |   8 +
 ...cols-Demo-ns3.spdl --timer=60 --plain.time |   2 +
 ...mo-nsl3-broken.spdl --timer=60 --plain.err |   0
 ...mo-nsl3-broken.spdl --timer=60 --plain.out |   8 +
 ...o-nsl3-broken.spdl --timer=60 --plain.time |   2 +
 ...3-updated-both.spdl --timer=60 --plain.err |   0
 ...3-updated-both.spdl --timer=60 --plain.out |  16 +
 ...-updated-both.spdl --timer=60 --plain.time |   2 +
 ...cols-Demo-nsl3.spdl --timer=60 --plain.err |   0
 ...cols-Demo-nsl3.spdl --timer=60 --plain.out |   8 +
 ...ols-Demo-nsl3.spdl --timer=60 --plain.time |   2 +
 ...9798-iso25-tag.spdl --timer=60 --plain.err |   0
 ...9798-iso25-tag.spdl --timer=60 --plain.out |  12 +
 ...798-iso25-tag.spdl --timer=60 --plain.time |   2 +
 ...9798-iso26-tag.spdl --timer=60 --plain.err |   1 +
 ...9798-iso26-tag.spdl --timer=60 --plain.out |  12 +
 ...798-iso26-tag.spdl --timer=60 --plain.time |   2 +
 ...9798-2-1-udkey.spdl --timer=60 --plain.err |   0
 ...9798-2-1-udkey.spdl --timer=60 --plain.out |   3 +
 ...798-2-1-udkey.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-2-1.spdl --timer=60 --plain.err |   0
 ...soiec-9798-2-1.spdl --timer=60 --plain.out |   3 +
 ...oiec-9798-2-1.spdl --timer=60 --plain.time |   2 +
 ...9798-2-2-udkey.spdl --timer=60 --plain.err |   0
 ...9798-2-2-udkey.spdl --timer=60 --plain.out |   3 +
 ...798-2-2-udkey.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-2-2.spdl --timer=60 --plain.err |   0
 ...soiec-9798-2-2.spdl --timer=60 --plain.out |   3 +
 ...oiec-9798-2-2.spdl --timer=60 --plain.time |   2 +
 ...9798-2-3-udkey.spdl --timer=60 --plain.err |   0
 ...9798-2-3-udkey.spdl --timer=60 --plain.out |   6 +
 ...798-2-3-udkey.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-2-3.spdl --timer=60 --plain.err |   0
 ...soiec-9798-2-3.spdl --timer=60 --plain.out |   6 +
 ...oiec-9798-2-3.spdl --timer=60 --plain.time |   2 +
 ...9798-2-4-udkey.spdl --timer=60 --plain.err |   0
 ...9798-2-4-udkey.spdl --timer=60 --plain.out |   6 +
 ...798-2-4-udkey.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-2-4.spdl --timer=60 --plain.err |   0
 ...soiec-9798-2-4.spdl --timer=60 --plain.out |   6 +
 ...oiec-9798-2-4.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-2-5.spdl --timer=60 --plain.err |   1 +
 ...soiec-9798-2-5.spdl --timer=60 --plain.out |  12 +
 ...oiec-9798-2-5.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-2-6.spdl --timer=60 --plain.err |   1 +
 ...soiec-9798-2-6.spdl --timer=60 --plain.out |  12 +
 ...oiec-9798-2-6.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-3-1.spdl --timer=60 --plain.err |   0
 ...soiec-9798-3-1.spdl --timer=60 --plain.out |   3 +
 ...oiec-9798-3-1.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-3-2.spdl --timer=60 --plain.err |   0
 ...soiec-9798-3-2.spdl --timer=60 --plain.out |   3 +
 ...oiec-9798-3-2.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-3-3.spdl --timer=60 --plain.err |   0
 ...soiec-9798-3-3.spdl --timer=60 --plain.out |   6 +
 ...oiec-9798-3-3.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-3-4.spdl --timer=60 --plain.err |   0
 ...soiec-9798-3-4.spdl --timer=60 --plain.out |   6 +
 ...oiec-9798-3-4.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-3-5.spdl --timer=60 --plain.err |   0
 ...soiec-9798-3-5.spdl --timer=60 --plain.out |   6 +
 ...oiec-9798-3-5.spdl --timer=60 --plain.time |   2 +
 ...iec-9798-3-6-1.spdl --timer=60 --plain.err |   0
 ...iec-9798-3-6-1.spdl --timer=60 --plain.out |   4 +
 ...ec-9798-3-6-1.spdl --timer=60 --plain.time |   2 +
 ...iec-9798-3-6-2.spdl --timer=60 --plain.err |   0
 ...iec-9798-3-6-2.spdl --timer=60 --plain.out |   4 +
 ...ec-9798-3-6-2.spdl --timer=60 --plain.time |   2 +
 ...iec-9798-3-7-1.spdl --timer=60 --plain.err |   0
 ...iec-9798-3-7-1.spdl --timer=60 --plain.out |   4 +
 ...ec-9798-3-7-1.spdl --timer=60 --plain.time |   2 +
 ...iec-9798-3-7-2.spdl --timer=60 --plain.err |   0
 ...iec-9798-3-7-2.spdl --timer=60 --plain.out |   4 +
 ...ec-9798-3-7-2.spdl --timer=60 --plain.time |   2 +
 ...9798-4-1-udkey.spdl --timer=60 --plain.err |   0
 ...9798-4-1-udkey.spdl --timer=60 --plain.out |   3 +
 ...798-4-1-udkey.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-4-1.spdl --timer=60 --plain.err |   1 +
 ...soiec-9798-4-1.spdl --timer=60 --plain.out |   3 +
 ...oiec-9798-4-1.spdl --timer=60 --plain.time |   2 +
 ...9798-4-2-udkey.spdl --timer=60 --plain.err |   0
 ...9798-4-2-udkey.spdl --timer=60 --plain.out |   3 +
 ...798-4-2-udkey.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-4-2.spdl --timer=60 --plain.err |   1 +
 ...soiec-9798-4-2.spdl --timer=60 --plain.out |   3 +
 ...oiec-9798-4-2.spdl --timer=60 --plain.time |   2 +
 ...9798-4-3-udkey.spdl --timer=60 --plain.err |   0
 ...9798-4-3-udkey.spdl --timer=60 --plain.out |   6 +
 ...798-4-3-udkey.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-4-3.spdl --timer=60 --plain.err |   1 +
 ...soiec-9798-4-3.spdl --timer=60 --plain.out |   6 +
 ...oiec-9798-4-3.spdl --timer=60 --plain.time |   2 +
 ...9798-4-4-udkey.spdl --timer=60 --plain.err |   0
 ...9798-4-4-udkey.spdl --timer=60 --plain.out |   6 +
 ...798-4-4-udkey.spdl --timer=60 --plain.time |   2 +
 ...soiec-9798-4-4.spdl --timer=60 --plain.err |   0
 ...soiec-9798-4-4.spdl --timer=60 --plain.out |   6 +
 ...oiec-9798-4-4.spdl --timer=60 --plain.time |   2 +
 ...ISO-9798-sasl.spdl --timer=60 --plain.time |   2 +
 ...w-ban-concrete.spdl --timer=60 --plain.err |   0
 ...w-ban-concrete.spdl --timer=60 --plain.out |   4 +
 ...-ban-concrete.spdl --timer=60 --plain.time |   2 +
 ...ols-andrew-ban.spdl --timer=60 --plain.err |   0
 ...ols-andrew-ban.spdl --timer=60 --plain.out |   8 +
 ...ls-andrew-ban.spdl --timer=60 --plain.time |   2 +
 ...ndrew-lowe-ban.spdl --timer=60 --plain.err |   0
 ...ndrew-lowe-ban.spdl --timer=60 --plain.out |   4 +
 ...drew-lowe-ban.spdl --timer=60 --plain.time |   2 +
 ...otocols-andrew.spdl --timer=60 --plain.err |   0
 ...otocols-andrew.spdl --timer=60 --plain.out |   6 +
 ...tocols-andrew.spdl --timer=60 --plain.time |   2 +
 ...ols-ccitt509-1.spdl --timer=60 --plain.err |   0
 ...ols-ccitt509-1.spdl --timer=60 --plain.out |   1 +
 ...ls-ccitt509-1.spdl --timer=60 --plain.time |   2 +
 ...ls-ccitt509-1c.spdl --timer=60 --plain.err |   0
 ...ls-ccitt509-1c.spdl --timer=60 --plain.out |   1 +
 ...s-ccitt509-1c.spdl --timer=60 --plain.time |   2 +
 ...ols-ccitt509-3.spdl --timer=60 --plain.err |   0
 ...ols-ccitt509-3.spdl --timer=60 --plain.out |   6 +
 ...ls-ccitt509-3.spdl --timer=60 --plain.time |   2 +
 ...-ccitt509-ban3.spdl --timer=60 --plain.err |   0
 ...-ccitt509-ban3.spdl --timer=60 --plain.out |   2 +
 ...ccitt509-ban3.spdl --timer=60 --plain.time |   2 +
 ...ing-sacco-lowe.spdl --timer=60 --plain.err |   0
 ...ing-sacco-lowe.spdl --timer=60 --plain.out |   6 +
 ...ng-sacco-lowe.spdl --timer=60 --plain.time |   2 +
 ...-denning-sacco.spdl --timer=60 --plain.err |   0
 ...-denning-sacco.spdl --timer=60 --plain.out |   6 +
 ...denning-sacco.spdl --timer=60 --plain.time |   2 +
 ...ols-kaochow-v2.spdl --timer=60 --plain.err |   0
 ...ols-kaochow-v2.spdl --timer=60 --plain.out |   6 +
 ...ls-kaochow-v2.spdl --timer=60 --plain.time |   2 +
 ...ols-kaochow-v3.spdl --timer=60 --plain.err |   0
 ...ols-kaochow-v3.spdl --timer=60 --plain.out |   6 +
 ...ls-kaochow-v3.spdl --timer=60 --plain.time |   2 +
 ...tocols-kaochow.spdl --timer=60 --plain.err |   0
 ...tocols-kaochow.spdl --timer=60 --plain.out |   6 +
 ...ocols-kaochow.spdl --timer=60 --plain.time |   2 +
 ...schroeder-lowe.spdl --timer=60 --plain.err |   0
 ...schroeder-lowe.spdl --timer=60 --plain.out |   6 +
 ...chroeder-lowe.spdl --timer=60 --plain.time |   2 +
 ...oeder-sk-amend.spdl --timer=60 --plain.err |   0
 ...oeder-sk-amend.spdl --timer=60 --plain.out |   4 +
 ...eder-sk-amend.spdl --timer=60 --plain.time |   2 +
 ...dham-schroeder.spdl --timer=60 --plain.err |   0
 ...dham-schroeder.spdl --timer=60 --plain.out |   6 +
 ...ham-schroeder.spdl --timer=60 --plain.time |   2 +
 ...-guttman-hwang.spdl --timer=60 --plain.err |   1 +
 ...-guttman-hwang.spdl --timer=60 --plain.out |   0
 ...guttman-hwang.spdl --timer=60 --plain.time |   2 +
 ...nnstub-guttman.spdl --timer=60 --plain.err |   1 +
 ...nnstub-guttman.spdl --timer=60 --plain.out |   0
 ...nstub-guttman.spdl --timer=60 --plain.time |   2 +
 ...mannstub-hwang.spdl --timer=60 --plain.err |   0
 ...mannstub-hwang.spdl --timer=60 --plain.out |   6 +
 ...annstub-hwang.spdl --timer=60 --plain.time |   2 +
 ...-keycompromise.spdl --timer=60 --plain.err |   1 +
 ...-keycompromise.spdl --timer=60 --plain.out |   0
 ...keycompromise.spdl --timer=60 --plain.time |   2 +
 ...ls-neumannstub.spdl --timer=60 --plain.err |   1 +
 ...ls-neumannstub.spdl --timer=60 --plain.out |   0
 ...s-neumannstub.spdl --timer=60 --plain.time |   2 +
 ...ols-smartright.spdl --timer=60 --plain.err |   0
 ...ols-smartright.spdl --timer=60 --plain.out |   1 +
 ...ls-smartright.spdl --timer=60 --plain.time |   2 +
 ...s-splice-as-hc.spdl --timer=60 --plain.err |   0
 ...s-splice-as-hc.spdl --timer=60 --plain.out |   6 +
 ...-splice-as-hc.spdl --timer=60 --plain.time |   2 +
 ...cols-splice-as.spdl --timer=60 --plain.err |   0
 ...cols-splice-as.spdl --timer=60 --plain.out |   6 +
 ...ols-splice-as.spdl --timer=60 --plain.time |   2 +
 ...-Protocols-tmn.spdl --timer=60 --plain.err |   0
 ...-Protocols-tmn.spdl --timer=60 --plain.out |   4 +
 ...Protocols-tmn.spdl --timer=60 --plain.time |   2 +
 ...ocols-wmf-lowe.spdl --timer=60 --plain.err |   0
 ...ocols-wmf-lowe.spdl --timer=60 --plain.out |   4 +
 ...cols-wmf-lowe.spdl --timer=60 --plain.time |   2 +
 ...-Protocols-wmf.spdl --timer=60 --plain.err |   0
 ...-Protocols-wmf.spdl --timer=60 --plain.out |   3 +
 ...Protocols-wmf.spdl --timer=60 --plain.time |   2 +
 ...s-woo-lam-pi-1.spdl --timer=60 --plain.err |   0
 ...s-woo-lam-pi-1.spdl --timer=60 --plain.out |   1 +
 ...-woo-lam-pi-1.spdl --timer=60 --plain.time |   2 +
 ...s-woo-lam-pi-2.spdl --timer=60 --plain.err |   0
 ...s-woo-lam-pi-2.spdl --timer=60 --plain.out |   1 +
 ...-woo-lam-pi-2.spdl --timer=60 --plain.time |   2 +
 ...s-woo-lam-pi-3.spdl --timer=60 --plain.err |   0
 ...s-woo-lam-pi-3.spdl --timer=60 --plain.out |   1 +
 ...-woo-lam-pi-3.spdl --timer=60 --plain.time |   2 +
 ...s-woo-lam-pi-f.spdl --timer=60 --plain.err |   0
 ...s-woo-lam-pi-f.spdl --timer=60 --plain.out |   1 +
 ...-woo-lam-pi-f.spdl --timer=60 --plain.time |   2 +
 ...ols-woo-lam-pi.spdl --timer=60 --plain.err |   0
 ...ols-woo-lam-pi.spdl --timer=60 --plain.out |   1 +
 ...ls-woo-lam-pi.spdl --timer=60 --plain.time |   2 +
 ...tocols-woo-lam.spdl --timer=60 --plain.err |   0
 ...tocols-woo-lam.spdl --timer=60 --plain.out |   4 +
 ...ocols-woo-lam.spdl --timer=60 --plain.time |   2 +
 ...lson-modified.spdl --timer=60 --plain.time |   2 +
 ...ls-yahalom-ban.spdl --timer=60 --plain.err |   0
 ...ls-yahalom-ban.spdl --timer=60 --plain.out |   4 +
 ...s-yahalom-ban.spdl --timer=60 --plain.time |   2 +
 ...s-yahalom-lowe.spdl --timer=60 --plain.err |   0
 ...s-yahalom-lowe.spdl --timer=60 --plain.out |   4 +
 ...-yahalom-lowe.spdl --timer=60 --plain.time |   2 +
 ...ahalom-paulson.spdl --timer=60 --plain.err |   0
 ...ahalom-paulson.spdl --timer=60 --plain.out |   4 +
 ...halom-paulson.spdl --timer=60 --plain.time |   2 +
 ...tocols-yahalom.spdl --timer=60 --plain.err |   0
 ...tocols-yahalom.spdl --timer=60 --plain.out |   4 +
 ...ocols-yahalom.spdl --timer=60 --plain.time |   2 +
 .../test-gui-mpa.spdl --timer=60 --plain.err  |   0
 .../test-gui-mpa.spdl --timer=60 --plain.out  |  16 +
 .../test-gui-mpa.spdl --timer=60 --plain.time |   2 +
 ...ui-nsl3-broken.spdl --timer=60 --plain.err |   0
 ...ui-nsl3-broken.spdl --timer=60 --plain.out |   8 +
 ...i-nsl3-broken.spdl --timer=60 --plain.time |   2 +
 .../test-gui-nsl3.spdl --timer=60 --plain.err |   0
 .../test-gui-nsl3.spdl --timer=60 --plain.out |  14 +
 ...test-gui-nsl3.spdl --timer=60 --plain.time |   2 +
 .../test-src-ns3.spdl --timer=60 --plain.err  |   0
 .../test-src-ns3.spdl --timer=60 --plain.out  |  14 +
 .../test-src-ns3.spdl --timer=60 --plain.time |   2 +
 src/regression-tests/tests.txt                | 316 ++++++++++++++++++
 227 files changed, 1008 insertions(+)
 create mode 100644 src/regression-tests/Makefile
 create mode 100755 src/regression-tests/regression-test.py
 create mode 100644 src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.err
 create mode 100644 src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.out
 create mode 100644 src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.time
 create mode 100644 src/regression-tests/tests.txt

diff --git a/src/regression-tests/Makefile b/src/regression-tests/Makefile
new file mode 100644
index 0000000..c2bd104
--- /dev/null
+++ b/src/regression-tests/Makefile
@@ -0,0 +1,5 @@
+
+results:
+	./regression-test.py
+
+.PHONY:	results
diff --git a/src/regression-tests/regression-test.py b/src/regression-tests/regression-test.py
new file mode 100755
index 0000000..a27e5df
--- /dev/null
+++ b/src/regression-tests/regression-test.py
@@ -0,0 +1,140 @@
+#!/usr/bin/env python
+"""
+Scyther : An automatic verifier for security protocols.
+Copyright (C) 2007-2012 Cas Cremers
+
+This program is free software; you can redistribute it and/or
+modify it under the terms of the GNU General Public License
+as published by the Free Software Foundation; either version 2
+of the License, or (at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program; if not, write to the Free Software
+Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
+"""
+
+"""
+regression-test.py
+
+Regression tests for changes to the Scyther executable.
+"""
+
+"""
+For each file, we run a test with some parameters, and check the result.
+
+We do this for a large set of protocols, but also for some subset with 'special' parameters.
+The tests are described in "tests.txt"
+
+Each line is considered a sequence of arguments.
+The output is written to test-X.out, where X is a sanitized version of the argument line.
+"""
+
+def sanitize(arg):
+    """
+    Take an argument line and sanitize it.
+
+    Return argument may well be empty, which causes an error
+    """
+    from string import printable
+
+    l = ""
+    for c in arg:
+        if c in printable:
+            l = l + c
+    l = l.strip()
+
+    removes = "\\\"'`{}$"
+    for x in removes:
+        l = l.replace(x,"")
+    
+    l = l.replace("\t"," ")
+    #ol = l 
+    #l = ol + "x"
+    #while l != ol:
+    #    l = ol.replace("  "," ")
+
+    #l = l.replace(" ","_")
+    l = l.replace("/","-")
+
+    l = l.strip()
+    assert(len(l) > 0)
+    return l
+
+
+def runTest(arg,destdir="."):
+    """
+    Run a test and store the result.
+
+    Time measurement is super coarse and depends, among other things, on me
+    browsing in the background during the tests.
+    """
+    import subprocess
+    import time
+    from os.path import join
+
+    nm = sanitize(arg)
+    outfile = join(destdir,"test-%s.out" % (nm))
+    errfile = join(destdir,"test-%s.err" % (nm))
+    clkfile = join(destdir,"test-%s.time" % (nm))
+
+    starttime = time.time()         # Time in seconds
+
+    cmd = "../scyther-linux ../../%s --output=\"%s\" --errors=\"%s\"" % (arg,outfile,errfile)
+    subprocess.call(cmd,shell=True)
+
+    delta = time.time() - starttime # Duration in seconds
+
+    fp = open(clkfile,'w')
+    fp.write("Passed wall time in seconds:\n%i\n" % (delta))
+    fp.close()
+
+
+def runTests(fn,destdir="."):
+
+    fp = open(fn,'r')
+    tests = []
+    clen = 0
+    for l in fp.xreadlines():
+        if l.startswith("#") or l.startswith("%"):
+            continue
+        d = l.strip()
+        if len(d) > 0:
+            tests.append(d)
+            if not d.startswith("="):
+                # We skip the 'global' settings
+                clen = clen + 1
+    fp.close()
+
+    print "Running %i tests." % (clen)
+    print "Destination: %s" % (destdir)
+    cnt = 1
+    setting = ""
+    for l in tests:
+        if l.startswith("="):
+
+            setting = l[1:]
+            if len(setting.strip()) == 0:
+                setting = ""
+
+            print "Changing global setting to \"%s\"" % (setting)
+
+        else:
+            print "%i/%i: Evaluating %s" % (cnt,clen,l+setting)
+            runTest(l+setting,destdir)
+            cnt = cnt + 1
+
+
+def main():
+    runTests("tests.txt","results")
+
+
+if __name__ == "__main__":
+    main()
+
+
+
diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..91b2ee0
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.out	
@@ -0,0 +1,8 @@
+claim	ns3,I	Secret_i1	ni	Ok	[proof of correctness]
+claim	ns3,I	Secret_i2	nr	Ok	[proof of correctness]
+claim	ns3,I	Niagree_i3	-	Ok	[proof of correctness]
+claim	ns3,I	Nisynch_i4	-	Ok	[proof of correctness]
+claim	ns3,R	Secret_r1	ni	Fail	[at least 1 attack]
+claim	ns3,R	Secret_r2	nr	Fail	[at least 1 attack]
+claim	ns3,R	Niagree_r3	-	Fail	[at least 1 attack]
+claim	ns3,R	Nisynch_r4	-	Fail	[at least 1 attack]
diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..39d339c
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.out	
@@ -0,0 +1,8 @@
+claim	nsl3-broken,I	Secret_i1	ni	Fail	[at least 1 attack]
+claim	nsl3-broken,I	Secret_i2	nr	Fail	[at least 1 attack]
+claim	nsl3-broken,I	Niagree_i3	-	Fail	[at least 1 attack]
+claim	nsl3-broken,I	Nisynch_i4	-	Fail	[at least 1 attack]
+claim	nsl3-broken,R	Secret_r1	ni	Fail	[at least 1 attack]
+claim	nsl3-broken,R	Secret_r2	nr	Ok	[proof of correctness]
+claim	nsl3-broken,R	Niagree_r3	-	Ok	[proof of correctness]
+claim	nsl3-broken,R	Nisynch_r4	-	Ok	[proof of correctness]
diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..d76f35e
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.out	
@@ -0,0 +1,16 @@
+claim	nsl3-broken,I	Secret_i1	ni	Fail	[at least 3 attacks]
+claim	nsl3-broken,I	Secret_i2	nr	Fail	[at least 1 attack]
+claim	nsl3-broken,I	Niagree_i3	-	Fail	[at least 1 attack]
+claim	nsl3-broken,I	Nisynch_i4	-	Fail	[at least 1 attack]
+claim	nsl3-broken,R	Secret_r1	ni	Fail	[at least 2 attacks]
+claim	nsl3-broken,R	Secret_r2	nr	Ok	[proof of correctness]
+claim	nsl3-broken,R	Niagree_r3	-	Fail	[at least 1 attack]
+claim	nsl3-broken,R	Nisynch_r4	-	Fail	[at least 1 attack]
+claim	nsl3,I	Secret_i1	ni	Fail	[at least 2 attacks]
+claim	nsl3,I	Secret_i2	nr	Fail	[at least 1 attack]
+claim	nsl3,I	Niagree_i3	-	Fail	[at least 1 attack]
+claim	nsl3,I	Nisynch_i4	-	Fail	[at least 1 attack]
+claim	nsl3,R	Secret_r1	ni	Fail	[at least 2 attacks]
+claim	nsl3,R	Secret_r2	nr	Ok	[proof of correctness]
+claim	nsl3,R	Niagree_r3	-	Fail	[at least 1 attack]
+claim	nsl3,R	Nisynch_r4	-	Fail	[at least 1 attack]
diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..b0c4054
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.out	
@@ -0,0 +1,8 @@
+claim	nsl3,I	Secret_i1	ni	Ok	[proof of correctness]
+claim	nsl3,I	Secret_i2	nr	Ok	[proof of correctness]
+claim	nsl3,I	Niagree_i3	-	Ok	[proof of correctness]
+claim	nsl3,I	Nisynch_i4	-	Ok	[proof of correctness]
+claim	nsl3,R	Secret_r1	ni	Ok	[proof of correctness]
+claim	nsl3,R	Secret_r2	nr	Ok	[proof of correctness]
+claim	nsl3,R	Niagree_r3	-	Ok	[proof of correctness]
+claim	nsl3,R	Nisynch_r4	-	Ok	[proof of correctness]
diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..8254692
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.out	
@@ -0,0 +1,12 @@
+claim	isoiec-9798-2-5,A	Commit_A2	(B,Kab,Text5,Text7)	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,A	Secret_A3	Kab	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,A	Secret_A4	Text5	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,A	Secret_A5	Text7	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,A	Alive_A6	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,A	Weakagree_A7	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,B	Commit_B2	(A,Kab,Text5)	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,B	Secret_B3	Kab	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,B	Secret_B4	Text5	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,B	Secret_B5	Text7	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,B	Alive_B6	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,B	Weakagree_B7	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..711e64e
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+4
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..d3b1ed1
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.err	
@@ -0,0 +1 @@
+warning: protocol @keysymm26 has empty role definitions for the roles: [B, P]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..843770a
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.out	
@@ -0,0 +1,12 @@
+claim	isoiec-9798-2-6-tag,A	Commit_A2	(B,Kab,Text6,Text8)	Fail	[at least 2 attacks]
+claim	isoiec-9798-2-6-tag,A	Secret_A3	Kab	Ok	[no attack within bounds]
+claim	isoiec-9798-2-6-tag,A	Secret_A4	Text6	Ok	[no attack within bounds]
+claim	isoiec-9798-2-6-tag,A	Secret_A5	Text8	Ok	[no attack within bounds]
+claim	isoiec-9798-2-6-tag,A	Alive_A6	-	Fail	[at least 2 attacks]
+claim	isoiec-9798-2-6-tag,A	Weakagree_A7	-	Fail	[at least 2 attacks]
+claim	isoiec-9798-2-6-tag,B	Commit_B2	(A,Kab,Text6)	Fail	[at least 2 attacks]
+claim	isoiec-9798-2-6-tag,B	Secret_B3	Kab	Ok	[no attack within bounds]
+claim	isoiec-9798-2-6-tag,B	Secret_B4	Text6	Ok	[no attack within bounds]
+claim	isoiec-9798-2-6-tag,B	Secret_B5	Text8	Ok	[no attack within bounds]
+claim	isoiec-9798-2-6-tag,B	Alive_B6	-	Fail	[at least 2 attacks]
+claim	isoiec-9798-2-6-tag,B	Weakagree_B7	-	Fail	[at least 2 attacks]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..df42412
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+35
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..c581d3a
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.out	
@@ -0,0 +1,3 @@
+claim	isoiec-9798-2-1-udkey,B	Commit_B1	(A,TNA,Text1)	Ok	[no attack within bounds]
+claim	isoiec-9798-2-1-udkey,B	Alive_B2	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-1-udkey,B	Weakagree_B3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..0c647d4
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.out	
@@ -0,0 +1,3 @@
+claim	isoiec-9798-2-1,B	Commit_B1	(A,TNA,Text1)	Ok	[no attack within bounds]
+claim	isoiec-9798-2-1,B	Alive_B2	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-1,B	Weakagree_B3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..99a8dcd
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.out	
@@ -0,0 +1,3 @@
+claim	isoiec-9798-2-2-udkey,B	Commit_B1	(A,RB,Text2)	Ok	[no attack within bounds]
+claim	isoiec-9798-2-2-udkey,B	Alive_B2	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-2-udkey,B	Weakagree_B3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..86a6e87
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.out	
@@ -0,0 +1,3 @@
+claim	isoiec-9798-2-2,B	Commit_B1	(A,RB,Text2)	Ok	[no attack within bounds]
+claim	isoiec-9798-2-2,B	Alive_B2	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-2,B	Weakagree_B3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..1dd1c33
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	isoiec-9798-2-3-udkey,A	Commit_A2	(B,TNB,Text3)	Fail	[at least 1 attack]
+claim	isoiec-9798-2-3-udkey,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-3-udkey,A	Weakagree_A4	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-3-udkey,B	Commit_B2	(A,TNA,Text1)	Fail	[at least 3 attacks]
+claim	isoiec-9798-2-3-udkey,B	Alive_B3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-3-udkey,B	Weakagree_B4	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..a3905d1
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	isoiec-9798-2-3,A	Commit_A2	(B,TNB,Text3)	Fail	[at least 1 attack]
+claim	isoiec-9798-2-3,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-3,A	Weakagree_A4	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-3,B	Commit_B2	(A,TNA,Text1)	Fail	[at least 4 attacks]
+claim	isoiec-9798-2-3,B	Alive_B3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-3,B	Weakagree_B4	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..68d5a72
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	isoiec-9798-2-4-udkey,A	Commit_A2	(B,RA,RB,Text2,Text4)	Ok	[no attack within bounds]
+claim	isoiec-9798-2-4-udkey,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-4-udkey,A	Weakagree_A4	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-4-udkey,B	Commit_B2	(A,RA,RB,Text2)	Ok	[no attack within bounds]
+claim	isoiec-9798-2-4-udkey,B	Alive_B3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-4-udkey,B	Weakagree_B4	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..7b19e80
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	isoiec-9798-2-4,A	Commit_A2	(B,RA,RB,Text2,Text4)	Ok	[no attack within bounds]
+claim	isoiec-9798-2-4,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-4,A	Weakagree_A4	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-4,B	Commit_B2	(A,RA,RB,Text2)	Ok	[no attack within bounds]
+claim	isoiec-9798-2-4,B	Alive_B3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-2-4,B	Weakagree_B4	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e45b99d
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.err	
@@ -0,0 +1 @@
+warning: protocol @keysymm25 has empty role definitions for the roles: [B, P]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..69b82f2
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.out	
@@ -0,0 +1,12 @@
+claim	isoiec-9798-2-5,A	Commit_A2	(B,Kab,Text5,Text7)	Fail	[at least 3 attacks]
+claim	isoiec-9798-2-5,A	Secret_A3	Kab	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,A	Secret_A4	Text5	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,A	Secret_A5	Text7	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,A	Alive_A6	-	Fail	[at least 3 attacks]
+claim	isoiec-9798-2-5,A	Weakagree_A7	-	Fail	[at least 3 attacks]
+claim	isoiec-9798-2-5,B	Commit_B2	(A,Kab,Text5)	Fail	[at least 5 attacks]
+claim	isoiec-9798-2-5,B	Secret_B3	Kab	Ok	[no attack within bounds]
+claim	isoiec-9798-2-5,B	Secret_B4	Text5	Ok	[no attack within bounds]	time=60
+claim	isoiec-9798-2-5,B	Secret_B5	Text7	Ok	[no attack within bounds]	time=60
+claim	isoiec-9798-2-5,B	Alive_B6	-	Ok	[does not occur]	time=60
+claim	isoiec-9798-2-5,B	Weakagree_B7	-	Ok	[does not occur]	time=60
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..df21598
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+60
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..d3b1ed1
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.err	
@@ -0,0 +1 @@
+warning: protocol @keysymm26 has empty role definitions for the roles: [B, P]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..76e99d2
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.out	
@@ -0,0 +1,12 @@
+claim	isoiec-9798-2-6,A	Commit_A2	(B,Kab,Text6,Text8)	Fail	[at least 2 attacks]
+claim	isoiec-9798-2-6,A	Secret_A3	Kab	Ok	[no attack within bounds]
+claim	isoiec-9798-2-6,A	Secret_A4	Text6	Ok	[no attack within bounds]
+claim	isoiec-9798-2-6,A	Secret_A5	Text8	Ok	[no attack within bounds]
+claim	isoiec-9798-2-6,A	Alive_A6	-	Fail	[at least 2 attacks]
+claim	isoiec-9798-2-6,A	Weakagree_A7	-	Fail	[at least 2 attacks]
+claim	isoiec-9798-2-6,B	Commit_B2	(A,Kab,Text6)	Fail	[at least 2 attacks]
+claim	isoiec-9798-2-6,B	Secret_B3	Kab	Ok	[no attack within bounds]
+claim	isoiec-9798-2-6,B	Secret_B4	Text6	Ok	[no attack within bounds]
+claim	isoiec-9798-2-6,B	Secret_B5	Text8	Ok	[no attack within bounds]	time=60
+claim	isoiec-9798-2-6,B	Alive_B6	-	Ok	[does not occur]	time=60
+claim	isoiec-9798-2-6,B	Weakagree_B7	-	Ok	[does not occur]	time=60
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..df21598
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+60
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..d2e10db
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.out	
@@ -0,0 +1,3 @@
+claim	isoiec-9798-3-1,B	Commit_B1	(A,TNA,Text1)	Ok	[no attack within bounds]
+claim	isoiec-9798-3-1,B	Alive_B2	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-1,B	Weakagree_B3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..b8a62d4
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.out	
@@ -0,0 +1,3 @@
+claim	isoiec-9798-3-2,B	Commit_B1	(A,Ra,Rb,Text2)	Ok	[no attack within bounds]
+claim	isoiec-9798-3-2,B	Alive_B2	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-2,B	Weakagree_B3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..b9573d2
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	isoiec-9798-3-3,A	Commit_A2	(B,TNB,Text3)	Fail	[at least 6 attacks]
+claim	isoiec-9798-3-3,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-3,A	Weakagree_A4	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-3,B	Commit_B2	(A,TNA,Text1)	Fail	[at least 3 attacks]
+claim	isoiec-9798-3-3,B	Alive_B3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-3,B	Weakagree_B4	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..058730e
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	isoiec-9798-3-4,A	Commit_A2	(B,RA,RB,Text2,Text4)	Ok	[no attack within bounds]
+claim	isoiec-9798-3-4,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-4,A	Weakagree_A4	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-4,B	Commit_B2	(A,RA,RB,Text2)	Ok	[no attack within bounds]
+claim	isoiec-9798-3-4,B	Alive_B3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-4,B	Weakagree_B4	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..4d2a79b
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	isoiec-9798-3-5,A	Commit_A2	(B,RA,RB,Text5)	Ok	[no attack within bounds]
+claim	isoiec-9798-3-5,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-5,A	Weakagree_A4	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-5,B	Commit_B2	(A,RA,RB,Text3,Text5)	Ok	[no attack within bounds]
+claim	isoiec-9798-3-5,B	Alive_B3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-5,B	Weakagree_B4	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..571c456
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	isoiec-9798-3-6-1,A	Commit_A2	(B,Ra,Rb,Text2)	Ok	[no attack within bounds]	time=60
+claim	isoiec-9798-3-6-1,A	Alive_A3	-	Ok	[does not occur]	time=60
+claim	isoiec-9798-3-6-1,B	Commit_B2	(A,Ra,Rb,Text8)	Ok	[does not occur]	time=60
+claim	isoiec-9798-3-6-1,B	Alive_B3	-	Ok	[does not occur]	time=60
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..df21598
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+60
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..3ff3b13
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	isoiec-9798-3-6-2,A	Commit_A2	(B,Ra,Rb,Text2)	Ok	[no attack within bounds]
+claim	isoiec-9798-3-6-2,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-6-2,B	Commit_B2	(A,Ra,Rb,Text8)	Ok	[no attack within bounds]
+claim	isoiec-9798-3-6-2,B	Alive_B3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..7fda290
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+9
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..3802f29
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	isoiec-9798-3-7-1,A	Commit_A2	(B,Ra,Rb,Text8)	Ok	[no attack within bounds]	time=60
+claim	isoiec-9798-3-7-1,A	Alive_A3	-	Ok	[does not occur]	time=60
+claim	isoiec-9798-3-7-1,B	Commit_B2	(A,Ra,Rb,Text6)	Ok	[does not occur]	time=60
+claim	isoiec-9798-3-7-1,B	Alive_B3	-	Ok	[does not occur]	time=60
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..df21598
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+60
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..59c72eb
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	isoiec-9798-3-7-2,A	Commit_A2	(B,Ra,Rb,Text8)	Ok	[no attack within bounds]
+claim	isoiec-9798-3-7-2,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-3-7-2,B	Commit_B2	(A,Ra,Rb,Text6)	Ok	[no attack within bounds]
+claim	isoiec-9798-3-7-2,B	Alive_B3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..20932a6
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+7
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..103d248
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.out	
@@ -0,0 +1,3 @@
+claim	isoiec-9798-4-1-udkey,B	Commit_B1	(A,TNA,Text1)	Ok	[no attack within bounds]
+claim	isoiec-9798-4-1-udkey,B	Alive_B2	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-1-udkey,B	Weakagree_B3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..a1acda1
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.err	
@@ -0,0 +1 @@
+warning: protocol @keysymm-41 has empty role definitions for the roles: [B]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..235bc6b
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.out	
@@ -0,0 +1,3 @@
+claim	isoiec-9798-4-1,B	Commit_B1	(A,TNA,Text1)	Ok	[no attack within bounds]
+claim	isoiec-9798-4-1,B	Alive_B2	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-1,B	Weakagree_B3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..1d8fc28
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.out	
@@ -0,0 +1,3 @@
+claim	isoiec-9798-4-2-udkey,B	Commit_B1	(A,Rb,Text2)	Ok	[no attack within bounds]
+claim	isoiec-9798-4-2-udkey,B	Alive_B2	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-2-udkey,B	Weakagree_B3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..7d6a765
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.err	
@@ -0,0 +1 @@
+warning: protocol @keysymm-42 has empty role definitions for the roles: [B]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..242ec1a
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.out	
@@ -0,0 +1,3 @@
+claim	isoiec-9798-4-2,B	Commit_B1	(A,Rb,Text2)	Ok	[no attack within bounds]
+claim	isoiec-9798-4-2,B	Alive_B2	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-2,B	Weakagree_B3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..9680050
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	isoiec-9798-4-3-udkey,A	Commit_A2	(B,TNb,Text3)	Fail	[at least 1 attack]
+claim	isoiec-9798-4-3-udkey,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-3-udkey,A	Weakagree_A4	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-3-udkey,B	Commit_B2	(A,TNa,Text1)	Fail	[at least 3 attacks]
+claim	isoiec-9798-4-3-udkey,B	Alive_B3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-3-udkey,B	Weakagree_B4	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..bf87b0b
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.err	
@@ -0,0 +1 @@
+warning: protocol @keysymm-43 has empty role definitions for the roles: [B]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..3e2a2f7
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	isoiec-9798-4-3,A	Commit_A2	(B,TNb,Text3)	Fail	[at least 1 attack]
+claim	isoiec-9798-4-3,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-3,A	Weakagree_A4	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-3,B	Commit_B2	(A,TNa,Text1)	Fail	[at least 4 attacks]
+claim	isoiec-9798-4-3,B	Alive_B3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-3,B	Weakagree_B4	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..e131a97
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	isoiec-9798-4-4-udkey,A	Commit_A2	(B,Ra,Rb,Text2,Text4)	Ok	[no attack within bounds]
+claim	isoiec-9798-4-4-udkey,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-4-udkey,A	Weakagree_A4	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-4-udkey,B	Commit_B2	(A,Ra,Rb,Text2)	Ok	[no attack within bounds]
+claim	isoiec-9798-4-4-udkey,B	Alive_B3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-4-udkey,B	Weakagree_B4	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..4dd3a5a
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	isoiec-9798-4-4,A	Commit_A2	(B,Ra,Rb,Text2,Text4)	Ok	[no attack within bounds]
+claim	isoiec-9798-4-4,A	Alive_A3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-4,A	Weakagree_A4	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-4,B	Commit_B2	(A,Ra,Rb,Text2)	Ok	[no attack within bounds]
+claim	isoiec-9798-4-4,B	Alive_B3	-	Ok	[no attack within bounds]
+claim	isoiec-9798-4-4,B	Weakagree_B4	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..32a0a19
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	andrew-Concrete,I	Secret_I1	kir	Ok	[no attack within bounds]
+claim	andrew-Concrete,I	Nisynch_I2	-	Fail	[at least 1 attack]
+claim	andrew-Concrete,R	Secret_R1	kir	Ok	[no attack within bounds]
+claim	andrew-Concrete,R	Nisynch_R2	-	Fail	[at least 1 attack]
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..2011c4f
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.out	
@@ -0,0 +1,8 @@
+claim	andrew-Ban,I	Nisynch_I1	-	Ok	[proof of correctness]
+claim	andrew-Ban,I	Niagree_I2	-	Ok	[proof of correctness]
+claim	andrew-Ban,I	Secret_I3	kir	Ok	[proof of correctness]
+claim	andrew-Ban,I	Secret_I4	k(I,R)	Ok	[proof of correctness]
+claim	andrew-Ban,R	Nisynch_R1	-	Ok	[proof of correctness]
+claim	andrew-Ban,R	Niagree_R2	-	Ok	[proof of correctness]
+claim	andrew-Ban,R	Secret_R3	kir	Ok	[proof of correctness]
+claim	andrew-Ban,R	Secret_R4	k(I,R)	Ok	[proof of correctness]
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..91fc492
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	andrew-LoweBan,I	Nisynch_I1	-	Ok	[proof of correctness]
+claim	andrew-LoweBan,I	Secret_I2	kir	Ok	[proof of correctness]
+claim	andrew-LoweBan,R	Nisynch_R1	-	Ok	[proof of correctness]
+claim	andrew-LoweBan,R	Secret_R2	kir	Ok	[proof of correctness]
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..ec24c37
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	andrew,I	Secret_I1	kir	Ok	[no attack within bounds]
+claim	andrew,I	Nisynch_I2	-	Fail	[at least 1 attack]
+claim	andrew,I	Niagree_I3	-	Fail	[at least 1 attack]
+claim	andrew,R	Secret_R1	kir	Ok	[no attack within bounds]
+claim	andrew,R	Nisynch_R2	-	Ok	[no attack within bounds]
+claim	andrew,R	Niagree_R3	-	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..97d01d7
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+14
diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..0fddf90
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.out	
@@ -0,0 +1 @@
+claim	ccitt509-1,R	Nisynch_3	-	Ok	[proof of correctness]
diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..710d27e
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.out	
@@ -0,0 +1 @@
+claim	ccitt509-1c,R	Nisynch_3	-	Ok	[proof of correctness]
diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..bf351ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	ccitt509-3,I	Nisynch_I1	-	Ok	[proof of correctness]
+claim	ccitt509-3,I	Secret_I2	Ya	Ok	[proof of correctness]
+claim	ccitt509-3,I	Secret_I3	Yb	Ok	[proof of correctness]
+claim	ccitt509-3,R	Nisynch_R1	-	Fail	[at least 3 attacks]
+claim	ccitt509-3,R	Secret_R2	Ya	Ok	[no attack within bounds]
+claim	ccitt509-3,R	Secret_R3	Yb	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..c711226
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.out	
@@ -0,0 +1,2 @@
+claim	ccitt509-ban3,I	Nisynch_4	-	Ok	[proof of correctness]
+claim	ccitt509-ban3,R	Nisynch_5	-	Ok	[proof of correctness]
diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..3ea7e70
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	denningSacco-Lowe,I	Niagree_I1	-	Ok	[no attack within bounds]
+claim	denningSacco-Lowe,I	Nisynch_I2	-	Fail	[at least 1 attack]
+claim	denningSacco-Lowe,I	SKR_I3	Kir	Ok	[no attack within bounds]
+claim	denningSacco-Lowe,R	Niagree_R1	-	Ok	[no attack within bounds]
+claim	denningSacco-Lowe,R	Nisynch_R2	-	Fail	[at least 1 attack]
+claim	denningSacco-Lowe,R	Secret_R3	Kir	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..5f53683
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	denningSacco,I	Niagree_I1	-	Ok	[no attack within bounds]
+claim	denningSacco,I	Nisynch_I2	-	Fail	[at least 1 attack]
+claim	denningSacco,I	Secret_I3	Kir	Ok	[no attack within bounds]
+claim	denningSacco,R	Niagree_R1	-	Ok	[no attack within bounds]
+claim	denningSacco,R	Nisynch_R2	-	Fail	[at least 1 attack]
+claim	denningSacco,R	Secret_R3	Kir	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..f42247a
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	kaochow-2,I	Nisynch_I1	-	Fail	[at least 2 attacks]
+claim	kaochow-2,I	Niagree_I2	-	Fail	[at least 2 attacks]
+claim	kaochow-2,I	Secret_I3	kir	Ok	[no attack within bounds]
+claim	kaochow-2,R	Nisynch_R1	-	Fail	[at least 2 attacks]
+claim	kaochow-2,R	Niagree_R2	-	Fail	[at least 2 attacks]
+claim	kaochow-2,R	Secret_R3	kir	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..4674dbd
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+5
diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..f3cf440
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	kaochow-3,I	Nisynch_I1	-	Fail	[at least 2 attacks]
+claim	kaochow-3,I	Niagree_I2	-	Fail	[at least 2 attacks]
+claim	kaochow-3,I	Secret_I3	kir	Ok	[no attack within bounds]
+claim	kaochow-3,R	Nisynch_R1	-	Fail	[at least 2 attacks]
+claim	kaochow-3,R	Niagree_R2	-	Fail	[at least 2 attacks]
+claim	kaochow-3,R	Secret_R3	kir	Ok	[no attack within bounds]	time=60
diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..df21598
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+60
diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..5e05c55
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	kaochow,I	Nisynch_I1	-	Fail	[at least 2 attacks]
+claim	kaochow,I	Niagree_I2	-	Fail	[at least 2 attacks]
+claim	kaochow,I	Secret_I3	kir	Ok	[no attack within bounds]
+claim	kaochow,R	Nisynch_R1	-	Fail	[at least 2 attacks]
+claim	kaochow,R	Niagree_R2	-	Fail	[at least 2 attacks]
+claim	kaochow,R	Secret_R3	kir	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..a4bc84c
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+2
diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..81a7e6f
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	needhamschroederpk-Lowe,I	Secret_I1	Ni	Ok	[no attack within bounds]
+claim	needhamschroederpk-Lowe,I	Secret_I2	Nr	Ok	[no attack within bounds]
+claim	needhamschroederpk-Lowe,I	Nisynch_I3	-	Fail	[at least 3 attacks]
+claim	needhamschroederpk-Lowe,R	Secret_R1	Nr	Ok	[no attack within bounds]
+claim	needhamschroederpk-Lowe,R	Secret_R2	Ni	Ok	[no attack within bounds]
+claim	needhamschroederpk-Lowe,R	Nisynch_R3	-	Fail	[at least 3 attacks]
diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..37da462
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+23
diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..38f78d0
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	needhamschroedersk-amend,I	Secret_I2	Kir	Ok	[no attack within bounds]
+claim	needhamschroedersk-amend,I	Nisynch_I3	-	Fail	[at least 1 attack]
+claim	needhamschroedersk-amend,R	Secret_R1	Nr	Ok	[no attack within bounds]
+claim	needhamschroedersk-amend,R	Nisynch_R3	-	Fail	[at least 1 attack]
diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..a4bc84c
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+2
diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..d8d506e
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	needhamschroederpk,I	Secret_I1	Ni	Ok	[no attack within bounds]
+claim	needhamschroederpk,I	Secret_I2	Nr	Ok	[no attack within bounds]
+claim	needhamschroederpk,I	Nisynch_I3	-	Fail	[at least 3 attacks]
+claim	needhamschroederpk,R	Secret_R1	Nr	Fail	[at least 7 attacks]
+claim	needhamschroederpk,R	Secret_R2	Ni	Fail	[at least 7 attacks]
+claim	needhamschroederpk,R	Nisynch_R3	-	Fail	[at least 3 attacks]
diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..27fb100
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+28
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..89b9ed9
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.err	
@@ -0,0 +1 @@
+error: fresh terms [Kir] should be declared inside roles, on line 19.
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..89b9ed9
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.err	
@@ -0,0 +1 @@
+error: fresh terms [Kir] should be declared inside roles, on line 19.
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..153113f
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	neustub-Hwang,I	Secret_I1	Kir	Ok	[no attack within bounds]	time=60
+claim	neustub-Hwang,I	Niagree_I2	-	Ok	[does not occur]	time=60
+claim	neustub-Hwang,I	Nisynch_I3	-	Ok	[does not occur]	time=60
+claim	neustub-Hwang,R	Secret_R1	Kir	Ok	[no attack within bounds]	time=60
+claim	neustub-Hwang,R	Niagree_R2	-	Ok	[does not occur]	time=60
+claim	neustub-Hwang,R	Nisynch_R3	-	Ok	[does not occur]	time=60
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..df21598
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+60
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..89b9ed9
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.err	
@@ -0,0 +1 @@
+error: fresh terms [Kir] should be declared inside roles, on line 19.
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e52a51e
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.err	
@@ -0,0 +1 @@
+error: fresh terms [Kir] should be declared inside roles, on line 16.
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..15e3371
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.out	
@@ -0,0 +1 @@
+claim	smartright,R	Nisynch_R1	-	Fail	[at least 1 attack]
diff --git a/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..cdd6305
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	spliceAS-HC,I	Secret_7	N2	Ok	[no attack within bounds]	time=60
+claim	spliceAS-HC,I	Niagree_9	-	Ok	[does not occur]	time=60
+claim	spliceAS-HC,I	Nisynch_10	-	Ok	[does not occur]	time=60
+claim	spliceAS-HC,R	Secret_8	N2	Ok	[no attack within bounds]	time=60
+claim	spliceAS-HC,R	Niagree_11	-	Ok	[does not occur]	time=60
+claim	spliceAS-HC,R	Nisynch_12	-	Ok	[does not occur]	time=60
diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..df21598
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+60
diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..a8474fb
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out	
@@ -0,0 +1,6 @@
+claim	spliceAS,I	Secret_7	N2	Ok	[no attack within bounds]	time=60
+claim	spliceAS,I	Niagree_9	-	Ok	[does not occur]	time=60
+claim	spliceAS,I	Nisynch_10	-	Ok	[does not occur]	time=60
+claim	spliceAS,R	Secret_8	N2	Ok	[no attack within bounds]	time=60
+claim	spliceAS,R	Niagree_11	-	Ok	[does not occur]	time=60
+claim	spliceAS,R	Nisynch_12	-	Ok	[does not occur]	time=60
diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..df21598
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+60
diff --git a/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..a6a11dd
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	tmn,I	Secret_I1	Kr	Fail	[at least 4 attacks]
+claim	tmn,I	Nisynch_I2	-	Fail	[at least 2 attacks]
+claim	tmn,R	Secret_R1	Kr	Fail	[at least 2 attacks]
+claim	tmn,R	Nisynch_R2	-	Fail	[exactly 1 attack]
diff --git a/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..1fb959d
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	wmf-Lowe,I	Secret_I1	Kir	Ok	[no attack within bounds]
+claim	wmf-Lowe,I	Nisynch_I2	-	Fail	[at least 3 attacks]
+claim	wmf-Lowe,R	Secret_R1	Kir	Ok	[no attack within bounds]
+claim	wmf-Lowe,R	Nisynch_R2	-	Fail	[at least 3 attacks]
diff --git a/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..039a65a
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.out	
@@ -0,0 +1,3 @@
+claim	wmf,I	Secret_I1	Kir	Ok	[no attack within bounds]
+claim	wmf,R	Secret_R1	Kir	Ok	[no attack within bounds]
+claim	wmf,R	Nisynch_R2	-	Fail	[at least 3 attacks]
diff --git a/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..3ac7ab5
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.out	
@@ -0,0 +1 @@
+claim	woolamPi-1,R	Nisynch_R1	-	Fail	[at least 2 attacks]
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..63b6634
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.out	
@@ -0,0 +1 @@
+claim	woolamPi-2,R	Nisynch_R1	-	Fail	[at least 3 attacks]
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..756742c
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.out	
@@ -0,0 +1 @@
+claim	woolamPi-3,R	Nisynch_R1	-	Fail	[at least 2 attacks]
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..eb93f90
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.out	
@@ -0,0 +1 @@
+claim	woolamPi-f,R	Nisynch_R1	-	Fail	[at least 1 attack]
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..233b5fc
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.out	
@@ -0,0 +1 @@
+claim	woolamPi,R	Nisynch_R1	-	Fail	[at least 4 attacks]
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..f34f204
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	woolam,I	Secret_I1	Kir	Ok	[no attack within bounds]
+claim	woolam,I	Nisynch_I2	-	Fail	[at least 2 attacks]
+claim	woolam,R	Secret_R1	Kir	Ok	[no attack within bounds]
+claim	woolam,R	Nisynch_R2	-	Fail	[at least 2 attacks]
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..b449a72
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+36
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..d2006f0
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	yahalom-BAN,I	Secret_I1	Kir	Ok	[no attack within bounds]
+claim	yahalom-BAN,I	Nisynch_I2	-	Fail	[at least 1 attack]
+claim	yahalom-BAN,R	Secret_R1	Kir	Ok	[no attack within bounds]
+claim	yahalom-BAN,R	Nisynch_R2	-	Fail	[at least 2 attacks]
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..1d1be5a
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	yahalom-Lowe,I	Secret_I1	Kir	Ok	[proof of correctness]
+claim	yahalom-Lowe,I	Nisynch_I2	-	Ok	[proof of correctness]
+claim	yahalom-Lowe,R	Secret_R1	Kir	Ok	[proof of correctness]
+claim	yahalom-Lowe,R	Nisynch_R2	-	Ok	[proof of correctness]
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..ea12ec0
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	yahalom-Paulson,I	Secret_I1	Kir	Ok	[no attack within bounds]
+claim	yahalom-Paulson,I	Nisynch_I2	-	Fail	[at least 1 attack]
+claim	yahalom-Paulson,R	Secret_R1	Kir	Ok	[no attack within bounds]
+claim	yahalom-Paulson,R	Nisynch_R2	-	Fail	[at least 1 attack]
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..5606f67
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.out	
@@ -0,0 +1,4 @@
+claim	yahalom,I	Secret_I1	Kir	Ok	[no attack within bounds]
+claim	yahalom,R	Secret_R1	Kir	Ok	[no attack within bounds]
+claim	yahalom,S	Secret_S1	Ni	Fail	[at least 1 attack]
+claim	yahalom,S	Secret_S2	Nr	Ok	[no attack within bounds]
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..fa4ead8
--- /dev/null
+++ b/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.out	
@@ -0,0 +1,16 @@
+claim	nsl3,I	Secret_i1	ni	Fail	[at least 2 attacks]
+claim	nsl3,I	Secret_i2	nr	Fail	[at least 1 attack]
+claim	nsl3,I	Niagree_i3	-	Fail	[at least 1 attack]
+claim	nsl3,I	Nisynch_i4	-	Fail	[at least 1 attack]
+claim	nsl3,R	Secret_r1	ni	Fail	[at least 2 attacks]
+claim	nsl3,R	Secret_r2	nr	Ok	[proof of correctness]
+claim	nsl3,R	Niagree_r3	-	Fail	[at least 1 attack]
+claim	nsl3,R	Nisynch_r4	-	Fail	[at least 1 attack]
+claim	nsl3-broken,I	Secret_i1	ni	Fail	[at least 1 attack]
+claim	nsl3-broken,I	Secret_i2	nr	Fail	[at least 1 attack]
+claim	nsl3-broken,I	Niagree_i3	-	Fail	[at least 1 attack]
+claim	nsl3-broken,I	Nisynch_i4	-	Fail	[at least 1 attack]
+claim	nsl3-broken,R	Secret_r1	ni	Fail	[at least 1 attack]
+claim	nsl3-broken,R	Secret_r2	nr	Ok	[proof of correctness]
+claim	nsl3-broken,R	Niagree_r3	-	Fail	[at least 1 attack]
+claim	nsl3-broken,R	Nisynch_r4	-	Fail	[at least 1 attack]
diff --git a/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..39d339c
--- /dev/null
+++ b/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.out	
@@ -0,0 +1,8 @@
+claim	nsl3-broken,I	Secret_i1	ni	Fail	[at least 1 attack]
+claim	nsl3-broken,I	Secret_i2	nr	Fail	[at least 1 attack]
+claim	nsl3-broken,I	Niagree_i3	-	Fail	[at least 1 attack]
+claim	nsl3-broken,I	Nisynch_i4	-	Fail	[at least 1 attack]
+claim	nsl3-broken,R	Secret_r1	ni	Fail	[at least 1 attack]
+claim	nsl3-broken,R	Secret_r2	nr	Ok	[proof of correctness]
+claim	nsl3-broken,R	Niagree_r3	-	Ok	[proof of correctness]
+claim	nsl3-broken,R	Nisynch_r4	-	Ok	[proof of correctness]
diff --git a/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..b61e892
--- /dev/null
+++ b/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.out	
@@ -0,0 +1,14 @@
+claim	nsl3,I	Secret_I2	ni	Ok	[proof of correctness]
+claim	nsl3,I	Secret_I3	nr	Ok	[proof of correctness]
+claim	nsl3,I	Alive_I4	-	Ok	[proof of correctness]
+claim	nsl3,I	Weakagree_I5	-	Ok	[proof of correctness]
+claim	nsl3,I	Commit_I6	(R,ni,nr)	Ok	[proof of correctness]
+claim	nsl3,I	Niagree_I7	-	Ok	[proof of correctness]
+claim	nsl3,I	Nisynch_I8	-	Ok	[proof of correctness]
+claim	nsl3,R	Secret_R2	ni	Ok	[proof of correctness]
+claim	nsl3,R	Secret_R3	nr	Ok	[proof of correctness]
+claim	nsl3,R	Alive_R4	-	Ok	[proof of correctness]
+claim	nsl3,R	Weakagree_R5	-	Ok	[proof of correctness]
+claim	nsl3,R	Commit_R6	(I,ni,nr)	Ok	[proof of correctness]
+claim	nsl3,R	Niagree_R7	-	Ok	[proof of correctness]
+claim	nsl3,R	Nisynch_R8	-	Ok	[proof of correctness]
diff --git a/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.err
new file mode 100644
index 0000000..e69de29
diff --git a/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.out
new file mode 100644
index 0000000..f4d4594
--- /dev/null
+++ b/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.out	
@@ -0,0 +1,14 @@
+claim	ns3,I	Secret_I2	ni	Ok	[proof of correctness]
+claim	ns3,I	Secret_I3	nr	Ok	[proof of correctness]
+claim	ns3,I	Alive_I4	-	Ok	[proof of correctness]
+claim	ns3,I	Weakagree_I5	-	Ok	[proof of correctness]
+claim	ns3,I	Commit_I6	(R,ni,nr)	Ok	[proof of correctness]
+claim	ns3,I	Niagree_I7	-	Ok	[proof of correctness]
+claim	ns3,I	Nisynch_I8	-	Ok	[proof of correctness]
+claim	ns3,R	Secret_R2	ni	Fail	[at least 1 attack]
+claim	ns3,R	Secret_R3	nr	Fail	[at least 1 attack]
+claim	ns3,R	Alive_R4	-	Ok	[proof of correctness]
+claim	ns3,R	Weakagree_R5	-	Fail	[at least 1 attack]
+claim	ns3,R	Commit_R6	(I,ni,nr)	Fail	[at least 1 attack]
+claim	ns3,R	Niagree_R7	-	Fail	[at least 1 attack]
+claim	ns3,R	Nisynch_R8	-	Fail	[at least 1 attack]
diff --git a/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.time
new file mode 100644
index 0000000..80f32ca
--- /dev/null
+++ b/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.time	
@@ -0,0 +1,2 @@
+Passed wall time in seconds:
+0
diff --git a/src/regression-tests/tests.txt b/src/regression-tests/tests.txt
new file mode 100644
index 0000000..65ed360
--- /dev/null
+++ b/src/regression-tests/tests.txt
@@ -0,0 +1,316 @@
+# Test file for scyther
+#
+# Essentially contains argument lines for the tool, where the first
+# argument is the file name, relative to the base directory of the
+# repository.
+#
+# For each, we then record the output.
+#
+# Empty lines or lines starting with '%' or '#' are not considered.
+# Lines with '=' set the "global" concatenation.
+#
+= --timer=60 --plain
+# testing/bke.spdl 
+# testing/bke-one.spdl
+# testing/ibe.spdl
+# testing/otwayrees.spdl
+# testing/ns-symmetric.spdl
+# testing/bkepk-ce.spdl
+# testing/unknown2.spdl
+# testing/splice-as.spdl
+# testing/nst2.spdl
+# testing/boyd.spdl
+testing/ksl.spdl -r3
+# testing/andrew-ban.spdl
+# testing/tmn.spdl
+# testing/carkey-broken-limited.spdl
+# testing/bunava-1-4.spdl
+# testing/soph.spdl
+# testing/kaochow-v2.spdl
+# testing/2r890-ex3-a.spdl
+# testing/tmn-Gijs.spdl
+# testing/nsl3-nisynch-rep.spdl
+# testing/ns3.spdl
+# testing/yahalom-paulson.spdl
+# testing/localclaims-seq1.spdl
+# testing/bke-variation.spdl
+# testing/localclaims.spdl
+# testing/carkey-ni2.spdl
+# testing/broken1.spdl
+# testing/gong-nonce-b.spdl
+# testing/isoiec11770-2-13.spdl
+# testing/ccitt509-ban.spdl
+# testing/bunava-2-3.spdl
+# testing/wmf-brutus.spdl
+# testing/five-run-bound.spdl
+# testing/tls/tls-BM-1.spdl
+# testing/tls/tls-HSDDM05-2.spdl
+# testing/tls/tls-HSDDM05-fix.spdl
+# testing/tls/tls-HSDDM05.spdl
+# testing/tls/tls-paulson.spdl
+# testing/tls/tls-paulson-avispa.spdl
+# testing/ns-symmetric-amended.spdl
+# testing/bunava-2-4.spdl
+# testing/soph-keyexch.spdl
+# testing/gong-nonce.spdl
+# testing/splice-as-hc.spdl
+# testing/onetrace.spdl
+# testing/woolam-pi-f.spdl
+# testing/nst1.spdl
+# testing/nsl3.spdl
+# testing/andrew-lowe-ban.spdl
+# testing/kaochow-palm.spdl
+# testing/yahalom-lowe.spdl
+# testing/speedtest.spdl
+# testing/carkey-ni.spdl
+# testing/woolam-cmv.spdl
+# testing/compositionality-examples/th-1.spdl
+# testing/compositionality-examples/th-1seq2-rename-ni.spdl
+# testing/compositionality-examples/th-1seq2-rename-nr.spdl
+# testing/compositionality-examples/th-2.spdl
+# testing/compositionality-examples/th-1seq2.spdl
+# testing/compositionality-examples/th-1par2.spdl
+# testing/samasc-broken.spdl
+# testing/kaochow.spdl
+# testing/splice-as-hc-cj.spdl
+# testing/2r890-ex3-b.spdl
+# testing/carkey-broken.spdl
+# testing/denning-sacco-shared.spdl
+# testing/kaochow-v3.spdl
+# testing/fourway-HSDDM05.spdl
+# testing/bke-broken.spdl
+# testing/simplest.spdl
+# testing/kerberos-rddm.spdl
+# testing/f5.spdl
+# testing/yahalom-ban.spdl
+# testing/ns3-brutus.spdl
+# testing/ibe-ns.spdl
+# testing/boyd-nsl-fix.spdl
+# testing/localclaims-breaker.spdl
+# testing/helloworld.spdl
+# testing/bkepk-ce2.spdl
+# testing/bunava-1-3.spdl
+# testing/athena-breaker.spdl
+# testing/f4.spdl
+# gui/yhl.spdl
+# gui/Protocols-reachable/reach_yahalom-lowe.spdl
+# gui/Protocols-reachable/reach_woo-lam-pi-f.spdl
+# gui/Protocols-reachable/reach_splice-as.spdl
+# gui/Protocols-reachable/reach_kaochow-v2.spdl
+# gui/Protocols-reachable/reach_wmf-lowe.spdl
+# gui/Protocols-reachable/reach_woo-lam-pi-1.spdl
+# gui/Protocols-reachable/reach_needham-schroeder-sk.spdl
+# gui/Protocols-reachable/reach_neumannstub-guttman.spdl
+# gui/Protocols-reachable/reach_splice-as-hc.spdl
+# gui/Protocols-reachable/reach_tmn.spdl
+# gui/Protocols-reachable/reach_needham-schroeder-lowe.spdl
+# gui/Protocols-reachable/reach_woo-lam-pi.spdl
+# gui/Protocols-reachable/reach_yahalom-ban-paulson.spdl
+# gui/Protocols-reachable/reach_ccitt509-3.spdl
+# gui/Protocols-reachable/reach_woo-lam-pi-2.spdl
+# gui/Protocols-reachable/reach_kaochow-v3.spdl
+# gui/Protocols-reachable/reach_neumannstub-guttman-hwang.spdl
+# gui/Protocols-reachable/reach_denning-sacco.spdl
+# gui/Protocols-reachable/reach_yahalom.spdl
+# gui/Protocols-reachable/reach_kaochow.spdl
+# gui/Protocols-reachable/reach_andrew-lowe-ban.spdl
+# gui/Protocols-reachable/reach_woo-lam.spdl
+# gui/Protocols-reachable/reach_neumannstub-keycompromise.spdl
+# gui/Protocols-reachable/reach_wmf.spdl
+# gui/Protocols-reachable/reach_ccitt509-1c.spdl
+# gui/Protocols-reachable/reach_ccitt509-ban3.spdl
+# gui/Protocols-reachable/reach_neumannstub-hwang.spdl
+# gui/Protocols-reachable/reach_needham-schroeder-sk-amend.spdl
+# gui/Protocols-reachable/reach_splice-as-cj.spdl
+# gui/Protocols-reachable/reach_BKE.spdl
+# gui/Protocols-reachable/reach_andrew-ban-concrete.spdl
+# gui/Protocols-reachable/reach_andrew-ban.spdl
+# gui/Protocols-reachable/reach_otwayrees.spdl
+# gui/Protocols-reachable/reach_andrew.spdl
+# gui/Protocols-reachable/reach_denning-sacco-lowe.spdl
+# gui/Protocols-reachable/reach_yahalom-paulson.spdl
+# gui/Protocols-reachable/reach_neumannstub.spdl
+# gui/Protocols-reachable/reach_TLS-Paulson.spdl
+# gui/Protocols-reachable/reach_yahalom-ban.spdl
+# gui/Protocols-reachable/reach_ccitt509-1.spdl
+# gui/Protocols-reachable/reach_needham-schroeder.spdl
+# gui/Protocols-reachable/reach_smartright.spdl
+# gui/Protocols-reachable/reach_woo-lam-pi-3.spdl
+# gui/ns3.spdl
+# gui/nsl3-ibake.spdl
+# gui/Protocols/otwayrees.spdl
+# gui/Protocols/splice-as-cj.spdl
+# gui/Protocols/MultiProtocolAttacks/otwayrees.spdl
+# gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl
+# gui/Protocols/MultiProtocolAttacks/splice-as.spdl
+# gui/Protocols/MultiProtocolAttacks/boyd.spdl
+# gui/Protocols/MultiProtocolAttacks/ksl.spdl
+# gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl
+# gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl
+# gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl
+# gui/Protocols/MultiProtocolAttacks/tmn.spdl
+# gui/Protocols/MultiProtocolAttacks/soph.spdl
+# gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl
+# gui/Protocols/MultiProtocolAttacks/ns3.spdl
+# gui/Protocols/MultiProtocolAttacks/woo-lam-pi-2.spdl
+# gui/Protocols/MultiProtocolAttacks/woo-lam-pi-3.spdl
+# gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl
+# gui/Protocols/MultiProtocolAttacks/woo-lam-pi-1.spdl
+# gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl
+# gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl
+# gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl
+# gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl
+# gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl
+# gui/Protocols/MultiProtocolAttacks/wmf.spdl
+# gui/Protocols/MultiProtocolAttacks/yahalom.spdl
+# gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl
+# gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl
+# gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl
+# gui/Protocols/MultiProtocolAttacks/BKE.spdl
+# gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl
+# gui/Protocols/MultiProtocolAttacks/woo-lam.spdl
+# gui/Protocols/MultiProtocolAttacks/nsl3.spdl
+# gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl
+# gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl
+# gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl
+# gui/Protocols/MultiProtocolAttacks/kaochow.spdl
+# gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl
+# gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl
+# gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl
+gui/Protocols/splice-as.spdl
+gui/Protocols/ksl.spdl -r3
+gui/Protocols/andrew-ban.spdl
+gui/Protocols/denning-sacco-lowe.spdl
+gui/Protocols/needham-schroeder-sk-amend.spdl
+gui/Protocols/tmn.spdl
+gui/Protocols/andrew.spdl
+gui/Protocols/neumannstub-guttman.spdl
+gui/Protocols/kaochow-v2.spdl
+gui/Protocols/ccitt509-1.spdl
+gui/Protocols/ccitt509-1c.spdl
+gui/Protocols/yahalom-paulson.spdl
+gui/Protocols/woo-lam-pi-2.spdl
+gui/Protocols/Demo/ns3.spdl
+gui/Protocols/Demo/nsl3-updated-both.spdl
+gui/Protocols/Demo/nsl3.spdl
+gui/Protocols/Demo/nsl3-broken.spdl
+gui/Protocols/woo-lam-pi-3.spdl
+gui/Protocols/woo-lam-pi.spdl
+gui/Protocols/needham-schroeder-lowe.spdl
+gui/Protocols/woo-lam-pi-1.spdl
+gui/Protocols/ccitt509-ban3.spdl
+gui/Protocols/denning-sacco.spdl
+gui/Protocols/wmf-lowe.spdl
+gui/Protocols/wmf.spdl
+# gui/Protocols/IEEE-WIMAX/rsaplussatek.spdl
+# gui/Protocols/IEEE-WIMAX/pkmv2rsa-noid.spdl
+# gui/Protocols/IEEE-WIMAX/rsaplussatekcorrected.spdl
+# gui/Protocols/IEEE-WIMAX/pkmv2rsa.spdl
+# gui/Protocols/IEEE-WIMAX/pkmv2rsacorrected.spdl
+# gui/Protocols/IEEE-WIMAX/pkmv2satek.spdl
+# gui/Protocols/IEEE-WIMAX/pqr.spdl
+gui/Protocols/neumannstub-hwang.spdl
+gui/Protocols/yahalom.spdl
+gui/Protocols/splice-as-hc.spdl
+# gui/Protocols/needham-schroeder-sk.spdl
+gui/Protocols/ISO-9798/isoiec-9798-3-7-1.spdl
+gui/Protocols/ISO-9798/isoiec-9798-2-4.spdl
+gui/Protocols/ISO-9798/isoiec-9798-3-6-2.spdl
+gui/Protocols/ISO-9798/isoiec-9798-4-2-udkey.spdl
+gui/Protocols/ISO-9798/isoiec-9798-2-2.spdl
+gui/Protocols/ISO-9798/isoiec-9798-4-3.spdl
+gui/Protocols/ISO-9798/isoiec-9798-3-1.spdl
+gui/Protocols/ISO-9798/isoiec-9798-4-4.spdl
+gui/Protocols/ISO-9798/isoiec-9798-2-6.spdl
+gui/Protocols/ISO-9798/isoiec-9798-3-2.spdl
+gui/Protocols/ISO-9798/isoiec-9798-3-5.spdl
+gui/Protocols/ISO-9798/isoiec-9798-3-4.spdl
+gui/Protocols/ISO-9798/iso26-tag.spdl
+gui/Protocols/ISO-9798/isoiec-9798-4-3-udkey.spdl
+gui/Protocols/ISO-9798/isoiec-9798-2-1-udkey.spdl
+gui/Protocols/ISO-9798/isoiec-9798-2-2-udkey.spdl
+gui/Protocols/ISO-9798/isoiec-9798-2-4-udkey.spdl
+gui/Protocols/ISO-9798/iso25-tag.spdl
+gui/Protocols/ISO-9798/isoiec-9798-4-2.spdl
+gui/Protocols/ISO-9798/isoiec-9798-2-1.spdl
+gui/Protocols/ISO-9798/isoiec-9798-2-3-udkey.spdl
+gui/Protocols/ISO-9798/isoiec-9798-3-7-2.spdl
+gui/Protocols/ISO-9798/isoiec-9798-2-3.spdl
+gui/Protocols/ISO-9798/isoiec-9798-4-1.spdl
+gui/Protocols/ISO-9798/isoiec-9798-2-5.spdl
+gui/Protocols/ISO-9798/isoiec-9798-4-1-udkey.spdl
+gui/Protocols/ISO-9798/isoiec-9798-3-3.spdl
+gui/Protocols/ISO-9798/isoiec-9798-3-6-1.spdl
+gui/Protocols/ISO-9798/isoiec-9798-4-4-udkey.spdl
+gui/Protocols/neumannstub.spdl
+gui/Protocols/neumannstub-guttman-hwang.spdl
+gui/Protocols/woo-lam.spdl
+gui/Protocols/andrew-lowe-ban.spdl
+gui/Protocols/andrew-ban-concrete.spdl
+gui/Protocols/yahalom-lowe.spdl
+gui/Protocols/needham-schroeder.spdl
+gui/Protocols/kaochow.spdl
+gui/Protocols/ccitt509-3.spdl
+gui/Protocols/ksl-lowe.spdl -r3
+gui/Protocols/woo-lam-pi-f.spdl
+gui/Protocols/smartright.spdl
+gui/Protocols/kaochow-v3.spdl
+gui/Protocols/yahalom-ban.spdl
+gui/Protocols/neumannstub-keycompromise.spdl
+# gui/Protocols/IKE/ikev1-pk2-m.spdl
+# gui/Protocols/IKE/ikev1-quick-nopfs.spdl
+# gui/Protocols/IKE/ikev2-sig-child2-composed.spdl
+# gui/Protocols/IKE/ikev1-pk2-a2.spdl
+# gui/Protocols/IKE/ikev1-psk-a.spdl
+# gui/Protocols/IKE/sts-mac.spdl
+# gui/Protocols/IKE/ikev2-eap2.spdl
+# gui/Protocols/IKE/oakley-a.spdl
+# gui/Protocols/IKE/jfkr.spdl
+# gui/Protocols/IKE/jfki-core.spdl
+# gui/Protocols/IKE/ikev2-child-nopfs.spdl
+# gui/Protocols/IKE/ikev1-psk-m-perlman.spdl
+# gui/Protocols/IKE/ikev2-sig-child-composed.spdl
+# gui/Protocols/IKE/ikev2-sig-child2.spdl
+# gui/Protocols/IKE/ikev2-mac2.spdl
+# gui/Protocols/IKE/oakley-c.spdl
+# gui/Protocols/IKE/ikev1-pk-a12.spdl
+# gui/Protocols/IKE/ikev1-quick.spdl
+# gui/Protocols/IKE/sts-main.spdl
+# gui/Protocols/IKE/ikev1-quick-noid.spdl
+# gui/Protocols/IKE/ikev1-pk-a1.spdl
+# gui/Protocols/IKE/ikev2-sigtomac.spdl
+# gui/Protocols/IKE/ikev1-pk2-a.spdl
+# gui/Protocols/IKE/jfkr-core.spdl
+# gui/Protocols/IKE/oakley-alt.spdl
+# gui/Protocols/IKE/ikev1-pk-m.spdl
+# gui/Protocols/IKE/ikev1-sig-m-perlman.spdl
+# gui/Protocols/IKE/ikev1-sig-a-perlman2.spdl
+# gui/Protocols/IKE/ikev1-sig-m.spdl
+# gui/Protocols/IKE/jfki.spdl
+# gui/Protocols/IKE/ikev1-sig-a1.spdl
+# gui/Protocols/IKE/skeme-rekey.spdl
+# gui/Protocols/IKE/skeme-basic.spdl
+# gui/Protocols/IKE/ikev2-sig-child.spdl
+# gui/Protocols/IKE/skeme-psk.spdl
+# gui/Protocols/IKE/ikev1-pk-a22.spdl
+# gui/Protocols/IKE/ikev2-child.spdl
+# gui/Protocols/IKE/ikev2-mac.spdl
+# gui/Protocols/IKE/ikev2-eap.spdl
+# gui/Protocols/IKE/sts-modified.spdl
+# gui/Protocols/IKE/ikev1-sig-a-perlman1.spdl
+# gui/Protocols/IKE/ikev2-mactosig.spdl
+# gui/Protocols/IKE/ikev1-psk-m.spdl
+# gui/Protocols/IKE/ikev1-pk-a2.spdl
+# gui/Protocols/IKE/ikev2-sig.spdl
+# gui/Protocols/IKE/ikev2-sigtomac2.spdl
+# gui/Protocols/IKE/ikev1-pk2-m2.spdl
+# gui/Protocols/IKE/ikev1-sig-a2.spdl
+# gui/Protocols/IKE/ikev2-sig2.spdl
+# gui/Protocols/IKE/ikev2-mactosig2.spdl
+# gui/Protocols/IKE/ikev1-pk-m2.spdl
+gui/nsl3.spdl
+gui/mpa.spdl
+gui/nsl3-broken.spdl
+src/ns3.spdl
+
+