piha.m~

CheckMate is a MATLAB-based tool for modeling, simulating and investigating properties of hybrid dyn

end

%**************************************************************
%Create list of locations and all guards for each location
%**************************************************************
k=ones(1,length(sfdata));
%Find the total number of possible locations
no_loc=1;
for j=1:length(sfdata)
   machine{j}.states=sf('get',sfdata{j}.StateflowChartID,'.states');
   no_loc=no_loc*length(machine{j}.states);
end
locations=[];

% Reset operation. It maps the FSMB to SCSB
% Ansgar Fehnker 09/16/2002


% Compute which fsmb is connceted to which scsb
for k0 =1:length(fsmbHandle)
  fsmb2scsb{k0} = [];
end

for k1 = 1:length(scsbHandle)
  if strcmp(get_param(scsbHandle(k1),'use_reset'),'on')
    inputfsmb_Handle = trace_scsb_input(scsbHandle(k1),'reset');
    % The error checking in trace_scsb_input ensures that only one FSMB
    % is returned in inputfsmb_Handle.
    fsmbindex = find(inputfsmb_Handle == fsmbHandle);
    fsmb2scsb{fsmbindex} = [fsmb2scsb{fsmbindex} k1];
  end
end

%Find all possible locations by attempting all combinations of states
%and machines
for j=1:no_loc

   %Test each combination to see if it is a null state
   for i=1:length(sfdata)
      q(i)=machine{i}.states(k(i));
   end
   null_state=is_terminal_state(q);
   if null_state==0
      new=length(locations)+1;
      number_trans=0;
      for l=1:length(q)
         % "only_condition_inputs_flag" added by JimK (11/2002).  The purpose of the flag
         % is to notify "create_guard" if there are only condition inputs into the stateflow
         % block.  If this is the case, all edges should be flagged as event edges.
         if isempty(sfdata{l}.InputEvent)
            only_condition_inputs_flag = 1;
         else
            only_condition_inputs_flag = 0;
         end
      	transitions=sf('get',q(l),'.srcTransitions');
      	names=sf('get',transitions,'.labelString');
         for p=1:size(names,1)
            number_trans=number_trans+1;
            locations{new}.transitions{number_trans}.id=transitions(p);
            [event_expr,condition_expr,clock,reset_flag]=process_label_string(names(p,:),sfdata,l,clockHandle);
            [total_expression,event_expression,condition_expression]=find_cond_expr(sfdata,condition_expr,event_expr,l);
            locations{new}.transitions{number_trans}.expression=total_expression;
            locations{new}.transitions{number_trans}.clock=clock;
                        locations{new}.transitions{number_trans}.idx=l;    % Zhi add this to record the index of transition in q
            locations{new}.transitions{number_trans}.source=sf('get',transitions(p),'.src.id');
            locations{new}.transitions{number_trans}.destination=sf('get',transitions(p),'.dst.id');
            locations{new}.transitions{number_trans}.destination_name=sf('get',sf('get',transitions(p),'.dst.id'),'.name');
            locations{new}.transitions{number_trans}.reset_flag=reset_flag;

            % Stores the scsb that defines the reset
            locations{new}.transitions{number_trans}.reset_scs_index=fsmb2scsb{l};

            %Find guard region.  Result will be pointers to cell locations which describe this guard
            [guard_cells,guard_cell_event_flags,guard_compl_cells]=create_guard(condition_expression,event_expression,pthbHandle,pthb,NAR,only_condition_inputs_flag);
            locations{new}.transitions{number_trans}.guard=guard_cells;
            locations{new}.transitions{number_trans}.guard_cell_event_flags=guard_cell_event_flags;
            locations{new}.transitions{number_trans}.guard_compl=guard_compl_cells;

         end %for
      end%for
      %Use guard complements from every transition from this location to compute
      %the 'invariant' for this location.  The idea is to intersect all of the
      %complements of the guards for this location.  This is done iteratively by
      %intersecting the first guard complement with the next, then taking the result
      %and intersecting it with the 3rd and so on (i.e  ( A and B ) and C ....)
%       clean_loc=clean_transition(locations{new});
%        locations{new}.transitions=clean_loc.transitions;
           locations{new}.q=q;
      locations{new}.state=sf('get',q,'.name');
      locations{new}.interior_cells=[];
           invariant=intersect_complements(locations,new);
      locations{new}.interior_cells=invariant;
   end%if



   for n=1:length(k)
      if k(n)+1<=length(machine{n}.states)
            k(n)=k(n)+1;
            break;
      else
            k(n)=1;
      end%if
   end%for
end%for


% **********************************************************************
% (4.1) Reposition the locations to make the initial locations the first ones.
% **********************************************************************


