00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00038 #ifndef __NUSMV_CORE_PARSER_PSL_PSL_INT_H__
00039 #define __NUSMV_CORE_PARSER_PSL_PSL_INT_H__
00040
00041 #include "nusmv/core/parser/psl/pslNode.h"
00042 #include "nusmv/core/parser/parserInt.h"
00043 #include "nusmv/core/utils/utils.h"
00044 #include "nusmv/core/utils/error.h"
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057
00064 #define PSL_EMPTYSTAR PSL_NULL
00065
00066
00067
00068
00069
00070
00076 int psl_yylex(void);
00077
00083 int psl_yyparse(void);
00084
00090 void psl_yyrestart(FILE* input_file);
00091
00097 YY_BUFFER_STATE psl_yy_scan_buffer(char *base, size_t size);
00098
00104 YY_BUFFER_STATE psl_yy_create_buffer(FILE *file, int size);
00105
00111 void psl_yy_switch_to_buffer(YY_BUFFER_STATE new_buffer);
00112
00118 void psl_yy_delete_buffer(YY_BUFFER_STATE b);
00119
00125 YY_BUFFER_STATE psl_yy_scan_string(const char *yy_str);
00126
00140 PslNode_ptr
00141 psl_new_node(NodeMgr_ptr nodemgr,
00142 PslOp _type, PslNode_ptr left, PslNode_ptr right);
00143
00151 void psl_node_set_left(PslNode_ptr n, PslNode_ptr l);
00152
00160 void psl_node_set_right(PslNode_ptr n, PslNode_ptr r);
00161
00169 PslNode_ptr psl_node_make_number(NodeMgr_ptr nodemgr,
00170 int value);
00171
00177 PslOp psl_conv_op(const NuSMVEnv_ptr env,
00178 PslOpConvType type, PslOp op);
00179
00188 boolean psl_node_is_sere(PslNode_ptr expr);
00189
00198 boolean
00199 psl_node_is_handled_star(const NuSMVEnv_ptr env,
00200 PslNode_ptr expr, boolean toplevel);
00201
00210 PslNode_ptr
00211 psl_node_sere_star_get_count(const PslNode_ptr e);
00212
00221 boolean psl_node_sere_is_propositional(PslNode_ptr e);
00222
00230 boolean psl_node_sere_is_repeated(PslNode_ptr e);
00231
00239 boolean psl_node_sere_is_star(PslNode_ptr e);
00240
00249 boolean psl_node_sere_is_standalone_star(PslNode_ptr e);
00250
00258 boolean psl_node_sere_is_plus(PslNode_ptr e);
00259
00268 boolean psl_node_sere_is_standalone_plus(PslNode_ptr e);
00269
00278 boolean psl_node_sere_is_star_count(PslNode_ptr e);
00279
00288 PslNode_ptr psl_node_sere_repeated_get_expr(PslNode_ptr e);
00289
00297 boolean psl_node_sere_is_stareq(PslNode_ptr e);
00298
00306 boolean psl_node_sere_is_starminusgt(PslNode_ptr e);
00307
00316 PslNode_ptr
00317 psl_node_make_sere_compound(NodeMgr_ptr nodemgr,
00318 PslNode_ptr seq1,
00319 PslOp op, PslNode_ptr seq2);
00320
00328 boolean psl_node_is_sere_compound_binary(PslNode_ptr e);
00329
00338 boolean psl_node_is_suffix_implication(PslNode_ptr expr);
00339
00348 boolean psl_node_is_suffix_implication_weak(PslNode_ptr expr);
00349
00358 boolean psl_node_is_suffix_implication_strong(PslNode_ptr expr);
00359
00367 PslNode_ptr
00368 psl_node_suffix_implication_get_premise(PslNode_ptr e);
00369
00377 PslNode_ptr
00378 psl_node_suffix_implication_get_consequence(PslNode_ptr e);
00379
00388 boolean psl_node_sere_is_concat_holes_free(PslNode_ptr e);
00389
00398 boolean psl_node_sere_is_concat_fusion(PslNode_ptr e);
00399
00417 boolean psl_node_sere_is_concat_fusion_holes_free(PslNode_ptr e);
00418
00426 PslNode_ptr psl_node_prune(NodeMgr_ptr nodemgr,
00427 PslNode_ptr tree, PslNode_ptr branch);
00428
00437 boolean psl_node_is_propstar(PslNode_ptr e);
00438
00447 boolean psl_node_sere_is_2ampersand(PslNode_ptr e);
00448
00457 PslNode_ptr
00458 psl_node_make_cons(NodeMgr_ptr nodemgr,
00459 PslNode_ptr elem, PslNode_ptr next);
00460
00469 PslNode_ptr
00470 psl_node_make_cons_new(NodeMgr_ptr nodemgr,
00471 PslNode_ptr elem, PslNode_ptr next);
00472
00480 boolean psl_node_is_cons(PslNode_ptr e);
00481
00490 PslNode_ptr psl_node_cons_reverse(PslNode_ptr e);
00491
00499 boolean psl_node_is_ite(PslNode_ptr _ite);
00500
00508 PslNode_ptr psl_node_get_ite_cond(PslNode_ptr _ite);
00509
00517 PslNode_ptr psl_node_get_ite_then(PslNode_ptr _ite);
00518
00526 PslNode_ptr psl_node_get_ite_else(PslNode_ptr _ite);
00527
00535 boolean psl_node_is_case(PslNode_ptr _case);
00536
00544 PslNode_ptr psl_node_get_case_cond(PslNode_ptr _case);
00545
00553 PslNode_ptr psl_node_get_case_then(PslNode_ptr _case);
00554
00562 PslNode_ptr psl_node_get_case_next(PslNode_ptr _case);
00563
00571 boolean
00572 psl_node_is_num_equal(PslNode_ptr _id1, PslNode_ptr _id2);
00573
00582 boolean psl_node_is_boolean_type(PslNode_ptr expr);
00583
00592 boolean psl_node_is_id(PslNode_ptr expr);
00593
00601 boolean psl_node_is_id_equal(PslNode_ptr _id1, PslNode_ptr _id2);
00602
00611 boolean psl_node_is_leaf(PslNode_ptr expr);
00612
00621 boolean psl_node_is_repl_prop(PslNode_ptr _prop);
00622
00633 PslNode_ptr psl_node_repl_prop_get_replicator(PslNode_ptr _prop);
00634
00645 PslNode_ptr psl_node_repl_prop_get_property(PslNode_ptr _prop);
00646
00655 boolean psl_node_is_replicator(PslNode_ptr _repl);
00656
00665 PslNode_ptr
00666 psl_node_make_extended_next(NodeMgr_ptr nodemgr,
00667 PslOp op, PslNode_ptr expr,
00668 PslNode_ptr when,
00669 PslNode_ptr condition);
00670
00679 boolean psl_node_is_extended_next(PslNode_ptr e);
00680
00686 void psl_yyerror(char* s, ...);
00687
00688 #endif