compute_mapping_no_sd.m

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

      % guard cell face.
      dst_cell_inv = return_invariant(guard_cells(i));
      for k = 1:length(mapping)
        if isfeasible(mapping{k}, dst_cell_inv) 
          % If the event flag set to 1 for the current guard cell face being
          % hit, then we know that the parent transition for this guard cell
          % must be enabled. Add the enabled transition to the list for
          % its parent FSMB.
          if guard_cell_event_flags{i}(boundary_idx)
            fsm_idx = transitions{j}.idx;
            enabled{fsm_idx} = [enabled{fsm_idx} j];
            enabled_transition_found = 1;
          end
          % Keep the list of guard cells reached by the mapping.
          guard_cells_reached = union(guard_cells_reached,guard_cells(i));
          break;
        end
      end
    end
  end
end

destination = [];
terminal=[];

if enabled_transition_found
  
  % If there are enabled transitions, find all next possible
  % locations. 
  [dest_loc,dest_scs_reset,terminal] = ...
      find_destination_location(srcloc,transitions,enabled);

  % For each non-terminal destination location, find the destination
  % interior cells and a new entry into the destination list for each
  % destination cell found.
  for i = 1:length(dest_loc)
    % Apply the reset transformation for the destination location to
    % the mapping polytopes.
    q = GLOBAL_PIHA.Locations{dest_loc(i)}.q;
    scs_reset_indices = dest_scs_reset{i};
    [T,v] = overall_system_reset(GLOBAL_PIHA.SCSBlocks,q,scs_reset_indices);
    reset_mapping = {};
    for k = 1:length(mapping)
      % The new transform routine should give full dimensional polytope even
      % if T is singular.
      reset_mapping{k} = transform(mapping{k},T,v);
    end
    
    % Intersect each interior cell with the reset mapping polytopes. Add
    % each non-empty result to the destination list.
    found = 0;
    interior_cells = GLOBAL_PIHA.Locations{dest_loc(i)}.interior_cells;
    for j = 1:length(interior_cells)
      dst_cell_inv = return_invariant(interior_cells(j));
      intersection = {};
      for k = 1:length(reset_mapping)
        intersection_k = reset_mapping{k} & dst_cell_inv;
        if isfeasible(reset_mapping{k}, dst_cell_inv)
          intersection{end+1} = reset_mapping{k};
        end
      end
      if ~isempty(intersection)
        % Over approximate the intersection between the reset mapping
        % polytopes and the destination cell by a single polytope and
        % intersect it with the destination cell again before adding
        % the mapping to the destination list.
        temp.cell = interior_cells(j);
        temp.location = dest_loc(i); 
        temp.mapping = bounding_box(intersection) & dst_cell_inv;
        temp.Tstamp = [];
        destination = [destination temp];
        % Turn on the flag indicating that we have found at least one
        % destination cell in the interior region.
        found = 1;
      end
    end
      
    % If no destination interior cell is found, issue an error message to
    % the user about this.
    if ~found
      src_name = location_name(srcloc);
      dst_name = location_name(dest_loc(i));
      msg = [sprintf('\n\n') 'Transition from location ' src_name ...
             ' to location ' dst_name ' lands the system completely ' ...
             'outside of ' sprintf('\n') 'the interior region of the ' ...
             'destination location. Reachability not reliable!'];
      error(msg);
    end
  end %for i

else

  % If no transition is enabled but some guard cells have been reached,
  % warn the user about this.
  if ~isempty(guard_cells_reached)
    msg = ['Warning: Reachability analysis indicates that the system may ' ...
           'exit the interior region' sprintf('\n') 'without taking any ' ...
           'transition from cell ' num2str(srccell) ' of location ' ...
           location_name(srcloc) '.'];
    fprintf(1,'%s\n',msg);
    return
  end
  
end
  
return

% =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

function [dest_loc,dest_reset,terminal] = ...
    find_destination_location(srcloc,transitions,enabled)
                 
% Given the list of enabled transitions for all FSMBs, find the list of
% next possible destination locations and the indices of SCSBs to be
% reset for each destination location.
%
% Inputs:
%   * "srcloc" - Source location index.
%   * "transitions" - A structure representing the list of FSM transitions
%      for the current location.
%   * "enabled" - A cell array of the same length as the number of
%     FSMBs. Each cell "enabled{i}" is a vector containing the indices for
%     the transitions that have been enabled for the i-th FSMB.
%
% Outputs:
%   * "dest_loc" - A vector of location indices representing the list of
%     next possible locations.
%   * "dest_reset" - A cell array of vectors. Each element "dest_reset{i}" 
%     of the cell array contains the indices of the SCSBs to be reset if
%     the transition to the location "dest_loc(i)" is taken.
%   * "terminal" - A matrix of row vectors. Each row contains the FSMB
%     state vector corresponding to a terminal FSM state that can be
%     reached.

global GLOBAL_PIHA 

q = GLOBAL_PIHA.Locations{srcloc}.q;

