piha.m

一个matlab的将军模型

      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);
       locations{k}.transitions{l}.source=...
          get_labeled_state(locations{k}.transitions{l}.source);

  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

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

function [pthb,NAR]=create_hyperplanes(NBDHP,AR,pthb)

global GLOBAL_PIHA
global GLOBAL_APPROX_PARAM
global GLOBAL_OPTIM_PAR

hyperplanes = [];

% This function creates the list of hyperplanes. It originally resided in the 
% 'partition_ss' function, but it has become necessary to have the hp's before
% the state space is divided. 

% Put hyperplanes constituting the boundary of AR at the beginning of the
% hyperplane list.

[CE,dE,CAR,dAR] = linearcon_data(AR);
hyperplanes = {};
for k = 1:length(dAR)
  hyperplanes{k}.pthb = -1;
  hyperplanes{k}.index = k;
  hyperplanes{k}.c = CAR(k,:);
  hyperplanes{k}.d = dAR(k);
end
NAR = length(hyperplanes);

hyperplane_tol = GLOBAL_APPROX_PARAM.poly_hyperplane_tol;
counter_hyperplanes=NAR;
for k = 1:length(NBDHP)
    dup=0;
  for j=1:counter_hyperplanes
        c1 = hyperplanes{j}.c;
        b1 = hyperplanes{j}.d;
        c =NBDHP{k}.c;
        b=NBDHP{k}.d;
        MATRIX = [c1 b1; c b];
        if rank(MATRIX,hyperplane_tol) < 2 
         dup=1;
         i=NBDHP{k}.pthb;
         pthb{i}.hps=[pthb{i}.hps j];
         break;
     else
         dup=0;
     end
  end
  if dup==0
  counter_hyperplanes = counter_hyperplanes+1;
  hyperplanes{counter_hyperplanes}.pthb = NBDHP{k}.pthb;
  hyperplanes{counter_hyperplanes}.index = NBDHP{k}.index;
  hyperplanes{counter_hyperplanes}.c = NBDHP{k}.c;
  hyperplanes{counter_hyperplanes}.d = NBDHP{k}.d;
  end
end

%Sort out which HP's go with which pthb
for n=NAR+1:length(hyperplanes)
   j=hyperplanes{n}.pthb;
   if j~=-1
      pthb{j}.hps=[pthb{j}.hps n];
   end
end

GLOBAL_PIHA.Hyperplanes = hyperplanes;

return

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

function [guard_cells,guard_cell_event_flags,guard_compl_cells] = ...
    create_guard(cond_expr,event_expr,pthbHandle,pthb,NAR,only_condition_inputs_flag)

% This procedure divides up the analysis region and returns pointers
% to cells that describe a guard region.

global CELLS 

guard_cells=[];
guard_compl_cells=[];
guard_cell_event_flags=[];

% Find all PTHBs which appear in condition expression.
guard_pthbs = [];
for i = 1:length(pthbHandle)
  name = get_param(pthbHandle(i),'name');
  % Need to fix the code below since findstr() will return all
  % matching substrings, which may be incorrect.
  if ~isempty(findstr(cond_expr,name))
    guard_pthbs=[guard_pthbs i];
  end   
end

% Find all PTHBs which appear in event expression. Also, create the
% list of all hyperplanes associated with event PTHBs.
event_pthbs = [];
event_hps = [];
for i = 1:length(pthbHandle)
  name = get_param(pthbHandle(i),'name');
  % Need to fix the code below since findstr() will return all
  % matching substrings, which may be incorrect.
  if ~isempty(findstr(event_expr,name))
    event_pthbs = [event_pthbs i];
    event_hps = union(event_hps,pthb{i}.hps);
  end
end

% Find overall transition expression, which is the conjunction of
% event and condition expressions.
if ~isempty(cond_expr) & ~isempty(event_expr)
  trans_expr= ['(' event_expr ')&(' cond_expr ')'];
elseif ~isempty(event_expr)
  trans_expr = event_expr;  
elseif ~isempty(cond_expr)
  trans_expr = cond_expr;
else
  error('No transition expression found.')
end

% Initialize the state-space partition with the analysis region as
% a single cell in the partition. The partition will be refined
% iteratively by subtracting each PTHB off each cell in the
% partition in each pass.
[CAR,dAR] = cell_ineq([1:NAR],ones(1,NAR));
partition.poly = linearcon([],[],CAR,dAR);
partition.pthflags = -1*ones(1,length(pthbHandle));

% Refine the state space partition with PTHBs associated with
% condition and event expressions, respectively.
pthbs_used = [guard_pthbs event_pthbs];
partition = partition_ss(partition,pthbs_used,pthb);

% Classify each cell in the partition created above as 'guard' or
% 'guard complement' cells. Add new cells in the partition just
% created to the global cell list CELLS. The result of this function
% will point to regions in this cell list.
for k = 1:length(partition)
  cells_length = length(CELLS);
  
  % Find the boundary hyperplane indices along with their direction
  % and event flags in the global hyperplane list HYPERPLANES.
  [CEk,dEk,CIk,dIk] = linearcon_data(partition(k).poly);
  [boundary,hpflags] = ineq2cell(CIk,dIk);
  pthflags = partition(k).pthflags;
  
  % Test to see if the current cell is a 'repeat' of a region that was
  % already created in the global cell list CELLS.
  repeat_test = is_repeat(boundary,hpflags);
  if repeat_test == 0 
    new = length(CELLS)+1;
    CELLS{new}.boundary = boundary;
    CELLS{new}.hpflags = hpflags;
    CELLS{new}.pthflags = pthflags;
  end
  
  % Test to see if current cell satisfies overall transition
  % expression. If it does, add current cell to guard list. If it does
  % not, add current cell to guard complement list.
  
  % First replace PTHB names in the transition expression with their
  % logical values for the current cell.
  test_expr = trans_expr;
  for pthb_index = pthbs_used
    flag = pthflags(pthb_index);
    name = get_param(pthbHandle(pthb_index),'name');
    % Need to fix the code below since strrep() will also replace
    % matching substrings, which may be incorrect.
    test_expr = strrep(test_expr,name,num2str(flag));
  end
  % Now evaluate transition expression.
  test = eval(test_expr);
  
  if test
    % Compute event flags for the current cell boundary hyperplanes.
    if only_condition_inputs_flag
      event_flags = ones(size(boundary));
    else
      event_flags = zeros(size(boundary));
    end
    [temp,iboundary,ievent_hps] = intersect(boundary,event_hps);
    event_flags(iboundary) = 1;
    guard_cell_event_flags{end+1} = event_flags;
    % Add the current cell index (w.r.t. CELLS) to the list of guard cells.
    if repeat_test == 0
      guard_cells = [guard_cells new];
    else
      guard_cells = [guard_cells repeat_test];
    end
  else
    % Add the current cell index (w.r.t. CELLS) to the list of guard
    % complement cells.
    if repeat_test == 0
      guard_compl_cells = [guard_compl_cells new];
    else
      guard_compl_cells = [guard_compl_cells repeat_test];
    end
  end
  
end

return
% -----------------------------------------------------------------------------

function result = is_terminal_state(q)

result = 1;
for k = 1:length(q)