From f8e76a5308d2752b6402d0bea5096e54a16b8ec6 Mon Sep 17 00:00:00 2001
From: GadiTellez <gadi.tellez.isc@gmail.com>
Date: Sat, 25 Feb 2017 11:48:16 +0000
Subject: [PATCH] Added script to execute test suite

---
 cade-temporal-tests.sh | 88 ++++++++++++++++++++++++++++++++++++++++++
 examples/bt.def        |  4 ++
 2 files changed, 92 insertions(+)
 create mode 100755 cade-temporal-tests.sh
 create mode 100644 examples/bt.def

diff --git a/cade-temporal-tests.sh b/cade-temporal-tests.sh
new file mode 100755
index 00000000..09effe18
--- /dev/null
+++ b/cade-temporal-tests.sh
@@ -0,0 +1,88 @@
+#!/bin/bash
+
+./temporal_ctl_prove.native -s -P ./benchmarks/temporal/cade/exmp1_1.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 40 -F -s -P ./benchmarks/temporal/cade/exmp1_2.ctl
+printf "\n";
+./temporal_ctl_prove.native -s -P ./benchmarks/temporal/cade/exmp1_3.ctl
+printf "\n";
+./temporal_ctl_prove.native -s -P ./benchmarks/temporal/cade/exmp1_4.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 30 -F -s -P ./benchmarks/temporal/cade/exmp1_5.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 28 -F -s -P ./benchmarks/temporal/cade/exmp1_6.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 20 -s -P ./benchmarks/temporal/cade/Fin-Lock1.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 12 -s -P ./benchmarks/temporal/cade/Fin-Lock2.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 20 -s -P ./benchmarks/temporal/cade/Fin-Lock3.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 16 -s -P ./benchmarks/temporal/cade/Inf-Lock1.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 16 -s -P ./benchmarks/temporal/cade/Inf-Lock2.ctl
+printf "\n";
+./temporal_ctl_prove.native -t 0 -M 20 -s -P ./benchmarks/temporal/cade/Inf-Lock3.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 18 -F -s -P ./benchmarks/temporal/cade/Nd-Inf-Lock1.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 19 -F -s -P ./benchmarks/temporal/cade/Nd-Inf-Lock2.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 7 -s -P ./benchmarks/temporal/cade/Insert-List1.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 18 -F -s -P ./benchmarks/temporal/cade/Insert-List2.ctl
+printf "\n";
+./temporal_ctl_prove.native -t 0 -NC -M 28 -F -s -P ./benchmarks/temporal/cade/Insert-List3.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 5 -s -P ./benchmarks/temporal/cade/Cyclic-List1.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 6 -s -P ./benchmarks/temporal/cade/Cyclic-List2.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 6 -s -D examples/bt.def -P ./benchmarks/temporal/cade/Inf-BinTree.ctl
+printf "\n";
+./temporal_ctl_prove.native -t 0 -M 40 -NC -s -P ./benchmarks/temporal/cade/AFEFBranch.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 26 -NC -s -P ./benchmarks/temporal/cade/AFAGBranch.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 7 -s -P ./benchmarks/temporal/cade/EGAGBranch.ctl
+printf "\n";
+./temporal_ctl_prove.native -t 0 -M 44 -c -NC -s -P ./benchmarks/temporal/cade/EGAFBranch.ctl
+printf "\n";
+./temporal_ctl_prove.native -t 0 -M 30 -NC -s -P ./benchmarks/temporal/cade/EGImpEFBranch.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 50 -NC -F -s -P ./benchmarks/temporal/cade/EGImpAFBranch.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 14 -NC -s -P ./benchmarks/temporal/cade/AGImpEGBranch.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 24 -NC -s -P ./benchmarks/temporal/cade/AGImpEFBranch.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 16 -s -P ./benchmarks/temporal/cade/Acq-rel3.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 12 -F -s -P ./benchmarks/temporal/cade/Acq-rel4.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 16 -s -P ./benchmarks/temporal/cade/Acq-rel5.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 10 -F -s -P ./benchmarks/temporal/cade/Acq-rel6.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 40 -s -P ./benchmarks/temporal/cade/PostgreSQL1.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 40 -s -P ./benchmarks/temporal/cade/PostgreSQL1.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 40 -s -P ./benchmarks/temporal/cade/PostgreSQL2.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 40 -s -P ./benchmarks/temporal/cade/PostgreSQL3.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 40 -s -P ./benchmarks/temporal/cade/PostgreSQL4.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 31 -s -P ./benchmarks/temporal/cade/WinUpdate1.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 5 -s -P ./benchmarks/temporal/cade/WinUpdate2.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 31 -s -P ./benchmarks/temporal/cade/WinUpdate3.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 31 -F -s -P ./benchmarks/temporal/cade/WinUpdate4.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 5 -s -P ./benchmarks/temporal/cade/WinUpdate5.ctl
+printf "\n";
+./temporal_ctl_prove.native -M 31 -F -s -P ./benchmarks/temporal/cade/WinUpdate6.ctl
+printf "\n";
diff --git a/examples/bt.def b/examples/bt.def
new file mode 100644
index 00000000..dff04531
--- /dev/null
+++ b/examples/bt.def
@@ -0,0 +1,4 @@
+bt {
+	x=nil => bt(x) |
+	x->y',x' * bt(y') * bt(x') => bt(x)
+}
\ No newline at end of file