NuSMV/code/nusmv/core/ltl/ltl.h

Go to the documentation of this file.

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


  This file is part of the ``ltl'' package of NuSMV version 2.
  Copyright (C) 1998-2001 by CMU and 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_LTL_LTL_H__
#define  __NUSMV_CORE_LTL_LTL_H__

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/prop/Prop.h"
#include "nusmv/core/wff/ExprMgr.h"
#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/utils/OStream.h"

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

typedef struct Ltl_StructCheckLtlSpec_TAG* Ltl_StructCheckLtlSpec_ptr;

typedef node_ptr (*Ltl_StructCheckLtlSpec_oreg2smv)(NuSMVEnv_ptr,
                                                    unsigned int,
                                                    node_ptr);
typedef node_ptr (*Ltl_StructCheckLtlSpec_ltl2smv)(NuSMVEnv_ptr,
                                                   unsigned int,
                                                   node_ptr);

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

#define LTL_STRUCTCHECKLTLSPEC(self) \
         ((Ltl_StructCheckLtlSpec_ptr) self)

#define LTL_STRUCTCHECKLTLSPEC_CHECK_INSTANCE(self) \
         (nusmv_assert(LTL_STRUCTCHECKLTLSPEC(self) != \
          LTL_STRUCTCHECKLTLSPEC(NULL)))


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

void print_ltlspec(OStream_ptr, Prop_ptr, Prop_PrintFmt);

void Ltl_CheckLtlSpec(NuSMVEnv_ptr env, Prop_ptr prop);

void
Ltl_spec_to_hierarchy(NuSMVEnv_ptr env,
                      Expr_ptr spec, node_ptr context,
                      node_ptr (*what2smv)(NuSMVEnv_ptr env,
                                           unsigned int id,
                                           node_ptr expr),
                      SymbLayer_ptr layer,
                      FlatHierarchy_ptr outfh);

Expr_ptr
Ltl_apply_input_vars_rewriting(Expr_ptr spec, SymbTable_ptr st,
                               SymbLayer_ptr layer,
                               FlatHierarchy_ptr outfh);

Ltl_StructCheckLtlSpec_ptr Ltl_StructCheckLtlSpec_create(NuSMVEnv_ptr env,
                                                                Prop_ptr prop);

void Ltl_StructCheckLtlSpec_destroy(Ltl_StructCheckLtlSpec_ptr self);

void Ltl_StructCheckLtlSpec_set_oreg2smv(Ltl_StructCheckLtlSpec_ptr self,
                                                Ltl_StructCheckLtlSpec_oreg2smv oreg2smv);

void Ltl_StructCheckLtlSpec_set_ltl2smv(Ltl_StructCheckLtlSpec_ptr self,
                                               Ltl_StructCheckLtlSpec_ltl2smv ltl2smv);

void Ltl_StructCheckLtlSpec_set_negate_formula(Ltl_StructCheckLtlSpec_ptr self,
                                                      boolean negate_formula);

void Ltl_StructCheckLtlSpec_set_do_rewriting(Ltl_StructCheckLtlSpec_ptr self,
                                                   boolean do_rewriting);

bdd_ptr Ltl_StructCheckLtlSpec_get_s0(Ltl_StructCheckLtlSpec_ptr self);

bdd_ptr Ltl_StructCheckLtlSpec_get_clean_s0(Ltl_StructCheckLtlSpec_ptr self);

void Ltl_StructCheckLtlSpec_build(Ltl_StructCheckLtlSpec_ptr self);

void Ltl_StructCheckLtlSpec_check(Ltl_StructCheckLtlSpec_ptr self);

void Ltl_StructCheckLtlSpec_print_result(Ltl_StructCheckLtlSpec_ptr self);

Trace_ptr
Ltl_StructCheckLtlSpec_build_counter_example(Ltl_StructCheckLtlSpec_ptr self,
                                             NodeList_ptr symbols);

void
Ltl_StructCheckLtlSpec_explain(Ltl_StructCheckLtlSpec_ptr self,
                               NodeList_ptr symbols);

#endif /*  __NUSMV_CORE_LTL_LTL_H__ */

---