% From the list of enabled transitions, find the unique combinations of the
% next state and reset flag for each FSMB.
dest = cell(1,length(q));
for k = 1:length(q)
  if isempty(enabled{k})
    % If no transition is enabled for the current FSMB, then the only
    % possible combination is that the next state is the same as the current
    % state and the reset flag is zero.
    dest{k} = [q(k) 0];
  else
    dest{k} = [];
    for i = 1:length(enabled{k})
      % Find the next q and reset flag for the current transition for the
      % current FSMB.
      next_q = transitions{enabled{k}(i)}.destination;
      next_reset = transitions{enabled{k}(i)}.reset_flag;
      next_combo = [next_q next_reset];
      % Verify that the next state and reset flag combo is unique before
      % including it in the destination list for the current FSMB.
      found = 0;
      for j = 1:size(dest{k},1)
        if all(next_combo == dest{k}(j,:))
          found = 1;
          break;
        end
      end
      if ~found
        dest{k} = [dest{k}; next_combo];
      end
    end
  end
end

% Compute all possible combinations (cross products of the next 'q' vectors
% and 'reset' vectors across all FSMBs. When the loop below finishes,
% "dest_q" and "dest_reset_fsm" are matrices of the same size. "dest_q(i,:)"
% and "dest_reset_fsm(i,:)" go together to represent a combination being
% generated below. For the i-th combination, "dest_q(i,j)" is the next state
% and "dest_reset_fsm(i,j)" is the reset flag for the j-th FSMB.
dest_q = dest{1}(:,1);
dest_reset_fsm = dest{1}(:,2);
for k = 2:length(q)
  dest_q_new = [];
  dest_reset_fsm_new = [];
  m = size(dest_q,1);
  for i = 1:size(dest{k},1)
    dest_q_new = [dest_q_new; [dest_q dest{k}(i,1)*ones(m,1)]];
    dest_reset_fsm_new = [dest_reset_fsm_new;
                    [dest_reset_fsm dest{k}(i,2)*ones(m,1)]];
  end
  dest_q = dest_q_new;
  dest_reset_fsm = dest_reset_fsm_new;
end
clear dest_q_new
clear dest_reset_fsm_new

% Get the list of SCSBs to be reset by each FSMB. This list is identical for
% all transitions under the same FSM, so we can just grab the list from the
% first transition found under each FSM.
for k = 1:length(q)
  if isempty(enabled{k})
    reset_scs_idx{k} = [];
  else
    reset_scs_idx{k} = transitions{enabled{k}(1)}.reset_scs_index;
  end
end

% Convert the reset flag vector for each FSMB in each row of
% "dest_reset_fsm" into an index vector for SCSB to be reset.
dest_reset_scs_idx = cell(size(dest_reset_fsm,1),1);
for i = 1:size(dest_reset_fsm,1)
  for j = 1:size(dest_reset_fsm,2)
    if dest_reset_fsm(i,j)
      dest_reset_scs_idx{i} = ...
          union(dest_reset_scs_idx{i},reset_scs_idx{j});
    end
  end
end

% Find the destination location in GLOBAL_PIHA that corresponds to each
% row of "dest_q".
dest_loc = [];
dest_reset = {};
terminal = [];
for i = 1:size(dest_q,1)
  found = 0;
  for j = 1:length(GLOBAL_PIHA.Locations)
    if all(GLOBAL_PIHA.Locations{j}.q == dest_q(i,:))
      found = 1;
      break;
    end
  end
  if found
    % If a matching location is found, add the location index and the
    % corresponding list of SCSB to be reset to output list.
    dest_loc = [dest_loc; j];
    dest_reset = [dest_reset; {dest_reset_scs_idx{i}}];
  else
    % If a matching location is not found, add the 'q' vector to the
    % terminal state list.
    terminal = [terminal; dest_q(i,:)];
  end
end

return

% =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

function str = location_name(loc)

global GLOBAL_PIHA

% The state names stored in the .state field of the locations are
% character matrices, i.e. each row of .state contains the name
% of each component state.
name = GLOBAL_PIHA.Locations{loc}.state;
str = '(';
for k = 1:size(name,1)
  if (k > 1)
    str = [str ','];
  end
  str = [str deblank(name(k,:))];
end
str = [str ')'];

return

% =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

function box = bounding_box(mapping)

% New version of this routine: uses the chosen option for hull computation to
% determine the bounding box.
%
% --OS--06/21/02

global GLOBAL_APPROX_PARAM

V = vertices;
if length(mapping) > 1
  for j = 1:length(mapping)
    vj = vertices(mapping{j});
    V = V | vj;
  end   
  box = linearcon(polyhedron(V));
else
%   Changed from
%  box = mapping{1};
%   to the following codes by Dong Jia, Mar. 27.
     [CE,dE,CI,dI]=linearcon_data(mapping{1});
%     if length(CE)==0
%         box=mapping{1};
%     else
         CI=[CI;CE;-CE];
         dI=[dI;[dE;-dE]+ones(2*length(dE),1)*GLOBAL_APPROX_PARAM.poly_bloat_tol];
         box=linearcon([],[],CI,dI);
         box=clean_up(box);
%     end
end
return