NuSMV/code/nusmv/core/hrc/HrcNode.h

Go to the documentation of this file.

/* ---------------------------------------------------------------------------


  This file is part of the ``hrc'' package of NuSMV version 2.
  Copyright (C) 2009 by FBK-irst.

  NuSMV version 2 is free software; you can redistribute it and/or
  modify it under the terms of the GNU Lesser General Public
  License as published by the Free Software Foundation; either
  version 2 of the License, or (at your option) any later version.

  NuSMV version 2 is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  Lesser General Public License for more details.

  You should have received a copy of the GNU Lesser General Public
  License along with this library; if not, write to the Free Software
  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.

  For more information on NuSMV see <http://nusmv.fbk.eu>
  or email to <nusmv-users@fbk.eu>.
  Please report bugs to <nusmv-users@fbk.eu>.

  To contact the NuSMV development board, email to <nusmv@fbk.eu>. 

-----------------------------------------------------------------------------*/

#ifndef __NUSMV_CORE_HRC_HRC_NODE_H__
#define __NUSMV_CORE_HRC_HRC_NODE_H__

#if HAVE_CONFIG_H
# include "nusmv-config.h"
#endif

#include <stdlib.h>
#include <stdio.h>
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/utils/Slist.h"
#include "nusmv/core/utils/Olist.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"

typedef struct HrcNode_TAG*  HrcNode_ptr;

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#define HRC_NODE(self) \
         ((HrcNode_ptr) self)

#define HRC_NODE_CHECK_INSTANCE(self) \
         (nusmv_assert(HRC_NODE(self) != HRC_NODE(NULL)))



/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

/* Constructors, Destructors, Copiers and Cleaners ****************************/

HrcNode_ptr HrcNode_create(const NuSMVEnv_ptr env);

HrcNode_ptr HrcNode_copy(const HrcNode_ptr self);

HrcNode_ptr HrcNode_copy_rename(const HrcNode_ptr self,
                                      node_ptr new_module_name);

HrcNode_ptr HrcNode_recursive_copy(const HrcNode_ptr self);

void HrcNode_cleanup(HrcNode_ptr self);

void HrcNode_destroy(HrcNode_ptr self);

void HrcNode_destroy_recur(HrcNode_ptr self);


/* Getters and Setters ********************************************************/

void HrcNode_set_symbol_table(HrcNode_ptr self, SymbTable_ptr st);

SymbTable_ptr HrcNode_get_symbol_table(HrcNode_ptr self);

void HrcNode_set_lineno(HrcNode_ptr self, int lineno);

int HrcNode_get_lineno(const HrcNode_ptr self);

void HrcNode_set_name(HrcNode_ptr self, node_ptr name);
/* Get the normalized name of the current node */

node_ptr HrcNode_get_name(const HrcNode_ptr self);
/* Get the name of the current node, NOT normalized and as passed to SetName */

node_ptr HrcNode_get_crude_name(const HrcNode_ptr self);

void HrcNode_set_instance_name(HrcNode_ptr self, node_ptr name);

node_ptr HrcNode_get_instance_name(const HrcNode_ptr self);

node_ptr HrcNode_get_flattened_instance_name(const HrcNode_ptr self);

void HrcNode_set_parent(const HrcNode_ptr self, HrcNode_ptr father);
/* NULL if it is the root */

HrcNode_ptr HrcNode_get_parent(const HrcNode_ptr self);

HrcNode_ptr HrcNode_get_root(const HrcNode_ptr self);

void HrcNode_replace_formal_parameters(HrcNode_ptr self, Olist_ptr par);

Oiter HrcNode_get_formal_parameters_iter(const HrcNode_ptr self);

void HrcNode_add_formal_parameter(HrcNode_ptr self, node_ptr par);

node_ptr HrcNode_find_formal_parameter(const HrcNode_ptr self,
                                              node_ptr par_name);

int HrcNode_get_formal_parameters_length(const HrcNode_ptr self);

void HrcNode_replace_actual_parameters(HrcNode_ptr self, Olist_ptr par);

Oiter HrcNode_get_actual_parameters_iter(const HrcNode_ptr self);

void HrcNode_add_actual_parameter(HrcNode_ptr self, node_ptr par);

int HrcNode_get_actual_parameters_length(const HrcNode_ptr self);

void HrcNode_replace_state_variables(HrcNode_ptr self, Olist_ptr vars);

