build_ap.m

一个matlab的将军模型

function atomic_propositions = build_ap(ap_build_list)

% Build regions corresponding to the atomic propositions specified in the
% input list.
% 
% Syntax:
%   "build_ap(ap_build_list)"
% 
% Description:
%   Builds "region" objects for the atomic propositions specified in the
%   input list "ap_build_list", which is a cell array. 
%
% Implementation:
%   Each element of "ap_build_list" is a structure with the following
%   fields.
%
%   * "name", the name of the atomic proposition. For a `polyhedral
%     threshold atomic proposition (PTHAP)`, this is the name of the
%     corresponding PTHB. For a `finite-state machine atomic proposition`
%     (FSMAP) of the form "<FSMB> == <state>", the name is
%     "<FSMB>_in_<state>". For example, the FSMAP "switch == on" will
%     be named "switch_in_on".
%
%   * "build_info". This is the field that is used to specify the type
%     of each atomic proposition. For a PTHAP, "build_info" is simply
%     "'polyap'". For an FSMAP, "build_info" is a cell array of the form
%     "{'fsmap' fsmname statename}". For example, "build_info" for the
%     FSMAP "switch == on" is "{'fsmap' 'switch' 'on'}".
%
%   A "region" object is computed for each atomic proposition as
%   follows. For a PTHAP, include all states such that the "pthflags" for
%   cell of the parent location is true for the corresponding PTHB. There
%   are 4 special atomic propositions which have the same form as a PTHAP,
%   namely "null_event", "time_limit", "out_of_bound", and
%   "indeterminate". For each of these atomic propositions, the
%   corresponding special terminal states in all locations are included in
%   the "region" object. For an FSMAP, include all states such that the FSM
%   state of the parent location indicates that the FSMB specified in the
%   FSMAP is in the state specified in the FSMAP. See help on "piha.m" for
%   more information of the data structure of `locations` in the PIHA. See
%   help on "auto2xsys.m" for the correspondence between states in
%   "GLOBAL_AUTOMATON" and states in "GLOBAL_TRANSITION".
%
%
%
%   Put the "region" computed for each atomic proposition in the field with
%   the same name as the atomic proposition in the output variable
%   "atomic_propositions". For example, the region corresponding to an FSMAP
%   named "switch_in_on" is stored in "atomic_propositions.switch_in_on".
%
% See Also:
%   parse,identerm,compile_ap,evaluate,model_check,piha,auto2xsys

atomic_propositions = [];
for k = 1:length(ap_build_list)
  switch ap_build_list{k}.build_info{1}
    case 'polyap',
      temp = build_poly_ap(ap_build_list{k}.name);
    case 'fsmap',
      fsmname = ap_build_list{k}.build_info{2};
      statename = ap_build_list{k}.build_info{3};
      temp = build_fsm_ap(fsmname,statename);
    otherwise
      error(['Invalid atomic proposition type ''' ... 
            ap_build_list{k}.build_info{1} '''.'])
  end
  eval(['atomic_propositions.' ap_build_list{k}.name ' = temp;'])
end

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

function ap = build_poly_ap(apname)

global GLOBAL_PIHA GLOBAL_TRANSITION GLOBAL_XSYS2AUTO_MAP GLOBAL_AUTO2XSYS_MAP

% build region for apname if it is a new atomic proposition
N = length(GLOBAL_TRANSITION);
NL = length(GLOBAL_PIHA.Locations);
switch apname
  case 'null_event',
    ap = region(N,[0:NL-1] + GLOBAL_AUTO2XSYS_MAP.ne_start);
  case 'time_limit',
    ap = region(N,[0:NL-1] + GLOBAL_AUTO2XSYS_MAP.tl_start);
  case 'out_of_bound',
    ap = region(N,[0:NL-1] + GLOBAL_AUTO2XSYS_MAP.oob_start);
  case 'indeterminate',
    ap = region(N,[0:NL-1] + GLOBAL_AUTO2XSYS_MAP.ind_start);
  otherwise,

% ******************************************************************
% The following was commented out by JPK 6/2002 because we no
% longer want to allow CheckMate to permit PTHB names in CTL
% expressions
% ******************************************************************
%     % otherwise apname must be PTHB name
%     found = 0;
%     for k = 1:length(GLOBAL_PIHA.PTHBlocks)
%       if strcmp(apname,GLOBAL_PIHA.PTHBlocks{k}.name)
%         found = 1;
%         pthidx = k;
%         break
%       end
%     end
%     if found
%       ap = region(N,'false');
%       for k = 1:N
%         if isa(GLOBAL_XSYS2AUTO_MAP{k},'double')
%           loc = GLOBAL_XSYS2AUTO_MAP{k}(1);
%         else 
%           % must be special states
% 	  if strcmp(GLOBAL_XSYS2AUTO_MAP{k}{1},'terminal')
% 	    loc = -1;
% 	  else
% 	    loc = GLOBAL_XSYS2AUTO_MAP{k}{2};
% 	  end
%         end
% 	if (loc == -1) % for terminal FSM state we should give a "don't
%                        % care" for all PTHB signals but since we can't do
%                        % this yet, we set the default value to 0.
% 	  ap = set_state(ap,k,0);
% 	else
% 	  pthflags = GLOBAL_PIHA.Cells{GLOBAL_PIHA.Locations{loc}.p}.pthflags;
% 	  if pthflags(pthidx)
% 	    ap = set_state(ap,k,1);
% 	  end
% 	end
%       end
%     else
%       error(['Invalid atomic proposition name ''' apname '''.'])
%     end
% ******************************************************************
     error(['Invalid atomic proposition name ''' apname '''.'])
end

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

function ap = build_fsm_ap(fsmname,statename)

global GLOBAL_PIHA GLOBAL_TRANSITION GLOBAL_XSYS2AUTO_MAP

found = 0;
for k = 1:length(GLOBAL_PIHA.FSMBlocks)
  if strcmp(fsmname,GLOBAL_PIHA.FSMBlocks{k}.name)
    fsmidx = k;
    found = 1;
    break;
  end
end
if ~found
  error(['Invalid FSM block name ''' fsmname '''.'])
end

found = 0;
for k = 1:length(GLOBAL_PIHA.FSMBlocks{fsmidx}.states)
  if strcmp(statename,GLOBAL_PIHA.FSMBlocks{fsmidx}.states{k})
    stateidx = k;
    found = 1;
    break;
  end
end
if ~found
  error(['Invalid state name ''' statename ''' for FSM block ''' ...
        fsmname '''.'])
end

N = length(GLOBAL_TRANSITION);
ap = region(N,'false');
for k = 1:N
    if isa(GLOBAL_XSYS2AUTO_MAP{k},'double')
        loc = GLOBAL_XSYS2AUTO_MAP{k}(1);
        q = GLOBAL_PIHA.Locations{loc}.q;
    else 
        % must be special states
        if strcmp(GLOBAL_XSYS2AUTO_MAP{k}{1},'terminal')
            q = GLOBAL_XSYS2AUTO_MAP{k}{2};
            if (q(fsmidx) == stateidx)
            ap = set_state(ap,k,1);
            end 
        else
            loc = GLOBAL_XSYS2AUTO_MAP{k}{2};
            q = GLOBAL_PIHA.Locations{loc}.q;
        end                                      % I move that part into the else block to bypass the terminal 
    end
      
    if (q(fsmidx) == stateidx)
        ap = set_state(ap,k,1);
    end 
end
return