% Delivered to the Government in Accordance with Contract FA8650-10-C-7080
% 
%  (c) 2011 United Technologies Corp.
% Developed with the sponsorship of the Defense Advanced Research Projects Agency (DARPA).
%  
% Permission is hereby granted, free of charge, to any person obtaining a copy of this data, including any software or models in source or binary form, as well as any drawings, specifications, and documentation (collectively "the Data"), to deal in the Data without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Data, and to permit persons to whom the Data is furnished to do so, subject to the following conditions:
%  
% The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Data.
%  
% THE DATA IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS, SPONSORS, DEVELOPERS, CONTRIBUTORS, OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE DATA OR THE USE OR OTHER DEALINGS IN THE DATA.
% 


function y = Abstract(I_d,I_c,Output,Model)

%% Read Inputs from files
fid = fopen(I_c); % 'inputc.csv'
Inp = textscan(fid, '%s%s%f%f');
fclose(fid);

inp_id = find(strcmp(Inp{2},'keep'));
I_c = Inp{1}(inp_id);

A_c.lower = Inp{3}(inp_id);
A_c.upper = Inp{4}(inp_id);

clear Inp

fid = fopen(I_d);%'inputd.csv'
Inp = textscan(fid, '%s%s%s%s');
fclose(fid);

I_d = find(strcmp(Inp{2},'keep'));

fid = fopen(Output);%('output.csv');
Inp = textscan(fid, '%s%s');
fclose(fid);

inp_id = find(strcmp(Inp{2},'keep'));
O = Inp{1}(inp_id);

fid = fopen(Model); % 'model.csv'
model_ref = fgetl(fid);
fclose(fid);




%% code
model = str2func(model_ref);

[out,output,in,params,vars_keep,discrete_vars_names,discrete_vars] = model(I_c,A_c);

abs_u = setdiff(1:size(in,2),vars_keep); % these are the variables to abstract out

abs_x = [];
% these are the outputs of interest
for i = 1:size(O,2),
    elem = find(strcmp(O{i},output));
    if ~isempty(elem),
        abs_x = [abs_x elem];
        Xtilde{i} = out{elem};
    else
        error('check the output list O');
    end
end



%% this part computes the maxima and the minima over the abstracted variables
for i = 1:size(Xtilde,2),
    for j = 1:size(Xtilde{i},2),
        tmax = Xtilde{i}{j};
        tmin = tmax;
        for k = 1:length(abs_u),
            tmax = max(tmax,[],abs_u(k));
            tmin = min(tmin,[],abs_u(k));
        end
        Xtildemax{i}{j} = tmax;
        Xtildemin{i}{j} = tmin;
    end
end

%% this part performs the least squares linear fit

vars_keep = sort(vars_keep);

for i = 1:length(abs_x),
   
    for j = 1:size(Xtildemax{i},2),
        
        data = in{vars_keep(1)}';
        
        for k = 2:length(vars_keep),
        
            xbar = repmat(data,length(in{vars_keep(k)}),1);
            ybar = repmat(in{vars_keep(k)},size(data,1),1);
            data = [xbar ybar(:)];
        end
        z = Xtildemax{i}{j}(:);
        
        % least squares step 
        [CoeffsUB{i}{j},ResnormUB{i}(j)] = lsqcurvefit(@linearfun,ones(1,(length(vars_keep)+1)),data,z);
       
        
        z = Xtildemin{i}{j}(:);
        % least squares step 
        [CoeffsLB{i}{j},ResnormLB{i}(j)] = lsqcurvefit(@linearfun,ones(1,(length(vars_keep)+1)),data,z);
        
    end
end

%% this part writes the guarantees to the file guarantees.out
fid = fopen('Abstraction_output.out','w');

for i = 1:length(abs_x),
     for j = 1:size(Xtildemax{i},2),
        G_upper{i}{j} = strcat(num2str(output{abs_x(i)}),32,'<=',32,num2str(CoeffsUB{i}{j}(end)));
        G_lower{i}{j} = strcat(num2str(output{abs_x(i)}),32,'>=',32,num2str(CoeffsUB{i}{j}(end)));
     end
end

        
for i = 1:length(abs_x),
    for j = 1:size(Xtildemax{i},2),
        for k = 1:length(vars_keep),
            G_upper{i}{j} = strcat(G_upper{i}{j},32,'+',32,num2str(CoeffsUB{i}{j}(k)),'*',num2str(params{vars_keep(k)}));
            G_lower{i}{j} = strcat(G_lower{i}{j},32,'+',32,num2str(CoeffsLB{i}{j}(k)),'*',num2str(params{vars_keep(k)}));
        end
    end
end



if isempty(I_d),
    for i = 1:length(abs_x),
        for j = 1:size(Xtildemax{i},2),
            fprintf(fid,'((%s) AND (%s))',G_upper{i}{j},G_lower{i}{j});
            if (j < size(Xtildemax{i},2)),
                fprintf(fid,' OR ');
            end
        end
        fprintf(fid,' ;');
        fprintf(fid,'\n\n');
    end
else
    n = 1;
    for i = 1:size(discrete_vars,2),
        for j = 1:size(discrete_vars{i},2),
            disc_string{i}{j} = strcat(discrete_vars_names{i},' = ',32,discrete_vars{i}{j});
        end
        L{i} = 1:j;
        n = n*j;
    end
    
    P = allcomb(L{:});
    
    for k = 1:n,
        str{k} = strcat('if',32,disc_string{1}{P(k,1)});
        for i = 2:size(discrete_vars,2),
            str{k} = strcat(str{k},32,'AND',32,disc_string{i}{P(k,i)});
        end
        
        str{k} = strcat(str{k},32,'then');
        fprintf(fid,'%s \n',str{k});
        for i = 1:length(abs_x),
                
            fprintf(fid,'(%s) AND (%s)',G_upper{i}{k},G_lower{i}{k});
            fprintf(fid,' ;');
            fprintf(fid,'\n\n');
        end
        
    end
end

fclose(fid);
