piha.m

一个matlab的将军模型

function piha(sys)

% Polyhedral invariant hybrid automaton compiler 
%
% This compiler uses a modified method to create a PIHA from the switched
% continuous system.  Instead of dividing the entire state space region with
% every hyperplane associated with all of the PTHB's, this method creates a
% partition of the analysis region for each discrete location.  The analysis 
% region for each location is then partitioned only with the pthb's that
% are relevant for that location (i.e. only the pthb's which define the guards).
%Also, clock information and reset information are collected and attached to the 
%transition information.  
%
%A location is created for each finite state in the
%Stateflow machine(s).  An interior region is defined for each location.  This interior
%region is a collection of pointers to the structure 'cells' which is a collection
%of convex regions (i.e. so the interior regions are made up of a collection of smaller
%convex regions).  
%
%Each location also contains information about each of its 'exiting'
%transitions.  Information about transitions are contained within each 'transition'.
%This information includes:
%
%-'id'	     					the number of the transition (assigned by Stateflow)
%-'expression'					the expression attached to the transition
%-'clock'							the clock number (if there is one)
%-'source'						the source state (identified by the value of 'q')
%-'destination'					the source state (identified by the value of 'q')
%-'destination_name'			the label given to the destination
%-'reset_flag'					set if there is a reset associated with this transition
%-'guard'							pointers to elements in 'cells' that define the guard regions
%-'guard_cell_event_flags'	a matrix where the i'th row is a vector of flags identifying
%									which boundary hyperplane of the i'th guard cell is an event
%									hyperplane
%-'guard_compl'					cells which define the complement of the cells in 'guard'
%
%
%
% Syntax:
%   "HA = piha(sys)"
%
% Description:
%   "piha(sys)" returns a PIHA object.  The returned PIHA object is
%   equivalent to the Simulink CheckMate model "sys" within the analysis
%   region.
%

% "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.

%
% Last change: 11/18/2002 JPK


global GLOBAL_PIHA SSTREE CELLS LOCATIONS

CELLS={};

if ~isstr(sys)
  error(['Input argument must be a string.'])
  return
end

if strcmp(sys,'help')
  fid = fopen('@piha/piha_structure.txt');
  while 1
    line = fgetl(fid);
    if ~isstr(line), break, end
    fprintf(1,'%s\n',line)
  end
  fclose(fid);
  return
end

% Check the model syntax before performing conversion
if ~check_model_syntax(sys)
  fprintf(1,'\007Syntax error, model conversion aborted.\n')
  return
end

% Find Simulink handles for switched continuous system blocks (SCSB),
% finite state machine blocks (FSMB), and polyhedral threshold blocks
% (PTHB) in the CheckMate model.
scsbHandle = find_masked_blocks(sys,'SwitchedContinuousSystem');
fsmbHandle = find_masked_blocks(sys,'Stateflow');
pthbHandle = find_masked_blocks(sys,'PolyhedralThreshold');
clockHandle = find_masked_blocks(sys,'VariableZeroOrderHold');

clockList=[];
%Create a list of all clocks and their associated parameters
for c=1:length(clockHandle)
   clockList{c}.name  = get_param(clockHandle(c),'name');
   clockList{c}.period =evalin('base',get_param(clockHandle(c),'period'));
   clockList{c}.jitter =evalin('base',get_param(clockHandle(c),'jitter'));
   clockList{c}.phase =evalin('base',get_param(clockHandle(c),'theta'));
end

% **********************************
% (1) Construct list of hyperplanes.
% **********************************

% Get threshold hyperplanes from the PTHBs in the simulink model.
disp('Compiling threshold hyperplanes.')
NBDHP = {};
for k = 1:length(pthbHandle)
    [Ck,dk] = augment_poly_constraints(scsbHandle,pthbHandle(k));
    pthb{k}.c=Ck;
    pthb{k}.d=dk;
    pthb{k}.hps=[];
    for l = 1:length(dk)  
        new = length(NBDHP)+1;
        NBDHP{new}.pthb = k;
        NBDHP{new}.index = l;
        NBDHP{new}.c = Ck(l,:);
        NBDHP{new}.d = dk(l,:);
    end%for
end%for

%Create hyperplane list
AR = get_analysis_region(scsbHandle);
[pthb,NAR]=create_hyperplanes(NBDHP,AR,pthb);


% **************************************************************************
% (3) Build data base for Stateflow blocks that will be used for conversion.
% **************************************************************************

machine_id = get_machine_id(sys);
if isempty(machine_id)
  fprintf(1,['\007Error: Cannot find machine id for ''' sys '''!!!\n'])
  return
end

sfdata = {};

for k = 1:length(fsmbHandle)

    block_name = get_param(fsmbHandle(k),'Name');
    chart_id = find_chart_id(machine_id,block_name);
  
    if isempty(chart_id)
        fprintf(1,['\007Error: Cannot find chart id for "' block_name '"!!!\n'])
        return
    else
    
        data_id = sf('find',sf('DataOf',chart_id),'.scope','INPUT_DATA');
        input_data = {};
        clock=[];
        in_num=0;

        for l = 1:length(data_id)
      
            [expression,clock_handle]=sf_input_expression(fsmbHandle(k),'data',l);
            if ~isempty(clock_handle)
                error(['Clocks must be event inputs.'])
            else
                in_num=in_num+1;
                input_data{in_num}.Name = sf('get',data_id(l),'.name');
                if input_data{in_num}.Name(1)==' '|input_data{in_num}.Name(length(input_data{in_num}.Name))==' '
                            error('The names of Stateflow input data variables cannot have leading or trailing spaces.')
                end
                        
                input_data{in_num}.Expression = expression;
      	    end%if
        
        end%for
    
        event_id = sf('find',sf('EventsOf',chart_id),'.scope','INPUT_EVENT');
        input_event = {}; 

        for l = 1:length(event_id)

            event_name = sf('get',event_id(l),'.name');
            if event_name(1)==' '|event_name(length(event_name))==' '
                            error('The names of Stateflow input events cannot have leading or trailing spaces.')
            end
            if ~strcmp(event_name,'start')

                [expression,clock_handle]=sf_input_expression(fsmbHandle(k),'event',l);

                if ~isempty(clock_handle)
                    clock_num=length(clock)+1;
                    clock{clock_num}.Name=sf('get',event_id(l),'.name');
                    clock{clock_num}.ClockBlock=get_param(clock_handle,'name');
                    clock{clock_num}.ClockHandle=clock_handle;
                else

       
               	    % ignore the start event, which is used only for simulation purpose
        	        new = length(input_event)+1;
        	        input_event{new}.Name = event_name;
    
                    if ~isempty(sf('find',event_id(l),'.trigger','RISING_EDGE_EVENT'))
                	    input_event{new}.Trigger = 'RISING_EDGE_EVENT';   
        	         end

                    if ~isempty(sf('find',event_id(l),'.trigger','FALLING_EDGE_EVENT'))
    	                input_event{new}.Trigger = 'FALLING_EDGE_EVENT';   
    	            end

                    if ~isempty(sf('find',event_id(l),'.trigger','EITHER_EDGE_EVENT'))
                	    input_event{new}.Trigger = 'EITHER_EDGE_EVENT';   
                    end
  
                     if strcmp('RISING_EDGE_EVENT',input_event{new}.Trigger)
                        input_event{new}.Expression = ...
                     	 sf_input_expression(fsmbHandle(k),'event',l);
                    elseif strcmp('FALLING_EDGE_EVENT',input_event{new}.Trigger)
                         input_event{new}.Expression = ...
                 	    ['~(' sf_input_expression(fsmbHandle(k),'event',l) ')'];
                    else
                        error('This version only supports  rising and falling event edges!')
                    end%if
               
                end%if
            end%if
        end%for
    
        sfdata{k}.BlockName = block_name;
        sfdata{k}.SimulinkHandle = fsmbHandle(k);
        sfdata{k}.StateflowChartID = chart_id;
        sfdata{k}.InputData = input_data;
        sfdata{k}.InputEvent = input_event;
        sfdata{k}.Clock = clock;
           
    end%if
    
end%for

% **************************************************************
% (4) Find initial discrete states for all the Stateflow blocks.
% **************************************************************

% Get initial state id for each Stateflow block, assuming that there is 
% only one default transition per machine.
q0 = []; 
for k = 1:length(sfdata)
  chart_id = sfdata{k}.StateflowChartID;
  DTid = sf('DefaultTransitionsOf',chart_id);
  q0id = sf('get',DTid,'.dst.id');
  q0(k) = q0id;
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;