# BIET

BIET.m — Objective-C source code, 2 kB (2417 bytes)

## File contents

function [t0, t1, p, n, x] = BIET(delta, c, alpha, beta, traces_res) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % BIET - Function of bayesian interval estimation testing % % BIET(DELTA, C, ALPHA, BETA, TRACES_RES) % % DELTA - half size of an estimation interval which may contain target % probability % % C - Bayesian coverage goal % % ALPHA, BETA - parameters of Beta prior % % TRACES_RES - the results of model-checking traces (0: fail, 1: success) % % % $Revision: 1.2.1 $ % $Date: 2012/12/19 14:07:32 $ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% n = 0; % initial total number of samples x = 0; % initial number of success samples r = 0; % initial posterior probability of estimation interval cnt = 1; % initial index of traces_res while r < c % until r satisfies user-given coverage goal % add 1 to total number of samples n = n + 1; % if cnt's result of model-checking traces is success, % add 1 to number of success samples if traces_res(cnt) == 1 x = x + 1; end cnt = cnt + 1; % compute the Beta prior probability with alpha and beta p = (x + alpha)/(n + alpha + beta); % compute the estimation interval which may contain target probability t0 = p - delta; t1 = p + delta; if t1 > 1 t0 = 1 - 2*delta; t1 = 1; elseif t0 < 0 t0 = 0; t1 = 2*delta; end % compute posterior probability r that target probability % is included within interval (t0,t1) r = posterior_prob(t0,t1,n,x,alpha,beta); % log for each step str=sprintf('t0: %f t1: %f p: %f n: %d x: %d\n',t0,t1,p,n,x); disp(str); end end function result = posterior_prob(t0,t1,n,x,alpha,beta) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % posterior_prob - Function of calculating the posterior probability of % Bernoulli samples and Beta prior of parameters alpha and beta % % POSTERIOR_PROB(T0,T1,N,X,ALPHA,BETA) % % T0 - left-open value of estimated interval % T1 - right-open value of estimated interval % N - total number of samples % X - number of success Bernoulli samples % ALPHA, BETA - parameters of Beta prior %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% result = betacdf(t1,x+alpha,n-x+beta)-betacdf(t0,x+alpha,n-x+beta); end