##### Personal tools
You are here: Home SMC BIET

# 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
```
##### Document Actions 