Commit 1139e94d authored by Thom Badings's avatar Thom Badings
Browse files

Updated computation of bounds

parent 15efff2b
#!/bin/bash
# Run all benchmarks at once
bash run_all_brp.sh;
bash run_all_crowds.sh;
bash run_all_nand.sh;
bash run_all_consensus.sh;
bash run_all_drone.sh;
\ No newline at end of file
This diff is collapsed.
import numpy as np
import math
import time # Import to create tic/toc functions
from scipy.stats import beta as betaF
# Approximation of binomial cdf with continuity correction for large n
# n: trials, p: success prob, m: starting successes
......@@ -37,7 +37,7 @@ def ticDiff():
# Records a time in TicToc, marks the beginning of a time interval
tocDiff(False)
def etaLow(N,k,beta):
def etaLow_RiskAndComplexity(N,k,beta):
'''
Rootfinding problem to compute the lower bound on the satprob (eta)
......@@ -96,7 +96,7 @@ def etaLow(N,k,beta):
return eta_star
def betaLow(N,k,eta):
def betaLow_RiskAndComplexity(N,k,eta):
'''
Rootfinding problem to compute the lower bound on the satprob (eta)
......@@ -152,6 +152,18 @@ def betaLow(N,k,eta):
return beta_star
def computeBetaPPF(N, k, d, beta):
epsilon = betaF.ppf(beta, k+d, N-(d+k)+1)
return epsilon
def computeBetaCDF(N, k, d, epsilon):
cum_prob = betaF.cdf(epsilon, k+d, N-(d+k)+1)
return cum_prob
def compute_eta(N, nr_discarded, beta):
'''
Compute the lower bound on the satisfaction probability (eta) based on the
......@@ -180,16 +192,17 @@ def compute_eta(N, nr_discarded, beta):
else:
# Constraints discarded
k = nr_discarded + 1
if k >= N:
if nr_discarded >= N:
eta_low = 0
else:
# Use bisection procedure to find eta
eta_low = etaLow(N, k, beta)
# eta_low = etaLow_RiskAndComplexity(N, nr_discarded+1, beta)
beta_bar = (1-beta)/N
eta_low = 1 - computeBetaPPF(N, k=nr_discarded, d=1, beta=1-beta_bar)
return eta_low
......@@ -221,16 +234,17 @@ def compute_beta(N, nr_discarded, eta_low):
else:
# Samples discarded
k = nr_discarded + 1
if k >= N:
if nr_discarded >= N:
beta = 0
else:
# Use bisection procedure to find beta
beta = betaLow(N, k, eta_low)
# beta = betaLow_RiskAndComplexity(N, nr_discarded+1, eta_low)
RHS = computeBetaCDF(N, k=nr_discarded, d=1, epsilon=1-eta_low)
beta = 1 - N * (1-RHS)
return beta
\ No newline at end of file
return max(0, beta)
\ No newline at end of file
......@@ -2,51 +2,21 @@ OUTPUT FOR MODEL: brp/brp_256_5.pm
----------
Start for N=100
Run time per parameter sample in Storm: 3.964654922485
Run time per iteration (of N samples) in Storm: 0.204
Confidence probability for eta=0.055 is beta=0.0
Lower bound sat.prob. for beta=0.9 is eta=0.017686681890170995
Lower bound sat.prob. for beta=0.99 is eta=0.012327767993340406
Lower bound sat.prob. for beta=0.999 is eta=0.008859020435220771
Lower bound sat.prob. for beta=0.9999 is eta=0.006488133900387831
Time required to compute guarantees: 0.118131875992
Confidence probability for eta=0.055 is beta=0.09941
Lower bound sat.prob. for beta=0.9 is eta=0.0218
Lower bound sat.prob. for beta=0.99 is eta=0.01608
Lower bound sat.prob. for beta=0.999 is eta=0.01218
Lower bound sat.prob. for beta=0.9999 is eta=0.00938
Time required to compute guarantees: 0.017527580261
----------
Start for N=500
Run time per parameter sample in Storm: 10.976534605026
Run time per iteration (of N samples) in Storm: 1.02
Confidence probability for eta=0.055 is beta=0.2814739286026452
Lower bound sat.prob. for beta=0.9 is eta=0.04403912772347082
Lower bound sat.prob. for beta=0.99 is eta=0.0391127232657726
Lower bound sat.prob. for beta=0.999 is eta=0.03517302870583565
Lower bound sat.prob. for beta=0.9999 is eta=0.03189561148080651
Time required to compute guarantees: 0.06738114357
----------
Start for N=1000
Run time per parameter sample in Storm: 21.276072502136
Confidence probability for eta=0.055 is beta=0.536353821249213
Lower bound sat.prob. for beta=0.9 is eta=0.051225382795078836
Lower bound sat.prob. for beta=0.99 is eta=0.04737779662548451
Lower bound sat.prob. for beta=0.999 is eta=0.044191522352715264
Lower bound sat.prob. for beta=0.9999 is eta=0.041458895875569
Time required to compute guarantees: 0.080315113068
----------
Start for N=5000
Run time per parameter sample in Storm: 114.465609550476
Confidence probability for eta=0.055 is beta=0.9996292568626813
Lower bound sat.prob. for beta=0.9 is eta=0.06473572262653424
Lower bound sat.prob. for beta=0.99 is eta=0.06280930272313756
Lower bound sat.prob. for beta=0.999 is eta=0.06114327694982071
Lower bound sat.prob. for beta=0.9999 is eta=0.059661999852972714
Time required to compute guarantees: 0.668165445328
----------
Start for N=10000
Run time per parameter sample in Storm: 199.494306087494
Confidence probability for eta=0.055 is beta=0.9999999999417923
Lower bound sat.prob. for beta=0.9 is eta=0.0699534833359233
Lower bound sat.prob. for beta=0.99 is eta=0.06855265189220769
Lower bound sat.prob. for beta=0.999 is eta=0.06732810971248507
Lower bound sat.prob. for beta=0.9999 is eta=0.06623008822231909
Time required to compute guarantees: 0.981542110443
Confidence probability for eta=0.055 is beta=0.38309
Lower bound sat.prob. for beta=0.9 is eta=0.04426
Lower bound sat.prob. for beta=0.99 is eta=0.0398
Lower bound sat.prob. for beta=0.999 is eta=0.03611
Lower bound sat.prob. for beta=0.9999 is eta=0.03297
Time required to compute guarantees: 0.020167827606
\ No newline at end of file
......@@ -2,51 +2,51 @@ OUTPUT FOR MODEL: consensus/coin2.pm
----------
Start for N=100
Run time per parameter sample in Storm: 0.744772195816
Run time per iteration (of N samples) in Storm: 0.057
Confidence probability for eta=0.28 is beta=0.0
Lower bound sat.prob. for beta=0.9 is eta=0.16388104088540187
Lower bound sat.prob. for beta=0.99 is eta=0.14086084271198646
Lower bound sat.prob. for beta=0.999 is eta=0.12328277841116682
Lower bound sat.prob. for beta=0.9999 is eta=0.1091022988683045
Time required to compute guarantees: 0.049267530441
Confidence probability for eta=0.28 is beta=0.09347
Lower bound sat.prob. for beta=0.9 is eta=0.2051
Lower bound sat.prob. for beta=0.99 is eta=0.17899
Lower bound sat.prob. for beta=0.999 is eta=0.15883
Lower bound sat.prob. for beta=0.9999 is eta=0.14237
Time required to compute guarantees: 0.039784669876
----------
Start for N=500
Run time per parameter sample in Storm: 3.557334184647
Run time per iteration (of N samples) in Storm: 0.281
Confidence probability for eta=0.28 is beta=0.16580844005220569
Lower bound sat.prob. for beta=0.9 is eta=0.24070488439810647
Lower bound sat.prob. for beta=0.99 is eta=0.22852285991119473
Lower bound sat.prob. for beta=0.999 is eta=0.21841674422467633
Lower bound sat.prob. for beta=0.9999 is eta=0.20966918686030495
Time required to compute guarantees: 0.185102939606
Confidence probability for eta=0.28 is beta=0.28749
Lower bound sat.prob. for beta=0.9 is eta=0.2652
Lower bound sat.prob. for beta=0.99 is eta=0.25248
Lower bound sat.prob. for beta=0.999 is eta=0.24192
Lower bound sat.prob. for beta=0.9999 is eta=0.23276
Time required to compute guarantees: 0.136856079102
----------
Start for N=1000
Run time per parameter sample in Storm: 7.637410402298
Run time per iteration (of N samples) in Storm: 0.595
Confidence probability for eta=0.28 is beta=0.29131160586257465
Lower bound sat.prob. for beta=0.9 is eta=0.26310366311458033
Lower bound sat.prob. for beta=0.99 is eta=0.25433441511943267
Lower bound sat.prob. for beta=0.999 is eta=0.2469358717088598
Lower bound sat.prob. for beta=0.9999 is eta=0.24044842040271758
Time required to compute guarantees: 0.326511621475
Confidence probability for eta=0.28 is beta=0.82738
Lower bound sat.prob. for beta=0.9 is eta=0.28775
Lower bound sat.prob. for beta=0.99 is eta=0.27866
Lower bound sat.prob. for beta=0.999 is eta=0.27098
Lower bound sat.prob. for beta=0.9999 is eta=0.26425
Time required to compute guarantees: 0.265974521637
----------
Start for N=5000
Run time per parameter sample in Storm: 47.126279592514
Run time per iteration (of N samples) in Storm: 2.686
Confidence probability for eta=0.28 is beta=0.9911584894580301
Lower bound sat.prob. for beta=0.9 is eta=0.2890970205100354
Lower bound sat.prob. for beta=0.99 is eta=0.28523187240814885
Lower bound sat.prob. for beta=0.999 is eta=0.2818896070061145
Lower bound sat.prob. for beta=0.9999 is eta=0.27890707121095015
Time required to compute guarantees: 2.316249132156
Confidence probability for eta=0.28 is beta=1.0
Lower bound sat.prob. for beta=0.9 is eta=0.32257
Lower bound sat.prob. for beta=0.99 is eta=0.31856
Lower bound sat.prob. for beta=0.999 is eta=0.31509
Lower bound sat.prob. for beta=0.9999 is eta=0.31199
Time required to compute guarantees: 1.563100337982
----------
Start for N=10000
Run time per parameter sample in Storm: 94.269612073898
Run time per iteration (of N samples) in Storm: 5.91
Confidence probability for eta=0.28 is beta=0.9999917433364317
Lower bound sat.prob. for beta=0.9 is eta=0.29224254975203035
Lower bound sat.prob. for beta=0.99 is eta=0.2895582152140982
Lower bound sat.prob. for beta=0.999 is eta=0.2872194661241423
Lower bound sat.prob. for beta=0.9999 is eta=0.28512177879940487
Time required to compute guarantees: 6.91422867775
\ No newline at end of file
Confidence probability for eta=0.28 is beta=1.0
Lower bound sat.prob. for beta=0.9 is eta=0.32645
Lower bound sat.prob. for beta=0.99 is eta=0.32367
Lower bound sat.prob. for beta=0.999 is eta=0.32124
Lower bound sat.prob. for beta=0.9999 is eta=0.31907
Time required to compute guarantees: 4.046259880066
\ No newline at end of file
......@@ -2,51 +2,51 @@ OUTPUT FOR MODEL: crowds/crowds_10_5.pm
----------
Start for N=100
Run time per parameter sample in Storm: 0.213780164719
Run time per iteration (of N samples) in Storm: 0.018
Confidence probability for eta=0.537 is beta=0.0
Lower bound sat.prob. for beta=0.9 is eta=0.3974279794215893
Lower bound sat.prob. for beta=0.99 is eta=0.3619583136368937
Lower bound sat.prob. for beta=0.999 is eta=0.333733182651508
Lower bound sat.prob. for beta=0.9999 is eta=0.30996800568126204
Time required to compute guarantees: 0.067635536194
Lower bound sat.prob. for beta=0.9 is eta=0.37572
Lower bound sat.prob. for beta=0.99 is eta=0.34645
Lower bound sat.prob. for beta=0.999 is eta=0.32173
Lower bound sat.prob. for beta=0.9999 is eta=0.30024
Time required to compute guarantees: 0.010838508606
----------
Start for N=500
Run time per parameter sample in Storm: 1.094228029251
Run time per iteration (of N samples) in Storm: 0.077
Confidence probability for eta=0.537 is beta=0.14465595572255552
Lower bound sat.prob. for beta=0.9 is eta=0.49540552930893983
Lower bound sat.prob. for beta=0.99 is eta=0.4798602352729066
Lower bound sat.prob. for beta=0.999 is eta=0.46686002573339974
Lower bound sat.prob. for beta=0.9999 is eta=0.4554787702468303
Time required to compute guarantees: 0.250858545303
Confidence probability for eta=0.537 is beta=0.0891
Lower bound sat.prob. for beta=0.9 is eta=0.47326
Lower bound sat.prob. for beta=0.99 is eta=0.46065
Lower bound sat.prob. for beta=0.999 is eta=0.44948
Lower bound sat.prob. for beta=0.9999 is eta=0.43938
Time required to compute guarantees: 0.009683132172
----------
Start for N=1000
Run time per parameter sample in Storm: 1.525440216064
Run time per iteration (of N samples) in Storm: 0.159
Confidence probability for eta=0.537 is beta=0.19935117455315776
Lower bound sat.prob. for beta=0.9 is eta=0.5172872141763809
Lower bound sat.prob. for beta=0.99 is eta=0.5065939244449508
Lower bound sat.prob. for beta=0.999 is eta=0.49755220488203367
Lower bound sat.prob. for beta=0.9999 is eta=0.48957875486568503
Time required to compute guarantees: 0.499408006668
Confidence probability for eta=0.537 is beta=0.09415
Lower bound sat.prob. for beta=0.9 is eta=0.50431
Lower bound sat.prob. for beta=0.99 is eta=0.49568
Lower bound sat.prob. for beta=0.999 is eta=0.48795
Lower bound sat.prob. for beta=0.9999 is eta=0.48091
Time required to compute guarantees: 0.012845993042
----------
Start for N=5000
Run time per parameter sample in Storm: 7.498879909515
Run time per iteration (of N samples) in Storm: 0.723
Confidence probability for eta=0.537 is beta=0.8190426624205429
Lower bound sat.prob. for beta=0.9 is eta=0.5408039047614432
Lower bound sat.prob. for beta=0.99 is eta=0.5363355768350605
Lower bound sat.prob. for beta=0.999 is eta=0.5324864503219592
Lower bound sat.prob. for beta=0.9999 is eta=0.5290536486079057
Time required to compute guarantees: 5.221586227417
Confidence probability for eta=0.537 is beta=0.78279
Lower bound sat.prob. for beta=0.9 is eta=0.54065
Lower bound sat.prob. for beta=0.99 is eta=0.53709
Lower bound sat.prob. for beta=0.999 is eta=0.53385
Lower bound sat.prob. for beta=0.9999 is eta=0.53087
Time required to compute guarantees: 0.015043497086
----------
Start for N=10000
Run time per parameter sample in Storm: 16.033114433289
Run time per iteration (of N samples) in Storm: 1.507
Confidence probability for eta=0.537 is beta=0.9998606626642867
Lower bound sat.prob. for beta=0.9 is eta=0.5501342007004074
Lower bound sat.prob. for beta=0.99 is eta=0.5470590988338845
Lower bound sat.prob. for beta=0.999 is eta=0.544393146973724
Lower bound sat.prob. for beta=0.9999 is eta=0.5420064263195189
Time required to compute guarantees: 24.205697059631
\ No newline at end of file
Confidence probability for eta=0.537 is beta=0.95431
Lower bound sat.prob. for beta=0.9 is eta=0.54359
Lower bound sat.prob. for beta=0.99 is eta=0.54115
Lower bound sat.prob. for beta=0.999 is eta=0.53892
Lower bound sat.prob. for beta=0.9999 is eta=0.53686
Time required to compute guarantees: 0.012798786163
\ No newline at end of file
......@@ -2,51 +2,61 @@ OUTPUT FOR MODEL: nand/nand_10_5.pm
----------
Start for N=100
Run time per parameter sample in Storm: 6.11959695816
Run time per iteration (of N samples) in Storm: 0.492
Confidence probability for eta=0.733 is beta=0.097228731069481
Lower bound sat.prob. for beta=0.9 is eta=0.6051868543136985
Lower bound sat.prob. for beta=0.99 is eta=0.5661075238969969
Lower bound sat.prob. for beta=0.999 is eta=0.5343041390658658
Lower bound sat.prob. for beta=0.9999 is eta=0.5068831258665012
Time required to compute guarantees: 0.081788301468
Confidence probability for eta=0.733 is beta=0.0
Lower bound sat.prob. for beta=0.9 is eta=0.60137
Lower bound sat.prob. for beta=0.99 is eta=0.56965
Lower bound sat.prob. for beta=0.999 is eta=0.5419
Lower bound sat.prob. for beta=0.9999 is eta=0.51701
Time required to compute guarantees: 0.012278079987
----------
Start for N=500
Run time per parameter sample in Storm: 30.702702045441
Run time per iteration (of N samples) in Storm: 2.266
Confidence probability for eta=0.733 is beta=0.047547994827618824
Lower bound sat.prob. for beta=0.9 is eta=0.697288761265879
Lower bound sat.prob. for beta=0.99 is eta=0.6819627936549837
Lower bound sat.prob. for beta=0.999 is eta=0.6690899694507308
Lower bound sat.prob. for beta=0.9999 is eta=0.6577354182186682
Time required to compute guarantees: 0.496330976486
Confidence probability for eta=0.733 is beta=0.0
Lower bound sat.prob. for beta=0.9 is eta=0.66756
Lower bound sat.prob. for beta=0.99 is eta=0.6553
Lower bound sat.prob. for beta=0.999 is eta=0.64431
Lower bound sat.prob. for beta=0.9999 is eta=0.63425
Time required to compute guarantees: 0.010138034821
----------
Start for N=1000
Run time per parameter sample in Storm: 64.471849918365
Run time per iteration (of N samples) in Storm: 4.739
Confidence probability for eta=0.733 is beta=0.07357396809966303
Lower bound sat.prob. for beta=0.9 is eta=0.7019781820743859
Lower bound sat.prob. for beta=0.99 is eta=0.6916440057984532
Lower bound sat.prob. for beta=0.999 is eta=0.6829017881254865
Lower bound sat.prob. for beta=0.9999 is eta=0.6751652499475381
Time required to compute guarantees: 0.908617019653
Confidence probability for eta=0.733 is beta=0.0
Lower bound sat.prob. for beta=0.9 is eta=0.6973
Lower bound sat.prob. for beta=0.99 is eta=0.68919
Lower bound sat.prob. for beta=0.999 is eta=0.68186
Lower bound sat.prob. for beta=0.9999 is eta=0.67513
Time required to compute guarantees: 0.013652086258
----------
Start for N=5000
Run time per parameter sample in Storm: 330.378761291504
Run time per iteration (of N samples) in Storm: 24.991
Confidence probability for eta=0.733 is beta=0.38597298676031644
Lower bound sat.prob. for beta=0.9 is eta=0.7278936436265727
Lower bound sat.prob. for beta=0.99 is eta=0.7237332182419827
Lower bound sat.prob. for beta=0.999 is eta=0.7201626534361432
Lower bound sat.prob. for beta=0.9999 is eta=0.7169807162045384
Time required to compute guarantees: 11.112593650818
Confidence probability for eta=0.733 is beta=0.0
Lower bound sat.prob. for beta=0.9 is eta=0.72116
Lower bound sat.prob. for beta=0.99 is eta=0.71792
Lower bound sat.prob. for beta=0.999 is eta=0.71497
Lower bound sat.prob. for beta=0.9999 is eta=0.71224
Time required to compute guarantees: 0.010655403137
----------
Start for N=10000
Run time per parameter sample in Storm: 725.542737960815
Run time per iteration (of N samples) in Storm: 50.138
Confidence probability for eta=0.733 is beta=0.7080008370394353
Lower bound sat.prob. for beta=0.9 is eta=0.733870358384696
Lower bound sat.prob. for beta=0.99 is eta=0.7310354916531173
Lower bound sat.prob. for beta=0.999 is eta=0.7285886548311538
Lower bound sat.prob. for beta=0.9999 is eta=0.7264017693768775
Time required to compute guarantees: 42.894950628281
\ No newline at end of file
Confidence probability for eta=0.733 is beta=0.48425
Lower bound sat.prob. for beta=0.9 is eta=0.7315
Lower bound sat.prob. for beta=0.99 is eta=0.72931
Lower bound sat.prob. for beta=0.999 is eta=0.72731
Lower bound sat.prob. for beta=0.9999 is eta=0.72545
Time required to compute guarantees: 0.010615825653
----------
Start for N=25000
Run time per iteration (of N samples) in Storm: 139.958
Confidence probability for eta=0.733 is beta=0.89696
Lower bound sat.prob. for beta=0.9 is eta=0.73643
Lower bound sat.prob. for beta=0.99 is eta=0.73511
Lower bound sat.prob. for beta=0.999 is eta=0.7339
Lower bound sat.prob. for beta=0.9999 is eta=0.73277
Time required to compute guarantees: 0.013022184372
\ No newline at end of file
OUTPUT FOR MODEL: brp/brp_256_5.pm
----------
Start for N=100
Run time per parameter sample in Storm: 3.964654922485
Confidence probability for eta=0.055 is beta=0.0
Lower bound sat.prob. for beta=0.9 is eta=0.017686681890170995
Lower bound sat.prob. for beta=0.99 is eta=0.012327767993340406
Lower bound sat.prob. for beta=0.999 is eta=0.008859020435220771
Lower bound sat.prob. for beta=0.9999 is eta=0.006488133900387831
Time required to compute guarantees: 0.118131875992
----------
Start for N=500
Run time per parameter sample in Storm: 10.976534605026
Confidence probability for eta=0.055 is beta=0.2814739286026452
Lower bound sat.prob. for beta=0.9 is eta=0.04403912772347082
Lower bound sat.prob. for beta=0.99 is eta=0.0391127232657726
Lower bound sat.prob. for beta=0.999 is eta=0.03517302870583565
Lower bound sat.prob. for beta=0.9999 is eta=0.03189561148080651
Time required to compute guarantees: 0.06738114357
----------
Start for N=1000
Run time per parameter sample in Storm: 21.276072502136
Confidence probability for eta=0.055 is beta=0.536353821249213
Lower bound sat.prob. for beta=0.9 is eta=0.051225382795078836
Lower bound sat.prob. for beta=0.99 is eta=0.04737779662548451
Lower bound sat.prob. for beta=0.999 is eta=0.044191522352715264
Lower bound sat.prob. for beta=0.9999 is eta=0.041458895875569
Time required to compute guarantees: 0.080315113068
----------
Start for N=5000
Run time per parameter sample in Storm: 114.465609550476
Confidence probability for eta=0.055 is beta=0.9996292568626813
Lower bound sat.prob. for beta=0.9 is eta=0.06473572262653424
Lower bound sat.prob. for beta=0.99 is eta=0.06280930272313756
Lower bound sat.prob. for beta=0.999 is eta=0.06114327694982071
Lower bound sat.prob. for beta=0.9999 is eta=0.059661999852972714
Time required to compute guarantees: 0.668165445328
----------
Start for N=10000
Run time per parameter sample in Storm: 199.494306087494
Confidence probability for eta=0.055 is beta=0.9999999999417923
Lower bound sat.prob. for beta=0.9 is eta=0.0699534833359233
Lower bound sat.prob. for beta=0.99 is eta=0.06855265189220769
Lower bound sat.prob. for beta=0.999 is eta=0.06732810971248507
Lower bound sat.prob. for beta=0.9999 is eta=0.06623008822231909
Time required to compute guarantees: 0.981542110443
OUTPUT FOR MODEL: brp/brp_256_5.pm
----------
Start for N=100
Run time per iteration (of N samples) in Storm: 0.17193617820739998
Confidence probability for eta=0.055 is beta=0.09252784480340778
Lower bound sat.prob. for beta=0.9 is eta=0.01957309401520428
Lower bound sat.prob. for beta=0.99 is eta=0.013873261824668595
Lower bound sat.prob. for beta=0.999 is eta=0.010169174483189072
Lower bound sat.prob. for beta=0.9999 is eta=0.007623045240642003
Time required to compute guarantees: 0.030745744705
----------
Start for N=500
Run time per iteration (of N samples) in Storm: 0.7899937152863
Confidence probability for eta=0.055 is beta=0.23443321015220137
Lower bound sat.prob. for beta=0.9 is eta=0.042417193898141005
Lower bound sat.prob. for beta=0.99 is eta=0.03757861942219767
Lower bound sat.prob. for beta=0.999 is eta=0.03371348733905952
Lower bound sat.prob. for beta=0.9999 is eta=0.030501941901854623
Time required to compute guarantees: 0.045060396194
----------
Start for N=1000
Run time per iteration (of N samples) in Storm: 1.4779496669769
Confidence probability for eta=0.055 is beta=0.354489951353753
Lower bound sat.prob. for beta=0.9 is eta=0.05097401453696747
Lower bound sat.prob. for beta=0.99 is eta=0.047136597263176705
Lower bound sat.prob. for beta=0.999 is eta=0.043959036700511836
Lower bound sat.prob. for beta=0.9999 is eta=0.04123415201687457
Time required to compute guarantees: 0.063256263733
----------
Start for N=5000
Run time per iteration (of N samples) in Storm: 8.549068236351001
Confidence probability for eta=0.055 is beta=0.9999656140629668
Lower bound sat.prob. for beta=0.9 is eta=0.06447605013757067
Lower bound sat.prob. for beta=0.99 is eta=0.06255340518142041
Lower bound sat.prob. for beta=0.999 is eta=0.060890664054760825
Lower bound sat.prob. for beta=0.9999 is eta=0.05941233576382958
Time required to compute guarantees: 0.272138595581
----------
Start for N=10000
Run time per iteration (of N samples) in Storm: 16.7263259410858
Confidence probability for eta=0.055 is beta=0.9999999999417923
Lower bound sat.prob. for beta=0.9 is eta=0.07109763310506087
Lower bound sat.prob. for beta=0.99 is eta=0.06968529460052382
Lower bound sat.prob. for beta=0.999 is eta=0.06845068658748185
Lower bound sat.prob. for beta=0.9999 is eta=0.06734360071515903
Time required to compute guarantees: 0.642244815826OUTPUT FOR MODEL: brp/brp_256_5.pm
----------
Start for N=100
Run time per iteration (of N samples) in Storm: 0.143
Confidence probability for eta=0.055 is beta=-19.6483
Lower bound sat.prob. for beta=0.9 is eta=0.20421
Lower bound sat.prob. for beta=0.99 is eta=0.23246
Lower bound sat.prob. for beta=0.999 is eta=0.2582
Lower bound sat.prob. for beta=0.9999 is eta=0.28209
Time required to compute guarantees: 0.011152505875
----------
Start for N=10000
Run time per iteration (of N samples) in Storm: 13.789
Confidence probability for eta=0.055 is beta=1.0
Lower bound sat.prob. for beta=0.9 is eta=0.08984
Lower bound sat.prob. for beta=0.99 is eta=0.09128
Lower bound sat.prob. for beta=0.999 is eta=0.0926
Lower bound sat.prob. for beta=0.9999 is eta=0.09383
Time required to compute guarantees: 0.01039648056
\ No newline at end of file
OUTPUT FOR MODEL: consensus/coin2.pm
----------
Start for N=100
Run time per parameter sample in Storm: 0.744772195816
Confidence probability for eta=0.28 is beta=0.0
Lower bound sat.prob. for beta=0.9 is eta=0.16388104088540187
Lower bound sat.prob. for beta=0.99 is eta=0.14086084271198646
Lower bound sat.prob. for beta=0.999 is eta=0.12328277841116682
Lower bound sat.prob. for beta=0.9999 is eta=0.1091022988683045
Time required to compute guarantees: 0.049267530441
----------
Start for N=500
Run time per parameter sample in Storm: 3.557334184647
Confidence probability for eta=0.28 is beta=0.16580844005220569
Lower bound sat.prob. for beta=0.9 is eta=0.24070488439810647
Lower bound sat.prob. for beta=0.99 is eta=0.22852285991119473
Lower bound sat.prob. for beta=0.999 is eta=0.21841674422467633
Lower bound sat.prob. for beta=0.9999 is eta=0.20966918686030495
Time required to compute guarantees: 0.185102939606
----------
Start for N=1000
Run time per parameter sample in Storm: 7.637410402298
Confidence probability for eta=0.28 is beta=0.29131160586257465
Lower bound sat.prob. for beta=0.9 is eta=0.26310366311458033
Lower bound sat.prob. for beta=0.99 is eta=0.25433441511943267
Lower bound sat.prob. for beta=0.999 is eta=0.2469358717088598
Lower bound sat.prob. for beta=0.9999 is eta=0.24044842040271758
Time required to compute guarantees: 0.326511621475
----------
Start for N=5000
Run time per parameter sample in Storm: 47.126279592514
Confidence probability for eta=0.28 is beta=0.9911584894580301
Lower bound sat.prob. for beta=0.9 is eta=0.2890970205100354
Lower bound sat.prob. for beta=0.99 is eta=0.28523187240814885
Lower bound sat.prob. for beta=0.999 is eta=0.2818896070061145