explore_svm.m

来自「一个matlab的将军模型」· M 代码 · 共 459 行 · 第 1/2 页

GLOBAL_SPEC_TEMP={};
for j=1:length(GLOBAL_SPEC)-spec_count
    GLOBAL_SPEC_TEMP{j}=GLOBAL_SPEC{j};
end
GLOBAL_SPEC=GLOBAL_SPEC_TEMP;


%*********************************************************************
% Recover the path, clear workspace, etc.
%*********************************************************************
cd(svm_current_dir);
if nargout>0
    if ~result
        varargout{1} = -1;
    else
        varargout{1} = double(result);
    end
end
if nargout >1
    diary off;
end


return

% -----------------------------------------------------------------------------
function [result, sysinfo]=validate_vertex(clipboard,sysinfo,spec_tree,ap_build_list, ...
                        timespan,simoptions,scsb_no,special_CTL_flag)
% Recursive function that either selects new vertices or, 
% if the vertices are completely determined, validates the trajectory

 if scsb_no<=length(sysinfo.scsbList)
  blokH = sysinfo.scsbList{scsb_no}.handle;
  %get the vertices of the initial set
  ICS=evalin('base',get_param(blokH,'ICS'));
  V0=vertices(ICS{1});
  
  %get the vertices of the parameter set
  P0=vertices(evalin('base',get_param(blokH,'PaCs')));
  for i=1:length(V0) 
    set_param(blokH,'x0',mat2str(V0(i)));
    % if there is no parameter move to the next blok
    if isempty(P0)
        set_param(blokH,'p0','[]');        
        sysinfo=validate_vertex(clipboard,sysinfo,spec_tree,ap_build_list, ...
                        timespan,simoptions,scsb_no+1,special_CTL_flag);
    else
        for j=1:length(P0)
            set_param(blokH,'p0',mat2str(P0(j)));
            sysinfo=validate_vertex(clipboard,sysinfo,spec_tree,ap_build_list, ...
                        timespan,simoptions,scsb_no+1,special_CTL_flag);
        end;
    end;
    end;
else
    % if for all blocks we determined a vertex validate the trajectory
    
    fprintf('\nSelect parameters\n')
    for k = 1:length(sysinfo.scsbList)
       blokH = sysinfo.scsbList{k}.handle; 
       if ~isempty(eval(get_param(blokH,'p0')))
       fprintf('block %s: \t %s \n',get_param(blokH,'Name'),get_param(blokH,'p0'));
        end;
    end;
    fprintf('\nSelect vertices\n')
    for k = 1:length(sysinfo.scsbList)
       blokH = sysinfo.scsbList{k}.handle; 
       if ~isempty(eval(get_param(blokH,'x0')))
       fprintf('block %s: \t %s \n',get_param(blokH,'Name'),get_param(blokH,'x0'));
       end;
    end;
    fprintf('\n')
    result = validate_trajectory(clipboard,sysinfo,spec_tree,ap_build_list, ...
                        timespan,simoptions,special_CTL_flag);
end;

% -----------------------------------------------------------------------------
function result = validate_trajectory(sys,sysinfo,...
                                      spec_tree,ap_build_list,timespan,simoptions,special_CTL_flag)

global GLOBAL_AP
global GLOBAL_SYSTEM

% 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);

% Simulate the system and put data in the main workspace
sim(sys,timespan,simoptions,[]);

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

% Extract the discrete-trace from  the simulated trajectory, store the chain of
% transitions in GLOBAL_TRANSITION
trace = extract_trace(sysinfo);

% build regions in the transition system GLOBAL_TRANSITION 
% for atomic propositions in the build list
GLOBAL_AP = build_trace_ap(ap_build_list,sysinfo,trace);

% compute region in GLOBAL_TRANSITION corresponding to ACTL specification
spec = evaluate(spec_tree);

