explore_svm.m

一个matlab的将军模型

function varargout = explore_svm(model_file, setup_file, varargin)

% Explore Tests one or more trajectories from the CheckMate model
%
% Syntax:
%   "explore_svm"
%
%   "explore -vertices"
%
%   "explore -points <matrix-of-points>"
%
% Description:
%   "validate" is used to verify a single trajectory of a CheckMate
%   model.  The trajectory originates from the point specified in the
%   `initial condition` property of the switched continuous system blocks
%   (SCSBs) in the model.  
%
%   If the "-vertices" switch is used, several
%   trajectories are verified each one begining from one of the vertices
%   of the composite `initial continuous set (ICS)` specified in the
%   CheckMate model.
%
%   If the option "-points" switch is used, the 
%   trajectories starting in the points given in <matrix-of-points> (the points are the columns of the matrix) are  tested.
%
% Implementation:
%   The validation routine is carried out using numerical simulation of
%   the CheckMate model.  The initial point(s) are simulated according to
%   the Simulink simulation properties.  The simulation data is captured
%   in the workspace using a `clock` block and several `to workspace`
%   blocks from Simulink.  A discrete trace is then extracted from the
%   simulation data, and used to verify the ACTL specifiation given in
%   the variable "GLOBAL_SPEC".  Finally, the result of the verification
%   is returned to the user, and the routine terminates.
%
% See Also:
%   verify


% Declare global variables (see the file global_var.m for details)

global_var;
%*****************************************************************
% Zhi's update, use filename as input
%*****************************************************************

svm_current_dir = pwd;
[working_dir,model_file] = fileparts(model_file);
[working_dir,setup_file] = fileparts(setup_file);
cd(working_dir);
evalin('base',setup_file);
eval(model_file);
result = 1;
if nargout >1
    diary([working_dir '\diary_explore.log']);
    varargout{2} = [working_dir '\diary_explore.log'];
end
%*******************************************************************
%  End of Zhi's update
%*******************************************************************

GLOBAL_APPROX_PARAM=parameters(1);


if ~ischar(GLOBAL_SYSTEM) | isempty(GLOBAL_SYSTEM)
  error('The variable GLOBAL_SYSTEM has not been set up properly.')
end

% Default flags
vertices_flag = 0;
%Points flag test added by Jim Kapinski 2/2002
points_flag = 0;


