// Check the inductiveness axiom
*operation* int check_inductiveness()
  *init* (@ 1 @)

  *traverse* *from*    Cd_graph
             *through* =>Neighbors_wc,Construct_ns
             *to*      Term


  *carry* *in* Cd_graph* graph = (@ this @)
          *along* *from* Cd_graph
                  *to*   Adjacency

  *carry* *inout* int num_viols
          *along* *from* Cd_graph
                  *to*   Adjacency

  *carry* *inout* Ind_list* ilist
          *along* *from* Cd_graph
                  *to*   Adjacency
                  
  *wrapper* Cd_graph
    *prefix* (@ cout << endl
                     << "Checking the Inductiveness Axiom ..."
                     << endl;
                num_viols = 0;
              @)

    *suffix* (@ if (num_viols > 0) {
                  cout << endl << endl << "Warning: There are " << num_viols
                       << " violations of the Inductiveness Axiom" << endl;
                  return_val = 0;
                }
              @)
              
  *wrapper* Adjacency
    *prefix* (@
                ilist = new Ind_list;
                ilist->append(this->get_source());
              
                if (this->check_inductiveness1(graph, this->get_source(), ilist)) {
                  cout << endl << "\tThere are no non-cyclic objects for the "
                       << "following classes:"
                       << endl << "\t";
                  ilist->g_print();
                  num_viols++;
                  return_val = 0;
                }
              @)
    *suffix* (@ 
                delete ilist;
              @)
                            
*operation* int check_inductiveness1(Cd_graph* graph, Vertex* src, 
                                     Ind_list* ilist)
  *init* (@ 0 @)
  
  *traverse* *from* Adjacency
             *to*   {Construct_ns, Alternat_ns}
             
  *wrapper* Alternat_ns
    *prefix* (@ 
                if (this->check_inductiveness2(graph, src, ilist)) {
                  return_val = 1;
                }
              @)
              
  *wrapper* Construct_ns
    *prefix* (@ 
                if (this->check_inductiveness3(graph, src, ilist)) {
                  return_val = 1;
                }
              @)
              
                            
*operation* int check_inductiveness2(Cd_graph* graph, Vertex* src, Ind_list* ilist) 
  *init* (@ 1 @)

  *traverse* *from*    Alternat_ns 
             *through* ->Alternat_ns,alternat_ns,*
             *to*      Term

  *wrapper* Term
    *prefix* (@ 
                if (return_val == 1) {
                  if (!ilist->check_inductiveness4(this->get_vertex())) {
                    Adjacency* adjclass = graph->find_adjacency(this->get_vertex());
                    if (adjclass != NULL) {
                      ilist->append(this->get_vertex());
                      if (!adjclass->check_inductiveness1(graph, src, ilist)) {
                          return_val = 0;
                      }

                    }
                  }
                  else if (this->find_line_number() <= 
                           src->get_vertex_name()->get_line_number()) { 
                    return_val = 0;
                  }
                }
              @)

*operation* int check_inductiveness3(Cd_graph* graph, Vertex* src, Ind_list* ilist)
  *init* (@ 0 @)
  
  *traverse* *from*      Construct_ns
             *bypassing* ->Optional_term,opt,*
             *to*        Term
             
  *wrapper* Term
    *prefix* (@ 
                if (return_val == 0) {
                  if (ilist->check_inductiveness4(this->get_vertex())) {
                    if (this->find_line_number() > 
                        src->get_vertex_name()->get_line_number()) {
                      return_val = 1;
                    }
                  }
                  else {
                    Adjacency* adjclass = graph->find_adjacency(this->get_vertex());
                    if (adjclass != NULL) {
                      ilist->append(this->get_vertex());
                      if (adjclass->check_inductiveness1(graph, src, ilist)) {
                        return_val = 1;
                      }                      
                    }
                  }
                }
              @)

*operation* int check_inductiveness4(Vertex* v) 
  *init* (@ 0 @)
  
  *traverse* *from* Ind_list
             *to*   Vertex
             
  *wrapper* Vertex
    *prefix* (@ if (this->g_equal(v)) return_val = 1; @)