-
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
-
psl_conv_op()
- 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
Last updated on 2010/05/19 22h:26