NuSMV/code/nusmv/core/compile/FlatHierarchy.h

Go to the documentation of this file.

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


  This file is part of the ``compile'' package of NuSMV version 2.
  Copyright (C) 2005 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_COMPILE_FLAT_HIERARCHY_H__
#define __NUSMV_CORE_COMPILE_FLAT_HIERARCHY_H__

#include "nusmv/core/node/node.h"
#include "nusmv/core/set/set.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/utils/assoc.h"

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef struct FlatHierarchy* FlatHierarchy_ptr;

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#define FLAT_HIERARCHY(x) ((FlatHierarchy_ptr) x)

#define FLAT_HIERARCHY_CHECK_INSTANCE(x) \
         ( nusmv_assert(FLAT_HIERARCHY(x) != FLAT_HIERARCHY(NULL)) )


/* ---------------------------------------------------------------------- */
/* Public interface                                                       */
/* ---------------------------------------------------------------------- */
/* Constructors, Destructors, Copiers and Cleaners ****************************/

FlatHierarchy_ptr FlatHierarchy_create(SymbTable_ptr st);

FlatHierarchy_ptr
FlatHierarchy_create_from_members(SymbTable_ptr st,
                                  node_ptr init,
                                  node_ptr invar,
                                  node_ptr trans,
                                  node_ptr input,
                                  node_ptr justice,
                                  node_ptr compassion);

void  FlatHierarchy_destroy(FlatHierarchy_ptr self);

FlatHierarchy_ptr
FlatHierarchy_copy(const FlatHierarchy_ptr self);

void FlatHierarchy_mergeinto(FlatHierarchy_ptr self,
                                    const FlatHierarchy_ptr other);



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

NuSMVEnv_ptr
FlatHierarchy_get_environment(const FlatHierarchy_ptr self);

SymbTable_ptr
FlatHierarchy_get_symb_table(const FlatHierarchy_ptr self);

void
FlatHierarchy_set_symb_table(const FlatHierarchy_ptr self,
                             SymbTable_ptr symb_table);

/* Access function to the class's fields : constrains and specifications ******/

node_ptr FlatHierarchy_get_init(FlatHierarchy_ptr cmp);

void FlatHierarchy_set_init(FlatHierarchy_ptr cmp, node_ptr n);

void FlatHierarchy_add_init(FlatHierarchy_ptr cmp, node_ptr n);

node_ptr FlatHierarchy_get_invar(FlatHierarchy_ptr cmp);

void FlatHierarchy_set_invar(FlatHierarchy_ptr cmp, node_ptr n);

void FlatHierarchy_add_invar(FlatHierarchy_ptr cmp, node_ptr n);

node_ptr FlatHierarchy_get_trans(FlatHierarchy_ptr cmp);

void FlatHierarchy_set_trans(FlatHierarchy_ptr cmp, node_ptr n);

void FlatHierarchy_add_trans(FlatHierarchy_ptr cmp, node_ptr n);

node_ptr FlatHierarchy_get_input(FlatHierarchy_ptr cmp);

void FlatHierarchy_set_input(FlatHierarchy_ptr cmp, node_ptr n);

node_ptr FlatHierarchy_get_assign(FlatHierarchy_ptr cmp);

void
FlatHierarchy_set_assign(FlatHierarchy_ptr cmp, node_ptr n);


/* properties *****************************************************************/

node_ptr FlatHierarchy_get_justice(FlatHierarchy_ptr cmp);

void
FlatHierarchy_set_justice(FlatHierarchy_ptr cmp, node_ptr n);

node_ptr FlatHierarchy_get_compassion(FlatHierarchy_ptr cmp);

void FlatHierarchy_set_compassion(FlatHierarchy_ptr cmp,
                                         node_ptr n);

boolean FlatHierarchy_add_property_name(FlatHierarchy_ptr cmp,
                                            node_ptr name);

node_ptr FlatHierarchy_get_spec(FlatHierarchy_ptr cmp);

void FlatHierarchy_set_spec(FlatHierarchy_ptr cmp, node_ptr n);

node_ptr FlatHierarchy_get_ltlspec(FlatHierarchy_ptr cmp);

