piha.m

一个matlab的将军模型

	end
end





return

% ----------------------------------------------------------------------------
function [initial_conditions,locations_updated] = find_initial_conditions(X0,locations_list)

%This function finds the list of continuous set, the discrete set, the initial cells
% and the initial location for the initial conditions set X0.
% INPUT
% X0 : a Linearcon object with the state-space region defined as the initial condition
% locations_list : set of locations. We will assume that the default initial location is one (01)
% scsbList : List of SCSB with parameters. For reset purposes.
%
% OUTPUT
% initial_conditions: Cell array with the following fields:
%
%   .continuousSet    = linearcon object with the region for the initial region
%   .initialCells          = cell where the initial conditon is located
%   .discreteCells      = configuration of the SFM when in this element (value of vector q)
%   .initialLocation    = Location where the initial condition is located
%
% locations: list of locations updated for some guard;
% In the future, this routine will receive a structure containing the state (q) and X0.

global CELLS

ICL{1}.location = 01;
ICL{1}.X0        = X0;

for counter_list = 1:length(ICL)

    init_loc = ICL{counter_list}.location;
    X0       = ICL{counter_list}.X0;
    initial_invariant=locations_list{init_loc}.interior_cells;
    init_cond ={};
    init_counter = 1;

    for j=1:length(X0)

        for i=1:length(initial_invariant)

            [C,d] = cell_ineq(CELLS{initial_invariant(i)}.boundary,CELLS{initial_invariant(i)}.hpflags);
    	    INV = linearcon([],[],C,d);

            if isfeasible(X0{j},INV)

                init_counter = length(init_cond);
                init_cond{init_counter+1}.continuousSet      = and(X0{j},INV);
                init_cond{init_counter+1}.initialCells            = initial_invariant(i);
                init_cond{init_counter+1}.discreteSet           = locations_list{01}.q;
                init_cond{init_counter+1}.initialLocation      = 01; 
                
           end%if
           
       end%if
       
    end%if

    %Test to see if any of the initial continuous set either a.) satifies a guard or b.) is outside of the 
    %analysis region.
    disc_state = locations_list{init_loc}.q;
    transitions=locations_list{init_loc}.transitions;

    for i=1:length(transitions)
   
        guards=transitions{i}.guard;

        for j=1:length(guards)
    	    [C,d] = cell_ineq(CELLS{guards(j)}.boundary,CELLS{guards(j)}.hpflags);
    	    GUARD = linearcon([],[],C,d);

            for m=1:length(X0)

                if isfeasible(X0{m},GUARD)

                    if isempty(transitions{i}.clock)

                        warning(['Some section of the initial continuous set satisfies the guard of the initial location.'...
                      	'  This section will be neglected.']);
                
                    else

                        init_counter = length(init_cond);
                        init_cond{init_counter+1}.continuousSet      = and(X0{m},GUARD);
                        init_cond{init_counter+1}.initialCells            = guards(j);
                        init_cond{init_counter+1}.discreteSet           = disc_state;
                        init_cond{init_counter+1}.initialLocation       = 01;
                        [dum1,dum2,cell_idx]=intersect(guards(j),locations_list{init_loc}.interior_cells);
                        if isempty(cell_idx)
                            locations_list{init_loc}.interior_cells(length(locations_list{init_loc}.interior_cells)+1)= guards(j);
                            
                        end%if
                        
                    end %if
            
                end %if
        
            end %for
    
        end%for
    
    end%for

end%for

initial_conditions      = init_cond;
locations_updated    = locations_list;

return

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

function test=is_repeat(boundary,hpflags)

%This function tests if CELLS already contains a region described by the HP's
%in the vector 'boundary'

global CELLS

test=0;
size=length(CELLS);
for i=1:size
   %if isequal(wcommon(CELLS{i}.boundary,boundary),ones(1,length(boundary)))&...
   if length(intersect(boundary,CELLS{i}.boundary))==length(boundary)&...
         length(boundary)==length(CELLS{i}.boundary)
      
     %If all boundary HP's are equal, cell must be tested to see if all HP sides are
     %also equal.  (Added by JPK 6/2002)
     not_eq=0; 
     for j=1:length(boundary)
           [dum1,dum2,member_num]=intersect(boundary(j),CELLS{i}.boundary);
           if hpflags(j)~=CELLS{i}.hpflags(member_num)
                not_eq=1;
                break;
           end
      end
      if ~not_eq
        test=i;
        break;
      end
   end
end

return

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

function invariant=intersect_complements(locations,loc)

%This function takes all of the complements of all if the guards for the location 'loc'
%and intersects them.  The resulting regions are the 'invariant'.

global CELLS 

previous_invariant=locations{loc}.transitions{1}.guard_compl;

