NuSMV/code/nusmv/core/prop/Prop.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_H__
#define __NUSMV_CORE_PROP_PROP_H__

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

#include "nusmv/core/fsm/FsmBuilder.h"
#include "nusmv/core/wff/ExprMgr.h"
#include "nusmv/core/set/set.h"
#include "nusmv/core/fsm/sexp/SexpFsm.h"
#include "nusmv/core/fsm/sexp/BoolSexpFsm.h"
#include "nusmv/core/fsm/bdd/BddFsm.h"
#include "nusmv/core/fsm/be/BeFsm.h"

#include "nusmv/core/utils/object.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/OStream.h"


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
enum _Prop_Status {Prop_NoStatus, Prop_Unchecked, Prop_True, Prop_False,
                   Prop_Number, Prop_Error};

#define PROP_NOSTATUS_STRING "NoStatus"

#define PROP_UNCHECKED_STRING "Unchecked"

#define PROP_TRUE_STRING "True"

#define PROP_FALSE_STRING "False"

#define PROP_NUMBER_STRING "Number"


 /* warning [MD] Bad practice: downcase constants */
enum _Prop_Type {
  Prop_Prop_Type_First = 100, /* Do not touch this */
  /* ---------------------------------------------------------------------- */
  Prop_NoType,
  Prop_Ctl,
  Prop_Ltl,
  Prop_Psl,
  Prop_Invar,
  Prop_Compute,
  Prop_CompId, /* For properties names comparison */
  /* ---------------------------------------------------------------------- */
  Prop_Prop_Type_Last /* Do not touch this */
};


enum _PropDb_PrintFmt {
  PROPDB_PRINT_FMT_TABULAR,
  PROPDB_PRINT_FMT_DEFAULT = PROPDB_PRINT_FMT_TABULAR,
  PROPDB_PRINT_FMT_XML,
};

enum _Prop_PrintFmt {
  PROP_PRINT_FMT_FORMULA,
  PROP_PRINT_FMT_FORMULA_TRUNC,
  PROP_PRINT_FMT_INDEX,
  PROP_PRINT_FMT_NAME,
  PROP_PRINT_FMT_DEFAULT = PROP_PRINT_FMT_FORMULA
};

#define PROP_NOTYPE_STRING "NoType"

#define PROP_CTL_STRING "CTL"

#define PROP_LTL_STRING "LTL"

#define PROP_PSL_STRING "PSL"

#define PROP_INVAR_STRING "Invar"

#define PROP_COMPUTE_STRING "Quantitative"

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef enum _Prop_Status Prop_Status;
typedef enum _Prop_Type Prop_Type;
typedef enum _PropDb_PrintFmt PropDb_PrintFmt;
typedef enum _Prop_PrintFmt Prop_PrintFmt;

typedef struct Prop_TAG*  Prop_ptr;

#define PROP(self) \
         ((Prop_ptr) self)

#define PROP_CHECK_INSTANCE(self) \
         (nusmv_assert(PROP(self) != PROP(NULL)))



/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/
/* Constructors, Destructors, Copiers and Cleaners ****************************/

Prop_ptr Prop_create(const NuSMVEnv_ptr env);

Prop_ptr Prop_create_partial(const NuSMVEnv_ptr env,
                             Expr_ptr expr, Prop_Type type);

Prop_ptr Prop_copy(Prop_ptr input);

Prop_ptr Prop_create_from_string(NuSMVEnv_ptr env, char* str, Prop_Type type);

void Prop_destroy(Prop_ptr self);


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

Expr_ptr Prop_get_expr(const Prop_ptr self);

Expr_ptr Prop_get_expr_core(const Prop_ptr self);

Expr_ptr Prop_get_expr_core_for_coi(const Prop_ptr self);

Expr_ptr Prop_get_flattened_expr(const Prop_ptr self, SymbTable_ptr st);

Set_t    Prop_get_cone(const Prop_ptr self);

void Prop_set_cone(Prop_ptr self, Set_t cone);

Prop_Type Prop_get_type(const Prop_ptr self);

const char* Prop_get_type_as_string(Prop_ptr self);

node_ptr Prop_get_name(const Prop_ptr self);

char* Prop_get_name_as_string(const Prop_ptr self);

void Prop_set_name(Prop_ptr self, const node_ptr name);

