visit.m

CheckMate is a MATLAB-based tool for modeling, simulating and investigating properties of hybrid dyn

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'])
% moved
  end
else
  if ~ischar(node.value)
    for k = 1:length(node.value)
      node.value{k} = visit(node.value{k});
    end
  end
end