pyudbm.binding.utap

High-level read-only UTAP API.

This module layers immutable Python snapshot objects on top of the native pyudbm.binding._utap bindings. It is the public high-level inspection layer for parsed UPPAAL models and queries.

The surface is intentionally read-only in this phase:

model parsing returns a ModelDocument;
nested model objects are frozen dataclass snapshots;
query parsing returns immutable ParsedQuery values;
the owning ModelDocument retains the native document for XML round-tripping helpers.

Compared with pyudbm.binding._utap, this module focuses on a stable Python-facing object model for templates, processes, locations, edges, queries, diagnostics, and selected document-level declarations.

all

pyudbm.binding.utap.__all__ = ['Branchpoint', 'Diagnostic', 'Edge', 'Expectation', 'Expression', 'FeatureFlags', 'Location', 'MAPPED_FIELDS', 'MAPPED_FIELD_NOTES', 'ModelDocument', 'Option', 'ParsedQuery', 'ParsedQueryExpectation', 'Position', 'Process', 'Query', 'Resource', 'Symbol', 'Template', 'TypeInfo', 'UNMAPPED_FIELDS', 'UNMAPPED_FIELD_REASONS', 'builtin_declarations', 'load_query', 'load_xml', 'load_xta', 'loads_query', 'loads_xml', 'loads_xta', 'parse_query', 'textual_builtin_preamble']

Built-in mutable sequence.

If no argument is given, the constructor creates a new empty list. The argument must be an iterable if specified.

MAPPED_FIELDS

pyudbm.binding.utap.MAPPED_FIELDS = {'Branchpoint': ('name', 'index', 'position', 'symbol'), 'Document': ('templates', 'processes', 'queries', 'options', 'features', 'errors', 'warnings', 'modified'), 'Edge': ('index', 'control', 'action_name', 'source_name', 'source_kind', 'target_name', 'target_kind', 'guard', 'assign', 'sync', 'prob', 'select_text', 'select_symbols', 'select_values'), 'FeatureFlags': ('has_priority_declaration', 'has_strict_invariants', 'has_stop_watch', 'has_strict_lower_bound_on_controllable_edges', 'has_clock_guard_recv_broadcast', 'has_urgent_transition', 'has_dynamic_templates', 'all_broadcast', 'sync_used', 'supports_symbolic', 'supports_stochastic', 'supports_concrete'), 'Location': ('name', 'index', 'position', 'symbol', 'name_expression', 'invariant', 'exp_rate', 'cost_rate', 'is_urgent', 'is_committed'), 'Option': ('name', 'value'), 'ParsedQuery': ('line', 'no', 'builder', 'text', 'quantifier', 'options', 'expression', 'is_smc', 'declaration', 'result_type', 'expectation'), 'Process': ('name', 'index', 'position', 'template_name', 'parameters', 'arguments', 'mapping', 'argument_count', 'unbound_count', 'restricted_symbols'), 'Query': ('formula', 'comment', 'options', 'expectation', 'location'), 'Template': ('name', 'index', 'position', 'parameter', 'declaration', 'init_name', 'type', 'mode', 'is_ta', 'is_instantiated', 'dynamic', 'is_defined', 'locations', 'branchpoints', 'edges'), 'diagnostic_t': ('message', 'context', 'position', 'line', 'column', 'end_line', 'end_column', 'path'), 'expectation_t': ('result_kind', 'status', 'value', 'time_ms', 'mem_kib'), 'expression_t': ('text', 'kind', 'position', 'type', 'size', 'children', 'is_empty'), 'position_t': ('start', 'end', 'line', 'column', 'end_line', 'end_column', 'path'), 'symbol_t': ('name', 'type', 'position'), 'type_t': ('kind', 'position', 'size', 'text', 'declaration', 'is_unknown', 'is_range', 'is_integer', 'is_boolean', 'is_function', 'is_function_external', 'is_clock', 'is_process', 'is_process_set', 'is_location', 'is_location_expr', 'is_instance_line', 'is_branchpoint', 'is_channel', 'is_record', 'is_array', 'is_scalar', 'is_diff', 'is_void', 'is_cost', 'is_integral', 'is_invariant', 'is_probability', 'is_guard', 'is_constraint', 'is_formula', 'is_double', 'is_string')}

Public snapshot fields currently exposed for each native UTAP payload type.

This mapping documents the first-phase Python-facing surface that ModelDocument and related value objects guarantee to populate.

MAPPED_FIELD_NOTES

pyudbm.binding.utap.MAPPED_FIELD_NOTES = {'Template': {'declaration': 'Conservative first-phase field. The current binding keeps this empty instead of calling unstable upstream pretty-printers on every template.'}, 'expression_t': {'text': 'Safe pretty-printer wrapper. Some upstream expressions still fall back to synthesized text when direct stringification is unstable.'}, 'type_t': {'declaration': 'Safe declaration wrapper. Returns a stable fallback when upstream pretty-printers throw.', 'text': 'Safe pretty-printer wrapper. Returns a stable fallback when upstream stringification throws.'}}

Additional compatibility notes for selected mapped fields.

These notes explain conservative wrappers and intentionally restricted representations where the Python layer avoids exposing unstable native pretty-printer or parser internals directly.

UNMAPPED_FIELDS

