iauto_build.m

一个matlab的将军模型

function iauto_build_dong(continu)

% Build the initial `approximating automaton` given the initial partition
% of the initial continuous set and the invariant faces.
%
% Syntax:
%   "iauto_build(continu)"
%
% Description:
%   Compute the transitions for the states in the initial approximation
%   automaton using `flow pipe approximations` iteratively. The inputs to
%   this function are
%
%   * "continu": a flag indicating whether the CheckMate verification
%     step implemented in this function should be started from scratch or
%     continud from the last break point.
%
% Implementation:
%   The progress of this function is saved in the global variable
%   "GLOBAL_PROGRESS". For this function, "GLOBAL_PROGRESS" has a single
%   field ".step", which is always set to "'iauto_build'" for the CheckMate
%   verification step implemented in this function.
%
%   The transitions in the initial automaton (stored in the global variable
%   "GLOBAL_AUTOMATON") are computed iteratively as follows. In each
%   iteration, the set of reachable states are computed (the computation of
%   the reachable set in the function "reach" is performed on the generic
%   transition system "GLOBAL_TRANSITION" obtained from "GLOBAL_AUTOMATON"
%   using the function "auto2xsys"). The `mapping set` is computed using the
%   function "compute_mapping" for each newly reachable state. The mapping
%   set is then used to define the transitions (the destination states) for
%   each state in the function "find_children". After the transitions for
%   all reachable states are defined, recompute the set of reachable states
%   and repeat the process until no new reachable state is found. Finally,
%   set the "indeterminate" flag for all unreachable states. This iterative
%   process is used so that the mapping set computations, which are
%   extremely expensive, will not wasted on the states that are not
%   reachable.
%
% See Also:
%   iauto_part,compute_mapping,find_children,auto2xsys,region,reach

global_var;

% >>>>>>>>>>>> Eliminating Second Round Reachability -- DJ -- 06/30/03 <<<<<<<<<<<<

% Only perform reachability computation when necessary.
% The changes are in routine assign_children.

% >>>>>>>>>>>> -------------- end (Eliminating Second Round Reachability) --------------- <<<<<<<<<<<<

% >>>>>>>>>>>> Parameter Change -- OS -- 06/13/02 <<<<<<<<<<<<

% use of param-file eliminated

% >>>>>>>>>>>> -------------- end (Parameter Change) --------------- <<<<<<<<<<<<


