NuSMV/code/nusmv/core/prop/PropDb.h

Go to the documentation of this file.

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


  This file is part of the ``prop'' package of NuSMV version 2.
  Copyright (C) 2010 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_PROP_PROP_DB_H__
#define __NUSMV_CORE_PROP_PROP_DB_H__

#include "nusmv/core/prop/Prop.h"

#include "nusmv/core/utils/object.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/list.h"
#include "nusmv/core/utils/ErrorMgr.h"


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

typedef struct PropDb_TAG*  PropDb_ptr;

#define PROP_DB(self) \
         ((PropDb_ptr) self)

#define PROP_DB_CHECK_INSTANCE(self) \
         (nusmv_assert(PROP_DB(self) != PROP_DB(NULL)))

#define PROP_DB_FOREACH(self, i)                \
  for (i = 0; i < PropDb_get_size(self); ++i)


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

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

PropDb_ptr PropDb_create(NuSMVEnv_ptr env);

void PropDb_destroy(PropDb_ptr self);

void PropDb_clean(PropDb_ptr self);


/* Getters and Setters ********************************************************/
/* List of Properties --------------------------------------------------------*/

lsList PropDb_get_props_of_type(const PropDb_ptr self,
                                const Prop_Type type);

lsList PropDb_get_ordered_props_of_type(const PropDb_ptr self,
                                        const FlatHierarchy_ptr hierarchy,
                                        const Prop_Type type);

NodeList_ptr
PropDb_get_ordered_properties(const PropDb_ptr self,
                              const FlatHierarchy_ptr hierarchy);

NodeList_ptr
PropDb_get_coi_grouped_properties(const PropDb_ptr self,
                                  const FlatHierarchy_ptr hierarchy);

lsList PropDb_prepare_prop_list(const PropDb_ptr self,
                                const Prop_Type type);

/* ---------------------------------------------------------------------------*/
/* Property ------------------------------------------------------------------*/

Prop_ptr PropDb_get_last(const PropDb_ptr self);

Prop_ptr PropDb_get_prop_at_index(const PropDb_ptr self,
                                  int num);

Set_t PropDb_get_props_at_indices(const PropDb_ptr self,
                                  const ErrorMgr_ptr errmgr,
                                  const char* indices);

/* ---------------------------------------------------------------------------*/
/* Index ---------------------------------------------------------------------*/

int PropDb_get_prop_name_index(const PropDb_ptr self,
                               const node_ptr name);

int PropDb_get_prop_index_from_string(const PropDb_ptr self,
                                      const char* idx);

int PropDb_get_prop_index_from_trace_index(const PropDb_ptr self,
                                           const int trace_idx);
/* ---------------------------------------------------------------------------*/

int PropDb_get_size(const PropDb_ptr self);

int PropDb_prop_parse_name(const PropDb_ptr self,
                           const char* str);

PropDb_PrintFmt PropDb_set_print_fmt(const PropDb_ptr self,
                                     PropDb_PrintFmt new_fmt);


/* Printing********************************************************************/

void PropDb_print_list_header(const PropDb_ptr self,
                              OStream_ptr file);

void PropDb_print_list_footer(const PropDb_ptr self,
                              OStream_ptr file);

int PropDb_print_prop_at_index(const PropDb_ptr self,
                               OStream_ptr file, const int index);

void PropDb_print_all(const PropDb_ptr self,
                      OStream_ptr file);

void PropDb_print_all_type(const PropDb_ptr self,
                           OStream_ptr file, Prop_Type type);

void PropDb_print_all_status(const PropDb_ptr self,
                             OStream_ptr file, Prop_Status status);

void PropDb_print_all_status_type(const PropDb_ptr self,
                                  OStream_ptr file, Prop_Status status,
                                  Prop_Type type);


/* Verify**********************************************************************/

int
PropDb_check_property(const PropDb_ptr self,
                      const Prop_Type pt,
                      const char* formula,
                      const int prop_no);

void PropDb_verify_all(const PropDb_ptr self);

void PropDb_verify_all_type(const PropDb_ptr self, Prop_Type);

void PropDb_ordered_verify_all(const PropDb_ptr self,
                                      const FlatHierarchy_ptr hierarchy);

void
PropDb_ordered_verify_all_type(const PropDb_ptr self,
                               const FlatHierarchy_ptr hierarchy,
                               const Prop_Type type);

void PropDb_verify_prop_at_index(const PropDb_ptr self,
                                 const int index);

void PropDb_verify_all_type_wrapper(PropDb_ptr const self,
                                    const Prop_Type type);

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

int PropDb_prop_parse_and_add(const PropDb_ptr self,
                              SymbTable_ptr symb_table,
                              const char* str,
                              const Prop_Type type,
                              const node_ptr expr_name);

PropDb_PrintFmt PropDb_get_print_fmt(const PropDb_ptr self);

int
PropDb_fill(PropDb_ptr self, SymbTable_ptr symb_table,
            node_ptr, node_ptr, node_ptr,
            node_ptr, node_ptr);

boolean PropDb_add(PropDb_ptr self, Prop_ptr);

int
PropDb_prop_create_and_add(PropDb_ptr self, SymbTable_ptr symb_table,
                           node_ptr, Prop_Type);

int
PropDb_show_property(const PropDb_ptr self,
                     const boolean print_props_num,
                     const PropDb_PrintFmt fmt,
                     const Prop_Type type,
                     const Prop_Status status,
                     const int prop_no,
                     FILE* outstream);

boolean
PropDb_is_prop_registered(PropDb_ptr self,
                          Prop_ptr prop);


#endif /* __NUSMV_CORE_PROP_PROP_DB_H__ */

---