pyudbm.binding.utap.UNMAPPED_FIELDS = {'Branchpoint': (), 'Document': ('globals', 'before_update', 'after_update', 'chan_priorities', 'strings'), 'Edge': (), 'FeatureFlags': (), 'Location': (), 'Option': (), 'ParsedQuery': ('subjections', 'imitation'), 'Process': ('restricted',), 'Query': ('results',), 'Template': ('messages', 'updates', 'conditions', 'dynamic_evals'), 'diagnostic_t': (), 'expectation_t': (), 'expression_t': ('value', 'double_value', 'sync', 'record_label_index', 'string_value', 'symbol'), 'position_t': (), 'symbol_t': ('frame', 'user_data'), 'type_t': ('children', 'range', 'labels')}: Native UTAP fields that are currently not promoted to the public snapshot layer.

UNMAPPED_FIELD_REASONS

pyudbm.binding.utap.UNMAPPED_FIELD_REASONS = {'Document': {'after_update': 'Exposed via the after_update_text property instead of re-exporting raw expression_t on the first-phase document snapshot.', 'before_update': 'Exposed via the before_update_text property instead of re-exporting raw expression_t on the first-phase document snapshot.', 'chan_priorities': 'Exposed via the channel_priority_texts property instead of re-exporting raw chan_priority_t objects.', 'globals': 'Exposed via the global_declarations property instead of re-exporting raw declarations_t as a first-phase value object.', 'strings': 'Internal interned-string table is not a stable user-facing semantic object.'}, 'ParsedQuery': {'imitation': 'Not yet promoted to a stable first-phase Python value object.', 'subjections': 'Not yet promoted to a stable first-phase Python value object.'}, 'Process': {'restricted': 'The raw restricted-variable set is exposed indirectly via restricted_symbols; the original native container itself is not re-exported.'}, 'Query': {'results': 'Upstream query_t does not currently preserve structured result entries in the live document object.'}, 'Template': {'conditions': 'LSC-specific structures need dedicated wrappers instead of string summaries.', 'dynamic_evals': 'Deferred until dynamic-template introspection gets a stable public shape.', 'messages': 'LSC-specific structures need dedicated wrappers instead of string summaries.', 'updates': 'LSC-specific structures need dedicated wrappers instead of string summaries.'}, 'expression_t': {'double_value': 'Literal-value extraction needs a typed Python value layer instead of ad hoc unions.', 'record_label_index': 'Record-label internals need a dedicated typed accessor instead of leaking parser internals.', 'string_value': 'Literal-value extraction needs a typed Python value layer instead of ad hoc unions.', 'symbol': 'Expression-bound symbol references need a dedicated stable wrapper contract.', 'sync': 'Sync-kind internals are better exposed together with higher-level synchronization helpers.', 'value': 'Literal-value extraction needs a typed Python value layer instead of ad hoc unions.'}, 'symbol_t': {'frame': 'Raw frame_t is an implementation-level scope object without a stable first-phase Python API.', 'user_data': 'Raw user_data pointers are native implementation details and not a safe Python-facing field.'}, 'type_t': {'children': 'Deferred until recursive type-shape wrappers are stabilized for records, arrays, and process fields.', 'labels': 'Deferred until recursive type-shape wrappers are stabilized for record/process field labels.', 'range': 'Deferred until recursive type-shape wrappers are stabilized for ranged and dependent types.'}}: Explanations for why entries in UNMAPPED_FIELDS are not yet exposed directly in the high-level Python API.

Position

Source span of one parsed UTAP object.

Positions are immutable snapshots produced from UTAP source metadata. Line, column, and path information may be absent for synthesized nodes that do not correspond to a concrete file-backed location.

Parameters:

start (int) – Start offset in the normalized source buffer.
end (int) – End offset in the normalized source buffer.
line (int or None) – One-based starting line number, if available.
column (int or None) – One-based starting column number, if available.
end_line (int or None) – One-based ending line number, if available.
end_column (int or None) – One-based ending column number, if available.
path (str or None) – Source path associated with the position, if available.

Example:

>>> from pyudbm.binding.utap import Position
>>> position = Position(0, 4, 1, 1, 1, 5, "model.xta")
>>> position.line
1

Option

class pyudbm.binding.utap.Option(name: str, value: str)[source]

One XML or query option expressed as a key/value pair.

Parameters:

name (str) – Option name.
value (str) – Option value as text.

Example:

>>> from pyudbm.binding.utap import Option
>>> Option("trace", "short").name
'trace'

Resource

class pyudbm.binding.utap.Resource(name: str, value: str, unit: str | None)[source]

One resource measurement attached to a query expectation.

Parameters:

name (str) – Resource kind, for example time or memory.
value (str) – Resource value as text.
unit (str or None) – Optional unit associated with the value.

Example:

>>> from pyudbm.binding.utap import Resource
>>> Resource("time", "100", "ms").unit
'ms'

Expectation

class pyudbm.binding.utap.Expectation(value_type: str, status: str, value: str, resources: Tuple[Resource, ...])[source]

Expected verification outcome stored with a model query.

value_type and status mirror UTAP’s expectation metadata, while resources stores optional time or memory budgets.

Parameters:

value_type (str) – Expectation category such as "Symbolic" or "Probability".
status (str) – Expected outcome status.
value (str) – Expected scalar value rendered as text, when present.
resources (Tuple[Resource, ...]) – Optional resource constraints or measurements.

Example:

>>> from pyudbm.binding.utap import Expectation, Resource
>>> expectation = Expectation("Probability", "True", "0.95", (Resource("time", "100", "ms"),))
>>> expectation.value
'0.95'

TypeInfo

