NuSMV/code/nusmv/core/fsm/bdd/BddFsm.h

Go to the documentation of this file.

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

  This file is part of the ``fsm.bdd'' package of NuSMV version 2.
  Copyright (C) 2003 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_FSM_BDD_BDD_FSM_H__
#define __NUSMV_CORE_FSM_BDD_BDD_FSM_H__

#include "nusmv/core/fsm/bdd/bdd.h"
#include "nusmv/core/fsm/bdd/FairnessList.h"

#include "nusmv/core/dd/dd.h"
#include "nusmv/core/trans/bdd/BddTrans.h"
#include "nusmv/core/enc/bdd/BddEnc.h" /* Encoding */
#include "nusmv/core/fsm/sexp/sexp.h" /* VarSet_ptr */

typedef struct BddFsm_TAG*  BddFsm_ptr;

#define BDD_FSM(x) \
         ((BddFsm_ptr) x)

#define BDD_FSM_CHECK_INSTANCE(x) \
         (nusmv_assert( BDD_FSM(x) != BDD_FSM(NULL) ))


enum Bdd_Fsm_dir_TAG {BDD_FSM_DIR_BWD, BDD_FSM_DIR_FWD};
typedef enum Bdd_Fsm_dir_TAG BddFsm_dir;

enum BddFsmTransPrinterFormat {
  BDD_FSM_TRANS_PRINTER_SILENT,  /* use to avoid printing */
  BDD_FSM_TRANS_PRINTER_SMV,
  BDD_FSM_TRANS_PRINTER_CSV,
  BDD_FSM_TRANS_PRINTER_DOT,
  BDD_FSM_TRANS_PRINTER_INVALID = -1,
};


/* ---------------------------------------------------------------------- */
/* public interface                                                       */
/* ---------------------------------------------------------------------- */

BddFsm_ptr
BddFsm_create(BddEnc_ptr encoding, BddStates init,
              BddInvarStates invar_states, BddInvarInputs invar_inputs,
              BddTrans_ptr trans,
              JusticeList_ptr justice, CompassionList_ptr compassion);

void BddFsm_destroy(BddFsm_ptr self);

BddFsm_ptr BddFsm_copy(const BddFsm_ptr self);

void BddFsm_copy_cache(BddFsm_ptr self, const BddFsm_ptr other,
                              boolean keep_family);

JusticeList_ptr BddFsm_get_justice(const BddFsm_ptr self);

CompassionList_ptr BddFsm_get_compassion(const BddFsm_ptr self);

BddStates BddFsm_get_init(const BddFsm_ptr self);

BddEnc_ptr BddFsm_get_bdd_encoding(const BddFsm_ptr self);

BddInvarStates
BddFsm_get_state_constraints(const BddFsm_ptr self);

BddInvarInputs
BddFsm_get_input_constraints(const BddFsm_ptr self);

BddTrans_ptr BddFsm_get_trans(const BddFsm_ptr self);

BddStates BddFsm_get_fair_states(BddFsm_ptr self);

BddStatesInputs BddFsm_get_fair_states_inputs(BddFsm_ptr self);

BddStates BddFsm_get_revfair_states(BddFsm_ptr self);

BddStatesInputs BddFsm_get_revfair_states_inputs(BddFsm_ptr self);

bdd_ptr BddFsm_get_monolithic_trans_bdd(BddFsm_ptr self);

boolean BddFsm_reachable_states_computed(BddFsm_ptr self);

BddStates BddFsm_get_reachable_states(BddFsm_ptr self);

void
BddFsm_copy_reachable_states(BddFsm_ptr self, BddFsm_ptr other,
                             boolean keep_family,
                             boolean force_calculation);

BddStates
BddFsm_get_reachable_states_at_distance(BddFsm_ptr self,
                                        int distance);

int
BddFsm_get_distance_of_states(BddFsm_ptr self,
                              BddStates states);

int
BddFsm_get_minimum_distance_of_states(BddFsm_ptr self,
                                      BddStates states);

int BddFsm_get_diameter(BddFsm_ptr self);

BddStates
BddFsm_get_not_successor_states(BddFsm_ptr self);

BddStates BddFsm_get_deadlock_states(BddFsm_ptr self);

boolean BddFsm_is_total(BddFsm_ptr self);

boolean BddFsm_is_deadlock_free(BddFsm_ptr self);

BddStates
BddFsm_get_forward_image(const BddFsm_ptr self, BddStates states);

BddStates
BddFsm_get_constrained_forward_image(const BddFsm_ptr self,
                                     BddStates states,
                                     BddStatesInputsNexts constraints);

BddStates BddFsm_get_sins_constrained_forward_image(
    const BddFsm_ptr self,
    BddStates states,
    BddStatesInputsNexts constraints);

BddStatesInputs
BddFsm_get_forward_image_states_inputs(const BddFsm_ptr self,
                                       BddStatesInputs si);

