add measuring script

aalta/Aalta_v2.0/cnf.dimacs

-p cnf 3 2
-3 0
--3 -1 -2 0
+p cnf 1 1
+1 0

aalta/Aalta_v2.0/main.cpp

@@ -14,7 +14,7 @@ nondeter_sat (int argc, char** argv)
 {
   if (argc == 1)
     {
-      puts ("please input the formula:");
+      // puts ("please input the formula:");
       if (fgets (in, MAXN, stdin) == NULL)
       {
         printf ("Error: read input!\n");
@@ -27,11 +27,11 @@ nondeter_sat (int argc, char** argv)
     }
   aalta_formula* af;
   
-  printf("Simplifying ...");
+  //printf("Simplifying ...");
   af = aalta_formula(in).unique();
   af = af->simplify ();
 
-  printf("Checking satisfiability...");
+  //printf("Checking satisfiability...");
   
   nondeter_checker ch (af);
   
@@ -77,7 +77,7 @@ sat (int argc, char** argv)
   bool f2l = false;
   if (argc == 1)
     {
-      puts ("please input the formula:");
+      // puts ("please input the formula:");
       if (fgets (in, MAXN, stdin) == NULL)
       {
         printf ("Error: read input!\n");
@@ -105,7 +105,7 @@ ltlf_sat (int argc, char** argv)
   bool f2l = false;
   if (argc == 1)
     {
-      puts ("please input the formula:");
+      // puts ("please input the formula:");
       if (fgets (in, MAXN, stdin) == NULL)
       {
         printf ("Error: read input!\n");
@@ -136,7 +136,7 @@ dnf (int argc, char** argv)
   }
   if (argc == 1)
     {
-      puts ("please input the formula:");
+      // puts ("please input the formula:");
       if (fgets (in, MAXN, stdin) == NULL)
       {
         printf ("Error: read input!\n");

cnf.dimacs

-p cnf 83 92
-23 0
--23 24 0
--23 31 0
--24 25 0
--24 26 0
--25 -1 2 0
--26 27 0
--26 28 0
--27 -3 4 0
--28 29 0
--28 30 0
--29 1 -2 0
--30 3 -4 0
--31 32 0
--31 39 0
--32 33 0
--32 34 0
--33 -5 6 0
--34 35 0
--34 36 0
--35 -7 8 0
--36 37 0
--36 38 0
--37 5 -6 0
--38 7 -8 0
--39 40 0
--39 47 0
--40 41 0
--40 42 0
--41 -9 10 0
--42 43 0
--42 44 0
--43 -11 12 0
--44 45 0
--44 46 0
--45 9 -10 0
--46 11 -12 0
--47 48 0
--47 55 0
--48 49 0
--48 50 0
--49 -13 14 0
--50 51 0
--50 52 0
--51 -15 16 0
--52 53 0
--52 54 0
--53 13 -14 0
--54 15 -16 0
--55 56 0
--55 57 0
--56 -17 -18 0
--57 58 0
--57 59 0
--58 -17 -19 0
--59 60 0
--59 61 0
--60 -20 -17 0
--61 62 0
--61 63 0
--62 -20 -21 0
--63 64 0
--63 65 0
--64 -20 -18 0
--65 66 0
--65 67 0
--66 -20 -19 0
--67 68 0
--67 69 0
--68 -17 -21 0
--69 70 0
--69 71 0
--70 -18 -19 0
--71 72 0
--71 73 0
--72 -22 -21 0
--73 74 0
--73 75 0
--74 -22 -19 0
--75 76 0
--75 77 0
--76 -21 -19 0
--77 78 0
--77 79 0
--78 -22 -18 0
--79 80 0
--79 81 0
--80 -21 -18 0
--81 82 0
--81 83 0
--82 -22 -17 0
--83 -22 -20 0
+p cnf 3 2
+3 0
+-3 -1 -2 0

examples/declasstest.spec

+Workflow
+
+forallmay x:A,p:P
+	True -> Conf += (x,p)
+loop {
+	forall xa:A,xb:A,p:P (!Conf(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
+	forallmay x:A,p:P (!Conf(x,p) ∧ O(x,p)) → Acc += (x,p)
+}
+
+Declassify
+
+O(x:A,p:P): G ¬ Conf(at:A,p:P)
+
+Target
+
+Read(at:A, bt:A, pt:P)

examples/easychair.spec

@@ -4,7 +4,7 @@ forallmay x:A,p:P
 	True → Conf += (x,p)
 forallmay x:A,p:P
 	!Conf(x,p) → Assign += (x,p)
-forallmay x:A,p:P,r:R
+forall x:A,p:P,r:R
 	(Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
 loop {
 	forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,xb,p,r)
@@ -13,11 +13,11 @@ loop {
 
 Declassify
 
-O(x:A,p:P,r:R): G ¬ Conf(x:A,p:P)
+O(x:A,p:P,r:R): G ¬ Conf(at:A,p:P)
 
 Target
 
-Read(xa:A, xb:A, p:P, r:R)
+Read(at:A, bt:A, pt:P, rt:R)
 
 Causality
 

examples/easychair3.spec

@@ -13,11 +13,11 @@ loop {
 
 Declassify
 
-O(x:A,p:P,r:R): G ¬ Conf(x:A,p:P)
+O(x:A,p:P): G ¬ Conf(at:A,p:P)
 
 Target
 
-Read(xa:A,xb:A,p:P)
+Read(at:A, bt:A, pt:P)
 
 Causality
 

examples/easychair_linear.spec

@@ -11,8 +11,8 @@ forallmay y:X,x:X,p:P
 
 Declassify
 
-O(x:X,p:P,r:R): G ¬ Conf(x:A,p:P)
+O(x:X,p:P,r:R): G ¬ Conf(xt:X,p:P)
 
 Target
 
-Comm(x:X, y:X, p:P)
+Comm(xt:X, yt:X, pt:P)

examples/simpleChoiceTypedDeclassified.spec

+Workflow
+
+forall x:X,s:S
+	O(s) -> R += (x,s)
+
+Declassify
+
+O(s:S): True
+
+Target
+
+R(x:X,s:S)

examples/simpleChoiceTypedPartlyDeclassified.spec

+Workflow
+
+forallmay x:X, s:S
+	True -> C += (x,s)
+forall x:X,s:S
+	(!C(x,s) ∧ O(x,s)) -> R += (x,s)
+
+Declassify
+
+O(x:X,s:S): G ¬ C(xt:X,s:S)
+
+Target
+
+R(xt:X,st:S)

measure.sh

+# /bin/bash
+RESULT=results/measure.txt
+TIMEOUT=3s
+touch ${RESULT}
+
+echo "Measurement $(date)" >> ${RESULT}
+echo "" >> ${RESULT}
+
+for FILE in results/*.ltl
+do
+	NAME=$(basename ${FILE} .ltl)
+	echo "Measuring ${FILE}"
+	echo "${FILE}:" >> ${RESULT}
+	echo "    FOLTL length: $(wc -m < results/${NAME}.foltl)" >> ${RESULT}
+	echo "    LTL length: $(wc -m < ${FILE})" >> ${RESULT}
+	if
+		timeout ${TIMEOUT} time -p aalta/Aalta_v2.0/aalta < ${FILE} >> ${RESULT} 2>&1 
+	then
+		echo "Finished successfully"
+		echo "    Finished successfully" >> ${RESULT}
+	else
+		echo "Timeout after ${TIMEOUT}"
+		echo "    Timeout after ${TIMEOUT}" >> ${RESULT}
+	fi
+	echo "" >> ${RESULT}
+done

results/measure.txt

+Measurement Fri May 12 17:33:30 WEST 2017
+
+results/declasstest_stubborn.ltl:
+    FOLTL length: 2927
+    LTL length: 4518
+unsat
+real 1.30
+user 1.26
+sys 0.00
+    Finished successfully
+
+results/easychair3_causal.ltl:
+    FOLTL length: 5962
+    LTL length: 51350
+    Timeout after 3s
+
+results/easychair3_stubborn.ltl:
+    FOLTL length: 5019
+    LTL length: 7318
+    Timeout after 3s
+
+results/easychair_causal.ltl:
+    FOLTL length: 6318
+    LTL length: 108512
+    Timeout after 3s
+
+results/easychair_linear_stubborn.ltl:
+    FOLTL length: 3851
+    LTL length: 4787
+unsat
+real 0.76
+user 0.76
+sys 0.00
+    Finished successfully
+
+results/easychair_stubborn.ltl:
+    FOLTL length: 5452
+    LTL length: 8304
+unsat
+real 2.18
+user 2.18
+sys 0.00
+    Finished successfully
+
+results/linear3_stubborn.ltl:
+    FOLTL length: 2163
+    LTL length: 13352
+    Timeout after 3s
+
+results/linear4_stubborn.ltl:
+    FOLTL length: 3506
+    LTL length: 154103
+    Timeout after 3s
+
+results/prevexampleNoOracle_stubborn.ltl:
+    FOLTL length: 2392
+    LTL length: 15687
+    Timeout after 3s
+
+results/prevexample_stubborn.ltl:
+    FOLTL length: 2442
+    LTL length: 15885
+sat
+real 0.13
+user 0.10
+sys 0.03
+    Finished successfully
+
+results/simpleChoiceNoOracle_stubborn.ltl:
+    FOLTL length: 513
+    LTL length: 820
+unsat
+real 0.01
+user 0.01
+sys 0.00
+    Finished successfully
+
+results/simpleChoice_stubborn.ltl:
+    FOLTL length: 559
+    LTL length: 908
+sat
+real 0.00
+user 0.00
+sys 0.00
+    Finished successfully
+
+results/simpleChoiceTypedDeclassified_stubborn.ltl:
+    FOLTL length: 555
+    LTL length: 349
+unsat
+real 0.00
+user 0.00
+sys 0.00
+    Finished successfully
+
+results/simpleChoiceTypedPartlyDeclassified_stubborn.ltl:
+    FOLTL length: 1276
+    LTL length: 844
+unsat
+real 0.04
+user 0.04
+sys 0.00
+    Finished successfully
+
+results/simpleChoiceTyped_stubborn.ltl:
+    FOLTL length: 505
+    LTL length: 316
+sat
+real 0.00
+user 0.00
+sys 0.00
+    Finished successfully
+
+results/simpleNoChoice_stubborn.ltl:
+    FOLTL length: 505
+    LTL length: 780
+sat
+real 0.00
+user 0.00
+sys 0.00
+    Finished successfully
+