class pyudbm.binding.utap.TypeInfo(kind: int, position: Position, size: int, text: str, declaration: str, is_unknown: bool, is_range: bool, is_integer: bool, is_boolean: bool, is_function: bool, is_function_external: bool, is_clock: bool, is_process: bool, is_process_set: bool, is_location: bool, is_location_expr: bool, is_instance_line: bool, is_branchpoint: bool, is_channel: bool, is_record: bool, is_array: bool, is_scalar: bool, is_diff: bool, is_void: bool, is_cost: bool, is_integral: bool, is_invariant: bool, is_probability: bool, is_guard: bool, is_constraint: bool, is_formula: bool, is_double: bool, is_string: bool)[source]

Immutable snapshot of one UTAP type_t descriptor.

The boolean flags mirror native predicate helpers so callers can inspect semantic categories without depending on unstable native internals.

Parameters:

kind (int) – Native type_t kind code.
position (Position) – Source position of the type node.
size (int) – Native size or arity field.
text (str) – Safe pretty-printed type text.
declaration (str) – Safe pretty-printed declaration text.
is_unknown (bool) – Whether the type is unresolved.
is_range (bool) – Whether the type is a ranged integer type.
is_integer (bool) – Whether the type is an integer type.
is_boolean (bool) – Whether the type is a boolean type.
is_function (bool) – Whether the type denotes a function.
is_function_external (bool) – Whether the function type is external.
is_clock (bool) – Whether the type denotes a clock.
is_process (bool) – Whether the type denotes a process.
is_process_set (bool) – Whether the type denotes a process set.
is_location (bool) – Whether the type denotes a location.
is_location_expr (bool) – Whether the type denotes a location expression.
is_instance_line (bool) – Whether the type denotes an instance line.
is_branchpoint (bool) – Whether the type denotes a branchpoint.
is_channel (bool) – Whether the type denotes a channel.
is_record (bool) – Whether the type denotes a record.
is_array (bool) – Whether the type denotes an array.
is_scalar (bool) – Whether the type denotes a scalar set.
is_diff (bool) – Whether the type denotes a clock-difference form.
is_void (bool) – Whether the type denotes void.
is_cost (bool) – Whether the type denotes a cost quantity.
is_integral (bool) – Whether the type is integral.
is_invariant (bool) – Whether the type denotes an invariant expression.
is_probability (bool) – Whether the type denotes a probability.
is_guard (bool) – Whether the type denotes a guard expression.
is_constraint (bool) – Whether the type denotes a constraint.
is_formula (bool) – Whether the type denotes a formula.
is_double (bool) – Whether the type denotes a floating-point value.
is_string (bool) – Whether the type denotes a string.

Example:

>>> from pyudbm.binding.utap import Position, TypeInfo
>>> position = Position(0, 0, None, None, None, None, None)
>>> type_info = TypeInfo(
...     kind=0,
...     position=position,
...     size=1,
...     text="int",
...     declaration="int",
...     is_unknown=False,
...     is_range=False,
...     is_integer=True,
...     is_boolean=False,
...     is_function=False,
...     is_function_external=False,
...     is_clock=False,
...     is_process=False,
...     is_process_set=False,
...     is_location=False,
...     is_location_expr=False,
...     is_instance_line=False,
...     is_branchpoint=False,
...     is_channel=False,
...     is_record=False,
...     is_array=False,
...     is_scalar=False,
...     is_diff=False,
...     is_void=False,
...     is_cost=False,
...     is_integral=True,
...     is_invariant=False,
...     is_probability=False,
...     is_guard=False,
...     is_constraint=False,
...     is_formula=False,
...     is_double=False,
...     is_string=False,
... )
>>> type_info.is_integer
True

Symbol

class pyudbm.binding.utap.Symbol(name: str, type: TypeInfo, position: Position)[source]

Immutable snapshot of one UTAP symbol reference.

Parameters:

name (str) – Symbol name.
type (TypeInfo) – Symbol type information.
position (Position) – Source position of the symbol declaration or reference.

Example:

>>> from pyudbm.binding.utap import Position, Symbol, TypeInfo
>>> position = Position(0, 0, None, None, None, None, None)
>>> type_info = TypeInfo(
...     0,
...     position,
...     1,
...     "clock",
...     "clock",
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     True,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
... )
>>> Symbol("x", type_info, position).name
'x'

Expression

class pyudbm.binding.utap.Expression(text: str, kind: int, position: Position, type: TypeInfo, size: int, children: Tuple[Expression, ...], is_empty: bool)[source]

Immutable snapshot of one parsed expression tree node.

children contains recursively converted expression nodes and is_empty marks optional fields that UTAP reports as structurally empty.

Parameters:

text (str) – Safe pretty-printed expression text.
kind (int) – Native expression_t kind code.
position (Position) – Source position of the expression node.
type (TypeInfo) – Static type information for the expression.
size (int) – Native size or child-count field.
children (Tuple[Expression, ...]) – Child expressions in native order.
is_empty (bool) – Whether the expression is structurally empty.

Example:

>>> from pyudbm.binding.utap import Expression, Position, TypeInfo
>>> position = Position(0, 0, None, None, None, None, None)
>>> type_info = TypeInfo(
...     0,
...     position,
...     1,
...     "int",
...     "int",
...     False,
...     False,
...     True,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     True,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
...     False,
... )
>>> expression = Expression("0", 0, position, type_info, 0, (), False)
>>> expression.text
'0'

Diagnostic

One parser or semantic diagnostic emitted by UTAP.

Parameters:

message (str) – Primary diagnostic message.
context (str) – Additional context text from UTAP.
position (Position) – Structured source span for the diagnostic.
line (int or None) – One-based starting line number, if available.
column (int or None) – One-based starting column number, if available.
end_line (int or None) – One-based ending line number, if available.
end_column (int or None) – One-based ending column number, if available.
path (str or None) – Source path associated with the diagnostic, if available.