void
FlatHierarchy_set_ltlspec(FlatHierarchy_ptr cmp, node_ptr n);

node_ptr FlatHierarchy_get_invarspec(FlatHierarchy_ptr cmp);

void FlatHierarchy_set_invarspec(FlatHierarchy_ptr cmp,
                                        node_ptr n);

node_ptr FlatHierarchy_get_pslspec(FlatHierarchy_ptr cmp);

void
FlatHierarchy_set_pslspec(FlatHierarchy_ptr cmp, node_ptr n);

node_ptr FlatHierarchy_get_compute(FlatHierarchy_ptr cmp);

void
FlatHierarchy_set_compute(FlatHierarchy_ptr cmp, node_ptr n);


/* -- access functions to the variable sets -- ********************************/

Set_t FlatHierarchy_get_vars(FlatHierarchy_ptr cmp);

void FlatHierarchy_add_var(FlatHierarchy_ptr cmp, node_ptr n);

void FlatHierarchy_remove_var(FlatHierarchy_ptr self, node_ptr n);

NodeList_ptr
FlatHierarchy_get_ordered_vars(const FlatHierarchy_ptr self,
                               hash_ptr* outbound_edges);

node_ptr FlatHierarchy_get_preds(FlatHierarchy_ptr cmp);

void FlatHierarchy_add_pred(FlatHierarchy_ptr cmp, node_ptr n);

void FlatHierarchy_set_pred(FlatHierarchy_ptr cmp, node_ptr n);

node_ptr FlatHierarchy_get_mirrors(FlatHierarchy_ptr cmp);

void FlatHierarchy_add_mirror(FlatHierarchy_ptr cmp, node_ptr n);

void FlatHierarchy_set_mirror(FlatHierarchy_ptr cmp, node_ptr n);


node_ptr FlatHierarchy_get_property_patterns(FlatHierarchy_ptr cmp);

void FlatHierarchy_add_property_pattern(FlatHierarchy_ptr cmp, node_ptr n);

void FlatHierarchy_set_property_patterns(FlatHierarchy_ptr cmp, node_ptr n);


/* Access function to the hash.
   Given a var name these functions can return right handside of
   init-assignment, invar-assignmnent and next-assign which have the given
   variable on the left handside.
   The functions also can return the list of INIT, INVAR and TRANS expressions
   which contain the given variable.
*/

node_ptr FlatHierarchy_lookup_assign(FlatHierarchy_ptr self,
                                            node_ptr name);

void FlatHierarchy_insert_assign(FlatHierarchy_ptr self,
                                        node_ptr name,
                                        node_ptr assign);

node_ptr FlatHierarchy_lookup_constrains(FlatHierarchy_ptr self,
                                                node_ptr name);

void FlatHierarchy_add_constrains(FlatHierarchy_ptr self,
                                         node_ptr name,
                                         node_ptr expr);

node_ptr
FlatHierarchy_lookup_constant_constrains(FlatHierarchy_ptr self,
                                         int type);

void FlatHierarchy_add_constant_constrains(FlatHierarchy_ptr self,
                                                  node_ptr expr,
                                                  int type);

void
FlatHierarchy_calculate_vars_constrains(FlatHierarchy_ptr self);

hash_ptr
FlatHierarchy_get_var_expr_associations(FlatHierarchy_ptr self);

void
FlatHierarchy_set_var_expr_associations(FlatHierarchy_ptr self,
                                        hash_ptr h);

void
FlatHierarchy_clear_var_expr_associations(FlatHierarchy_ptr self);

hash_ptr
FlatHierarchy_get_constants_associations(FlatHierarchy_ptr self);

void
FlatHierarchy_set_constants_associations(FlatHierarchy_ptr self,
                                         hash_ptr h);

void
FlatHierarchy_clear_constants_associations(FlatHierarchy_ptr self);


/* Miscellaneous **************************************************************/

void FlatHierarchy_self_check(const FlatHierarchy_ptr self);

void FlatHierarchy_type_check(FlatHierarchy_ptr self);


#endif /* __NUSMV_CORE_COMPILE_FLAT_HIERARCHY_H__ */

---