NuSMV/code/nusmv/core/parser/psl/pslInt.h

Go to the documentation of this file.

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


  This file is part of the ``parser.psl'' 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_PARSER_PSL_PSL_INT_H__
#define __NUSMV_CORE_PARSER_PSL_PSL_INT_H__

#include "nusmv/core/parser/psl/pslNode.h"
#include "nusmv/core/parser/parserInt.h" /* for YY_BUFFER_STATE */
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/error.h"

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

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

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

#define PSL_EMPTYSTAR PSL_NULL


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

int psl_yylex(void);

int psl_yyparse(void);

void psl_yyrestart(FILE* input_file);

YY_BUFFER_STATE psl_yy_scan_buffer(char *base, size_t size);

YY_BUFFER_STATE psl_yy_create_buffer(FILE *file, int size);

void psl_yy_switch_to_buffer(YY_BUFFER_STATE new_buffer);

void psl_yy_delete_buffer(YY_BUFFER_STATE b);

YY_BUFFER_STATE psl_yy_scan_string(const char *yy_str);

PslNode_ptr
psl_new_node(NodeMgr_ptr nodemgr,
             PslOp _type, PslNode_ptr left, PslNode_ptr right);

void psl_node_set_left(PslNode_ptr n, PslNode_ptr l);

void psl_node_set_right(PslNode_ptr n, PslNode_ptr r);

PslNode_ptr psl_node_make_number(NodeMgr_ptr nodemgr,
                                        int value);

PslOp psl_conv_op(const NuSMVEnv_ptr env,
                         PslOpConvType type, PslOp op);

boolean psl_node_is_sere(PslNode_ptr expr);

boolean
psl_node_is_handled_star(const NuSMVEnv_ptr env,
                         PslNode_ptr expr, boolean toplevel);

PslNode_ptr
psl_node_sere_star_get_count(const PslNode_ptr e);

boolean psl_node_sere_is_propositional(PslNode_ptr e);

boolean psl_node_sere_is_repeated(PslNode_ptr e);

boolean psl_node_sere_is_star(PslNode_ptr e);

boolean psl_node_sere_is_standalone_star(PslNode_ptr e);

boolean psl_node_sere_is_plus(PslNode_ptr e);

boolean psl_node_sere_is_standalone_plus(PslNode_ptr e);

boolean psl_node_sere_is_star_count(PslNode_ptr e);

PslNode_ptr psl_node_sere_repeated_get_expr(PslNode_ptr e);

boolean psl_node_sere_is_stareq(PslNode_ptr e);

boolean psl_node_sere_is_starminusgt(PslNode_ptr e);

PslNode_ptr
psl_node_make_sere_compound(NodeMgr_ptr nodemgr,
                            PslNode_ptr seq1,
                            PslOp op, PslNode_ptr seq2);

boolean psl_node_is_sere_compound_binary(PslNode_ptr e);

boolean psl_node_is_suffix_implication(PslNode_ptr expr);

boolean psl_node_is_suffix_implication_weak(PslNode_ptr expr);

boolean psl_node_is_suffix_implication_strong(PslNode_ptr expr);

PslNode_ptr
psl_node_suffix_implication_get_premise(PslNode_ptr e);

PslNode_ptr
psl_node_suffix_implication_get_consequence(PslNode_ptr e);

boolean psl_node_sere_is_concat_holes_free(PslNode_ptr e);

boolean psl_node_sere_is_concat_fusion(PslNode_ptr e);

boolean psl_node_sere_is_concat_fusion_holes_free(PslNode_ptr e);

PslNode_ptr psl_node_prune(NodeMgr_ptr nodemgr,
                                  PslNode_ptr tree, PslNode_ptr branch);

boolean psl_node_is_propstar(PslNode_ptr e);

boolean psl_node_sere_is_2ampersand(PslNode_ptr e);

PslNode_ptr
psl_node_make_cons(NodeMgr_ptr nodemgr,
                   PslNode_ptr elem, PslNode_ptr next);

PslNode_ptr
psl_node_make_cons_new(NodeMgr_ptr nodemgr,
                       PslNode_ptr elem, PslNode_ptr next);

boolean psl_node_is_cons(PslNode_ptr e);

PslNode_ptr psl_node_cons_reverse(PslNode_ptr e);

boolean psl_node_is_ite(PslNode_ptr _ite);

PslNode_ptr psl_node_get_ite_cond(PslNode_ptr _ite);

PslNode_ptr psl_node_get_ite_then(PslNode_ptr _ite);

PslNode_ptr psl_node_get_ite_else(PslNode_ptr _ite);

boolean psl_node_is_case(PslNode_ptr _case);

PslNode_ptr psl_node_get_case_cond(PslNode_ptr _case);

PslNode_ptr psl_node_get_case_then(PslNode_ptr _case);

PslNode_ptr psl_node_get_case_next(PslNode_ptr _case);

boolean
psl_node_is_num_equal(PslNode_ptr _id1, PslNode_ptr _id2);

boolean psl_node_is_boolean_type(PslNode_ptr expr);

boolean psl_node_is_id(PslNode_ptr expr);

boolean psl_node_is_id_equal(PslNode_ptr _id1, PslNode_ptr _id2);

boolean psl_node_is_leaf(PslNode_ptr expr);

boolean psl_node_is_repl_prop(PslNode_ptr _prop);

PslNode_ptr psl_node_repl_prop_get_replicator(PslNode_ptr _prop);

PslNode_ptr psl_node_repl_prop_get_property(PslNode_ptr _prop);

boolean psl_node_is_replicator(PslNode_ptr _repl);

PslNode_ptr
psl_node_make_extended_next(NodeMgr_ptr nodemgr,
                            PslOp op, PslNode_ptr expr,
                            PslNode_ptr when,
                            PslNode_ptr condition);

boolean psl_node_is_extended_next(PslNode_ptr e);

void psl_yyerror(char* s, ...);

#endif /* __NUSMV_CORE_PARSER_PSL_PSL_INT_H__ */

---