Example:

>>> from pyudbm.binding.utap import Diagnostic, Position
>>> position = Position(0, 5, 1, 1, 1, 6, "model.xml")
>>> diagnostic = Diagnostic("error", "context", position, 1, 1, 1, 6, "model.xml")
>>> diagnostic.message
'error'

FeatureFlags

class pyudbm.binding.utap.FeatureFlags(has_priority_declaration: bool, has_strict_invariants: bool, has_stop_watch: bool, has_strict_lower_bound_on_controllable_edges: bool, has_clock_guard_recv_broadcast: bool, has_urgent_transition: bool, has_dynamic_templates: bool, all_broadcast: bool, sync_used: int, supports_symbolic: bool, supports_stochastic: bool, supports_concrete: bool)[source]

Supported-language and capability flags detected for a document.

These fields summarize whether the parsed document uses or supports major UTAP feature families such as priorities, stochastic constructs, or symbolic verification.

Parameters:

has_priority_declaration (bool) – Whether channel priorities are declared.
has_strict_invariants (bool) – Whether strict invariants are used.
has_stop_watch (bool) – Whether stop-watch clocks are used.
has_strict_lower_bound_on_controllable_edges (bool) – Whether strict lower bounds on controllable edges are used.
has_clock_guard_recv_broadcast (bool) – Whether receive-broadcast guards use clock constraints.
has_urgent_transition (bool) – Whether urgent transitions are present.
has_dynamic_templates (bool) – Whether dynamic templates are present.
all_broadcast (bool) – Whether synchronization is broadcast-only.
sync_used (int) – Native synchronization-usage summary code.
supports_symbolic (bool) – Whether the document is suitable for symbolic analysis.
supports_stochastic (bool) – Whether the document is suitable for stochastic analysis.
supports_concrete (bool) – Whether the document is suitable for concrete simulation.

Example:

>>> from pyudbm.binding.utap import FeatureFlags
>>> flags = FeatureFlags(False, False, False, False, False, False, False, True, 0, True, True, True)
>>> flags.supports_symbolic
True

Branchpoint

class pyudbm.binding.utap.Branchpoint(name: str, index: int, position: Position, symbol: Symbol)[source]

Immutable snapshot of one branchpoint declared inside a template.

Parameters:

name (str) – Branchpoint name.
index (int) – Native branchpoint index within the template.
position (Position) – Source position of the branchpoint.
symbol (Symbol) – Symbol information for the branchpoint.

Example:

>>> from pyudbm.binding.utap import Branchpoint, loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> symbol = document.templates[0].locations[0].symbol
>>> Branchpoint("B", 0, symbol.position, symbol).name
'B'

Location

class pyudbm.binding.utap.Location(name: str, index: int, position: Position, symbol: Symbol, name_expression: Expression, invariant: Expression, exp_rate: Expression, cost_rate: Expression, is_urgent: bool, is_committed: bool)[source]

Immutable snapshot of one template location.

Expression fields such as invariant and cost_rate are already converted to Python expression snapshots.

Parameters:

name (str) – Location name.
index (int) – Native location index within the template.
position (Position) – Source position of the location.
symbol (Symbol) – Symbol information for the location.
name_expression (Expression) – Optional name expression payload.
invariant (Expression) – Invariant expression.
exp_rate (Expression) – Exponential-rate expression.
cost_rate (Expression) – Cost-rate expression.
is_urgent (bool) – Whether the location is urgent.
is_committed (bool) – Whether the location is committed.

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> document.templates[0].locations[0].name
'S'

Edge

class pyudbm.binding.utap.Edge(index: int, control: bool, action_name: str, source_name: str, source_kind: str, target_name: str, target_kind: str, guard: Expression, assign: Expression, sync: Expression, prob: Expression, select_text: str, select_symbols: Tuple[Symbol, ...], select_values: Tuple[int, ...])[source]

Immutable snapshot of one template edge.

Guard, assignment, synchronization, probability, and select metadata are exposed through converted expression and symbol snapshots.

Parameters:

index (int) – Native edge index within the template.
control (bool) – Whether the edge is controllable.
action_name (str) – Edge action name.
source_name (str) – Source node name.
source_kind (str) – Source node kind.
target_name (str) – Target node name.
target_kind (str) – Target node kind.
guard (Expression) – Guard expression.
assign (Expression) – Assignment expression.
sync (Expression) – Synchronization expression.
prob (Expression) – Probability expression.
select_text (str) – Raw select clause text.
select_symbols (Tuple[Symbol, ...]) – Symbols introduced by the select clause.
select_values (Tuple[int, ...]) – Native select values associated with the symbols.

Example:

>>> from pyudbm.binding.utap import Edge, loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> location = document.templates[0].locations[0]
>>> edge = Edge(
...     0,
...     False,
...     "",
...     "S",
...     "location",
...     "S",
...     "location",
...     location.invariant,
...     location.invariant,
...     location.invariant,
...     location.invariant,
...     "",
...     (),
...     (),
... )
>>> edge.source_name
'S'

Query

class pyudbm.binding.utap.Query(formula: str, comment: str, options: Tuple[Option, ...], expectation: Expectation, location: str)[source]

One query entry stored in the parsed document.

Parameters:

formula (str) – Query formula text.
comment (str) – Query comment text.
options (Tuple[Option, ...]) – Query-local option entries.
expectation (Expectation) – Stored expectation metadata.
location (str) – Query source-location text.

Example:

>>> from pyudbm.binding.utap import Expectation, Option, Query
>>> query = Query("A[] !deadlock", "safety", (Option("trace", "short"),), Expectation("Symbolic", "True", "", ()), "")
>>> query.formula
'A[] !deadlock'

ParsedQueryExpectation

class pyudbm.binding.utap.ParsedQueryExpectation(result_kind: str, status: str | None, value: float | None, time_ms: int, mem_kib: int)[source]

Structured expectation metadata produced by query parsing helpers.

Parameters:

result_kind (str) – Parsed result kind.
status (str or None) – Parsed expectation status, if present.
value (float or None) – Parsed expectation numeric value, if present.
time_ms (int) – Expected time budget or measurement in milliseconds.
mem_kib (int) – Expected memory budget or measurement in KiB.

Example:

>>> from pyudbm.binding.utap import ParsedQueryExpectation
>>> expectation = ParsedQueryExpectation("Symbolic", "True", None, 10, 32)
>>> expectation.time_ms
10

ParsedQuery

class pyudbm.binding.utap.ParsedQuery(line: int, no: int, builder: str, text: str, quantifier: str, options: Tuple[Option, ...], expression: Expression, is_smc: bool, declaration: str, result_type: str, expectation: ParsedQueryExpectation | None)[source]

Immutable snapshot of one query parsed against a document context.

The parsed expression tree, detected builder, and optional expectation metadata are all detached from the native parsing result.

Parameters:

line (int) – One-based source line of the query.
no (int) – Query number reported by UTAP.
builder (str) – Selected query builder name.
text (str) – Original query text.
quantifier (str) – Top-level query quantifier.
options (Tuple[Option, ...]) – Parsed query options.
expression (Expression) – Parsed query expression tree.
is_smc (bool) – Whether the query is an SMC query.
declaration (str) – Query-local declaration block.
result_type (str) – Parsed query result type.
expectation (ParsedQueryExpectation or None) – Structured expectation metadata, if present.

Example:

>>> from pyudbm.binding.utap import loads_xta, parse_query
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> query = parse_query("A[] not deadlock", document, builder="property")[0]
>>> query.quantifier
'AG'

Process

class pyudbm.binding.utap.Process(name: str, index: int, position: Position, template_name: str, parameters: str, arguments: str, mapping: str, argument_count: int, unbound_count: int, restricted_symbols: Tuple[Symbol, ...])[source]

Immutable snapshot of one instantiated process in the system section.

Parameters:

name (str) – Process instance name.
index (int) – Native process index.
position (Position) – Source position of the process declaration.
template_name (str) – Name of the referenced template.
parameters (str) – Template parameter text.
arguments (str) – Instantiation argument text.
mapping (str) – Native process mapping text.
argument_count (int) – Number of supplied arguments.
unbound_count (int) – Number of unresolved parameters.
restricted_symbols (Tuple[Symbol, ...]) – Restricted symbols associated with the process.

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> document.processes[0].name
'P1'

Template

class pyudbm.binding.utap.Template(name: str, index: int, position: Position, parameter: str, declaration: str, init_name: str, type: str, mode: str, is_ta: bool, is_instantiated: bool, dynamic: bool, is_defined: bool, locations: Tuple[Location, ...], branchpoints: Tuple[Branchpoint, ...], edges: Tuple[Edge, ...])[source]

Immutable snapshot of one UTAP template.

Locations, branchpoints, and edges are eagerly converted into immutable nested snapshots.

Parameters:

name (str) – Template name.
index (int) – Native template index.
position (Position) – Source position of the template.
parameter (str) – Template parameter declaration text.
declaration (str) – Template declaration text currently exposed by the high-level wrapper.
init_name (str) – Name of the initial location.
type (str) – Template type name.
mode (str) – Template mode string.
is_ta (bool) – Whether the template is a timed automaton.
is_instantiated (bool) – Whether the template is instantiated in the system section.
dynamic (bool) – Whether the template is dynamic.
is_defined (bool) – Whether the template is fully defined.
locations (Tuple[Location, ...]) – Template locations.
branchpoints (Tuple[Branchpoint, ...]) – Template branchpoints.
edges (Tuple[Edge, ...]) – Template edges.

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> document.templates[0].name
'P'

ModelDocument

class pyudbm.binding.utap.ModelDocument(native_document: _NativeDocument)[source]

Immutable Python snapshot of one parsed UTAP document.

Child objects are detached immutable snapshots created eagerly from the native document payload. The owning native document is still retained on this object for later phases, but nested wrappers do not depend on it for field access.

The public attributes templates, processes, queries, options, features, errors, warnings, and modified are populated eagerly during initialization.

Variables:

templates – Parsed template snapshots.
processes – Parsed process snapshots.
queries – Stored model queries.
options – Top-level query option entries.
features – Document feature and capability summary.
errors – Parser or semantic errors reported by UTAP.
warnings – Parser or semantic warnings reported by UTAP.
modified – Whether UTAP reports the document as modified.

Example:

>>> from pyudbm.binding.utap import ModelDocument, loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> isinstance(document, ModelDocument)
True

__init__(native_document: _NativeDocument)[source]

Initialize one immutable document snapshot from a native UTAP document.

Parameters:: native_document (_NativeDocument) – Parsed native document returned by pyudbm.binding._utap.
Returns:: None.
Return type:: None

Example:

>>> from pyudbm.binding._utap import loads_xta as native_loads_xta
>>> from pyudbm.binding.utap import ModelDocument
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = ModelDocument(native_loads_xta(xta))
>>> document.templates[0].name
'P'

__repr__() → str[source]: Return repr(self).

