-
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_is_trans_propositional()
- Checks for a formula being a propositional formula
-
PslNode_new_context()
- Creates a psl node that represents a contestualized
node
-
PslNode_propositional_contains_next()
- Checks if a propositional formula contains a next
-
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_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_false()
- Checks if a node is a FALSE node
-
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_propositional()
- Checks for a formula being a propositional formula
-
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_serebrackets()
- Returns true if the given expression is a SERE in the form {a}
-
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_true()
- Checks if a node is a TRUE node
-
psl_node_is_unbound_star_free()
- Returns true if the given sere doesn't contain any unbound
star
-
psl_node_is_word_number()
- Returns true if the given expression is a word number
-
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_2ampersand()
- Maker for a && sere
-
psl_node_make_sere_compound()
- Maker for the sere compound
-
psl_node_make_sere_concat()
- Maker for a concatenation sere
-
psl_node_make_sere_propositional()
- Maker for a propositional sere
-
psl_node_make_sere_star()
- Maker for a star sere
-
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_compound_get_left()
- Returns the left operand of a compound sere.
-
psl_node_sere_compound_get_right()
- Returns the right operand of a compound sere.
-
psl_node_sere_concat_cut_leftmost()
- Cuts the leftmost element of a concat sere
-
psl_node_sere_concat_fusion2ltl()
- Resolves concat/fusion and converts it to an equivalent LTL
expression
-
psl_node_sere_concat_get_leftmost()
- Returns the leftmost element of a concat sere
-
psl_node_sere_concat_get_left()
- Returns the left operand of a concat.
-
psl_node_sere_concat_get_rightmost()
- Returns the rightmost element of a concat sere
-
psl_node_sere_concat_get_right()
- Returns the right operand of a concat.
-
psl_node_sere_distrib_disj()
- Distributes the disjunction among SEREs
-
psl_node_sere_fusion_get_left()
- Returns the left operand of a fusion.
-
psl_node_sere_fusion_get_right()
- Returns the right operand of a fusion.
-
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_concat()
- Returns true if the given expression is a concat.
-
psl_node_sere_is_disj()
- Returns true if the given expression is a disjunction of SEREs.
-
psl_node_sere_is_fusion()
- Returns true if the given expression is a fusion.
-
psl_node_sere_is_or()
- Returns true if the given expression is an or.
-
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_zero()
- Returns true if the given expr is a star sere with
count zero
-
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_propositional_get_expr()
- Returns the expression in a propositional 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_star_get_starred()
- Getter for a star 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
-
()
- Converts the given operator into either a PSL operator, or
a SMV operator, depending on the value of 'type'
-
()
- Define to optimize the convertion of next
-
()
- This was implemented for the sake of readability
Last updated on 2011/04/06 21h:12