k = 1;
while (k <= length(varargin))
  switch varargin{k}
    case '-vertices'
      vertices_flag = 1;
    case '-points'
      points_flag = 1;
      points=evalin('base',varargin{k+1});
      break
    otherwise
      error(['Unknown option ''' varargin{k} '''.'])
  end
  k = k + 1;
end

%If 'explore_temp' is not a directory, then create it.
if ~isdir('explore_temp')
    mkdir('explore_temp');
end

clipboard = unique_sys_name('CheckMate_clipboard');
%clipboard = 'CheckMate_clipboard';
if ~isempty(find_system('SearchDepth',0,'Name',clipboard))
  close_system(clipboard,0)
end

%copy_model(GLOBAL_SYSTEM,clipboard);
if strcmp(get_param(GLOBAL_SYSTEM,'Dirty'),'on')
  fprintf(1,'Please save the system ''%s'' before running explore.\n', ...
          GLOBAL_SYSTEM)
  return
end
save_system(GLOBAL_SYSTEM,['explore_temp\' clipboard]);
open_system(GLOBAL_SYSTEM)

% copy simulation parameters to the clipboard system
timespan = [eval(get_param(GLOBAL_SYSTEM,'StartTime')) ...
             eval(get_param(GLOBAL_SYSTEM,'StopTime'))];
simoptions = simget(GLOBAL_SYSTEM);
sysinfo = compile_sys_info(clipboard);

% Save current path and directory
current_path = path;
current_dir = pwd;
addpath(current_dir)

% Change to the explore_temp directory, the Stateflow compilation of the
% clipboard model will be saved here.
temp = what('explore_temp');
cd(temp.path);

% dummy simulation call to update the Stateflow block if necessary

sim(clipboard,[0 0],simoptions,[]);

% Restore path and directory
cd(current_dir)
path(current_path)

%Call function that lists states in the FSMBlocks
[state_names,fsm_names] = get_fsm_state_names(GLOBAL_SYSTEM);

spec_count=0;
for i=1:length(state_names)
    if findstr('avoid',state_names{i})
        new=length(GLOBAL_SPEC)+1;
        GLOBAL_SPEC{new}=['(AG ~out_of_bound)&(AG ~' fsm_names{i} ' == ' state_names{i} ')'];
        spec_count=spec_count+1;
    elseif findstr('reach',state_names{i})
        new=length(GLOBAL_SPEC)+1;
        GLOBAL_SPEC{new}=['(AG ~out_of_bound)&(AF ' fsm_names{i} ' == ' state_names{i} ')'];
        spec_count=spec_count+1;
    end
    
end

GLOBAL_SPEC_TOTAL=GLOBAL_SPEC;
% ------ parse the specification ------
% (i) match parentheses
for count_GS=1:length(GLOBAL_SPEC_TOTAL)
    
    %Is this an automatically generated CTL expression?
    if count_GS>length(GLOBAL_SPEC_TOTAL)-spec_count
        special_CTL_flag=1;
    else
        special_CTL_flag=0;
    end
    
    fprintf(1,'\nComputing specification %d of %d in the list ',count_GS,length(GLOBAL_SPEC_TOTAL));
    GLOBAL_SPEC_ELEMENT=GLOBAL_SPEC_TOTAL{count_GS};
    match_paren(GLOBAL_SPEC_ELEMENT,0);
% (ii) identify terminal symbols in the ACTL specification string and
%      parse the symbols to obtain parse tree for the specification
spec_tree = parse(identerm(GLOBAL_SPEC_ELEMENT));
% (iii) compile the list of all atomic propositions in the parse tree and 
%       replace all the atomic proposition subtree by a single leaf
[spec_tree,ap_build_list] = compile_ap(spec_tree);

fprintf(1,'\nblock orders: ')
fprintf(1,'x = [');
for l = 1:length(sysinfo.scsbList)
  fprintf(1,'%s',sysinfo.scsbList{l}.name)
  if (l < length(sysinfo.scsbList))
    fprintf(1,' ')
  end
end
fprintf(1,'], ')
fprintf(1,'q = [');
for l = 1:length(sysinfo.fsmbList)
  fprintf(1,'%s',sysinfo.fsmbList{l}.name)
  if (l < length(sysinfo.fsmbList))
    fprintf(1,' ')
  end
end
fprintf(1,'], ')
fprintf(1,'pth = [');
for l = 1:length(sysinfo.pthbList)
  fprintf(1,'%s',sysinfo.pthbList{l}.name)
  if (l < length(sysinfo.pthbList))
    fprintf(1,' ')
  end
end
fprintf(1,']\n')

if vertices_flag
  %Compute the vertices of all polytopes in the initial continuous set 
  %and the parameter sets
 
  result = result & validate_vertex(clipboard,sysinfo,spec_tree,ap_build_list, ...
                        timespan,simoptions,1,special_CTL_flag);

    elseif points_flag==1
        %User defined set of simulation points added by Jim K 2/2002
        for i=1:size(points,2)
            fprintf(1,'Running simulation with initial condition %d',i)
            init_cond = points(:,i);
            start_idx = 0;
            for j = 1:length(sysinfo.scsbList)
                blkH = sysinfo.scsbList{j}.handle;
                nx = eval(get_param(blkH,'nx'));
                x0 = init_cond([1:nx]+start_idx);
                set_param(blkH,'x0',mat2str(x0));
                start_idx = start_idx+nx;
            end
            validate_trajectory(clipboard,sysinfo,spec_tree,ap_build_list, ...
                          timespan,simoptions,special_CTL_flag);   
        end
else
  fprintf(1,'init: ')
  result =  result & validate_trajectory(clipboard,sysinfo,spec_tree,ap_build_list, ...
                      timespan,simoptions,special_CTL_flag);
 end
end
close_system(clipboard,0);
close_system(GLOBAL_SYSTEM);