property after_update_text: str

Return the after_update declaration text, if present.

Returns:: after_update declaration text.
Return type:: str

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> loads_xta(xta).after_update_text
''

property before_update_text: str

Return the before_update declaration text, if present.

Returns:: before_update declaration text.
Return type:: str

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> loads_xta(xta).before_update_text
''

capability_summary() → Mapping[str, bool][source]

Return the coarse-grained capability summary.

Returns:: Mapping with supports_symbolic, supports_stochastic, and supports_concrete entries.
Return type:: Mapping[str, bool]

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> loads_xta(xta).capability_summary()["supports_concrete"]
True

property channel_priority_texts: Tuple[str, ...]

Return channel-priority declarations.

Returns:: Channel-priority declaration texts.
Return type:: Tuple[str, …]

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> loads_xta(xta).channel_priority_texts
()

dump(path: Any) → None[source]

Write the XML serialization of the document to path.

Parameters:: path (Any) – Output path.
Returns:: None.
Return type:: None

Example:

>>> import os
>>> import tempfile
>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> with tempfile.TemporaryDirectory() as tempdir:
...     path = os.path.join(tempdir, "dump.xml")
...     document.dump(path)
...     os.path.isfile(path)
True

dump_ta(path: Any, *, indent: int | None = 4) → None[source]

Write the old-syntax upstream-pretty-printed rendering to path.

Parameters:

path (Any) – Output path.
indent (Optional[int]) – Number of spaces used to replace each upstream tab indentation character. Pass None to preserve literal \t output from UTAP.

Returns:

None.

Return type:

None

dump_xta(path: Any, *, include_builtin_preamble: bool = False, indent: int | None = 4) → None[source]

Write the upstream-pretty-printed XTA rendering to path.

Parameters:

path (Any) – Output path.
include_builtin_preamble (bool) – Whether to keep the official UTAP built-in declaration preamble in the written XTA text.
indent (Optional[int]) – Number of spaces used to replace each upstream tab indentation character. Pass None to preserve literal \t output from UTAP.

Returns:

None.

Return type:

None

dumps() → str[source]

Serialize the document to one XML string.

The native UTAP writer is used as the structural base. Global declarations and query blocks are then patched back into the emitted XML so the round-tripped text matches the higher-level Python view.

Returns:: XML serialization of the current snapshot.
Return type:: str
Raises:: RuntimeError – If the native XML output does not contain the expected <declaration> or </nta> structure.

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> document.dumps().startswith("<?xml")
True

feature_summary() → Mapping[str, Any][source]

Return feature flags as a plain mapping.

Keys follow MAPPED_FIELDS["FeatureFlags"].

Returns:: Feature-flag mapping.
Return type:: Mapping[str, Any]

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> loads_xta(xta).feature_summary()["supports_symbolic"]
True

property global_clock_names: Tuple[str, ...]

Return the global clock names reported by the native document.

Returns:: Global clock names.
Return type:: Tuple[str, …]

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> loads_xta(xta).global_clock_names
('x',)

property global_declarations: str

Return the global declaration block as plain text.

Returns:: Global declarations.
Return type:: str

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> "clock x;" in document.global_declarations
True

load_query(path: Any, *, builder: str = 'auto') → Tuple[ParsedQuery, ...][source]

Parse queries from path against this document.

Parameters:

path (Any) – Query-file path accepted by the native binding.
builder (str) – Query parser selection such as "auto" or a concrete builder name.

Returns:

Parsed query snapshots.

Return type:

Tuple[ParsedQuery, …]

Raises:

FileNotFoundError – If path does not exist.
pyudbm.binding._utap.ParseError – If UTAP fails to parse the query file.

Example:

>>> import os
>>> import tempfile
>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> with tempfile.TemporaryDirectory() as tempdir:
...     path = os.path.join(tempdir, "model.q")
...     with open(path, "w", encoding="utf-8") as file:
...         _ = file.write("A[] not deadlock")
...     document.load_query(path, builder="property")[0].quantifier
'AG'

loads_query(buffer: str, *, builder: str = 'auto') → Tuple[ParsedQuery, ...][source]

Parse queries from an in-memory string against this document.

Parameters:

buffer (str) – Query text buffer.
builder (str) – Query parser selection such as "auto" or a concrete builder name.

Returns:

Parsed query snapshots.

Return type:

Tuple[ParsedQuery, …]

Raises:

pyudbm.binding._utap.ParseError – If UTAP fails to parse the query text.

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> document.loads_query("A[] not deadlock", builder="property")[0].builder
'property'

parse_query(buffer: str, *, builder: str = 'auto') → Tuple[ParsedQuery, ...][source]

Parse inline query text against this document.

This is a convenience alias over the native inline query parser.

Parameters:

buffer (str) – Query text buffer.
builder (str) – Query parser selection such as "auto" or a concrete builder name.

Returns:

Parsed query snapshots.

Return type:

Tuple[ParsedQuery, …]

Raises:

pyudbm.binding._utap.ParseError – If UTAP fails to parse the query text.

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> document.parse_query("A[] not deadlock", builder="property")[0].text
'A[] !deadlock'

pretty() → str[source]

Return a JSON-formatted summary of the document.

This helper is intended for debugging, snapshots, and human inspection, not as a stable machine-readable interchange contract.

Returns:: Pretty-printed JSON summary.
Return type:: str

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> '"templates"' in loads_xta(xta).pretty()
True

property template_clock_names: Mapping[str, Tuple[str, ...]]

Return per-template clock names.