if continu
  if ~ismember(GLOBAL_PROGRESS.step,{'iauto_build'})
    error(['Inconsistent continu step ''' GLOBAL_PROGRESS.step ...
          ''' (expected ''iauto_build'').'])
  end
else
  temp.step = 'iauto_build';
  GLOBAL_PROGRESS = temp;
end

first = 1;
location_one=1;
computed = 0;
stop = 0;
number_one = 1;
   
for number_of_locations = 1:length(GLOBAL_PIHA.InitialConditions)
	location_value =GLOBAL_PIHA.InitialConditions{number_of_locations}.initialLocation;
	for state_number = 1:length(GLOBAL_AUTOMATON{location_value}.initstate)
        cell=GLOBAL_AUTOMATON{location_value}.initstate{state_number}.cell;
        assign_children(GLOBAL_AUTOMATON{location_value}.initstate{state_number}.polytope,...
        GLOBAL_AUTOMATON{location_value}.initstate{state_number}.mapping,state_number,location_value,cell);
	end%for
end%for


auto2xsys;

return
%------------------------------------------------------------------------------------
function assign_children(X0,previous_mapping,state_num,location_number,cell)

global GLOBAL_PIHA 
global GLOBAL_AUTOMATON
global GLOBAL_APPROX_PARAM

% reachability depth should be independent of fsm discrete state q
max_depth = GLOBAL_APPROX_PARAM.reachability_depth;

% initialize the initial state and put it into the queue
init = [];
init.polytope = X0;
init.location = location_number;
init.cell=cell;
init.state=state_num;
queue = insert_queue([],init);

first = 1;
reachable = [];
transition_theta_flag=0;
while ~isempty(queue)
  % remove a state from the head of the queue and compute the mapping for it
  [queue,state] = remove_queue(queue);
  X0 = state.polytope; 
  loc = state.location; 
  cell=state.cell;
  state_idx=state.state;
  % Perform further reachability analysis if the maximum path depth is
  % not exceeded.
    % if entering this loop for the first time, set the state type to
    % 'init'
    
    if first
      sttype = 'init';
      fprintf(1,'initial state in location %d cell region %d.\n',loc,cell);
      polytope_region = GLOBAL_AUTOMATON{loc}.initstate{state_idx}.polytope;
      mapping_region = GLOBAL_AUTOMATON{loc}.initstate{state_idx}.mapping;
      children_value  = GLOBAL_AUTOMATON{loc}.initstate{state_idx}.children;
% >>>>>>>>>>>> Utilizing Previous Reachability Results (Initial State) -- DJ -- 06/30/03 <<<<<<<<<<<<
      destination = GLOBAL_AUTOMATON{loc}.initstate{state_idx}.destination;
      null_event = GLOBAL_AUTOMATON{loc}.initstate{state_idx}.null_event;   
      time_limit = GLOBAL_AUTOMATON{loc}.initstate{state_idx}.time_limit;   
      out_of_bound = GLOBAL_AUTOMATON{loc}.initstate{state_idx}.out_of_bound;   
      terminal = GLOBAL_AUTOMATON{loc}.initstate{state_idx}.terminal;   
% >>>>>>>>>>>> -------------- end (Utilizing Previous Reachability Results (Initial State)) --------------- <<<<<<<<<<<<
    else
      [dum1,dum2,cell_idx]=intersect(cell,GLOBAL_PIHA.Locations{loc}.interior_cells);
      polytope_region = GLOBAL_AUTOMATON{loc}.interior_region{cell_idx}.state{state_idx}.polytope;
      mapping_region = GLOBAL_AUTOMATON{loc}.interior_region{cell_idx}.state{state_idx}.mapping;
      children_value = GLOBAL_AUTOMATON{loc}.interior_region{cell_idx}.state{state_idx}.children;
% >>>>>>>>>>>> Utilizing Previous Reachability Results (Intermedia States) -- DJ -- 06/30/03 <<<<<<<<<<<<
      destination = GLOBAL_AUTOMATON{loc}.interior_region{cell_idx}.state{state_idx}.destination;
      null_event = GLOBAL_AUTOMATON{loc}.interior_region{cell_idx}.state{state_idx}.null_event;
      time_limit = GLOBAL_AUTOMATON{loc}.interior_region{cell_idx}.state{state_idx}.time_limit;
      out_of_bound = GLOBAL_AUTOMATON{loc}.interior_region{cell_idx}.state{state_idx}.out_of_bound;
      terminal = GLOBAL_AUTOMATON{loc}.interior_region{cell_idx}.state{state_idx}.terminal;
% >>>>>>>>>>>> -------------- end (Utilizing Previous Reachability Results (Intermedia States)) --------------- <<<<<<<<<<<<
      sttype = 'face';
      fprintf(1,'in location %d cell region %d.\n',loc,cell);
    end
    
    if length(mapping_region)==0 && null_event<=0 && time_limit<=0 && out_of_bound<=0 && length(terminal)==0
        [destination,null_event,time_limit,out_of_bounds,terminal] = compute_mapping(X0,sttype,[],loc,cell);
        [dum1,dum2,cell_idx]=intersect(cell,GLOBAL_PIHA.Locations{loc}.interior_cells);
		if (~first)  %if not dealing with initstate
            if null_event
                GLOBAL_AUTOMATON{loc}.interior_region{cell_idx}.state{state_idx}.null_event=1;   
            end
            if time_limit
                GLOBAL_AUTOMATON{loc}.interior_region{cell_idx}.state{state_idx}.time_limit=1;
            end
     	    if out_of_bounds
                GLOBAL_AUTOMATON{loc}.interior_region{cell_idx}.state{state_idx}.out_of_bound=1;   
            end
            if ~isempty(terminal)
                GLOBAL_AUTOMATON{loc}.interior_region{cell_idx}.state{state_idx}.terminal=terminal;
            end
        else
            if null_event
                GLOBAL_AUTOMATON{loc}.initstate{state_idx}.null_event=1;   
            end
            if time_limit
                GLOBAL_AUTOMATON{loc}.initstate{state_idx}.time_limit=1;
            end
     	    if out_of_bounds
                GLOBAL_AUTOMATON{loc}.initstate{state_idx}.out_of_bound=1;   
            end
            if ~isempty(terminal)
                GLOBAL_AUTOMATON{loc}.initstate{state_idx}.terminal=terminal;
            end
        end
    end
     
    %Identify which loc-cell-state the destination mappings landed in:
    %------------------------------------------------------------------------------
    destination_states=[];
    for i=1:length(destination)
       dst_loc      =   destination{i}.location;
       dst_cell     =   destination{i}.cell;
       dst_mapping  =   destination{i}.mapping;
       dst_theta    =   destination{i}.transition_theta;
       if dst_theta
           transition_theta_flag=1;
       end
       [dum1,dum2,cell_indx]=intersect(dst_cell,GLOBAL_PIHA.Locations{dst_loc}.interior_cells);
       %*************************************************************************************************
       %This section adds a new region to the PIHA because a guard region was entered and the transition was
       %not taken.
       if dst_loc==loc&isempty(cell_indx)
           add_region(loc,dst_cell);
           [dum1,dum2,cell_indx]=intersect(dst_cell,GLOBAL_PIHA.Locations{dst_loc}.interior_cells);
       end
       %**************************************************************************************************
       
      % save debug_test dst_loc cell_indx
       for j=1:length(GLOBAL_AUTOMATON{dst_loc}.interior_region{cell_indx}.state)
          inters=dst_mapping&GLOBAL_AUTOMATON{dst_loc}.interior_region{cell_indx}.state{j}.polytope;

          if ~isempty(inters)  % code to be changed by Izaias Silva%
             %Assign this state which the mapping 'hits' to the appropriate children field in
             %GLOBAL_AUTOMATON


             if ~first
                [dum1,dum2,old_cell]=intersect(cell,GLOBAL_PIHA.Locations{loc}.interior_cells);

                if isempty(intersect(GLOBAL_AUTOMATON{loc}.interior_region{old_cell}.state{state_idx}...
                        .children,[dst_loc cell_indx j],'rows'))
             	 GLOBAL_AUTOMATON{loc}.interior_region{old_cell}.state{state_idx}.children=[...
                       GLOBAL_AUTOMATON{loc}.interior_region{old_cell}.state{state_idx}.children ; dst_loc cell_indx j];   
                 already_exist =0;

                    for n=1:length(GLOBAL_AUTOMATON{loc}.interior_region{old_cell}.state{state_idx}.mapping)
                         inter1=and(inters,GLOBAL_AUTOMATON{loc}.interior_region{old_cell}.state{state_idx}.mapping{n});

                         if ~isempty(inter1)

                             if isempty(minus(inters,inter1))
                             already_exist = 1;    
                             end
                         end %if%
                    end %for%

                    if ~already_exist
                         GLOBAL_AUTOMATON{loc}.interior_region{old_cell}.state{state_idx}.mapping...
                        {length(GLOBAL_AUTOMATON{loc}.interior_region{old_cell}.state{state_idx}.mapping)+1}=inters;
                    end %if%
                 
                    GLOBAL_AUTOMATON{dst_loc}.interior_region{cell_indx}.state{j}.non_reachable=0;    
                end   
             else

                 if isempty(intersect(GLOBAL_AUTOMATON{loc}.initstate{state_num}.children,[dst_loc cell_indx j],'rows'))
                    GLOBAL_AUTOMATON{loc}.initstate{state_num}.children=[...
                      GLOBAL_AUTOMATON{loc}.initstate{state_num}.children ; dst_loc cell_indx j];
                    already_exist = 0;

                    for n=1:length(GLOBAL_AUTOMATON{loc}.initstate{state_num}.mapping)
                        inter1=and(inters,GLOBAL_AUTOMATON{loc}.initstate{state_num}.mapping{n});

                        if ~isempty(inter1)

                            if isempty(minus(inters,inter1))
                               already_exist = 1;    
                            end
                        end
                    end
                    if ~already_exist
                         GLOBAL_AUTOMATON{loc}.initstate{state_num}.mapping...
                      {length(GLOBAL_AUTOMATON{loc}.initstate{state_num}.mapping)+1}=inters;
                    end
                    GLOBAL_AUTOMATON{dst_loc}.interior_region{cell_indx}.state{j}.non_reachable=0;
                end
             end
             
             %Also provide information to add this state to the queue
                next=length(destination_states)+1;
                destination_states{next}.polytope=...
                   GLOBAL_AUTOMATON{dst_loc}.interior_region{cell_indx}.state{j}.polytope;
                destination_states{next}.location=dst_loc;
                destination_states{next}.cell=dst_cell;
                destination_states{next}.state=j;
                destination_states{next}.transition_theta = dst_theta;
          end  %if ~isempty(inters)%
       end %for j=1:length(GLOBAL_AUTOMATON{dst_loc}.interior_region{cell_indx}.state)%      
    end %i=1:length(destination)%
    %------------------------------------------------------------------------------
    
    %Add the states found above to the queue
    for k = 1:length(destination_states)
              
         newstate = {};
         newstate.polytope = destination_states{k}.polytope;
      	newstate.location = destination_states{k}.location;
         newstate.cell = destination_states{k}.cell;
         newstate.state = destination_states{k}.state;
         if ~GLOBAL_AUTOMATON{newstate.location}.interior_region{cell_indx}.state{newstate.state}.visited  
            queue = insert_queue(queue,newstate);
         end
         GLOBAL_AUTOMATON{newstate.location}.interior_region{cell_indx}.state{newstate.state}.visited=1;
    end

first = 0;

end

return

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

function queue = insert_queue(queue,tail)

queue = [queue tail];
return

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

function [queue_new,head] = remove_queue(queue)

if ~isempty(queue)
  head = queue(1);
  queue_new = queue(2:length(queue));
else
  head = [];
  queue_new = [];
end
return


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

function [C,d] = return_invariant(loc_idx)

% Get the `invariant` for the given `location`.
%
% Syntax:
%   "INV = location_invariant(loc_idx)"
%
% Description:
%   Return the "linearcon" object representing the `invariant` polytope for
%   the `location` specified by the "loc_idx".
%
% See Also:
%   piha,linearcon

global GLOBAL_PIHA

p = GLOBAL_PIHA.Locations{loc_idx}.p;
boundary = GLOBAL_PIHA.Cells{p}.boundary;
hpflags = GLOBAL_PIHA.Cells{p}.hpflags;

C = []; d = [];
for l = 1:length(boundary)
  if hpflags(l)
    C(l,:) = GLOBAL_PIHA.Hyperplanes{boundary(l)}.c;
    d(l,:) = GLOBAL_PIHA.Hyperplanes{boundary(l)}.d;
  else
    C(l,:) = -GLOBAL_PIHA.Hyperplanes{boundary(l)}.c;
    d(l,:) = -GLOBAL_PIHA.Hyperplanes{boundary(l)}.d;
  end
end

return

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