compile_ap.m

一个matlab的将军模型

function [tree,ap_build_list] = compile_ap(tree)

% Compile the list of atomic propositions present in the parse tree
% obtained from the function "parse()".
%
% Syntax:
%   "[tree,ap_build_list] = compile_ap(tree)"
% 
% Description:
%   The list of atomic propositions found in the parse tree is compiled
%   so that "region" objects corresponding to the atomic propositions can
%   be constructed later. "compile_ap()" also replaces each `ap` subtree
%   in the parse tree by a single `ap` leaf node.
% 
% Implementation:
%   For the atomic proposition founds in the parse tree, "compile_ap()"
%   collects the information nesscessary to build the corresponding "region"
%   object in the output cell array "ap_build_list". 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'}".
%
%   The output variables "tree" (with the `ap` subtrees replaced by a single
%   leaf) and "ap_build_list" are used subsequently by the function
%   "build_ap()".
%
% See Also:
%   parse,identerm,build_ap,evaluate,model_check

global AP_NAME AP_BUILD_INFO

AP_NAME = {};
AP_BUILD_INFO = {};
% Depth first search on parse tree for all atomic propositions
tree = visit(tree);

ap_build_list = {};
for k = 1:length(AP_NAME)
  ap_build_list{k}.name = AP_NAME{k};
  ap_build_list{k}.build_info = AP_BUILD_INFO{k};
end
return

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

function node = visit(node)

global AP_NAME AP_BUILD_INFO

% traverse the tree to find atomic propositions
if strcmp(node.symbol,'ap')
  switch node.production
    case 'polyap',
      apname = node.value{1}.value;
      if ~ismember(apname,AP_NAME)
        new = length(AP_NAME)+1;
        AP_NAME{new} = apname;
        AP_BUILD_INFO{new} = {'polyap'};
      end
      % replace subtree by a single leaf node representing apname
      node.production = 'none';
      node.value = apname;
    case 'fsmap',
      fsmname = node.value{1}.value;
      statename = node.value{3}.value;
      apname = [fsmname '_in_' statename];
      if ~ismember(apname,AP_NAME)
        new = length(AP_NAME)+1;
        AP_NAME{new} = apname;
        AP_BUILD_INFO{new} = {'fsmap' fsmname statename};
      end
      % replace subtree by a single leaf node representing this finite
      % state machine atomic proposition
      node.production = 'none';
      node.value = apname;
    otherwise,
      error(['Unknown production ''' node.production ...
            ''' for atomic proposition'])
  end
else
  if ~ischar(node.value)
    for k = 1:length(node.value)
      node.value{k} = visit(node.value{k});
    end
  end
end
return