Returns:: Mapping {template_name: (clock_names...)}.
Return type:: Mapping[str, Tuple[str, …]]

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> loads_xta(xta).template_clock_names
{'P': ()}

to_ta(*, indent: int | None = 4) → str[source]

Render the document using the upstream pretty printer in old-syntax mode.

This is the same official pretty-printing path as to_xta(), but with newxta=False when feeding XML back into UTAP.

Parameters:: indent (Optional[int]) – Number of spaces used to replace each upstream tab indentation character. Pass None to preserve literal \t output from UTAP.
Returns:: Textual TA rendering of the current document.
Return type:: str

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> "process P()" in loads_xta(xta).to_ta()
True

to_xml() → str[source]

Return the XML serialization of the document.

This is a convenience alias for dumps().

Returns:: XML serialization of the current snapshot.
Return type:: str

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> document.to_xml() == document.dumps()
True

to_xta(*, include_builtin_preamble: bool = False, indent: int | None = 4) → str[source]

Render the document as textual XTA using the upstream UTAP pretty printer.

This path goes through dumps() first and then reparses the resulting XML through the official UTAP PrettyPrinter. It therefore follows the current high-level XML semantics of this wrapper rather than the raw native writer.

By default the built-in declaration preamble injected by the official UTAP XML parser in new-syntax mode is removed again before returning the result. Set include_builtin_preamble=True to keep that official preamble in the returned text.

Important limitation: upstream pretty-printing focuses on the model text itself. Query formulas and comments may be emitted as comments, while XML-only query metadata such as query options and expectations are not preserved as a machine-readable textual round-trip format.

Parameters:

include_builtin_preamble (bool) – Whether to keep the official UTAP built-in declaration preamble in the returned XTA text.
indent (Optional[int]) – Number of spaces used to replace each upstream tab indentation character. Pass None to preserve literal \t output from UTAP.

Returns:

Textual XTA rendering of the current document.

Return type:

str

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> "process P()" in loads_xta(xta).to_xta()
True

write_xml(path: Any) → None[source]

Write the native XML serialization to path.

This delegates directly to the underlying native document writer, before Python-side query reinjection performed by dumps().

Parameters:: path (Any) – Output path accepted by the native binding.
Returns:: None.
Return type:: None

Example:

>>> import os
>>> import tempfile
>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> with tempfile.TemporaryDirectory() as tempdir:
...     path = os.path.join(tempdir, "model.xml")
...     document.write_xml(path)
...     os.path.isfile(path)
True

builtin_declarations

pyudbm.binding.utap.builtin_declarations() → str[source]

Return the built-in declaration block injected by the UTAP parser.

Returns:: Built-in declarations understood by the parser.
Return type:: str

Example:

>>> from pyudbm.binding.utap import builtin_declarations
>>> "INT32_MAX" in builtin_declarations()
True

textual_builtin_preamble

pyudbm.binding.utap.textual_builtin_preamble(*, newxta: bool = True) → str[source]

Return the official textual built-in preamble emitted by UTAP.

This uses the upstream UTAP declaration parser together with the official PrettyPrinter, so the returned string matches the exact preamble that parse_XML_* injects in new-syntax mode before user declarations.

Parameters:: newxta (bool) – Whether to request the new-syntax textual preamble. Old syntax does not prepend built-in declarations and therefore returns an empty string.
Returns:: Official textual built-in preamble.
Return type:: str

Example:

>>> from pyudbm.binding.utap import textual_builtin_preamble
>>> textual_builtin_preamble().startswith("const int INT8_MIN")
True
>>> textual_builtin_preamble(newxta=False)
''

load_query

pyudbm.binding.utap.load_query(path: Any, document: ModelDocument, *, builder: str = 'auto') → Tuple[ParsedQuery, ...][source]

Parse queries from path against a parsed model document.

Parameters:

path (Any) – Query-file path accepted by the native binding.
document (ModelDocument) – Parsed model document that provides the declaration context.
builder (str) – Query parser selection such as "auto" or a concrete builder name.

Returns:

Parsed query snapshots.

Return type:

Tuple[ParsedQuery, …]

Raises:

FileNotFoundError – If path does not exist.
TypeError – If document is not a ModelDocument.
pyudbm.binding._utap.ParseError – If UTAP fails to parse the query file.

Example:

>>> import os
>>> import tempfile
>>> from pyudbm.binding.utap import load_query, loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> with tempfile.TemporaryDirectory() as tempdir:
...     path = os.path.join(tempdir, "model.q")
...     with open(path, "w", encoding="utf-8") as file:
...         _ = file.write("A[] not deadlock")
...     load_query(path, document, builder="property")[0].quantifier
'AG'

loads_query

pyudbm.binding.utap.loads_query(buffer: str, document: ModelDocument, *, builder: str = 'auto') → Tuple[ParsedQuery, ...][source]

Parse queries from an in-memory string against a parsed model document.

Parameters:

buffer (str) – Query text buffer.
document (ModelDocument) – Parsed model document that provides the declaration context.
builder (str) – Query parser selection such as "auto" or a concrete builder name.

Returns:

Parsed query snapshots.

Return type:

Tuple[ParsedQuery, …]

Raises:

TypeError – If document is not a ModelDocument.
pyudbm.binding._utap.ParseError – If UTAP fails to parse the query text.

Example:

>>> from pyudbm.binding.utap import loads_query, loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> loads_query("A[] not deadlock", document, builder="property")[0].builder
'property'

parse_query

pyudbm.binding.utap.parse_query(buffer: str, document: ModelDocument, *, builder: str = 'auto') → Tuple[ParsedQuery, ...][source]

Parse inline query text against a parsed model document.