% Check if the initial state (state 1) satisfies the specification
result = isinregion(spec,1);
if result
  start_idx = 1 + (length(trace) > 1);
  fprintf(1,'t = %s, x = %s, q = %s, pth = %s\n', ...
          mat2str(trace{start_idx}.t),mat2str(trace{start_idx}.x), ...
          mat2str(trace{start_idx}.q),mat2str(trace{start_idx}.pth))
  fprintf(1,'  ---> ... --> %s',trace{length(trace)}.special)
  if special_CTL_flag
          temp=ap_build_list{2}.build_info{3};
      if ~isempty(findstr('avoid',temp))
          avoid_state_name = temp;
          fprintf(1,'\n\nFor initial condition x = %s: The system never enters the state "%s"\n',mat2str(trace{start_idx}.x),avoid_state_name);
      elseif ~isempty(findstr('reach',temp))
          reach_state_name = temp;
          fprintf(1,'\n\nFor initial condition x = %s: The system enters the state "%s".\n',mat2str(trace{start_idx}.x),reach_state_name);
      end
  end
  
  fprintf(1,' / specification satisfied\n');
else
  if (length(trace) > 1)
    for k = 2:length(trace)
      if k > 2
        fprintf(1,'  --> ');
      end
      fprintf(1,'t = %s, x = %s, q = %s, pth = %s\n', ...
              mat2str(trace{k}.t),mat2str(trace{k}.x), ...
              mat2str(trace{k}.q),mat2str(trace{k}.pth))
    end
    fprintf(1,'  --> %s',trace{length(trace)}.special)
  else
    fprintf(1,'t = %s, x = %s, q = %s, pth = %s\n', ...
            mat2str(trace{1}.t),mat2str(trace{1}.x), ...
            mat2str(trace{1}.q),mat2str(trace{1}.pth))
    fprintf(1,'  warning: init condition outside analysis region')
  end
  
  if special_CTL_flag
          temp=ap_build_list{2}.build_info{3};
      if ~isempty(findstr('avoid',temp))
          avoid_state_name = temp;
          fprintf(1,'\n\nFor initial condition x = %s: The system enters the state "%s"\nor the system leaves the analysis region.\n',mat2str(trace{1}.x),avoid_state_name);
      elseif ~isempty(findstr('reach',temp))
          reach_state_name = temp;
          fprintf(1,'\n\nFor initial condition x = %s: The system does not enter the state "%s"\nor the system leaves the analysis region.\n',mat2str(trace{1}.x),reach_state_name);
      end
  end
  
  fprintf(1,' / *** specification failed ***\n');
end

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

function sys = unique_sys_name(prefix)

count = 0;
sys = prefix;
while ~isempty(find_system('SearchDepth',0,'Name',sys))
  count = count + 1;
  sys = [prefix num2str(count)];
end
return

%------------------------------------------------------------------------------
function [names,fsm_names] = get_fsm_state_names(sys);

fsmbHandle = find_masked_blocks(sys,'Stateflow');
machine_id = get_machine_id(sys);
names={};
fsm_names={};
for k=1:length(fsmbHandle)
    block_name = get_param(fsmbHandle(k),'Name');
    chart_id = find_chart_id(machine_id,block_name);
    states = sf('find','all','state.chart',chart_id);
    names_temp = sf('get',states,'.name');
    for j=1:size(names_temp,1)
        new=length(names)+1;
        names{new}=deblank(names_temp(j,:));
        fsm_names{new}=block_name;
    end
end

return
% ----------------------------------------------------------------------------

function chart_id = find_chart_id(machine_id,block_name)

possible_id = sf('find','all','chart.machine',machine_id, ...
    'chart.name',block_name);
chart_id = [];
for l = 1:length(possible_id)
  name = sf('get',possible_id(l),'.name');
  if strcmp(name,block_name)
    chart_id = possible_id(l);
    break;
  end
end
return

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

function machine_id = get_machine_id(sys)

% the Stateflow function returns all block names whose begining substring
% matches with the name given in sys. thus, we have to make sure that we get
% an exact match.

possible_id = sf('find','all','machine.name',sys);
machine_id = [];
for k = 1:length(possible_id)
  name = sf('get',possible_id(k),'.name');
  if strcmp(name,sys)
    machine_id = possible_id(k);
    break;
  end
end
return