psl_grammar.y
Grammar (for Yacc and Bison) of PSL specification input language
psl_input.l
Lexical analyzer for the PSL specification input language
pslConv.c
Algorithms and conversions on PslNode structure
pslExpr.c
Implementation of the PSL parser interface

psl_grammar.y

Grammar (for Yacc and Bison) of PSL specification input language

By: Roberto Cavada

See Alsopsl_input.l


psl_input.l

Lexical analyzer for the PSL specification input language

By: Roberto Cavada

See Alsopsl_grammar.y


pslConv.c

Algorithms and conversions on PslNode structure

By: Fabio Barbon, Roberto Cavada, Simone Semprini

See Alsopsl_conv.h

()
Define to optimize the convertion of next
()
This was implemented for the sake of readability
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_id()
Converts an id to a different id type, for example a PSL id to a SMV id
PslNode_pslobe2ctl()
Takes a PSL OBE expression and builds the corresponding CTL expression
psl_node_pslobe2ctl()
Private service for high level function PslNode_pslobe2ctl
PslNode_remove_forall_replicators()
Takes a PSL expression and expands all forall constructs contained in the expression
psl_node_remove_forall_replicators()
Private service for high level function PslNode_remove_forall_replicators
PslNode_pslltl2ltl()
Takes a PSL LTL expression and builds the corresponding LTL expression
psl_node_pslltl2ltl()
Takes a PSL LTL expression and builds the corresponding LTL expression
PslNode_remove_sere()
Converts the given expression (possibly containing sere) into an equivalent LTL formula
()
Converts the given operator into either a PSL operator, or a SMV operator, depending on the value of 'type'
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_subst_id()
This is used to rename IDs occurring in the tree, when the replicator 'foreach' statement is resolved
psl_node_expand_replicator()
Expansion of a replicator 'forall' statement
psl_node_sere_remove_disj()
Removes the disjunction among SERE, by distributing it
psl_node_insert_inside_holes()
Service due to way concat_fusion expansion is implemented
psl_node_sere_concat_fusion2ltl()
Resolves concat/fusion and converts it to an equivalent LTL expression
psl_node_sere_translate()
High-level service of exported function PslNode_remove_sere
psl_node_sere_is_disj()
Returns true if the given expression is a disjunction of SEREs.
psl_node_sere_distrib_disj()
Distributes the disjunction among SEREs
psl_node_sere_remove_star_count()
Resolves starred SEREs
psl_node_sere_is_ampersand()
Returns true if the given SERE is in the form {a} & {b}
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_remove_plus()
Resolve SERE [+]
psl_node_remove_suffix_implication()
Resolves suffix implication
psl_node_sere_remove_star()
Resolves starred SEREs
psl_node_sere_remove_trailing_star()
Resolves trailing standalone stars
psl_node_sere_remove_trailing_plus()
Resolves the last trailing standalone plus
psl_node_sere_remove_ampersand()
Resolves {a}&{a}
psl_node_sere_remove_2ampersand()
Resolves {a} && {a}
psl_node_sere_remove_fusion()
Resolves {a}:{a}

pslExpr.c

Implementation of the PSL parser interface

By: Roberto Cavada, Marco Roveri

See AlsopslExpr.h

psl_expr_print_klass()
required
psl_expr_is_boolean()
Returns 1 if the given node is boolean compatible type, 0 otherwise
psl_expr_check_klass()
returns 0 if the given psl expr is not compatible with the given klass
psl_expr_base_num_to_val()
Converts from base to number: TO BE IMPLEMENTED
psl_expr_require_klass()
Checks that given expression is compatible with the given required syntactic class
psl_expr_is_valid_flproperty()
Checks that there is no violation of types for operators '=', '!=' and '==', that cannot be used with FL_PROPERTY expressions

Last updated on 2012/11/18 14h:37