SymbTable_ptr Prop_get_symb_table(const Prop_ptr self);

Prop_Status Prop_get_status(const Prop_ptr self);

const char* Prop_get_status_as_string(const Prop_ptr self);

int Prop_get_number(const Prop_ptr self);

char* Prop_get_number_as_string(const Prop_ptr self);

int Prop_get_trace(const Prop_ptr self);

void Prop_set_status(Prop_ptr self, Prop_Status s);

void Prop_set_number(Prop_ptr self, int n);

void Prop_set_number_infinite(Prop_ptr self);

void Prop_set_number_undefined(Prop_ptr self);

void Prop_set_trace(Prop_ptr self, int t);

int Prop_get_index(const Prop_ptr self);

void Prop_set_index(Prop_ptr self, const int index);

char* Prop_get_name_as_string(const Prop_ptr self);

SexpFsm_ptr
Prop_compute_ground_sexp_fsm(const NuSMVEnv_ptr env, const Prop_ptr self);

BddFsm_ptr
Prop_compute_ground_bdd_fsm(const NuSMVEnv_ptr env, const Prop_ptr self);

BeFsm_ptr
Prop_compute_ground_be_fsm(const NuSMVEnv_ptr env, const Prop_ptr self);

SexpFsm_ptr Prop_get_scalar_sexp_fsm(const Prop_ptr self);

BoolSexpFsm_ptr Prop_get_bool_sexp_fsm(const Prop_ptr self);

BddFsm_ptr  Prop_get_bdd_fsm(const Prop_ptr self);

BeFsm_ptr Prop_get_be_fsm(const Prop_ptr self);

void Prop_set_scalar_sexp_fsm(Prop_ptr self, SexpFsm_ptr fsm);

void Prop_set_bool_sexp_fsm(Prop_ptr self, BoolSexpFsm_ptr fsm);

void Prop_set_bdd_fsm(Prop_ptr self, BddFsm_ptr fsm);

void Prop_set_be_fsm(Prop_ptr self, BeFsm_ptr fsm);

char* Prop_get_text(const Prop_ptr self);

char* Prop_get_context_text(const Prop_ptr self);


/* COI ************************************************************************/

Set_t Prop_compute_cone(const Prop_ptr self,
                               FlatHierarchy_ptr hierarchy,
                               SymbTable_ptr symb_table);

void
Prop_apply_coi_for_scalar(const NuSMVEnv_ptr env, Prop_ptr self);

void
Prop_apply_coi_for_bdd(const NuSMVEnv_ptr env, Prop_ptr self);

void
Prop_apply_coi_for_bmc(const NuSMVEnv_ptr env, Prop_ptr self);

void Prop_destroy_coi_for_bmc(Prop_ptr self);


/* Printers *******************************************************************/

void Prop_print(Prop_ptr self, OStream_ptr file, Prop_PrintFmt fmt);

void Prop_print_db(Prop_ptr self, OStream_ptr file, PropDb_PrintFmt);


/* Miscellaneous **************************************************************/
SexpFsm_ptr
Prop_compute_ground_sexp_fsm(const NuSMVEnv_ptr env, const Prop_ptr self);
BddFsm_ptr
Prop_compute_ground_bdd_fsm(const NuSMVEnv_ptr env, const Prop_ptr self);
BeFsm_ptr
Prop_compute_ground_be_fsm(const NuSMVEnv_ptr env, const Prop_ptr self);

void Prop_set_environment_fsms(const NuSMVEnv_ptr env, Prop_ptr prop);

Set_t Prop_set_from_formula_list(NuSMVEnv_ptr env, node_ptr list, Prop_Type type);

Prop_ptr Prop_convert_to_invar(Prop_ptr self);


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

boolean Prop_needs_rewriting(SymbTable_ptr st,
                                    const Prop_ptr self);

boolean Prop_is_psl_ltl(const Prop_ptr self);

boolean Prop_is_psl_obe(const Prop_ptr self);

void Prop_verify(Prop_ptr self);

int Prop_check_type(const Prop_ptr self, Prop_Type type);


/* PropType sub-interface *****************************************************/

const char* PropType_to_string(const Prop_Type type);

const char* PropType_to_parsing_string(const Prop_Type type);

short int PropType_to_node_type(const Prop_Type type);


#endif /* __NUSMV_CORE_PROP_PROP_H__ */

---