#include "nusmv/core/parser/psl/pslNode.h"#include "nusmv/core/parser/parserInt.h"#include "nusmv/core/utils/utils.h"#include "nusmv/core/utils/error.h"Go to the source code of this file.
Defines | |
| #define | PSL_EMPTYSTAR PSL_NULL |
| Psl package private interface. | |
Functions | |
| PslOp | psl_conv_op (const NuSMVEnv_ptr env, PslOpConvType type, PslOp op) |
| PslNode_ptr | psl_new_node (NodeMgr_ptr nodemgr, PslOp _type, PslNode_ptr left, PslNode_ptr right) |
| Creates a new PSL node, re-using already an existing node if there is one. | |
| PslNode_ptr | psl_node_cons_reverse (PslNode_ptr e) |
| Reverse a list. | |
| PslNode_ptr | psl_node_get_case_cond (PslNode_ptr _case) |
| Returns the condition of the given case node. | |
| PslNode_ptr | psl_node_get_case_next (PslNode_ptr _case) |
| Returns the next case node of the given case. | |
| PslNode_ptr | psl_node_get_case_then (PslNode_ptr _case) |
| Returns the 'then' branch of the given case node. | |
| PslNode_ptr | psl_node_get_ite_cond (PslNode_ptr _ite) |
| Returns the condition of the given ITE node. | |
| PslNode_ptr | psl_node_get_ite_else (PslNode_ptr _ite) |
| Returns the 'else' branch of the given ITE node. | |
| PslNode_ptr | psl_node_get_ite_then (PslNode_ptr _ite) |
| Returns the 'then' branch of the given ITE node. | |
| boolean | psl_node_is_boolean_type (PslNode_ptr expr) |
| Returns true if the given node is the PSL syntactic type 'boolean'. | |
| boolean | psl_node_is_case (PslNode_ptr _case) |
| Returns true if the given expression is a case expression. | |
| boolean | psl_node_is_cons (PslNode_ptr e) |
| Returns true if the given node is a list. | |
| boolean | psl_node_is_extended_next (PslNode_ptr e) |
| Given a psl node returns true iff the expression belongs to the next operators family. | |
| boolean | psl_node_is_handled_star (const NuSMVEnv_ptr env, PslNode_ptr expr, boolean toplevel) |
| Returns true if the given starred sere can be handled by the system. | |
| boolean | psl_node_is_id (PslNode_ptr expr) |
| Returns true if the given node is an identifier. | |
| boolean | psl_node_is_id_equal (PslNode_ptr _id1, PslNode_ptr _id2) |
| Returns true if two ids are equal. | |
| boolean | psl_node_is_ite (PslNode_ptr _ite) |
| Returns true if the given expression is If Then Else. | |
| boolean | psl_node_is_leaf (PslNode_ptr expr) |
| Returns true if the given node is a leaf, i.e. PSL_NULL, a number, a boolean constant, or an atom. | |
| boolean | psl_node_is_num_equal (PslNode_ptr _id1, PslNode_ptr _id2) |
| Returns true if the given numbers are equal. | |
| boolean | psl_node_is_propstar (PslNode_ptr e) |
| Returns true if the given expression is a propositional starred sere. | |
| boolean | psl_node_is_repl_prop (PslNode_ptr _prop) |
| Returns true if the given expression is a replicated property. | |
| boolean | psl_node_is_replicator (PslNode_ptr _repl) |
| Returns true if the given expression represents a replicator. | |
| boolean | psl_node_is_sere (PslNode_ptr expr) |
| Returns true if the given expression is a SERE. | |
| boolean | psl_node_is_sere_compound_binary (PslNode_ptr e) |
| Returns true if the given expression is a sere compound. | |
| boolean | psl_node_is_suffix_implication (PslNode_ptr expr) |
| Returns true if the given expression is a suffix implication. | |
| boolean | psl_node_is_suffix_implication_strong (PslNode_ptr expr) |
| Returns true if the given expression is a strong suffix implication. | |
| boolean | psl_node_is_suffix_implication_weak (PslNode_ptr expr) |
| Returns true if the given expression is a weak suffix implication. | |
| PslNode_ptr | psl_node_make_cons (NodeMgr_ptr nodemgr, PslNode_ptr elem, PslNode_ptr next) |
| Maker for a list. | |
| PslNode_ptr | psl_node_make_cons_new (NodeMgr_ptr nodemgr, PslNode_ptr elem, PslNode_ptr next) |
| Maker for a list, does not use find_node. | |
| PslNode_ptr | psl_node_make_extended_next (NodeMgr_ptr nodemgr, PslOp op, PslNode_ptr expr, PslNode_ptr when, PslNode_ptr condition) |
| Maker for a NEXT* family node. | |
| PslNode_ptr | psl_node_make_number (NodeMgr_ptr nodemgr, int value) |
| Maker for a NUMBER node. | |
| PslNode_ptr | psl_node_make_sere_compound (NodeMgr_ptr nodemgr, PslNode_ptr seq1, PslOp op, PslNode_ptr seq2) |
| Maker for the sere compound. | |
| PslNode_ptr | psl_node_prune (NodeMgr_ptr nodemgr, PslNode_ptr tree, PslNode_ptr branch) |
| Prunes aways the given branch from the given tree. | |
| PslNode_ptr | psl_node_repl_prop_get_property (PslNode_ptr _prop) |
| Given a replicated property, returns the node that contains the property. | |
| PslNode_ptr | psl_node_repl_prop_get_replicator (PslNode_ptr _prop) |
| Given a replicated property, returns the node that contains the replicator. | |
| boolean | psl_node_sere_is_2ampersand (PslNode_ptr e) |
| Returns true if the given expression is a sere in the form { s2 && s1 }. | |
| boolean | psl_node_sere_is_concat_fusion (PslNode_ptr e) |
| Returns true if the given expression is a concat or fusion sere. | |
| boolean | psl_node_sere_is_concat_fusion_holes_free (PslNode_ptr e) |
| [Returns true if there are no holes in the given fusion/concat sere to be filled in.] | |
| boolean | psl_node_sere_is_concat_holes_free (PslNode_ptr e) |
| Returns true if there are no holes in the given concat sere to be filled in. | |
| boolean | psl_node_sere_is_plus (PslNode_ptr e) |
| Returns true if the given expression a plus repeated sere. | |
| boolean | psl_node_sere_is_propositional (PslNode_ptr e) |
| Returns true if the given sere contains a single propositional expression. | |
| boolean | psl_node_sere_is_repeated (PslNode_ptr e) |
| Returns true if the given expr is a repeated sere. | |
| boolean | psl_node_sere_is_standalone_plus (PslNode_ptr e) |
| Returns true if the given repeated sere is in the form <empty>\[+\]. | |
| boolean | psl_node_sere_is_standalone_star (PslNode_ptr e) |
| Returns true if the given expr is in the form <empty>\[*\], with or without a counter. | |
| boolean | psl_node_sere_is_star (PslNode_ptr e) |
| Returns true if the given expr is a starred repeated sere. | |
| boolean | psl_node_sere_is_star_count (PslNode_ptr e) |
| Returns true if the given starred repeated sere as also a counter. | |
| boolean | psl_node_sere_is_stareq (PslNode_ptr e) |
| Returns true if the given expr is a starred-eq repeated sere. | |
| boolean | psl_node_sere_is_starminusgt (PslNode_ptr e) |
| Returns true if the given expr is a starred-minusgt repeated sere. | |
| PslNode_ptr | psl_node_sere_repeated_get_expr (PslNode_ptr e) |
| Returns the repeated expression associated to the repeated sere. | |
| PslNode_ptr | psl_node_sere_star_get_count (const PslNode_ptr e) |
| Returns the count of a starred sere. | |
| void | psl_node_set_left (PslNode_ptr n, PslNode_ptr l) |
| Sets the given expression's left branch. | |
| void | psl_node_set_right (PslNode_ptr n, PslNode_ptr r) |
| Sets the given expression's right branch. | |
| PslNode_ptr | psl_node_suffix_implication_get_consequence (PslNode_ptr e) |
| Returns the consequence of the given suffix implication. | |
| PslNode_ptr | psl_node_suffix_implication_get_premise (PslNode_ptr e) |
| Returns the premise of the given suffix implication. | |
| YY_BUFFER_STATE | psl_yy_create_buffer (FILE *file, int size) |
| void | psl_yy_delete_buffer (YY_BUFFER_STATE b) |
| YY_BUFFER_STATE | psl_yy_scan_buffer (char *base, size_t size) |
| YY_BUFFER_STATE | psl_yy_scan_string (const char *yy_str) |
| void | psl_yy_switch_to_buffer (YY_BUFFER_STATE new_buffer) |
| void | psl_yyerror (char *s,...) |
| int | psl_yylex (void) |
| int | psl_yyparse (void) |
| void | psl_yyrestart (FILE *input_file) |
| #define PSL_EMPTYSTAR PSL_NULL |
Psl package private interface.
This integer value represents the count of a count-free starred repeated sere. For example {a}\[*\] that has no count.
| PslOp psl_conv_op | ( | const NuSMVEnv_ptr | env, | |
| PslOpConvType | type, | |||
| PslOp | op | |||
| ) |
| PslNode_ptr psl_new_node | ( | NodeMgr_ptr | nodemgr, | |
| PslOp | _type, | |||
| PslNode_ptr | left, | |||
| PslNode_ptr | right | |||
| ) |
Creates a new PSL node, re-using already an existing node if there is one.
WARNING: If this function is being called to build a branch of the parse-tree from a branch coming from the parsing phase (i.e. it is a token, and not a symbol), the token *must* be converted to a PSL node by calling psl_conv_op(TOK2PSL, op)
None
| PslNode_ptr psl_node_cons_reverse | ( | PslNode_ptr | e | ) |
Reverse a list.
Returns a new sequence containing the same elements as 'e' but in reverse order
None
| PslNode_ptr psl_node_get_case_cond | ( | PslNode_ptr | _case | ) |
Returns the condition of the given case node.
None
| PslNode_ptr psl_node_get_case_next | ( | PslNode_ptr | _case | ) |
Returns the next case node of the given case.
None
| PslNode_ptr psl_node_get_case_then | ( | PslNode_ptr | _case | ) |
Returns the 'then' branch of the given case node.
None
| PslNode_ptr psl_node_get_ite_cond | ( | PslNode_ptr | _ite | ) |
Returns the condition of the given ITE node.
None
| PslNode_ptr psl_node_get_ite_else | ( | PslNode_ptr | _ite | ) |
Returns the 'else' branch of the given ITE node.
None
| PslNode_ptr psl_node_get_ite_then | ( | PslNode_ptr | _ite | ) |
Returns the 'then' branch of the given ITE node.
None
| boolean psl_node_is_boolean_type | ( | PslNode_ptr | expr | ) |
Returns true if the given node is the PSL syntactic type 'boolean'.
None
| boolean psl_node_is_case | ( | PslNode_ptr | _case | ) |
Returns true if the given expression is a case expression.
None
| boolean psl_node_is_cons | ( | PslNode_ptr | e | ) |
Returns true if the given node is a list.
None
| boolean psl_node_is_extended_next | ( | PslNode_ptr | e | ) |
Given a psl node returns true iff the expression belongs to the next operators family.
None
| boolean psl_node_is_handled_star | ( | const NuSMVEnv_ptr | env, | |
| PslNode_ptr | expr, | |||
| boolean | toplevel | |||
| ) |
Returns true if the given starred sere can be handled by the system.
precond: expr must be a repeated sere
None
| boolean psl_node_is_id | ( | PslNode_ptr | expr | ) |
Returns true if the given node is an identifier.
The top level operator of an ID can be DOT, ATOM or ARRAY
None
| boolean psl_node_is_id_equal | ( | PslNode_ptr | _id1, | |
| PslNode_ptr | _id2 | |||
| ) |
Returns true if two ids are equal.
None
| boolean psl_node_is_ite | ( | PslNode_ptr | _ite | ) |
Returns true if the given expression is If Then Else.
None
| boolean psl_node_is_leaf | ( | PslNode_ptr | expr | ) |
Returns true if the given node is a leaf, i.e. PSL_NULL, a number, a boolean constant, or an atom.
None
| boolean psl_node_is_num_equal | ( | PslNode_ptr | _id1, | |
| PslNode_ptr | _id2 | |||
| ) |
Returns true if the given numbers are equal.
None
| boolean psl_node_is_propstar | ( | PslNode_ptr | e | ) |
Returns true if the given expression is a propositional starred sere.
None
| boolean psl_node_is_repl_prop | ( | PslNode_ptr | _prop | ) |
Returns true if the given expression is a replicated property.
None
| boolean psl_node_is_replicator | ( | PslNode_ptr | _repl | ) |
Returns true if the given expression represents a replicator.
None
| boolean psl_node_is_sere | ( | PslNode_ptr | expr | ) |
Returns true if the given expression is a SERE.
A SERE can be in the form {a}, {a};{b}, {a}:{b}, {a}\[*\], {a}\[+\], {a}|{b}, {a}&{a}, {a}&&{b}
None
| boolean psl_node_is_sere_compound_binary | ( | PslNode_ptr | e | ) |
Returns true if the given expression is a sere compound.
None
| boolean psl_node_is_suffix_implication | ( | PslNode_ptr | expr | ) |
Returns true if the given expression is a suffix implication.
None
| boolean psl_node_is_suffix_implication_strong | ( | PslNode_ptr | expr | ) |
Returns true if the given expression is a strong suffix implication.
None
| boolean psl_node_is_suffix_implication_weak | ( | PslNode_ptr | expr | ) |
Returns true if the given expression is a weak suffix implication.
None
| PslNode_ptr psl_node_make_cons | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | elem, | |||
| PslNode_ptr | next | |||
| ) |
Maker for a list.
This gets the element to insert at top level, and the list for next
None
| PslNode_ptr psl_node_make_cons_new | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | elem, | |||
| PslNode_ptr | next | |||
| ) |
Maker for a list, does not use find_node.
This gets the element to insert at top level, and the list for next
None
| PslNode_ptr psl_node_make_extended_next | ( | NodeMgr_ptr | nodemgr, | |
| PslOp | op, | |||
| PslNode_ptr | expr, | |||
| PslNode_ptr | when, | |||
| PslNode_ptr | condition | |||
| ) |
Maker for a NEXT* family node.
Warning: the operator must be a symbol, not a token. This means that psl_conv_op must be called to convert tokens before.
None
| PslNode_ptr psl_node_make_number | ( | NodeMgr_ptr | nodemgr, | |
| int | value | |||
| ) |
Maker for a NUMBER node.
None
| PslNode_ptr psl_node_make_sere_compound | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | seq1, | |||
| PslOp | op, | |||
| PslNode_ptr | seq2 | |||
| ) |
Maker for the sere compound.
Warning: the operator must be a symbol, not a token. This means that psl_conv_op must be called to convert tokens before.
None
| PslNode_ptr psl_node_prune | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | tree, | |||
| PslNode_ptr | branch | |||
| ) |
Prunes aways the given branch from the given tree.
None
| PslNode_ptr psl_node_repl_prop_get_property | ( | PslNode_ptr | _prop | ) |
Given a replicated property, returns the node that contains the property.
None
| PslNode_ptr psl_node_repl_prop_get_replicator | ( | PslNode_ptr | _prop | ) |
Given a replicated property, returns the node that contains the replicator.
None
| boolean psl_node_sere_is_2ampersand | ( | PslNode_ptr | e | ) |
Returns true if the given expression is a sere in the form { s2 && s1 }.
None
| boolean psl_node_sere_is_concat_fusion | ( | PslNode_ptr | e | ) |
Returns true if the given expression is a concat or fusion sere.
None
| boolean psl_node_sere_is_concat_fusion_holes_free | ( | PslNode_ptr | e | ) |
[Returns true if there are no holes in the given fusion/concat sere to be filled in.]
Description []
SideEffects [None]
SeeAlso []
[EXTRACT_DOC_NOTE: * /]
None
| boolean psl_node_sere_is_concat_holes_free | ( | PslNode_ptr | e | ) |
Returns true if there are no holes in the given concat sere to be filled in.
None
| boolean psl_node_sere_is_plus | ( | PslNode_ptr | e | ) |
Returns true if the given expression a plus repeated sere.
None
| boolean psl_node_sere_is_propositional | ( | PslNode_ptr | e | ) |
Returns true if the given sere contains a single propositional expression.
None
| boolean psl_node_sere_is_repeated | ( | PslNode_ptr | e | ) |
Returns true if the given expr is a repeated sere.
None
| boolean psl_node_sere_is_standalone_plus | ( | PslNode_ptr | e | ) |
Returns true if the given repeated sere is in the form <empty>\[+\].
None
| boolean psl_node_sere_is_standalone_star | ( | PslNode_ptr | e | ) |
Returns true if the given expr is in the form <empty>\[*\], with or without a counter.
None
| boolean psl_node_sere_is_star | ( | PslNode_ptr | e | ) |
Returns true if the given expr is a starred repeated sere.
None
| boolean psl_node_sere_is_star_count | ( | PslNode_ptr | e | ) |
Returns true if the given starred repeated sere as also a counter.
None
| boolean psl_node_sere_is_stareq | ( | PslNode_ptr | e | ) |
Returns true if the given expr is a starred-eq repeated sere.
None
| boolean psl_node_sere_is_starminusgt | ( | PslNode_ptr | e | ) |
Returns true if the given expr is a starred-minusgt repeated sere.
None
| PslNode_ptr psl_node_sere_repeated_get_expr | ( | PslNode_ptr | e | ) |
Returns the repeated expression associated to the repeated sere.
None
| PslNode_ptr psl_node_sere_star_get_count | ( | const PslNode_ptr | e | ) |
Returns the count of a starred sere.
Returned value can be either a positive integer value, or the constant PSL_EMPTYSTAR to represent an empty starred sere.
None
| void psl_node_set_left | ( | PslNode_ptr | n, | |
| PslNode_ptr | l | |||
| ) |
Sets the given expression's left branch.
None
| void psl_node_set_right | ( | PslNode_ptr | n, | |
| PslNode_ptr | r | |||
| ) |
Sets the given expression's right branch.
None
| PslNode_ptr psl_node_suffix_implication_get_consequence | ( | PslNode_ptr | e | ) |
Returns the consequence of the given suffix implication.
None
| PslNode_ptr psl_node_suffix_implication_get_premise | ( | PslNode_ptr | e | ) |
Returns the premise of the given suffix implication.
None
| YY_BUFFER_STATE psl_yy_create_buffer | ( | FILE * | file, | |
| int | size | |||
| ) |
| YY_BUFFER_STATE psl_yy_scan_buffer | ( | char * | base, | |
| size_t | size | |||
| ) |
| YY_BUFFER_STATE psl_yy_scan_string | ( | const char * | yy_str | ) |
| void psl_yy_switch_to_buffer | ( | YY_BUFFER_STATE | new_buffer | ) |
1.6.1