Oiter HrcNode_get_state_variables_iter(const HrcNode_ptr self);

void HrcNode_add_state_variable(HrcNode_ptr self, node_ptr var);

void HrcNode_replace_input_variables(HrcNode_ptr self, Olist_ptr vars);

Oiter HrcNode_get_input_variables_iter(const HrcNode_ptr self);

void HrcNode_add_input_variable(HrcNode_ptr self, node_ptr var);

void HrcNode_replace_frozen_variables(HrcNode_ptr self, Olist_ptr vars);

Oiter HrcNode_get_frozen_variables_iter(const HrcNode_ptr self);

void HrcNode_add_frozen_variable(HrcNode_ptr self, node_ptr var);

void HrcNode_replace_frozen_functions(HrcNode_ptr self, Olist_ptr functions);

Oiter HrcNode_get_frozen_functions_iter(const HrcNode_ptr self);

void HrcNode_add_frozen_function(HrcNode_ptr self, node_ptr fun);

void HrcNode_replace_defines(HrcNode_ptr self, Olist_ptr defs);

Oiter HrcNode_get_defines_iter(const HrcNode_ptr self);

void HrcNode_add_define(HrcNode_ptr self, node_ptr def);

node_ptr HrcNode_find_define(const HrcNode_ptr self,
                                    node_ptr def_name);

void HrcNode_replace_array_defines(HrcNode_ptr self, Olist_ptr mdefs);

Oiter HrcNode_get_array_defines_iter(const HrcNode_ptr self);

void HrcNode_add_array_define(HrcNode_ptr self, node_ptr mdef);

/* INIT */

void HrcNode_replace_init_exprs(HrcNode_ptr self, Olist_ptr exprs);

Oiter HrcNode_get_init_exprs_iter(const HrcNode_ptr self);

void HrcNode_add_init_expr(HrcNode_ptr self, node_ptr expr);

/* init(x) := expr */

void HrcNode_replace_init_assign_exprs(HrcNode_ptr self, Olist_ptr assigns);

Oiter HrcNode_get_init_assign_exprs_iter(const HrcNode_ptr self);

void HrcNode_add_init_assign_expr(HrcNode_ptr self, node_ptr assign);

/* INVAR */

void HrcNode_replace_invar_exprs(HrcNode_ptr self, Olist_ptr exprs);

Oiter HrcNode_get_invar_exprs_iter(const HrcNode_ptr self);

void HrcNode_add_invar_expr(HrcNode_ptr self, node_ptr expr);

/* x := expr */

void HrcNode_replace_invar_assign_exprs(HrcNode_ptr self, Olist_ptr assigns);

Oiter HrcNode_get_invar_assign_exprs_iter(const HrcNode_ptr self);

void HrcNode_add_invar_assign_expr(HrcNode_ptr self, node_ptr assign);


/* TRANS */

void HrcNode_replace_trans_exprs(HrcNode_ptr self, Olist_ptr exprs);

Oiter HrcNode_get_trans_exprs_iter(const HrcNode_ptr self);

void HrcNode_add_trans_expr(HrcNode_ptr self, node_ptr expr);

/* next(x) := epxr */

void HrcNode_replace_next_assign_exprs(HrcNode_ptr self, Olist_ptr assigns);

Oiter HrcNode_get_next_assign_exprs_iter(const HrcNode_ptr self);

void HrcNode_add_next_assign_expr(HrcNode_ptr self, node_ptr assign);

/* JUSTICE */

void HrcNode_replace_justice_exprs(HrcNode_ptr self, Olist_ptr justices);

Oiter HrcNode_get_justice_exprs_iter(const HrcNode_ptr self);

void HrcNode_add_justice_expr(HrcNode_ptr self, node_ptr justice);

/* COMPASSION */

void HrcNode_replace_compassion_exprs(HrcNode_ptr self, Olist_ptr compassions);

Oiter HrcNode_get_compassion_exprs_iter(const HrcNode_ptr self);

void HrcNode_add_compassion_expr(HrcNode_ptr self, node_ptr compassion);

/* CONSTANTS */

void HrcNode_replace_constants(HrcNode_ptr self, Olist_ptr constants);

Oiter HrcNode_get_constants_iter(const HrcNode_ptr self);

void HrcNode_add_constants(HrcNode_ptr self, node_ptr constant);

/* CTLSPEC */