if (size(q0,1)~=1) | ~all(locations{1}.q==q0(1,:))
    relocation_count = 1;
    for i=1:size(q0,1)
        for j=1:length(locations)
            if all(locations{j}.q==q0(i,:))

                location_to_move =locations{j};
                location_from_move=locations{relocation_count};
                locations{relocation_count}= location_to_move;
                locations{j}= location_from_move;
                relocation_count=relocation_count +1;

            end%if
            if relocation_count > size(q0,1)
                break
            end
        end%for
    end%for
end%end

% **********************************************************************
% (5) Create lists of blocks for each block type in the CheckMate model.
% **********************************************************************

% (i) Switched continuous system blocks (SCSB)
scsbList = cell(length(scsbHandle),1);
use_sd=0;
for k = 1:length(scsbHandle)
  scsbList{k}.name = get_param(scsbHandle(k),'Name');
  scsbList{k}.nx = eval(get_param(scsbHandle(k),'nx'));
  scsbList{k}.nz = eval(get_param(scsbHandle(k),'nz'));
  scsbList{k}.nup = eval(get_param(scsbHandle(k),'nup'));
  if strcmp(get_param(scsbHandle(k),'use_sd'),'on')
      use_sd=1;
  end
  scsbList{k}.nu = eval(get_param(scsbHandle(k),'nu'));
  scsbList{k}.swfunc = get_param(scsbHandle(k),'swfunc');
  % parametric information
  scsbList{k}.pacs = evalin('base',get_param(scsbHandle(k),'PaCs'));
  scsbList{k}.paradim = length(evalin('base',get_param(scsbHandle(k),'p0')));
  inputfsmb_Handle = trace_scsb_input(scsbHandle(k),'input');

  fsmbindices = [];
  for l = 1:length(inputfsmb_Handle)
    fsmbindices(l) = find(inputfsmb_Handle(l) == fsmbHandle);
  end
  scsbList{k}.fsmbindices = fsmbindices;
end

% (ii) Finite state machine blocks (FSMB)
fsmbList = cell(length(sfdata),1);
for k = 1:length(sfdata)
  chart_id = sfdata{k}.StateflowChartID;
  state_id = sf('find','all','state.chart',chart_id);
  states = {};
  for l = 1:length(state_id)
    state_number = get_state_number(state_id(l));
    states{state_number} = sf('get',state_id(l),'.name');
  end
  fsmbList{k}.name = get_param(sfdata{k}.SimulinkHandle,'Name');
  fsmbList{k}.states = states;
end

% (iii) Polyhedral threshold blocks (PTHB)
pthbList = cell(length(pthbHandle),1);
for k = 1:length(pthbHandle)
  pthbList{k}.name = get_param(pthbHandle(k),'Name');
end

% Finally, replace all Stateflow state id by the enumeration
% given in the label (the entry action) of each state.
for k = 1:length(locations)
  locations{k}.q = get_labeled_state(locations{k}.q);
  for l = 1:length(locations{k}.transitions)
    	locations{k}.transitions{l}.destination =            get_labeled_state(locations{k}.transitions{l}.destination);
% moved
       locations{k}.transitions{l}.source=           get_labeled_state(locations{k}.transitions{l}.source);
% moved

  end
end

%*************************************************************************************
%Find inital regions and initial states
%*************************************************************************************

% Get initial continuous set from the parameter block
X0 = get_initial_continuous_set(scsbHandle);

% Identify initial cells from intersection with initial continuous set X0.
% P0 contains all indices (to SSTREE) for the leaf nodes corresponding
% to initial cells.
P0 = [];
for k = 1:length(X0)
      test=find_initial_cells(X0{k},locations{1},AR);
      if ~isempty(test)
         P0 = union(P0,test);
      end
end

L0=[ones(length(P0),1) P0'];
for location_counter=1:length(locations)
    locations{location_counter}.orig_interior_cells=locations{location_counter}.interior_cells;
end

[initial_conditions , locations] = find_initial_conditions(X0,locations);

% Conversion completed, return the PIHA object.
% GLOBAL_PIHA.Hyperplanes should already be assigned.  Assign
% everything else here.
GLOBAL_PIHA.NAR                  = NAR;
GLOBAL_PIHA.InitialContinuousSet = X0;
GLOBAL_PIHA.InitialDiscreteSet   = {get_labeled_state(q0)};
GLOBAL_PIHA.Cells                = CELLS;
GLOBAL_PIHA.InitialCells         = P0;
GLOBAL_PIHA.Locations            = locations;
GLOBAL_PIHA.InitialConditions    = initial_conditions;
GLOBAL_PIHA.InitialLocation_Cells= L0;
GLOBAL_PIHA.CLOCKBlocks				= clockList;
GLOBAL_PIHA.SCSBlocks            = scsbList;
GLOBAL_PIHA.PTHBlocks            = pthbList;
GLOBAL_PIHA.FSMBlocks            = fsmbList;
GLOBAL_PIHA.use_sd               = use_sd;


disp('PIHA conversion successful.')
return

%------------------------------------------------------------------------------