metrics

examples/typedcausal2.spec

@@ -9,7 +9,7 @@ forallmay a:T2,b:T3
 
 Declassify
 
-O(x): True
+O(x:T1): True
 
 Target
 

results/causal1_causal.metrics

-results/causal1_causal.foltl: 747
-results/causal1_causal.ltl: 2805
-Universe: a1:T, a2:T, ca:T, causalcaT1:T
-
-Measuring run 1:
-Timeout after 1s
-
-Measuring run 2:
-Timeout after 1s
-
-Measuring run 1:
-sat
-real 6.28
-user 6.21
-sys 0.06
-Finished successfully
-
-Measuring run 2:
-sat
-real 6.28
-user 6.26
-sys 0.01
-Finished successfully
-
-Measuring run 3:
-sat
-real 6.29
-user 6.24
-sys 0.04
-Finished successfully
-
-Measuring run 4:
-sat
-real 6.15
-user 6.11
-sys 0.03
-Finished successfully
-
-Measuring run 5:
-sat
-real 6.31
-user 6.27
-sys 0.03
-Finished successfully
-
-Measuring run 6:
-sat
-real 6.36
-user 6.33
-sys 0.03
-Finished successfully
-
-Measuring run 7:
-sat
-real 6.18
-user 6.14
-sys 0.04
-Finished successfully
-
-Measuring run 8:
-sat
-real 6.21
-user 6.17
-sys 0.04
-Finished successfully
-
-Measuring run 9:
-sat
-real 6.17
-user 6.15
-sys 0.02
-Finished successfully
-
-Measuring run 10:
-sat
-real 6.18
-user 6.11
-sys 0.06
-Finished successfully

results/causal1_stubborn.metrics

-results/causal1_stubborn.foltl: 654
-results/causal1_stubborn.ltl: 1129
-Universe: a1:T, a2:T
-
-Measuring run 1:
-Timeout after 1s
-
-Measuring run 2:
-Timeout after 1s
-
-Measuring run 1:
-unsat
-real 2.92
-user 2.90
-sys 0.01
-Finished successfully
-
-Measuring run 2:
-unsat
-real 3.01
-user 2.95
-sys 0.00
-Finished successfully
-
-Measuring run 3:
-unsat
-real 2.93
-user 2.92
-sys 0.00
-Finished successfully
-
-Measuring run 4:
-unsat
-real 2.91
-user 2.90
-sys 0.00
-Finished successfully
-
-Measuring run 5:
-unsat
-real 2.95
-user 2.94
-sys 0.01
-Finished successfully
-
-Measuring run 6:
-unsat
-real 2.97
-user 2.96
-sys 0.00
-Finished successfully
-
-Measuring run 7:
-unsat
-real 3.18
-user 3.17
-sys 0.01
-Finished successfully
-
-Measuring run 8:
-unsat
-real 2.90
-user 2.89
-sys 0.01
-Finished successfully
-
-Measuring run 9:
-unsat
-real 2.91
-user 2.90
-sys 0.00
-Finished successfully
-
-Measuring run 10:
-unsat
-real 2.96
-user 2.95
-sys 0.00
-Finished successfully

results/causal2_causal.metrics

-results/causal2_causal.foltl: 965
-results/causal2_causal.ltl: 6338
-Universe: a1:T, a2:T, ca:T, causalcaT1:T, cb:T, causalcbT1:T
-
-Measuring run 1:
-Timeout after 1s
-
-Measuring run 2:
-Timeout after 1s
-
-Measuring run 1:
-sat
-real 57.45
-user 57.21
-sys 0.23
-Finished successfully
-
-Measuring run 2:
-sat
-real 57.36
-user 57.18
-sys 0.18
-Finished successfully
-
-Measuring run 3:
-sat
-real 57.63
-user 57.42
-sys 0.20
-Finished successfully
-
-Measuring run 4:
-sat
-real 56.76
-user 56.56
-sys 0.19
-Finished successfully
-
-Measuring run 5:
-sat
-real 56.79
-user 56.58
-sys 0.20
-Finished successfully
-
-Measuring run 6:
-sat
-real 59.80
-user 59.60
-sys 0.18
-Finished successfully
-
-Measuring run 7:
-sat
-real 56.94
-user 56.75
-sys 0.18
-Finished successfully
-
-Measuring run 8:
-sat
-real 56.60
-user 56.38
-sys 0.21
-Finished successfully
-
-Measuring run 9:
-sat
-real 57.26
-user 57.09
-sys 0.16
-Finished successfully
-
-Measuring run 10:
-sat
-real 57.04
-user 56.82
-sys 0.20
-Finished successfully

