Package tulip :: Package spec :: Module transformation

Module transformation

Syntactic manipulation of trees.

Classes
	Tree Abstract syntax tree as a graph data structure.

Functions

networkx.DiGraph

ast_to_labeled_graph(tree, detailed)
Convert AST to NetworkX.DiGraph for graphics.

check_for_undefined_identifiers(tree, domains)
Check that types in tree are incompatible with domains.

sub_values(tree, var_values)
Substitute given values for variables.

sub_constants(tree, var_str2int)
Replace string constants by integers.

sub_bool_with_subtree(tree, bool2subtree)
Replace selected Boolean variables with given AST.

(Var, Const)

pair_node_to_var(tree, c)
Find variable under Binary operator above given node.

str

infer_constants(formula, variables)
Enclose all non-variable names in quotes.

check_var_name_conflict(f, varname)

collect_primed_vars(t)
Return `set` of variable identifiers in the context of a next operator.

Variables
	logger = `logging.getLogger(__name__)`
	__package__ = `'tulip.spec'`

Function Details

ast_to_labeled_graph(tree, detailed)

Convert AST to NetworkX.DiGraph for graphics.

Parameters:

ast - Abstract syntax tree

Returns: networkx.DiGraph

check_for_undefined_identifiers(tree, domains)

Check that types in tree are incompatible with domains.

Raise a ValueError if tree either:

contains a variable missing from domains
binary operator between variable and invalid value for that variable.

Parameters:

domains (dict) - variable definitions:
{'varname': domain}

See GRSpec for more details of available domain types.
tree (Tree)

sub_values(tree, var_values)

Substitute given values for variables.

Parameters:

tree - AST
var_values (dict)

Returns:

AST with Var nodes replaces by Num, Const, or Bool

sub_constants(tree, var_str2int)

Replace string constants by integers.

To be used for converting arbitrary finite domains to integer domains prior to calling gr1c.

Parameters:

const2int (dict of list) - {'varname':['const_val0', ...], ...}

sub_bool_with_subtree(tree, bool2subtree)

Replace selected Boolean variables with given AST.

Parameters:

bool2form (dict from str to Tree) - map from each Boolean variable to some equivalent formula. A subset of Boolean varibles may be used.
Note that the types of variables in tree are defined by bool2form.
tree (LTL_AST)

pair_node_to_var(tree, c)

Find variable under Binary operator above given node.

First move up from nd, stop at first Binary node. Then move down, until first Var. This assumes that only Unary operators appear between a Binary and its variable and constant operands.

May be extended in the future, depending on what the tools support and is thus needed here.

Parameters:

tree (LTL_AST
@type nd: Const or Num
)

Returns: (Var, Const)

variable, constant

infer_constants(formula, variables)

Enclose all non-variable names in quotes.

Parameters:

formula (str or LTL_AST) - well-formed LTL formula
variables (dict as accepted by GRSpec or container of str) - domains of variables, or only their names. If the domains are given, then they are checked for ambiguities as for example a variable name duplicated as a possible value in the domain of a string variable (the same or another).
If the names are given only, then a warning is raised, because ambiguities cannot be checked in that case, since they depend on what domains will be used.

Returns: str

formula with all string literals not in variables enclosed in double quotes

collect_primed_vars(t)

Return `set` of variable identifiers in the context of a next operator.

Parameters:

t (recursive AST)