piha.m~

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

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);
% moved
                    elseif strcmp('FALLING_EDGE_EVENT',input_event{new}.Trigger)
                         input_event{new}.Expression =                   	    ['~(' sf_input_expression(fsmbHandle(k),'event',l) ')'];
% moved
                    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;