results/causal2_stubborn.metrics

-results/causal2_stubborn.foltl: 778
-results/causal2_stubborn.ltl: 1353
-Universe: a1:T, a2:T
-
-Measuring run 1:
-Timeout after 1s
-
-Measuring run 2:
-Timeout after 1s
-
-Measuring run 1:
-unsat
-real 34.63
-user 34.62
-sys 0.01
-Finished successfully
-
-Measuring run 2:
-unsat
-real 34.25
-user 34.24
-sys 0.00
-Finished successfully
-
-Measuring run 3:
-unsat
-real 34.22
-user 34.21
-sys 0.00
-Finished successfully
-
-Measuring run 4:
-unsat
-real 33.98
-user 33.96
-sys 0.01
-Finished successfully
-
-Measuring run 5:
-unsat
-real 33.90
-user 33.89
-sys 0.00
-Finished successfully
-
-Measuring run 6:
-unsat
-real 35.44
-user 35.42
-sys 0.00
-Finished successfully
-
-Measuring run 7:
-unsat
-real 33.83
-user 33.81
-sys 0.02
-Finished successfully
-
-Measuring run 8:
-unsat
-real 34.42
-user 34.41
-sys 0.00
-Finished successfully
-
-Measuring run 9:
-unsat
-real 34.42
-user 34.40
-sys 0.02
-Finished successfully
-
-Measuring run 10:
-unsat
-real 34.42
-user 34.41
-sys 0.01
-Finished successfully

results/causal3_causal.metrics

-results/causal3_causal.foltl: 1777
-results/causal3_causal.ltl: 26472
-Universe: a1:T, a2:T, ca:T, causalcaT1:T, cb:T, causalcbT1:T, cc:T, causalccT1:T
-
-Measuring run 1:
-Timeout after 1s
-
-Measuring run 2:
-Timeout after 1s
-
-Measuring run 1:
-Timeout after 20m
-
-Measuring run 2:
-Timeout after 20m
-
-Measuring run 3:
-Timeout after 20m
-
-Measuring run 4:
-Timeout after 20m
-
-Measuring run 5:
-Timeout after 20m
-
-Measuring run 6:
-Timeout after 20m
-
-Measuring run 7:
-Timeout after 20m
-
-Measuring run 8:
-Timeout after 20m
-
-Measuring run 9:
-Timeout after 20m
-
-Measuring run 10:
-Timeout after 20m

results/causal3_stubborn.metrics

-results/causal3_stubborn.foltl: 1395
-results/causal3_stubborn.ltl: 2764
-Universe: a1:T, a2:T
-
-Measuring run 1:
-Timeout after 1s
-
-Measuring run 2:
-Timeout after 1s
-
-Measuring run 1:
-unsat
-real 131.39
-user 131.29
-sys 0.09
-Finished successfully
-
-Measuring run 2:
-unsat
-real 128.74
-user 128.72
-sys 0.02
-Finished successfully
-
-Measuring run 3:
-unsat
-real 129.47
-user 129.45
-sys 0.02
-Finished successfully
-
-Measuring run 4:
-unsat
-real 127.11
-user 127.08
-sys 0.02
-Finished successfully
-
-Measuring run 5:
-unsat
-real 127.28
-user 127.25
-sys 0.02
-Finished successfully
-
-Measuring run 6:
-unsat
-real 127.37
-user 127.31
-sys 0.04
-Finished successfully
-
-Measuring run 7:
-unsat
-real 127.70
-user 127.66
-sys 0.03
-Finished successfully
-
-Measuring run 8:
-unsat
-real 129.37
-user 129.32
-sys 0.03
-Finished successfully
-
-Measuring run 9:
-unsat
-real 127.45
-user 127.41
-sys 0.04
-Finished successfully
-
-Measuring run 10:
-unsat
-real 127.32
-user 127.28
-sys 0.03
-Finished successfully