BddStatesInputs
BddFsm_get_constrained_forward_image_states_inputs(const BddFsm_ptr self,
BddStatesInputs si,
BddStatesInputsNexts constraints);

BddStates
BddFsm_get_backward_image(const BddFsm_ptr self, BddStates states);

BddStates
BddFsm_get_constrained_backward_image(const BddFsm_ptr self,
BddStates states,
BddStatesInputsNexts constraints);

BddStatesInputs
BddFsm_get_weak_backward_image(const BddFsm_ptr self,
                               BddStates states);

BddStatesInputs
BddFsm_get_k_backward_image(const BddFsm_ptr self,
                            BddStates states,
                            int k);

BddStatesInputs
BddFsm_get_strong_backward_image(const BddFsm_ptr self,
                                 BddStates states);

void BddFsm_print_info(const BddFsm_ptr self, OStream_ptr file);

void
BddFsm_print_reachable_states_info(const BddFsm_ptr self,
                                   const boolean print_states,
                                   const boolean print_defines,
                                   const boolean print_formula,
                                   OStream_ptr file);

void
BddFsm_print_fair_states_info(const BddFsm_ptr self,
                              const boolean verbose,
                              OStream_ptr file);

void BddFsm_print_fair_transitions_info(
    const BddFsm_ptr self,
    const enum BddFsmTransPrinterFormat format,
    OStream_ptr file);

void BddFsm_print_fair_state_input_pairs_info(const BddFsm_ptr self,
                                              const boolean print_transitions,
                                              OStream_ptr file);

void BddFsm_check_machine(const BddFsm_ptr self);

void
BddFsm_apply_synchronous_product_custom_varsets(BddFsm_ptr self,
                                                const BddFsm_ptr other,
                                                bdd_ptr state_vars_cube,
                                                bdd_ptr input_vars_cube,
                                                bdd_ptr next_vars_cube);

void
BddFsm_apply_synchronous_product(BddFsm_ptr self,
                                 const BddFsm_ptr other);

boolean BddFsm_is_fair_states(const BddFsm_ptr self,
                                     BddStates states);

BddInputs
BddFsm_states_to_states_get_inputs(const BddFsm_ptr self,
                                   BddStates cur_states,
                                   BddStates next_states);

BddStatesInputs
BddFsm_get_states_inputs_constraints(const BddFsm_ptr self,
                                     BddFsm_dir dir);

BddStates BddFsm_states_inputs_to_states(const BddFsm_ptr self,
                                         BddStatesInputs si);

BddStates BddFsm_states_inputs_to_inputs(const BddFsm_ptr self,
                                                BddStatesInputs si);

boolean BddFsm_get_cached_reachable_states(const BddFsm_ptr self,
                                                  BddStates** layers,
                                                  int* size);

void BddFsm_update_cached_reachable_states(const BddFsm_ptr self,
                                                  node_ptr layers,
                                                  int size,
                                                  boolean completed);

void BddFsm_set_reachable_states(const BddFsm_ptr self,
                                        BddStates reachable);

boolean BddFsm_has_cached_reachable_states(const BddFsm_ptr self);

boolean
BddFsm_expand_cached_reachable_states(BddFsm_ptr self,
                                      int k,
                                      int max_seconds);

/* Features directly called by commands */

boolean
BddFsm_compute_reachable(BddFsm_ptr self, int k, int t, int* diameter);


double
BddFsm_count_transitions(const BddFsm_ptr self,
                         BddStatesInputs bdd);

int
BddFsm_dump_fsm(BddFsm_ptr self,
                const NuSMVEnv_ptr env, node_ptr node_expr,
                char* str_constr,
                boolean init,
                boolean invar, boolean trans, boolean fair,
                boolean reachable,
                FILE* outfile);

int
BddFsm_print_reachable_states(BddFsm_ptr self,
                              NuSMVEnv_ptr env, OStream_ptr stream,
                              boolean verbose, boolean print_defines,
                              boolean formula);

int BddFsm_print_fair_states(BddFsm_ptr self,
                             const NuSMVEnv_ptr env,
                             const OStream_ptr outstream,
                             const boolean verbose);

int BddFsm_print_fair_transitions(BddFsm_ptr self,
                                  const NuSMVEnv_ptr env,
                                  const enum BddFsmTransPrinterFormat format,
                                  const OStream_ptr outstream);

int BddFsm_print_fair_state_input_pairs(BddFsm_ptr self,
                                        const NuSMVEnv_ptr env,
                                        const OStream_ptr outstream,
                                        const boolean verbose);
enum BddFsmTransPrinterFormat
BddFsm_trans_printer_format_from_string(const char* format_str);

const char*
BddFsm_trans_printer_format_to_string(enum BddFsmTransPrinterFormat format);

enum BddFsmTransPrinterFormat*
BddFsm_trans_printer_get_avail_formats(size_t* num);


#endif /* __NUSMV_CORE_FSM_BDD_BDD_FSM_H__ */

---