PslNode_convert_from_node_ptr()
Casts a PslNode_ptr to a node_ptr
PslNode_convert_id()
Converts an id to a different id type, for example a PSL id to a SMV id
PslNode_convert_psl_to_core()
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.
PslNode_convert_to_node_ptr()
Casts a node_ptr to a PslNode_ptr
PslNode_is_handled_psl()
Returns true iff given expression can be translated into LTL.
PslNode_is_ltl()
Checks for a formula being an LTL formula
PslNode_is_obe()
Checks for a formula being an CTL formula
PslNode_is_propositional()
Checks for a formula being a propositional formula
PslNode_new_context()
Creates a psl node that represents a contestualized node
PslNode_pslltl2ltl()
Takes a PSL LTL expression and builds the corresponding LTL expression
PslNode_pslobe2ctl()
Takes a PSL OBE expression and builds the corresponding CTL expression
PslNode_remove_forall_replicators()
Takes a PSL expression and expands all forall constructs contained in the expression
PslNode_remove_sere()
Converts the given expression (possibly containing sere) into an equivalent LTL formula
psl_conv_op()
Converts the given operator into either a PSL operator, or a SMV operator, depending on the value of 'type'
psl_expr_base_num_to_val()
Converts from base to number: TO BE IMPLEMENTED
psl_expr_check_klass()
returns 0 if the given psl expr is not compatible with the given klass
psl_expr_is_boolean()
Returns 1 if the given node is boolean compatible type, 0 otherwise
psl_expr_print_klass()
required
psl_expr_require_klass()
Checks that given expression is compatible with the given required syntactic class
psl_new_node()
Creates a new PSL node, re-using already an existing node if there is one
psl_node_cons_get_element()
Returns the currently pointed element of a list
psl_node_cons_get_next()
Returns the next element of a list
psl_node_cons_reverse()
Reverse a list.
psl_node_context_to_main_context()
Contestualizes a context node into the 'main' context
psl_node_expand_next_event()
During the conversion to LTL, this function is invoked when the expansion of next_event family is required.
psl_node_expand_replicator()
Expansion of a replicator 'forall' statement
psl_node_extended_next_get_condition()
Returns the boolean condition of a next expression node
psl_node_extended_next_get_expr()
Returns the FL expression of a next expression node
psl_node_extended_next_get_when()
Returns the when component of a next expression node
psl_node_get_case_cond()
Returns the condition of the given case node
psl_node_get_case_next()
Returns the next case node of the given case.
psl_node_get_case_then()
Returns the 'then' branch of the given case node
psl_node_get_ite_cond()
Returns the condition of the given ITE node
psl_node_get_ite_else()
Returns the 'else' branch of the given ITE node
psl_node_get_ite_then()
Returns the 'then' branch of the given ITE node
psl_node_get_left()
Returns the given expression's left branch
psl_node_get_op()
Returns the given expression's top level operator
psl_node_get_replicator_id()
Given a replicator, returns the its ID
psl_node_get_replicator_join_op()
Given a replicator, returns the operator joining each replicated expression
psl_node_get_replicator_normalized_value_set()
Given a replicator, returns its values set as a list of the enumerated values
psl_node_get_replicator_range()
Given a replicator, returns its range
psl_node_get_replicator_value_set()
Given a replicator, returns the its values set.
psl_node_get_right()
Returns the given expression's right branch
psl_node_insert_inside_holes()
Service due to way concat_fusion expansion is implemented
psl_node_is_boolean_type()
Returns true if the given node is the PSL syntactic type 'boolean'
psl_node_is_case()
Returns true if the given expression is a case expression
psl_node_is_cons()
Returns true if the given node is a list
psl_node_is_emptystar_free()
Returns true if the given expression is empty star-free
psl_node_is_equal()
psl_node_is_extended_next()
Given a psl node returns true iff the expression belongs to the next operators family.
psl_node_is_fl_op()
Private service of PslNode_is_handled_psl
psl_node_is_handled_fl_op()
Private service of PslNode_is_handled_psl
psl_node_is_handled_next()
Private service of PslNode_is_handled_psl
psl_node_is_handled_sere()
Private service of PslNode_is_handled_psl
psl_node_is_handled_star()
Returns true if the given starred sere can be handled by the system.
psl_node_is_id_equal()
Returns true if two ids are equal
psl_node_is_id()
Returns true if the given node is an identifier
psl_node_is_infinite()
Returns true if the given node is the PSL syntactic value 'inf'
psl_node_is_ite()
Returns true if the given expression is If Then Else
psl_node_is_leaf()
Returns true if the given node is a leaf, i.e. PSL_NULL, a number, a boolean constant, or an atom.
psl_node_is_num_equal()
Returns true if the given numbers are equal
psl_node_is_number()
Returns true if the given expression is an integer number
psl_node_is_obe_op()
Private service of PslNode_is_handled_psl
psl_node_is_propstar()
Returns true if the given expression is a propositional starred sere.
psl_node_is_range()
Returns true if the given node is a range
psl_node_is_repl_prop()
Returns true if the given expression is a replicated property
psl_node_is_replicator()
Returns true if the given expression represents a replicator.
psl_node_is_sere_compound_binary()
Returns true if the given expression is a sere compound
psl_node_is_sere()
Returns true if the given expression is a SERE
psl_node_is_star_free()
Returns true if the given sere is star-free
psl_node_is_suffix_implication_strong()
Returns true if the given expression is a strong suffix implication
psl_node_is_suffix_implication_weak()
Returns true if the given expression is a weak suffix implication
psl_node_is_suffix_implication()
Returns true if the given expression is a suffix implication
psl_node_is_unbound_star_free()
Returns true if the given sere doesn't contain any unbound star
psl_node_make_case()
Maker for a CASE node
psl_node_make_cons_new()
Maker for a list, does not use find_node
psl_node_make_cons()
Maker for a list
psl_node_make_extended_next()
Maker for a NEXT* family node
psl_node_make_failure()
Maker for a FAILURE node
psl_node_make_false()
Creates a new FALSE node
psl_node_make_number()
Maker for a NUMBER node
psl_node_make_sere_compound()
Maker for the sere compound
psl_node_make_true()
Creates a new TRUE node
psl_node_number_get_value()
Returns the integer value associated with the given number node.
psl_node_prune()
Prunes aways the given branch from the given tree
psl_node_pslltl2ltl()
Takes a PSL LTL expression and builds the corresponding LTL expression
psl_node_pslobe2ctl()
Private service for high level function PslNode_pslobe2ctl
psl_node_range_get_high()
Returns the high bound of the given range
psl_node_range_get_low()
Returns the low bound of the given range
psl_node_remove_forall_replicators()
Private service for high level function PslNode_remove_forall_replicators
psl_node_remove_suffix_implication()
Resolves suffix implication
psl_node_repl_prop_get_property()
Given a replicated property, returns the node that contains the property.
psl_node_repl_prop_get_replicator()
Given a replicated property, returns the node that contains the replicator.
psl_node_sere_concat_fusion2ltl()
Resolves concat/fusion and converts it to an equivalent LTL expression
psl_node_sere_distrib_disj()
Distributes the disjunction among SEREs
psl_node_sere_get_leftmost()
Returns the leftmost element of e that is not a SERE
psl_node_sere_get_rightmost()
Returns the rightmost element of e that is not a SERE
psl_node_sere_is_2ampersand()
Returns true if the given expression is a sere in the form { s2 && s1 }
psl_node_sere_is_ampersand()
Returns true if the given SERE is in the form {a} & {b}
psl_node_sere_is_concat_fusion_holes_free()
[Returns true if there are no holes in the given fusion/concat sere to be filled in.
psl_node_sere_is_concat_fusion()
Returns true if the given expression is a concat or fusion sere.
psl_node_sere_is_concat_holes_free()
Returns true if there are no holes in the given concat sere to be filled in.
psl_node_sere_is_disj()
Returns true if the given expression is a disjunction of SEREs.
psl_node_sere_is_plus()
Returns true if the given expression a plus repeated sere
psl_node_sere_is_propositional()
Returns true if the given sere contains a single propositional expression
psl_node_sere_is_repeated()
Returns true if the given expr is a repeated sere
psl_node_sere_is_standalone_plus()
Returns true if the given repeated sere is in the form [+]
psl_node_sere_is_standalone_star()
Returns true if the given expr is in the form [*], with or without a counter.
psl_node_sere_is_star_count()
Returns true if the given starred repeated sere as also a counter
psl_node_sere_is_stareq()
Returns true if the given expr is a starred-eq repeated sere
psl_node_sere_is_starminusgt()
Returns true if the given expr is a starred-minusgt repeated sere
psl_node_sere_is_star()
Returns true if the given expr is a starred repeated sere
psl_node_sere_remove_2ampersand()
Resolves {a} && {a}
psl_node_sere_remove_ampersand()
Resolves {a}&{a}
psl_node_sere_remove_disj()
Removes the disjunction among SERE, by distributing it
psl_node_sere_remove_fusion()
Resolves {a}:{a}
psl_node_sere_remove_plus()
Resolve SERE [+]
psl_node_sere_remove_star_count()
Resolves starred SEREs
psl_node_sere_remove_star()
Resolves starred SEREs
psl_node_sere_remove_trailing_plus()
Resolves the last trailing standalone plus
psl_node_sere_remove_trailing_star()
Resolves trailing standalone stars
psl_node_sere_repeated_get_count()
Returns the count associated to the repeated sere
psl_node_sere_repeated_get_expr()
Returns the repeated expression associated to the repeated sere
psl_node_sere_repeated_get_op()
Returns the count associated to the repeated sere
psl_node_sere_star_get_count()
Returns the count of a starred sere.
psl_node_sere_translate()
High-level service of exported function PslNode_remove_sere
psl_node_set_left()
Sets the given expression's left branch
psl_node_set_right()
Sets the given expression's right branch
psl_node_subst_id()
This is used to rename IDs occurring in the tree, when the replicator 'foreach' statement is resolved
psl_node_suffix_implication_get_consequence()
Returns the consequence of the given suffix implication
psl_node_suffix_implication_get_premise()
Returns the premise of the given suffix implication
()
Define to optimize the convertion of next
()
This was implemented for the sake of readability

Last updated on 2009/03/04 13h:34