verify_svm.m

一个matlab的将军模型

      GLOBAL_TIME_ELAPSED.piha_conversion = cputime - init_time;
      fprintf(1,'PIHA conversion completed in %6.2f seconds.\n',GLOBAL_TIME_ELAPSED.piha_conversion)
      % >>>>>>>>>>>> Parameter Change -- OS -- 06/13/02 <<<<<<<<<<<<
      % Update of the field 'W' of GLOBAL_APPROX_PARAM (requires GLOBAL_PIHA)
      if isempty(GLOBAL_APPROX_PARAM.W)
         states=0;
         for k=1:length(GLOBAL_PIHA.SCSBlocks);
            states=states+GLOBAL_PIHA.SCSBlocks{k}.nx;    
         end
         GLOBAL_APPROX_PARAM.W=eye(states);
      end
      % >>>>>>>>>>>> -------------- end --------------- <<<<<<<<<<<<
      if close_flag
        close_system(GLOBAL_SYSTEM)
      end
      next_step = 'iauto_part';
    case 'iauto_part',
      fprintf(1,'\n')
      init_time = cputime;
      iauto_part;
      GLOBAL_TIME_ELAPSED.iauto_part= cputime - init_time;
      fprintf(1,'reachability analysis and initial partition completed in %6.2f seconds.\n',GLOBAL_TIME_ELAPSED.iauto_part)
      next_step = 'iauto_build';
    case 'iauto_build',
       if try_before_iauto_build
          auto2xsys;
          next_step = 'parse_spec';
       else
      	fprintf(1,'\n')
      	continu = isfield(GLOBAL_PROGRESS,'idx');
      	init_time = cputime;
        iauto_build(continu);
        GLOBAL_TIME_ELAPSED.iauto_build(length(GLOBAL_TIME_ELAPSED.iauto_build)+1)= cputime - init_time;
        fprintf(1,'construction of transition system completed in %6.2f seconds.\n',...
            GLOBAL_TIME_ELAPSED.iauto_build(length(GLOBAL_TIME_ELAPSED.iauto_build)))
      	if discard_flag
				remove_unreachables;
      	end
         next_step = 'parse_spec';
       end
    case 'parse_spec',
          %Test Stateflow state names.  If any are named 'avoid' or 'reach' create
          %a new specification automatically.  The specification should be AG~avoid
          %and/or AFreach.  Added by Jim K 2/10/2002.
          GLOBAL_SPEC_TREE=cell(0);
          GLOBAL_AP_BUILD_LIST=cell(0);
          spec_count=0;
          for m=1:length(GLOBAL_PIHA.FSMBlocks)
              for n=1:length(GLOBAL_PIHA.FSMBlocks{m}.states)
                    state_name=GLOBAL_PIHA.FSMBlocks{m}.states{n};
                  if findstr('avoid',state_name)
                    new=length(GLOBAL_SPEC)+1;
                    fsmname = GLOBAL_PIHA.FSMBlocks{m}.name;
                    GLOBAL_SPEC{new}=['(AG ~out_of_bound)&(AG ~' fsmname ' == ' state_name ')'];
                    spec_count=spec_count+1;
                  elseif findstr('reach',state_name)
                    new=length(GLOBAL_SPEC)+1;
                    fsmname = GLOBAL_PIHA.FSMBlocks{m}.name;
                    GLOBAL_SPEC{new}=['(AG ~out_of_bound)&(AF ' fsmname ' == ' state_name ')'];
                    spec_count=spec_count+1;
                  end
              end
          end
          GLOBAL_SPEC{length(GLOBAL_SPEC)+1}=spec_count;
          
          for i=1:length(GLOBAL_SPEC)-1
            GLOBAL_SPEC_ELEMENT{i} = GLOBAL_SPEC{i}; 
            fprintf(1,'\nParsing specification %d: %s\n',i,GLOBAL_SPEC_ELEMENT{i});
            % match parentheses
            match_paren(GLOBAL_SPEC_ELEMENT{i},0);
            % identify terminal symbols in the ACTL specification string and
            % parse the symbols to obtain parse tree for the specification
            GLOBAL_SPEC_TREE{i} = parse(identerm(GLOBAL_SPEC_ELEMENT{i}));
            % compile the list of all atomic propositions in the parse tree and 
            % replace all the atomic proposition subtree by a single leaf
            fprintf(1,'Compiling list of atomic propositions.\n',GLOBAL_SPEC_ELEMENT{i});
            [GLOBAL_SPEC_TREE{i},GLOBAL_AP_BUILD_LIST{i}] = ...
                compile_ap(GLOBAL_SPEC_TREE{i});
            for k = 1:length(GLOBAL_AP_BUILD_LIST{i})
                fprintf(1,' * %s\n',GLOBAL_AP_BUILD_LIST{i}{k}.name)
            end
            
        end
          next_step = 'refinement_decision';
  
    case 'refinement_decision',
      fprintf(1,'\nMaking refinement decision.\n')
      % build regions in the transition system GLOBAL_TRANSITION 
      % for atomic propositions in the build list
      GLOBAL_TBR=region;
      for i=1:length(GLOBAL_SPEC)-1
          GLOBAL_AP = build_ap(GLOBAL_AP_BUILD_LIST{i});
          % compute region in GLOBAL_TRANSITION corresponding to 
          % ACTL specification
          spec = evaluate(GLOBAL_SPEC_TREE{i});
          % compute initial state region
          init = init_states;
          if isempty(init & ~spec)
              %Give explicit output for the cases where the user did not specify an ACTL
              %expression (i.e. the case where a state was named 'avoid'/'reach').  Added
              %by Jim K 2/10/2002.
              if i>(length(GLOBAL_SPEC)-GLOBAL_SPEC{length(GLOBAL_SPEC)}-1)
                if ~isempty(findstr('avoid',GLOBAL_SPEC{i}))
                    temp=GLOBAL_AP_BUILD_LIST{i}{2}.build_info{3};
                    avoid_state_name = temp;
                    fprintf(1,'\nSystem never enters the state "%s"\n\n',avoid_state_name);
                    success_svm =1 & success_svm;  %-- Zhi's update for SVM
                elseif ~isempty(findstr('reach',GLOBAL_SPEC{i}))
                    temp=GLOBAL_AP_BUILD_LIST{i}{2}.build_info{3};
                    reach_state_name = temp;
                    fprintf(1,'\nSystem enters the state "%s" in all cases.\n\n',reach_state_name);
                    success_svm =1 & success_svm;  %-- Zhi's update for SVM
                end
            else
              fprintf(1,['\nSystem already satisfies specification %d. No refinement' ...
                      ' necessary.\n\n'],i);
              success_svm =1 & success_svm;  %-- Zhi's update for SVM
            end
              refine(i)=0;
          else
              if i>(length(GLOBAL_SPEC)-GLOBAL_SPEC{length(GLOBAL_SPEC)}-1)
                if ~isempty(findstr('avoid',GLOBAL_SPEC{i}))
                    temp=GLOBAL_AP_BUILD_LIST{i}{2}.build_info{3};
                    avoid_state_name = temp;
                    fprintf(1,'\nSystem does not satisfy the specification of nevering entering the state "%s"\n',avoid_state_name);
                    fprintf(1,'The transition system may be too conservative.\n');
                    fprintf(1,'Computing the set of states in the transition system that will be refined in order\n');
                    fprintf(1,'to perform another verification attempt.\n\n');
                    success_svm =0;  %-- Zhi's update for SVM
                elseif ~isempty(findstr('reach',GLOBAL_SPEC{i}))
                    temp=GLOBAL_AP_BUILD_LIST{i}{2}.build_info{3};
                    reach_state_name = temp;
                    fprintf(1,'\nSystem does not satisfy the specification of always entering the state "%s"\n',reach_state_name);
                    fprintf(1,'The transition system may be too conservative.\n');
                    fprintf(1,'Computing the set of states in the transition system that will be refined in order\n');
                    fprintf(1,'to perform another verification attempt.\n\n');
                    success_svm =0;  %-- Zhi's update for SVM
                end
              else
                fprintf(1,['\nSystem does not satisfy specification %d.\n' ... 
                      'Computing the "to-be-refined" (TBR) set.\n\n'],i)
              end
              % compute the set of states that violate the bisimulation
              % condition, i.e. states that have more than one child.
              not_bisim = region(length(GLOBAL_TRANSITION),'false');
              for k = 1:length(GLOBAL_TRANSITION)
                  if (length(GLOBAL_TRANSITION{k}) > 1)
                      not_bisim = set_state(not_bisim,k,1);
                  end
              end
              GLOBAL_TBR = (reach(init & ~spec) & not_bisim)|GLOBAL_TBR;
              if isempty(GLOBAL_TBR)
                  fprintf(1,['No meaningful refinement to be done and ' ... 
                          'system does not satisfy specification.\n\n'])
                  refine(i)=0;
              success_svm =0;  %-- Zhi's update for SVM
              else
                  refine(i)=1;
              end
          end  
      end
      
        if ~all(refine)
            next_step='done';
        elseif try_before_iauto_build
            next_step='iauto_build';
        else
            next_step='refine_automaton';
        end
        %Now remove automatically generated CTL expressions from the list of GLOBAL_SPEC's
        GLOBAL_SPEC_TEMP={};
        for i=1:length(GLOBAL_SPEC)-GLOBAL_SPEC{length(GLOBAL_SPEC)}-1
                GLOBAL_SPEC_TEMP{i}=GLOBAL_SPEC{i};
        end
        GLOBAL_SPEC=GLOBAL_SPEC_TEMP;
        
    case 'refine_automaton',
      if save_flag
	save([savefile num2str(GLOBAL_ITERATION)])
      end
      if pause_flag
	fprintf(1,'Press any key to start refining the automaton...\n')
	pause
      end
      refine_auto(discard_flag);
      next_step = 'rauto_mapping';
    case 'rauto_mapping',
      fprintf(1,'\n')
      continu = isfield(GLOBAL_PROGRESS,'idx');
      rauto_mapping(continu);
      %next_step = 'rauto_transition';
      next_step = 'update_automaton';
    case 'rauto_transition',
      fprintf(1,'\n')
      continu = isfield(GLOBAL_PROGRESS,'idx');
      rauto_tran(continu);
      next_step = 'update_automaton';
    case 'update_automaton',
      GLOBAL_AUTOMATON = GLOBAL_NEW_AUTOMATON;
      GLOBAL_ITERATION = GLOBAL_ITERATION + 1;
      GLOBAL_NEW_AUTOMATON = {};
      next_step = 'auto_to_xsystem';
    case 'auto_to_xsystem',
      fprintf(1,'\nGenerating generic transition system.\n')
      % flatten out GLOBAL_AUTOMATON to generic transition system
      % GLOBAL_TRANSITION, the reverse transition system is also obtained in
      % GLOBAL_REV_TRANSITION
      auto2xsys;
      if discard_flag
	remove_unreachables;
      end
      next_step = 'parse_spec';
    otherwise,
      error(['Unknown verification step ''' GLOBAL_PROGRESS.step  '''.'])
  end
  GLOBAL_PROGRESS.step = next_step;
  if isfield(GLOBAL_PROGRESS,'idx')
    GLOBAL_PROGRESS = rmfield(GLOBAL_PROGRESS,'idx');
  end
  % If single step option is specified then stop.
  if single_step_flag
    break;
  end
end

if strcmp(GLOBAL_PROGRESS.step,'done') & save_flag 
  save([savefile num2str(GLOBAL_ITERATION)])
end

GLOBAL_TIME_ELAPSED.total_time = cputime - initial_time;
fprintf(1,'total verification time is %8.2f seconds.\n',GLOBAL_TIME_ELAPSED.total_time)


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

return