#include "nusmv/core/node/node.h"#include "nusmv/core/utils/utils.h"#include "nusmv/core/utils/error.h"#include "nusmv/core/utils/ErrorMgr.h"Go to the source code of this file.
| #define PSL_NULL ((PslNode_ptr) NULL) |
This value represents a null PslNode.
| #define PSLNODE_FROM_INT | ( | x | ) | ((PslNode_ptr) (nusmv_ptrint) x) |
Casts the given int to a PslNode_ptr.
| #define PSLNODE_TO_INT | ( | x | ) | ((int) (nusmv_ptrint) x) |
Casts the given node to an int.
| typedef node_ptr PslNode_ptr |
| enum PslOpConvType |
| PslNode_ptr psl_new_node | ( | NodeMgr_ptr | nodemgr, | |
| PslOp | op, | |||
| PslNode_ptr | left, | |||
| PslNode_ptr | right | |||
| ) |
| PslNode_ptr psl_node_cons_get_element | ( | PslNode_ptr | e | ) |
Returns the currently pointed element of a list.
None
| PslNode_ptr psl_node_cons_get_next | ( | PslNode_ptr | e | ) |
Returns the next element of a list.
None
| PslNode_ptr psl_node_cons_reverse | ( | PslNode_ptr | e | ) |
| PslNode_ptr psl_node_context_to_main_context | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | context | |||
| ) |
Contestualizes a context node into the 'main' context.
This function is used to build the internal structure of the context (e.g. module instance name) from the parse tree. The function is needed since with the grammar it is not possible/simple to build directly the desired structure.
None
| PslNode_ptr psl_node_extended_next_get_condition | ( | PslNode_ptr | next | ) |
Returns the boolean condition of a next expression node.
None
| PslNode_ptr psl_node_extended_next_get_expr | ( | PslNode_ptr | next | ) |
Returns the FL expression of a next expression node.
None
| PslNode_ptr psl_node_extended_next_get_when | ( | PslNode_ptr | next | ) |
Returns the when component of a next expression node.
None
| PslNode_ptr psl_node_get_case_cond | ( | PslNode_ptr | _case | ) |
| PslNode_ptr psl_node_get_case_next | ( | PslNode_ptr | _case | ) |
| PslNode_ptr psl_node_get_case_then | ( | PslNode_ptr | _case | ) |
| PslNode_ptr psl_node_get_ite_cond | ( | PslNode_ptr | _ite | ) |
| PslNode_ptr psl_node_get_ite_else | ( | PslNode_ptr | _ite | ) |
| PslNode_ptr psl_node_get_ite_then | ( | PslNode_ptr | _ite | ) |
| PslNode_ptr psl_node_get_left | ( | PslNode_ptr | n | ) |
Returns the given expression's left branch.
None
| PslOp psl_node_get_op | ( | PslNode_ptr | n | ) |
Returns the given expression's top level operator.
None
| PslNode_ptr psl_node_get_replicator_id | ( | PslNode_ptr | _repl | ) |
Given a replicator, returns the its ID.
None
| PslOp psl_node_get_replicator_join_op | ( | PslNode_ptr | _repl | ) |
Given a replicator, returns the operator joining each replicated expression.
None
| PslNode_ptr psl_node_get_replicator_normalized_value_set | ( | const NuSMVEnv_ptr | env, | |
| PslNode_ptr | rep | |||
| ) |
Given a replicator, returns its values set as a list of the enumerated values.
required
| PslNode_ptr psl_node_get_replicator_range | ( | PslNode_ptr | _repl | ) |
Given a replicator, returns its range.
None
| PslNode_ptr psl_node_get_replicator_value_set | ( | PslNode_ptr | _repl | ) |
Given a replicator, returns the its values set.
None
| PslNode_ptr psl_node_get_right | ( | PslNode_ptr | n | ) |
Returns the given expression's right branch.
None
| boolean psl_node_is_boolean_type | ( | PslNode_ptr | expr | ) |
| boolean psl_node_is_case | ( | PslNode_ptr | _case | ) |
| boolean psl_node_is_cons | ( | PslNode_ptr | e | ) |
| boolean psl_node_is_extended_next | ( | PslNode_ptr | e | ) |
| boolean psl_node_is_false | ( | PslNode_ptr | e | ) |
| boolean psl_node_is_handled_star | ( | const NuSMVEnv_ptr | env, | |
| PslNode_ptr | expr, | |||
| boolean | toplevel | |||
| ) |
| boolean psl_node_is_id | ( | PslNode_ptr | expr | ) |
| boolean psl_node_is_id_equal | ( | PslNode_ptr | _id1, | |
| PslNode_ptr | _id2 | |||
| ) |
| boolean psl_node_is_infinite | ( | PslNode_ptr | expr | ) |
Returns true if the given node is the PSL syntactic value 'inf'.
None
| boolean psl_node_is_ite | ( | PslNode_ptr | _ite | ) |
| boolean psl_node_is_leaf | ( | PslNode_ptr | expr | ) |
| boolean psl_node_is_num_equal | ( | PslNode_ptr | _id1, | |
| PslNode_ptr | _id2 | |||
| ) |
| boolean psl_node_is_number | ( | PslNode_ptr | e | ) |
Returns true if the given expression is an integer number.
None
| boolean psl_node_is_propstar | ( | PslNode_ptr | e | ) |
| boolean psl_node_is_range | ( | PslNode_ptr | expr | ) |
Returns true if the given node is a range.
None
| boolean psl_node_is_repl_prop | ( | PslNode_ptr | _prop | ) |
| boolean psl_node_is_replicator | ( | PslNode_ptr | _repl | ) |
| boolean psl_node_is_sere | ( | PslNode_ptr | expr | ) |
| boolean psl_node_is_sere_compound_binary | ( | PslNode_ptr | e | ) |
| boolean psl_node_is_serebrackets | ( | PslNode_ptr | e | ) |
| boolean psl_node_is_suffix_implication | ( | PslNode_ptr | expr | ) |
| boolean psl_node_is_suffix_implication_strong | ( | PslNode_ptr | expr | ) |
| boolean psl_node_is_suffix_implication_weak | ( | PslNode_ptr | expr | ) |
| boolean psl_node_is_true | ( | PslNode_ptr | e | ) |
| boolean psl_node_is_word_number | ( | PslNode_ptr | e | ) |
Returns true if the given expression is a word number.
None
| PslNode_ptr psl_node_make_case | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | _cond, | |||
| PslNode_ptr | _then, | |||
| PslNode_ptr | _next | |||
| ) |
Maker for a CASE node.
None
| 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 | |||
| ) |
| PslNode_ptr psl_node_make_extended_next | ( | NodeMgr_ptr | nodemgr, | |
| PslOp | op, | |||
| PslNode_ptr | expr, | |||
| PslNode_ptr | when, | |||
| PslNode_ptr | condition | |||
| ) |
| PslNode_ptr psl_node_make_failure | ( | NodeMgr_ptr | nodemgr, | |
| const char * | msg, | |||
| FailureKind | kind | |||
| ) |
Maker for a FAILURE node.
None
| PslNode_ptr psl_node_make_false | ( | NodeMgr_ptr | nodemgr | ) |
Creates a new FALSE node.
None
| PslNode_ptr psl_node_make_number | ( | NodeMgr_ptr | nodemgr, | |
| int | value | |||
| ) |
| PslNode_ptr psl_node_make_sere_2ampersand | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | seq1, | |||
| PslNode_ptr | seq2 | |||
| ) |
Maker for a && sere.
None
| PslNode_ptr psl_node_make_sere_compound | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | seq1, | |||
| PslOp | op, | |||
| PslNode_ptr | seq2 | |||
| ) |
| PslNode_ptr psl_node_make_sere_concat | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | seq1, | |||
| PslNode_ptr | seq2 | |||
| ) |
Maker for a concatenation sere.
None
| PslNode_ptr psl_node_make_sere_propositional | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | expr | |||
| ) |
Maker for a propositional sere.
None
| PslNode_ptr psl_node_make_sere_star | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | seq | |||
| ) |
Maker for a star sere.
None
| PslNode_ptr psl_node_make_true | ( | NodeMgr_ptr | nodemgr | ) |
Creates a new TRUE node.
None
| int psl_node_number_get_value | ( | PslNode_ptr | e | ) |
Returns the integer value associated with the given number node.
None
| PslNode_ptr psl_node_prune | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | tree, | |||
| PslNode_ptr | branch | |||
| ) |
| PslNode_ptr psl_node_range_get_high | ( | PslNode_ptr | expr | ) |
Returns the high bound of the given range.
None
| PslNode_ptr psl_node_range_get_low | ( | PslNode_ptr | expr | ) |
Returns the low bound of the given range.
None
| PslNode_ptr psl_node_repl_prop_get_property | ( | PslNode_ptr | _prop | ) |
| PslNode_ptr psl_node_repl_prop_get_replicator | ( | PslNode_ptr | _prop | ) |
| PslNode_ptr psl_node_sere_compound_get_left | ( | PslNode_ptr | e | ) |
Returns the left operand of a compound sere.
None
| PslNode_ptr psl_node_sere_compound_get_right | ( | PslNode_ptr | e | ) |
Returns the right operand of a compound sere.
None
| PslNode_ptr psl_node_sere_concat_cut_leftmost | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | e | |||
| ) |
Cuts the leftmost element of a concat sere.
| PslNode_ptr psl_node_sere_concat_get_left | ( | PslNode_ptr | e | ) |
Returns the left operand of a concat.
None
| PslNode_ptr psl_node_sere_concat_get_leftmost | ( | PslNode_ptr | e | ) |
Returns the leftmost element of a concat sere.
| PslNode_ptr psl_node_sere_concat_get_right | ( | PslNode_ptr | e | ) |
Returns the right operand of a concat.
None
| PslNode_ptr psl_node_sere_concat_get_rightmost | ( | PslNode_ptr | e | ) |
Returns the rightmost element of a concat sere.
| PslNode_ptr psl_node_sere_fusion_get_left | ( | PslNode_ptr | e | ) |
Returns the left operand of a fusion.
None
| PslNode_ptr psl_node_sere_fusion_get_right | ( | PslNode_ptr | e | ) |
Returns the right operand of a fusion.
None
| boolean psl_node_sere_is_2ampersand | ( | PslNode_ptr | e | ) |
| boolean psl_node_sere_is_concat | ( | PslNode_ptr | e | ) |
Returns true if the given expression is a concat.
Returns true if the top level operator is a concat.
None
| boolean psl_node_sere_is_concat_fusion | ( | PslNode_ptr | e | ) |
| boolean psl_node_sere_is_concat_fusion_holes_free | ( | PslNode_ptr | e | ) |
| boolean psl_node_sere_is_concat_holes_free | ( | PslNode_ptr | e | ) |
| boolean psl_node_sere_is_fusion | ( | PslNode_ptr | e | ) |
Returns true if the given expression is a fusion.
Returns true if the top level operator is a fusion.
None
| boolean psl_node_sere_is_or | ( | PslNode_ptr | e | ) |
Returns true if the given expression is an or.
Duplicate of psl_node_sere_is_disj.
None
| boolean psl_node_sere_is_plus | ( | 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_standalone_plus | ( | PslNode_ptr | e | ) |
| boolean psl_node_sere_is_standalone_star | ( | PslNode_ptr | e | ) |
| boolean psl_node_sere_is_star | ( | PslNode_ptr | e | ) |
| boolean psl_node_sere_is_star_count | ( | PslNode_ptr | e | ) |
| boolean psl_node_sere_is_star_count_zero | ( | PslNode_ptr | e | ) |
Returns true if the given expr is a star sere with count zero.
None
| boolean psl_node_sere_is_stareq | ( | PslNode_ptr | e | ) |
| boolean psl_node_sere_is_starminusgt | ( | PslNode_ptr | e | ) |
| PslNode_ptr psl_node_sere_propositional_get_expr | ( | PslNode_ptr | e | ) |
Returns the expression in a propositional sere.
None
| PslNode_ptr psl_node_sere_repeated_get_count | ( | PslNode_ptr | e | ) |
Returns the count associated to the repeated sere.
None
| PslNode_ptr psl_node_sere_repeated_get_expr | ( | PslNode_ptr | e | ) |
| PslOp psl_node_sere_repeated_get_op | ( | PslNode_ptr | e | ) |
Returns the count associated to the repeated sere.
None
| PslNode_ptr psl_node_sere_star_get_count | ( | const PslNode_ptr | e | ) |
| PslNode_ptr psl_node_sere_star_get_starred | ( | PslNode_ptr | e | ) |
Getter for a star sere.
None
| 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_suffix_implication_get_consequence | ( | PslNode_ptr | e | ) |
| PslNode_ptr psl_node_suffix_implication_get_premise | ( | PslNode_ptr | e | ) |
| PslNode_ptr PslNode_convert_from_node_ptr | ( | node_ptr | expr | ) |
Casts a PslNode_ptr to a node_ptr.
The returned structure will still contain operators in the SMV parser's domain
None
| PslNode_ptr PslNode_convert_id | ( | const NuSMVEnv_ptr | env, | |
| PslNode_ptr | id, | |||
| PslOpConvType | type | |||
| ) |
| node_ptr PslNode_convert_psl_to_core | ( | const NuSMVEnv_ptr | env, | |
| PslNode_ptr | expr | |||
| ) |
Reduces the given PSL formula to an equivalent formula that uses only core symbols. Resulting formula is either LTL of CTL, and can be used for model checking.
This is the high fcuntion used at system level to convert PSL expression to equivalent expressions that can be managed at system level. Warning: the resulting expression may have a different structure, do not refer to its structure to report errors to the user, use it internally intstead.
None
| node_ptr PslNode_convert_to_node_ptr | ( | PslNode_ptr | expr | ) |
Casts a node_ptr to a PslNode_ptr.
The returned structure will still contain operators in the PSL parser's domain
None
| boolean PslNode_is_handled_psl | ( | const NuSMVEnv_ptr | env, | |
| PslNode_ptr | e | |||
| ) |
Returns true iff given expression can be translated into LTL.
None
| boolean PslNode_is_ltl | ( | const PslNode_ptr | expr | ) |
Checks for a formula being an LTL formula.
Checks for a formula being an LTL formula
None
| boolean PslNode_is_obe | ( | const PslNode_ptr | expr | ) |
Checks for a formula being an CTL formula.
Checks for a formula being an CTL formula
None
| boolean PslNode_is_propositional | ( | const PslNode_ptr | expr | ) |
Checks for a formula being a propositional formula.
Checks for a formula being a propositional formula
None
| boolean PslNode_is_trans_propositional | ( | const PslNode_ptr | expr | ) |
Checks for a formula being a propositional formula.
Checks for a formula being a propositional formula, next operator here leaves the formula propositional
None
| PslNode_ptr PslNode_new_context | ( | NodeMgr_ptr | nodemgr, | |
| PslNode_ptr | ctx, | |||
| PslNode_ptr | node | |||
| ) |
| boolean PslNode_propositional_contains_next | ( | const PslNode_ptr | expr | ) |
Checks if a propositional formula contains a next.
Checks for a formula being a propositional formula
None
| PslNode_ptr PslNode_pslltl2ltl | ( | const NuSMVEnv_ptr | env, | |
| PslNode_ptr | expr, | |||
| PslOpConvType | type | |||
| ) |
| PslNode_ptr PslNode_pslobe2ctl | ( | const NuSMVEnv_ptr | env, | |
| PslNode_ptr | expr, | |||
| PslOpConvType | type | |||
| ) |
| PslNode_ptr PslNode_remove_forall_replicators | ( | const NuSMVEnv_ptr | env, | |
| PslNode_ptr | e | |||
| ) |
| PslNode_ptr PslNode_remove_sere | ( | const NuSMVEnv_ptr | env, | |
| PslNode_ptr | e | |||
| ) |
1.6.1