Data Formats

tulipcon XML

The tulipcon XML schema is defined in tulipcon.rnc using RELAX NG compact syntax. You may generate a W3C XML Schema definition from this using the tool trang, e.g.

$ trang -I rnc -O xsd doc/formats/tulipcon.rnc tulipcon.xsd

Versions are specified with a natural number (and no minor nor text appended). The root tag indicates the version in use, e.g., a file defined using version 0 would begin like

<?xml version="1.0" encoding="UTF-8"?>
<tulipcon xmlns="http://tulip-control.sourceforge.net/ns/0" version="0">
...

Processing for version 0 is quite lax—it allows many tags to be missing or incomplete by using default values. Once the format stabilizes (at version 1 or so), requirements for conformance will be more strict.

Version 0

Pseudo-code describing the specification follows. It is not normative. Also, see notes below.

<tulipcon version="0">
  <prob_type>rhtlp or synth or none or ...</prob_type>
  <c_dyn>
    <A type="matrix" r="3" c="3">...</A>
    <B type="matrix" r="3" c="1">...</B>
    <E>...same format as A and B...</E>
    <K>...</K>
    <sample_period>...optional; if included, then system is regarded
                   as the discretization of a continuous-time system,
                   using the given sampling period.</sample_period>
    <U_set type="polytope"><H type="matrix" r="3" c="3">...</H><K>...</K></U_set>
    <W_set>...same format as U_set...</W_set>
  </c_dyn>
  <env_vars><item key="" value="" />...</env_vars>
  <sys_vars><item key="" value="" />...</sys_vars>
  <spec>
    <assume>...assumption string...</assume>
    <guarantee>...guarantee string...</guarantee>

    ALTERNATIVELY (decision of which specification storage container
    to use is based on what tags are found under <spec>),

    <env_init><litem value="" />...</env_init>
    <env_safety>...</env_safety>
    <env_prog>...</env_prog>
    <sys_init>...</sys_init><sys_safety>...</sys_safety><sys_prog>...</sys_prog>
  </spec>
  <d_dyn>  N.B., this tag can also be empty (if disc dynamics is None).
    <domain type="polytope">...</domain>
    <trans type="matrix">...</trans>
    <prop_symbols>...space-separated list...</prop_symbols>
    <regions>
      <region>
        <list_prop>...space-separated list...</list_prop>
        <reg_item type="polytope">...</reg_item>
      </region>
      ...
    </regions>
    <orig_map>...space-separated list of indices...</orig_map>
    <orig_partition>
      <cell type="polytope">...</cell>
      ...
    </orig_partition>
  </d_dyn>
  <aut>
    <node>
      <id>a unique identifier number</id>
      <name>a string name or description (may be empty, or the <name> tag may be omitted)</name>
      <child_list>descendent nodes; space-separated list of node ID numbers</child_list>
      <state>
        <item key="" value="" />
        ...
      </state>
    </node>
    ...
  </aut>
  <smv_file>
...verbatim copy of corresponding SMV file...
  </smv_file>
  <spec_file>
...verbatim copy of corresponding specification (*.spc) file...
  </spec_file>
  <extra>
    Anything below here is arbitrary and ignored by tulip.  It is
    included as a convenience and to facilitate keeping
    application-specific notes with the synthesis results.  Please be
    careful to *not* include non-printing characters or arbitrary
    binary data; instead try base64 or similar, or include a reference
    to an external data file, e.g. HDF5.
  </extra>
</tulipcon>

Notes:

• Polytopes are defined in -representation, i.e. system of inequalities, .

• Matrices are in row-major. E.g.,

  A = [[1, 2, 3],
       [4, 5, 6]]
  

  would be saved as

  <A type="matrix" r="2" c="3">1 2 3 4 5 6</A>
  

Key Routines

conxml.loadXML(x, verbose=0, namespace='http://tulip-control.sourceforge.net/ns/0')

Return ({SynthesisProb,PropPreservingPartition}, CtsSysDyn, Automaton).

The first element of the returned tuple depends on the problem type detected. If type “none”, then it is an instance of PropPreservingPartition, e.g., as returned by the function discretize in module discretize. If of type “synth” or “rhtlp”, then an instance of SynthesisProb or a child class is returned.

Any empty or missing items are set to None, or an exception is raised if the missing item is required.

The argument x can also be an instance of xml.etree.ElementTree._ElementInterface ; this is mainly for internal use, e.g. by the function untagpolytope and some load/dumpXML methods elsewhere.

To easily read and process this string from a file, instead call the method readXMLfile

conxml.dumpXML(prob=None, spec=['', ''], sys_dyn=None, aut=None, disc_dynamics=None, synthesize_aut=False, verbose=0, pretty=False)

Return tulipcon XML string.

prob is an instance of SynthesisProb or a child class, such as RHTLPProb (both defined in rhtlp.py). sys_dyn is an instance of CtsSysDyn (defined in discretize.py), or None. If None, then continuous dynamics are considered empty (i.e., there are none).

disc_dynamics is an instance of PropPreservingPartition, such as returned by the function discretize in module discretize. This argument is supported to permit entire avoidance of SynthesisProb or related classes.

If pretty is True, then use indentation and newlines to make the resulting XML string more visually appealing.

aut is an instance of Automaton. If None (rather than an instance), then an empty <aut> tag is written.

spec may be an instance of GRSpec or a list. If of GRSpec, then it is formed as expected. If spec is a list, then first element of “assume” string, and second element of “guarantee” string. spec=None is also accepted, in which case the specification is considered empty, but note that this could cause problems later unless some content is introduced.

** synthesize_aut flag is IGNORED ** If synthesize_aut is True, then if prob.__realizable is not None, use its value to determine whether a previously computed *.aut file should be read. Else (if prob.__realizable is None or False), then try to compute automaton (saving to file prob.__jtlvfile + ‘.aut’, as usual). If synthesize_aut is False, then just save an empty <aut></aut>.

** verbose flag is IGNORED (but that will change...) **

To easily save the result here to a file, instead call the method writeXMLfile

Continuous Systems in YAML

To facilitate experimentation, code reuse, etc., continuous systems may be defined using YAML.

For example, to generate a proposition and reachability preserving partition from the linear system defined in examples/rsimple_example.yaml, try

$ tools/autopart.py examples/rsimple_example.yaml -p -v foo.xml

(If autopart.py is not marked as executable, you will need to prepend this with python.) The resulting tulipcon XML file is saved to foo.xml. The flag -p causes a plot of the (planar) partition to be shown, and the flag -v means be verbose.

Key Routines

conxml.loadYAML(x, verbose=0)

Read transition system specified using YAML in given string.

Return (sys_dyn, initial_partition, N), where:

• sys_dyn is the system dynamics (instance of CtsSysDyn),
• cont_prop is the continuous propositions of the space (instance of PropPreservingPartition), and
• N is the horizon length (default is 10).

To easily read and process this string from a file, instead call the method readYAMLfile.

Raise exception if critical error.