Parameters:

buffer (str) – Query text buffer.
document (ModelDocument) – Parsed model document that provides the declaration context.
builder (str) – Query parser selection such as "auto" or a concrete builder name.

Returns:

Parsed query snapshots.

Return type:

Tuple[ParsedQuery, …]

Raises:

TypeError – If document is not a ModelDocument.
pyudbm.binding._utap.ParseError – If UTAP fails to parse the query text.

Example:

>>> from pyudbm.binding.utap import loads_xta, parse_query
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> document = loads_xta(xta)
>>> parse_query("A[] not deadlock", document, builder="property")[0].text
'A[] !deadlock'

load_xml

pyudbm.binding.utap.load_xml(path: Any, newxta: bool = True, strict: bool = True, libpaths: Iterable[Any] = ()) → ModelDocument[source]

Parse one XML model file into a ModelDocument.

Parameters:

path (Any) – XML model path.
newxta (bool) – Whether to enable the newxta parser mode.
strict (bool) – Whether to request strict parsing.
libpaths (Iterable[Any]) – Additional include-library search paths.

Returns:

Parsed immutable document snapshot.

Return type:

ModelDocument

Raises:

FileNotFoundError – If path does not exist.
pyudbm.binding._utap.ParseError – If UTAP fails to parse the XML model.

Example:

>>> import os
>>> import tempfile
>>> from pyudbm.binding.utap import load_xml
>>> xml_text = '''<?xml version="1.0" encoding="utf-8"?>
... <!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
... <nta>
...   <declaration>clock x;</declaration>
...   <template>
...     <name x="0" y="0">P</name>
...     <location id="id0" x="0" y="0">
...       <name x="0" y="0">Init</name>
...     </location>
...     <init ref="id0"/>
...   </template>
...   <system>P1 = P();
... system P1;</system>
... </nta>
... '''
>>> with tempfile.TemporaryDirectory() as tempdir:
...     path = os.path.join(tempdir, "model.xml")
...     with open(path, "w", encoding="utf-8") as file:
...         _ = file.write(xml_text)
...     load_xml(path).templates[0].name
'P'

loads_xml

pyudbm.binding.utap.loads_xml(buffer: str, newxta: bool = True, strict: bool = True, libpaths: Iterable[Any] = ()) → ModelDocument[source]

Parse one XML model string into a ModelDocument.

Parameters:

buffer (str) – XML model text.
newxta (bool) – Whether to enable the newxta parser mode.
strict (bool) – Whether to request strict parsing.
libpaths (Iterable[Any]) – Additional include-library search paths.

Returns:

Parsed immutable document snapshot.

Return type:

ModelDocument

Raises:

pyudbm.binding._utap.ParseError – If UTAP fails to parse the XML model.

Example:

>>> from pyudbm.binding.utap import loads_xml
>>> xml_text = '''<?xml version="1.0" encoding="utf-8"?>
... <!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
... <nta>
...   <declaration>clock x;</declaration>
...   <template>
...     <name x="0" y="0">P</name>
...     <location id="id0" x="0" y="0">
...       <name x="0" y="0">Init</name>
...     </location>
...     <init ref="id0"/>
...   </template>
...   <system>P1 = P();
... system P1;</system>
... </nta>
... '''
>>> loads_xml(xml_text).processes[0].name
'P1'

load_xta

pyudbm.binding.utap.load_xta(path: Any, newxta: bool = True, strict: bool = True) → ModelDocument[source]

Parse one textual XTA model file into a ModelDocument.

Parameters:

path (Any) – XTA model path.
newxta (bool) – Whether to enable the newxta parser mode.
strict (bool) – Whether to request strict parsing.

Returns:

Parsed immutable document snapshot.

Return type:

ModelDocument

Raises:

FileNotFoundError – If path does not exist.
pyudbm.binding._utap.ParseError – If UTAP fails to parse the XTA model.

Example:

>>> import os
>>> import tempfile
>>> from pyudbm.binding.utap import load_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> with tempfile.TemporaryDirectory() as tempdir:
...     path = os.path.join(tempdir, "model.xta")
...     with open(path, "w", encoding="utf-8") as file:
...         _ = file.write(xta)
...     load_xta(path).templates[0].name
'P'

loads_xta

pyudbm.binding.utap.loads_xta(buffer: str, newxta: bool = True, strict: bool = True) → ModelDocument[source]

Parse one textual XTA model string into a ModelDocument.

Parameters:

buffer (str) – XTA model text.
newxta (bool) – Whether to enable the newxta parser mode.
strict (bool) – Whether to request strict parsing.

Returns:

Parsed immutable document snapshot.

Return type:

ModelDocument

Raises:

pyudbm.binding._utap.ParseError – If UTAP fails to parse the XTA model.

Example:

>>> from pyudbm.binding.utap import loads_xta
>>> xta = '''clock x;
... process P() {
... state S;
... init S;
... }
... P1 = P();
... system P1;
... '''
>>> loads_xta(xta).processes[0].name
'P1'

pyudbm.binding.utap

__all__

MAPPED_FIELDS

MAPPED_FIELD_NOTES

UNMAPPED_FIELDS

UNMAPPED_FIELD_REASONS

Position

Option

Resource

Expectation

TypeInfo

Symbol

Expression

Diagnostic

FeatureFlags

Branchpoint

Location

Edge

Query

ParsedQueryExpectation

ParsedQuery

Process

Template

ModelDocument

builtin_declarations

textual_builtin_preamble

load_query

loads_query

parse_query

load_xml

loads_xml

load_xta

loads_xta

all