% Save the models to the file

% Multiplication coefficient for timed automata
MULT_COEFF = 1;

% Time Lower Rate Interval (TLRI) in ms
TLRI = 1000;

% Convert time step in ms
tstep_ms=dt*1000;

fid=fopen('/Users/mereacre/Documents/Marco/Heart_Model/Model/heartio.pm','w+');

% PRISM PTA file
% pta
fprintf(fid,'pta\n\n');

% const int TLRI = 10000
fprintf(fid,'const int TLRI = %d;\n',TLRI*MULT_COEFF);

% const int tstep = ?
tstep_ms=ceil(tstep_ms*MULT_COEFF);

fprintf(fid,'const int tstep = %d;\n\n',tstep_ms);

% label "fail"=s=2;
fprintf(fid,'label "fail"=s=2;\n\n');


% module Monitor
fprintf(fid,'module Monitor\n');

%   s : [0..2] init 0;
fprintf(fid,'\t s : [0..2] init 0;\n');

%   x : clock;
fprintf(fid,'\t x : clock;\n\n');

%   [VS] s=0 -> (s'=1) & (x'=0);
fprintf(fid, '\t [VS] s=0 -> (s''=1) & (x''=0);\n');

%   [VS] (s=1) & (x<=TLRI) -> (s'=1) & (x'=0);
fprintf(fid, '\t [VS] (s=1) & (x<=TLRI) -> (s''=1) & (x''=0);\n');

%   [VS] (s=1) & (x>TLRI) -> (s'=2) & (x'=0);
fprintf(fid, '\t [VS] (s=1) & (x>TLRI) -> (s''=2) & (x''=0);\n');

% endmodule
fprintf(fid,'endmodule\n\n');

% module Heart_Example
fprintf(fid,'module Heart_Example\n');

%   s1 : [0..9] init 0;
fprintf(fid,'\t s1 : [0..%d] init 0;\n',N_STATES-1);

%   x1 : clock;
fprintf(fid,'\t x1 : clock;\n\n');

%   invariant
fprintf(fid,'\t invariant\n');

for i=1:N_STATES,
    
    %       (s1=0 => x1<=tstep) &
    fprintf(fid,'\t\t (s1=%d => x1<=tstep) ',i-1);
    
    if i~=N_STATES,
        fprintf(fid,'&\n');
    else
        fprintf(fid,'\n');
    end
end

%   endinvariant
fprintf(fid,'\t endinvariant\n\n');


% Write the automata transitions
cnt_A=1;
cnt_V=1;
A_V_event=0;
for i=1:N_STATES-1,
    
    % Check for both Atrium and Ventricle starting event
    if cnt_A<=size(AS,1) && cnt_V<=size(VS,1),
        if i+1==AS(cnt_A) && i+1==VS(cnt_V),
            error('Error: two events at the same time');
        end
    end
    
    % Check for the Atrium starting event
    if cnt_A<=size(AS,1) && A_V_event==0,
        if i+1==AS(cnt_A),
            fprintf(fid,'[Aget] s1=%d & (x1=tstep) -> (s1''=%d) & (x1''=0);\n',i-1,i);
            cnt_A=cnt_A+1;
            A_V_event=1;
        end
    end
    
    % Check for the Ventricle starting event
    if cnt_V<=size(VS,1) && A_V_event==0,
        if i+1==VS(cnt_V),
            fprintf(fid,'[Vget] s1=%d & (x1=tstep) -> (s1''=%d) & (x1''=0);\n',i-1,i);
            cnt_V=cnt_V+1;
            A_V_event=1;
        end
    end
    
    if A_V_event==0,
        fprintf(fid,'[] s1=%d & (x1=tstep) -> (s1''=%d) & (x1''=0);\n',i-1,i);
    end
    A_V_event=0;
end

% endmodule
fprintf(fid,'endmodule\n');

% Save the automata

fclose(fid);