results/conference-acceptance_causal.metrics

-results/conference-acceptance_causal.foltl: 700
-results/conference-acceptance_causal.ltl: 5187
-Universe: at:A, bt:A, pt:P, a:A, causalaA1:A, causalaP1:P
+results/conference-acceptance_causal.foltl: 727
+results/conference-acceptance_causal.ltl: 5275
+Universe: a:A, causalaA1:A, causalaP1:P, at:A, bt:A, pt:P
 
-Measuring run 1:
-Timeout after 1s
-
-Measuring run 2:
-Timeout after 1s
-
-Measuring run 1:
-sat
-real 45.94
-user 45.83
-sys 0.10
-Finished successfully
-
-Measuring run 2:
-sat
-real 46.06
-user 45.93
-sys 0.12
-Finished successfully
-
-Measuring run 3:
-sat
-real 45.34
-user 45.27
-sys 0.06
-Finished successfully
-
-Measuring run 4:
-sat
-real 45.37
-user 45.29
-sys 0.08
-Finished successfully
-
-Measuring run 5:
-sat
-real 45.27
-user 45.17
-sys 0.09
-Finished successfully
-
-Measuring run 6:
-sat
-real 45.45
-user 45.34
-sys 0.10
-Finished successfully
-
-Measuring run 7:
-sat
-real 45.28
-user 45.18
-sys 0.09
-Finished successfully
-
-Measuring run 8:
-sat
-real 45.40
-user 45.26
-sys 0.13
-Finished successfully
-
-Measuring run 9:
-sat
-real 45.62
-user 45.52
-sys 0.10
-Finished successfully
-
-Measuring run 10:
-sat
-real 46.62
-user 46.54
-sys 0.07
-Finished successfully
+Measuring on Fri May 19 15:28:36 WEST 2017:
+Timeout after 20s

results/conference-acceptance_stubborn.metrics

@@ -2,78 +2,9 @@ results/conference-acceptance_stubborn.foltl: 628
 results/conference-acceptance_stubborn.ltl: 1089
 Universe: at:A, bt:A, pt:P
 
-Measuring run 1:
-Timeout after 1s
-
-Measuring run 2:
-Timeout after 1s
-
-Measuring run 1:
-unsat
-real 2.50
-user 2.48
-sys 0.01
-Finished successfully
-
-Measuring run 2:
+Measuring on Fri May 19 15:28:56 WEST 2017:
 unsat
 real 2.48
 user 2.48
 sys 0.00
 Finished successfully
-
-Measuring run 3:
-unsat
-real 2.46
-user 2.45
-sys 0.00
-Finished successfully
-
-Measuring run 4:
-unsat
-real 2.46
-user 2.44
-sys 0.01
-Finished successfully
-
-Measuring run 5:
-unsat
-real 2.44
-user 2.43
-sys 0.00
-Finished successfully
-
-Measuring run 6:
-unsat
-real 2.49
-user 2.48
-sys 0.01
-Finished successfully
-
-Measuring run 7:
-unsat
-real 2.45
-user 2.45
-sys 0.00
-Finished successfully
-
-Measuring run 8:
-unsat
-real 2.46
-user 2.45
-sys 0.00
-Finished successfully
-
-Measuring run 9:
-unsat
-real 2.45
-user 2.44
-sys 0.01
-Finished successfully
-
-Measuring run 10:
-unsat
-real 2.54
-user 2.53
-sys 0.00
-Finished successfully

results/conference_causal.metrics

-results/conference_causal.foltl: 700
-results/conference_causal.ltl: 8771
-Universe: at:A, bt:A, pt:P, rt:R, a:A, causalaA1:A, causalaP1:P, causalaR1:R
+results/conference_causal.foltl: 730
+results/conference_causal.ltl: 8885
+Universe: a:A, causalaA1:A, causalaP1:P, causalaR1:R, at:A, bt:A, pt:P, rt:R
 
-Measuring run 1:
-Timeout after 1s
-
-Measuring run 2:
-Timeout after 1s
-
-Measuring run 1:
-sat
-real 92.89
-user 92.66
-sys 0.22
-Finished successfully
-
-Measuring run 2:
-sat
-real 92.18
-user 91.95
-sys 0.22
-Finished successfully
-
-Measuri