Package tulip :: Package spec :: Module translation

Module translation

AST subclasses to translate to each syntax of:

- gr1c: https://tulip-control.github.io/gr1c/md_spc_format.html
- JTLV
- SMV: http://nusmv.fbk.eu/NuSMV/userman/v21/nusmv_3.html
- SPIN: http://spinroot.com/spin/Man/ltl.html
        http://spinroot.com/spin/Man/operators.html
- python (Boolean formulas only)
- WRING: http://vlsi.colorado.edu/~rbloem/wring.html
      (see top of file: LTL.pm)

Functions

make_jtlv_nodes()

make_gr1c_nodes(opmap=None)

make_slugs_nodes()
Simple translation, unisigned arithmetic only.

make_promela_nodes()

make_smv_nodes()

make_wring_nodes()

make_python_nodes()

'boolean' or (min_int, max_int)

convert_domain(dom)
Return equivalent integer domain if dom contais strings.

translate(spec, lang)
Return str or tuple in tool format.

FOL.Node

translate_ast(tree, lang)
Return AST of formula tree.

Variables
	logger = `logging.getLogger(__name__)`
	lang2nodes = `{'jtlv': make_jtlv_nodes(), 'gr1c': make_gr1c_nod...`
	to_lang = `{'jtlv': _to_jtlv, 'gr1c': _to_gr1c, 'slugs': _to_sl...`
	__package__ = `'tulip.spec'`

Function Details

make_slugs_nodes()

Simple translation, unisigned arithmetic only.

For signed arithmetic use Promela instead.

convert_domain(dom)

Return equivalent integer domain if dom contais strings.

Parameters:

dom (list of str)

Returns: 'boolean' or (min_int, max_int)

translate(spec, lang)

Return str or tuple in tool format.

Consult the respective documentation in tulip.interfaces concerning formats and links to further reading.

Parameters:

lang ('gr1c', 'slugs', 'jtlv', or 'wring')
spec (GRSpec)

Returns:

spec formatted for input to tool; the type of the return value depends on the tool:

str if gr1c or slugs
(assumption, guarantee), where each element of the tuple is str

translate_ast(tree, lang)

Return AST of formula tree.

Parameters:

lang ('gr1c' or 'slugs' or 'jtlv' or 'promela' or 'smv' or 'python' or 'wring')
tree (Nodes.Node)

Returns: FOL.Node

tree using AST nodes of lang

Variables Details

lang2nodes

Value:

{'jtlv': make_jtlv_nodes(), 'gr1c': make_gr1c_nodes(), 'slugs': make_s
lugs_nodes(), 'promela': make_promela_nodes(), 'smv': make_smv_nodes()
, 'python': make_python_nodes(), 'wring': make_wring_nodes()}

to_lang

Value:

{'jtlv': _to_jtlv, 'gr1c': _to_gr1c, 'slugs': _to_slugs, 'wring': _to_
wring}