void HrcNode_replace_ctl_properties(HrcNode_ptr self, Olist_ptr ctls);

Oiter HrcNode_get_ctl_properties_iter(const HrcNode_ptr self);

void HrcNode_add_ctl_property_expr(HrcNode_ptr self, node_ptr ctl);

/* LTLSPEC */

void HrcNode_replace_ltl_properties(HrcNode_ptr self, Olist_ptr ltls);

Oiter HrcNode_get_ltl_properties_iter(const HrcNode_ptr self);

void HrcNode_add_ltl_property_expr(HrcNode_ptr self, node_ptr ltl);

/* PSLSPEC */

void HrcNode_replace_psl_properties(HrcNode_ptr self, Olist_ptr psls);

Oiter HrcNode_get_psl_properties_iter(const HrcNode_ptr self);

void HrcNode_add_psl_property_expr(HrcNode_ptr self, node_ptr psl);

/* INVARSPEC */

void HrcNode_replace_invar_properties(HrcNode_ptr self, Olist_ptr invars);

Oiter HrcNode_get_invar_properties_iter(const HrcNode_ptr self);

void HrcNode_add_invar_property_expr(HrcNode_ptr self, node_ptr invar);

/* COMPUTESPEC */

void HrcNode_replace_compute_properties(HrcNode_ptr self, Olist_ptr computes);

Oiter HrcNode_get_compute_properties_iter(const HrcNode_ptr self);

void HrcNode_add_compute_property_expr(HrcNode_ptr self, node_ptr compute);

void HrcNode_set_undef(const HrcNode_ptr self, void* undef);

void* HrcNode_get_undef(const HrcNode_ptr self);

/* We assume the father of the child has been set by someone else */

void HrcNode_set_child_hrc_nodes(HrcNode_ptr self, Slist_ptr list);

void HrcNode_add_child_hrc_node(HrcNode_ptr self, HrcNode_ptr node);

Slist_ptr HrcNode_get_child_hrc_nodes(const HrcNode_ptr self);


/* Queries  *******************************************************************/

boolean HrcNode_can_declare_assign(HrcNode_ptr self, node_ptr symbol,
                                          int assign_type);

boolean HrcNode_is_root(const HrcNode_ptr self);

boolean HrcNode_is_leaf(const HrcNode_ptr self);


/* Miscellaneous **************************************************************/
/* NULL if it does not exixts */

HrcNode_ptr
HrcNode_find_hrc_node_by_mod_type(const HrcNode_ptr self,
                                  node_ptr mod_type);

/* The caller has to free returned list */

Olist_ptr
HrcNode_find_hrc_nodes_by_mod_type(const HrcNode_ptr self,
                                   const node_ptr mod_type);

/* NULL if it does not exits */

HrcNode_ptr
HrcNode_find_hrc_node_by_instance_name(const HrcNode_ptr self,
                                       node_ptr name);

/* Find var_name of a given kind (state, frozen, input) in self node */

node_ptr
HrcNode_find_var(HrcNode_ptr self, node_ptr var_name, int type);

node_ptr
HrcNode_find_var_all(HrcNode_ptr self, node_ptr var_name);

void HrcNode_link_nodes(HrcNode_ptr self, HrcNode_ptr child);

void HrcNode_unlink_nodes(HrcNode_ptr self, HrcNode_ptr child);

void HrcNode_remove_state_variable(HrcNode_ptr self,
                                          node_ptr var);

void HrcNode_remove_frozen_variable(HrcNode_ptr self,
                                          node_ptr var);

void HrcNode_remove_input_variable(HrcNode_ptr self,
                                          node_ptr var);

int HrcNode_get_vars_num(const HrcNode_ptr self);

int HrcNode_get_state_vars_num(const HrcNode_ptr self);

int HrcNode_get_frozen_vars_num(const HrcNode_ptr self);

int HrcNode_get_input_vars_num(const HrcNode_ptr self);

int HrcNode_get_defines_num(const HrcNode_ptr self);

int HrcNode_get_array_defines_num(const HrcNode_ptr self);

int HrcNode_get_parameters_num(const HrcNode_ptr self);

int HrcNode_get_constants_num(const HrcNode_ptr self);

int HrcNode_get_functions_num(const HrcNode_ptr self);

int HrcNode_get_symbols_num(const HrcNode_ptr self);




#endif /* __NUSMV_CORE_HRC_HRC_NODE_H__ */

---