if length(locations{loc}.transitions)>1
%Intersect the first set of complements with the 2nd.  Then intersect that result
%with the 3rd, and so on...
for j=2:length(locations{loc}.transitions)
   
   new_guard_compl=locations{loc}.transitions{j}.guard_compl;
   invariant=[];
   
   for k=1:length(new_guard_compl)
      
      new_cell=new_guard_compl(k);
      new_hps=CELLS{new_cell}.boundary;
      new_hpflags=CELLS{new_cell}.hpflags;
      new_pthflags=CELLS{new_cell}.pthflags;
      for i=1:length(previous_invariant)
         
         existing_guard_compl=previous_invariant(i);
         old_hps=CELLS{existing_guard_compl}.boundary;
         old_hpflags=CELLS{existing_guard_compl}.hpflags;
         old_pthflags=CELLS{existing_guard_compl}.pthflags;
         [intersection_boundary,intersection_hpflags]=clean_up_boundary(old_hps,new_hps,old_hpflags,new_hpflags);
         if ~isempty(intersection_boundary)
            repeat_test=is_repeat(intersection_boundary,intersection_hpflags);
            if repeat_test~=0
               %************************************************
               %Since this CELL already exists, just point to the existing CELL
               invariant=[invariant repeat_test];
               %Now update existing pthb flag list
               for p=1:length(old_pthflags)
                    if old_pthflags(p)~=-1
                       pthflags(p)=old_pthflags(p);
                    elseif new_pthflags(p)~=-1
                       pthflags(p)=new_pthflags(p);
                    elseif CELLS{repeat_test}.pthflags(p)~=-1
                       pthflags(p)=CELLS{repeat_test}.pthflags(p);
                    else
                       pthflags(p)=-1;
                    end
                 end
					%***********************************************
               
            else
               new_cell=length(CELLS)+1;
               
  					%************************************
  					CELLS{new_cell}.boundary = intersection_boundary;
  					CELLS{new_cell}.hpflags = intersection_hpflags;
                 for p=1:length(old_pthflags)
                    if old_pthflags(p)~=-1
                       pthflags(p)=old_pthflags(p);
                    elseif new_pthflags(p)~=-1
                       pthflags(p)=new_pthflags(p);
                    else
                       pthflags(p)=-1;
                    end
                 end
               CELLS{new_cell}.pthflags = pthflags;
               %*************
               invariant=[invariant new_cell];
            end   
         end
      end
      end
      previous_invariant=invariant;
   
end

else
   invariant=previous_invariant;
end

if isempty(invariant)
   name=locations{loc}.state;
   fprintf(1,'\nWARNING: Location "')
   for i=1:size(name,1)
      fprintf(1,'%s ',name(i,:))
   end
   fprintf(1,'" has no guard invariant.\n')
end

return

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

function [boundary_new,hpflags_new] = clean_up_boundary(first_boundary,second_boundary,first_hpflags,second_hpflags)

global GLOBAL_PIHA
global GLOBAL_APPROX_PARAM

hyperplanes = GLOBAL_PIHA.Hyperplanes;

[c1,d1]=cell_ineq(first_boundary,first_hpflags);
[c2,d2]=cell_ineq(second_boundary,second_hpflags);

a=linearcon([],[],c1,d1);
b=linearcon([],[],c2,d2);

if isempty(a&b)
   boundary_new=[];
   hpflags_new=[];
else
boundary=[first_boundary second_boundary];
hpflags=[first_hpflags second_hpflags];

[CBND,dBND] = cell_ineq(boundary,hpflags);
[CE,dE,CI,dI] = linearcon_data(clean_up(linearcon([],[],CBND,dBND)));

%Use the following to indicate which hpflags elements will still be valid
hp_flag_index=[];

if (length(dI) == length(dBND))
  boundary_new = boundary;
else
  hyperplane_tol = GLOBAL_APPROX_PARAM.poly_hyperplane_tol;
  boundary_new = [];
  for k = 1:length(boundary)
    ck = hyperplanes{boundary(k)}.c;
    dk = hyperplanes{boundary(k)}.d;
    found = 0;
    for l = 1:length(dI)
      if rank([CI(l,:) dI(l); ck dk],hyperplane_tol) == 1
        found = 1;
        break;
      end
    end
    if found&~ismember(boundary(k),boundary_new)
      boundary_new = [boundary_new boundary(k)];
      hp_flag_index=[hp_flag_index k];
   end
end

%Create new hpflags vector
for j=1:length(hp_flag_index)
   hpflags_new(j)=hpflags(hp_flag_index(j));
end


end

end

return
%-------------------------------------------------------------------------------------------------------------------------------
%  function clean_transition()
%
% This function eliminates duplicate transitions. It compares the guards of two transitions. 
%If the lists of guards are equal, merge the transitions.
%
function clean_loc=clean_transition(location)
 counter=1;
    for i=1:length(location.transitions)
       if location.transitions{i}.id>0 
         cur_guard=location.transitions{i}.guard;
            for j=i+1:length(location.transitions)
                 if ~isempty(cur_guard)&~isempty(location.transitions{j}.guard)
                         %(isempty(cur_guard)&isempty(location.transitions{j}.guard))
                     if length(cur_guard)==length(location.transitions{j}.guard)
                        if (all(cur_guard==location.transitions{j}.guard))

                        location.transitions{i}.source=[location.transitions{i}.source location.transitions{j}.source];
                        location.transitions{i}.destination=[location.transitions{i}.destination location.transitions{j}.destination];
                        location.transitions{i}.idx=[location.transitions{i}.idx location.transitions{j}.idx];

                        % If either of the transitions resets, we should reset on the composite transion, too. Ansgar
                        location.transitions{i}.reset_flag=max(location.transitions{i}.reset_flag, location.transitions{j}.reset_flag);
                        location.transitions{i}.reset_scs_index=setdiff(...
                            [location.transitions{i}.reset_flag*location.transitions{i}.reset_scs_index, location.transitions{j}.reset_flag*location.transitions{j}.reset_scs_index],0);
                        
                        location.transitions{j}.id=-1;
                        end   %if
                    end %if
                end %if
            end   %for j
     clean_loc.transitions{counter}=location.transitions{i};
     counter=counter+1;
     end   %if location
        
        
    end   %for i
    
    return