pyudbm.binding.utap_builder

Python-first UTAP builder surface for authoring, patching, and exporting ModelDocument instances without writing XML directly.

This module provides two public styles:

mutable chain builders for interactive authoring and patching (ModelBuilder, TemplateBuilder);
immutable spec dataclasses for deterministic generation and snapshots (ModelSpec, TemplateSpec, LocationSpec, EdgeSpec, QuerySpec).

Both styles normalize into one payload and delegate final native model construction to the official UTAP-backed helper in pyudbm.binding._utap.

Note

This API is intentionally LLM-friendly: prefer semantic selectors (where=...), use inspect() and list_*() to retrieve stable snapshots and explicit indexes, and keep index operations as fallback only.

Note

Patch operations fail loudly by design: selector miss and selector ambiguity both raise clear errors, and ambiguity errors include candidate indexes for deterministic recovery in automation pipelines.

Example:

>>> from pyudbm.binding import ModelBuilder
>>> document = (
...     ModelBuilder()
...     .clock("x")
...     .template("P")
...         .location("Init", initial=True)
...         .location("Done")
...         .edge("Init", "Done", when="x >= 1")
...         .end()
...     .process("P1", "P")
...     .system("P1")
...     .query("A[] not deadlock")
...     .build()
... )
>>> document.templates[0].name
'P'

Example:

>>> builder = ModelBuilder.from_document(document)
>>> snapshot = builder.inspect()
>>> builder.update_query(where={"formula": "A[] not deadlock"}, comment="patched by pipeline")
>>> with builder.edit_template("P") as template:
...     template.update_edge(where={"source": "Init", "target": "Done"}, when="x >= 2")
>>> patched = builder.build()
>>> len(snapshot["templates"]) >= 1
True

Example:

>>> from pyudbm.binding.utap_builder import LocationSpec, ModelSpec, TemplateSpec, build_model
>>> spec_document = build_model(
...     ModelSpec(
...         templates=(TemplateSpec("P", locations=(LocationSpec("Init", initial=True),)),),
...         processes=(("P1", "P", ()),),
...         system_process_names=("P1",),
...     )
... )
>>> spec_document.processes[0].name
'P1'

all

pyudbm.binding.utap_builder.__all__ = ['EdgeSpec', 'LocationSpec', 'ModelBuilder', 'ModelSpec', 'QuerySpec', 'TemplateBuilder', 'TemplateSpec', 'build_model']

Built-in mutable sequence.

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

LocationSpec

class pyudbm.binding.utap_builder.LocationSpec(name: str, initial: bool = False, invariant: str = '', urgent: bool = False, committed: bool = False)[source]

Immutable specification of one template location.

Parameters:

name (str) – Location name.
initial (bool) – Whether this is the initial location.
invariant (str) – Optional invariant text.
urgent (bool) – Whether the location is urgent.
committed (bool) – Whether the location is committed.

Example:

>>> from pyudbm.binding.utap_builder import LocationSpec
>>> LocationSpec("Init", initial=True).initial
True

EdgeSpec

class pyudbm.binding.utap_builder.EdgeSpec(source: str, target: str, guard: str = '', sync: str = '', update: str = '')[source]

Immutable specification of one template edge.

guard, sync, and update are the normalized textual fields ultimately consumed by the native builder.

Parameters:

source (str) – Source location name.
target (str) – Target location name.
guard (str) – Optional normalized guard text.
sync (str) – Optional normalized synchronisation text.
update (str) – Optional normalized assignment text.

Example:

>>> from pyudbm.binding.utap_builder import EdgeSpec
>>> EdgeSpec("Idle", "Busy", sync="tick!").sync
'tick!'

QuerySpec

class pyudbm.binding.utap_builder.QuerySpec(formula: str, comment: str = '', options: Tuple[Option, ...] = (), expectation: Expectation | None = None, location: str = '')[source]

Immutable specification of one model query.

Parameters:

formula (str) – Query formula text.
comment (str) – Optional query comment text.
options (Tuple[Option, ...]) – Query-local option entries.
expectation (Expectation or None) – Optional expectation metadata.
location (str) – Optional query location text.

Example:

>>> from pyudbm.binding.utap_builder import QuerySpec
>>> QuerySpec("A[] not deadlock").formula
'A[] not deadlock'

TemplateSpec

class pyudbm.binding.utap_builder.TemplateSpec(name: str, parameters: str = '', declarations: Tuple[str, ...] = (), locations: Tuple[LocationSpec, ...] = (), edges: Tuple[EdgeSpec, ...] = ())[source]

Immutable specification of one template.

Parameters:

name (str) – Template name.
parameters (str) – Optional raw parameter text.
declarations (Tuple[str, ...]) – Raw local declaration blocks.
locations (Tuple[LocationSpec, ...]) – Template locations.
edges (Tuple[EdgeSpec, ...]) – Template edges.

Example:

>>> from pyudbm.binding.utap_builder import LocationSpec, TemplateSpec
>>> spec = TemplateSpec("P", locations=(LocationSpec("Init", initial=True),))
>>> spec.name
'P'

ModelSpec

class pyudbm.binding.utap_builder.ModelSpec(declarations: Tuple[str, ...] = (), templates: Tuple[TemplateSpec, ...] = (), processes: Tuple[Tuple[str, str, Tuple[str, ...]], ...] = (), system_process_names: Tuple[str, ...] = (), queries: Tuple[QuerySpec, ...] = ())[source]

Immutable specification of one UTAP model.

processes uses tuples of the shape (process_name, template_name, arguments) where arguments is a tuple of raw textual argument expressions.

Parameters:

declarations (Tuple[str, ...]) – Raw global declaration blocks.
templates (Tuple[TemplateSpec, ...]) – Template specifications.
processes (Tuple[Tuple[str, str, Tuple[str, ...]], ...]) – Process-instantiation tuples.
system_process_names (Tuple[str, ...]) – Process names listed in the system line.
queries (Tuple[QuerySpec, ...]) – Query specifications.

Example:

>>> from pyudbm.binding.utap_builder import LocationSpec, ModelSpec, TemplateSpec
>>> spec = ModelSpec(
...     declarations=("clock x;",),
...     templates=(TemplateSpec("P", locations=(LocationSpec("Init", initial=True),)),),
...     processes=(("P1", "P", ()),),
...     system_process_names=("P1",),
... )
>>> spec.system_process_names
('P1',)

ModelBuilder

class pyudbm.binding.utap_builder.ModelBuilder[source]

Build one UTAP model from lightweight Python authoring calls.

The builder focuses on the common small-model path: global declarations, templates, processes, system composition, and queries. Calling build() returns a public ModelDocument.

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> document = (
...     ModelBuilder()
...     .clock("x")
...     .template("P")
...         .location("Init", initial=True)
...         .end()
...     .process("P1", "P")
...     .system("P1")
...     .build()
... )
>>> document.templates[0].name
'P'

__init__()[source]

Initialize one empty model builder.

Returns:: None.
Return type:: None

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> isinstance(ModelBuilder(), ModelBuilder)
True

build() → ModelDocument[source]

Build the current model into one public ModelDocument.

Returns:: Parsed public model document.
Return type:: ModelDocument

Example:

>>> from pyudbm.binding import ModelBuilder, ModelDocument
>>> document = (
...     ModelBuilder()
...     .clock("x")
...     .template("P")
...         .location("Init", initial=True)
...         .end()
...     .process("P1", "P")
...     .system("P1")
...     .build()
... )
>>> isinstance(document, ModelDocument)
True

chan(*names: str, broadcast: bool = False, urgent: bool = False) → ModelBuilder[source]

Append one channel declaration for one or more names.

Parameters:

names (str) – Channel names declared in one statement.
broadcast (bool) – Whether the declaration is for broadcast channels.
urgent (bool) – Whether the declaration is for urgent channels.

Returns:

The current builder.

Return type:

ModelBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().chan("tick", urgent=True)
>>> isinstance(builder, ModelBuilder)
True

clock(*names: str) → ModelBuilder[source]

Append one clock declaration for one or more names.

Parameters:: names (str) – Clock names declared in one statement.
Returns:: The current builder.
Return type:: ModelBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().clock("x", "y")
>>> isinstance(builder, ModelBuilder)
True

declaration(text: str) → ModelBuilder[source]

Append one raw global declaration block.

Parameters:: text (str) – Declaration text appended to the global declaration section.
Returns:: The current builder.
Return type:: ModelBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().declaration("const int N = 1;")
>>> isinstance(builder, ModelBuilder)
True

edit_template(name: str) → TemplateBuilder[source]

Open one existing template for incremental edits.

This is intended for import-edit-export workflows started with from_document().

Parameters:: name (str) – Existing template name.
Returns:: Template builder bound to the existing template state.
Return type:: TemplateBuilder
Raises:: ValueError – If the template does not exist.

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> document = (
...     ModelBuilder()
...     .template("P")
...         .location("Init", initial=True)
...         .end()
...     .process("P1", "P")
...     .system("P1")
...     .build()
... )
>>> template = ModelBuilder.from_document(document).edit_template("P")
>>> isinstance(template, TemplateBuilder)
True

classmethod from_document(document: ModelDocument) → ModelBuilder[source]

Rebuild one mutable builder from a public ModelDocument.

This import path is limited to the current builder surface. Template branchpoints, document-level options, and other unsupported features are rejected with clear errors instead of being silently discarded.

Parameters:: document (ModelDocument) – Imported public document snapshot.
Returns:: Builder initialized from the imported document.
Return type:: ModelBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> document = (
...     ModelBuilder()
...     .clock("x")
...     .template("P")
...         .location("Init", initial=True)
...         .end()
...     .process("P1", "P")
...     .system("P1")
...     .build()
... )
>>> imported = ModelBuilder.from_document(document)
>>> isinstance(imported, ModelBuilder)
True

inspect() → dict[source]

Return one full JSON-friendly snapshot of current builder state.

Returns:: Full builder snapshot.
Return type:: dict

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> snapshot = ModelBuilder().template("P").location("Init", initial=True).end().inspect()
>>> snapshot["templates"][0]["name"]
'P'

integer(name: str, *, lower: object | None = None, upper: object | None = None, init: object | None = None, const: bool = False) → ModelBuilder[source]

Append one integer declaration.

When both lower and upper are provided, the declaration uses the bounded form int[min,max] name. When const=True, an initializer is required.

Parameters:

name (str) – Integer variable name.
lower (object or None) – Optional lower bound.
upper (object or None) – Optional upper bound.
init (object or None) – Optional initializer expression.
const (bool) – Whether to declare a constant integer.

Returns:

The current builder.

Return type:

ModelBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().integer("count", lower=0, upper=3, init=1)
>>> isinstance(builder, ModelBuilder)
True

list_edges(template: str) → Tuple[dict, ...][source]

List edges of one template with explicit indexes.

Parameters:: template (str) – Template name.
Returns:: Edge snapshots.
Return type:: Tuple[dict, …]

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().template("P").location("Init", initial=True).location("Done").edge("Init", "Done").end()
>>> builder.list_edges("P")[0]["source"]
'Init'

list_locations(template: str) → Tuple[dict, ...][source]

List locations of one template with explicit indexes.

Parameters:: template (str) – Template name.
Returns:: Location snapshots.
Return type:: Tuple[dict, …]

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().template("P").location("Init", initial=True).end()
>>> builder.list_locations("P")[0]["name"]
'Init'

list_processes() → Tuple[dict, ...][source]

List current process entries with explicit indexes.

Returns:: Process snapshots.
Return type:: Tuple[dict, …]

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().template("P").location("Init", initial=True).end().process("P1", "P")
>>> builder.list_processes()[0]["name"]
'P1'

list_queries() → Tuple[dict, ...][source]

List current query entries with explicit indexes.

Returns:: Query snapshots.
Return type:: Tuple[dict, …]

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().query("A[] not deadlock")
>>> builder.list_queries()[0]["formula"]
'A[] not deadlock'

list_templates() → Tuple[dict, ...][source]

List current template entries with explicit indexes.

Returns:: Template snapshots.
Return type:: Tuple[dict, …]

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().template("P").location("Init", initial=True).end()
>>> builder.list_templates()[0]["name"]
'P'

process(name: str, template: str, *arguments: object) → ModelBuilder[source]

Append one process instantiation line.

Parameters:

name (str) – Process instance name.
template (str) – Template name referenced by the process.
arguments (object) – Optional raw argument texts rendered with str().

Returns:

The current builder.

Return type:

ModelBuilder

Raises:

ValueError – If the process name already exists.

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = (
...     ModelBuilder()
...     .template("P")
...         .location("Init", initial=True)
...         .end()
...     .process("P1", "P")
... )
>>> isinstance(builder, ModelBuilder)
True

query(formula: str, *, comment: str = '', options: Iterable[Option | Tuple[str, str]] = (), expectation: Expectation | None = None, location: str = '') → ModelBuilder[source]

Append one model query.

Parameters:

formula (str) – Query formula text.
comment (str) – Optional query comment text.
options (Iterable[Option or Tuple[str, str]]) – Optional query-local options.
expectation (Expectation or None) – Optional structured expectation metadata.
location (str) – Optional query location text.

Returns:

The current builder.

Return type:

ModelBuilder

Example:

>>> from pyudbm.binding import Expectation
>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().query("A[] not deadlock", expectation=Expectation("", "", "", ()))
>>> isinstance(builder, ModelBuilder)
True

remove_process(name: str) → ModelBuilder[source]

Remove one process instantiation.

The process name is also removed from the current system order if present.

Parameters:: name (str) – Process name to remove.
Returns:: The current builder.
Return type:: ModelBuilder
Raises:: ValueError – If the process does not exist.

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = (
...     ModelBuilder()
...     .template("P")
...         .location("Init", initial=True)
...         .end()
...     .process("P1", "P")
...     .system("P1")
...     .remove_process("P1")
... )
>>> isinstance(builder, ModelBuilder)
True

remove_query(index: object = <object object>, *, where: object = <object object>) → ModelBuilder[source]

Remove one query by index or where selector.

Negative indexes follow normal Python indexing rules when index is used.

Parameters:

index (object) – Optional query index.
where (object) – Optional query selector mapping.

Returns:

The current builder.

Return type:

ModelBuilder

Note

For index-based deletion, retrieve current indexes from list_queries() or from the queries section returned by inspect().

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().query("A[] not deadlock").remove_query(where={"formula": "A[] not deadlock"})
>>> isinstance(builder, ModelBuilder)
True

remove_template(name: str) → ModelBuilder[source]

Remove one template and all processes instantiated from it.

Any matching process names are also removed from the current system declaration order.

Parameters:: name (str) – Template name to remove.
Returns:: The current builder.
Return type:: ModelBuilder
Raises:: ValueError – If the template does not exist.

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = (
...     ModelBuilder()
...     .template("P")
...         .location("Init", initial=True)
...         .end()
...     .process("P1", "P")
...     .system("P1")
...     .remove_template("P")
... )
>>> isinstance(builder, ModelBuilder)
True

set_declarations(*texts: str) → ModelBuilder[source]

Replace all global declaration blocks.

Passing no texts clears the current global declaration list.

Parameters:: texts (str) – Replacement declaration blocks.
Returns:: The current builder.
Return type:: ModelBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().clock("x").set_declarations("clock y;")
>>> isinstance(builder, ModelBuilder)
True

system(*process_names: str) → ModelBuilder[source]

Set the process order used by the system declaration.

Parameters:: process_names (str) – Process instance names listed in the system declaration.
Returns:: The current builder.
Return type:: ModelBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().system("P1")
>>> isinstance(builder, ModelBuilder)
True

template(name: str, *, parameters: str = '', declaration: str = '') → TemplateBuilder[source]

Start one template builder owned by this model.

Parameters:

name (str) – Template name.
parameters (str) – Optional raw template parameter text.
declaration (str) – Optional raw local declaration text.

Returns:

The template builder.

Return type:

TemplateBuilder

Raises:

ValueError – If the template name already exists.

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder, TemplateBuilder
>>> template = ModelBuilder().template("P")
>>> isinstance(template, TemplateBuilder)
True

to_spec() → ModelSpec[source]

Export the current builder state as one public ModelSpec.

Returns:: Immutable model specification snapshot.
Return type:: ModelSpec

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder, ModelSpec
>>> spec = ModelBuilder().clock("x").template("P").location("Init", initial=True).end().to_spec()
>>> isinstance(spec, ModelSpec)
True

update_process(name: str, *, new_name: object = <object object>, template: object = <object object>, arguments: object = <object object>) → ModelBuilder[source]

Update one existing process instantiation.

Parameters:

name (str) – Existing process name.
new_name (object) – Optional replacement process name.
template (object) – Optional replacement template name.
arguments (object) – Optional replacement iterable of argument texts.

Returns:

The current builder.

Return type:

ModelBuilder

Raises:

ValueError – If the process does not exist or the new name is duplicated.

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = (
...     ModelBuilder()
...     .template("P")
...         .location("Init", initial=True)
...         .end()
...     .process("P1", "P")
...     .update_process("P1", new_name="Main")
... )
>>> isinstance(builder, ModelBuilder)
True

update_query(index: object = <object object>, *, where: object = <object object>, formula: object = <object object>, comment: object = <object object>, options: object = <object object>, expectation: object = <object object>, location: object = <object object>) → ModelBuilder[source]

Update one existing query by index or where selector.

Negative indexes follow normal Python indexing rules when index is used.

Parameters:

index (object) – Optional query index.
where (object) – Optional query selector mapping.
formula (object) – Optional replacement formula text.
comment (object) – Optional replacement comment text.
options (object) – Optional replacement query options.
expectation (object) – Optional replacement expectation metadata.
location (object) – Optional replacement query location text.

Returns:

The current builder.

Return type:

ModelBuilder

Note

When you choose the index path, get stable query indexes first via list_queries() or from the queries section returned by inspect().

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().query("A[] not deadlock").update_query(where={"formula": "A[] not deadlock"}, comment="patched")
>>> isinstance(builder, ModelBuilder)
True

update_template(name: str, *, new_name: object = <object object>, parameters: object = <object object>) → ModelBuilder[source]

Update one existing template header.

Parameters:

name (str) – Existing template name.
new_name (object) – Optional replacement template name.
parameters (object) – Optional replacement parameter text.

Returns:

The current builder.

Return type:

ModelBuilder

Raises:

ValueError – If the template does not exist or the new name is duplicated.

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = (
...     ModelBuilder()
...     .template("P")
...         .location("Init", initial=True)
...         .end()
...     .update_template("P", new_name="Worker")
... )
>>> isinstance(builder, ModelBuilder)
True

TemplateBuilder

class pyudbm.binding.utap_builder.TemplateBuilder(model_builder: ModelBuilder, state: _TemplateState)[source]

Build one template inside a ModelBuilder.

The template builder is name-first and string-friendly. Locations and edges are accumulated on the owning model until end() returns the parent builder again.

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder, TemplateBuilder
>>> template = ModelBuilder().template("P")
>>> isinstance(template, TemplateBuilder)
True

__enter__() → TemplateBuilder[source]

Enter the template-builder context manager.

Returns:: The current template builder.
Return type:: TemplateBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> with ModelBuilder().template("P") as template:
...     template.location("Init", initial=True)
>>> type(template).__name__
'TemplateBuilder'

__exit__(exc_type, exc_val, exc_tb) → None[source]

Leave the template-builder context manager.

Parameters:

exc_type (type or None) – Exception type, if any.
exc_val (BaseException or None) – Exception value, if any.
exc_tb (object) – Exception traceback, if any.

Returns:

None.

Return type:

None

__init__(model_builder: ModelBuilder, state: _TemplateState)[source]

Initialize one template builder owned by model_builder.

Parameters:

model_builder (ModelBuilder) – Owning model builder.
state (_TemplateState) – Mutable internal template state.

Returns:

None.

Return type:

None

declaration(text: str) → TemplateBuilder[source]

Append one raw local declaration block.

Parameters:: text (str) – Local declaration text.
Returns:: The current template builder.
Return type:: TemplateBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> template = ModelBuilder().template("P").declaration("int i;")
>>> type(template).__name__
'TemplateBuilder'

edge(source: str, target: str, *, when: str = '', guard: str = '', sync: str = '', send: str = '', recv: str = '', update: str = '', reset: object = ()) → TemplateBuilder[source]

Append one edge between two named locations.

when is an alias for guard. send and recv are sugar for sync="name!" and sync="name?". reset is sugar for a comma-joined assignment list such as {"x": 0}.

Parameters:

source (str) – Source location name.
target (str) – Target location name.
when (str) – Optional guard alias.
guard (str) – Optional guard text.
sync (str) – Optional synchronisation text such as "tick?".
send (str) – Optional send-side synchronisation sugar.
recv (str) – Optional receive-side synchronisation sugar.
update (str) – Optional assignment text.
reset (object) – Optional mapping or pair-sequence rendered into an assignment list.

Returns:

The current template builder.

Return type:

TemplateBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> template = (
...     ModelBuilder()
...     .template("P")
...     .location("Init", initial=True)
...     .location("Done")
...     .edge("Init", "Done", send="tick", reset={"x": 0})
... )
>>> type(template).__name__
'TemplateBuilder'

end() → ModelBuilder[source]

Finish the current template and return the parent builder.

Returns:: The owning model builder.
Return type:: ModelBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> builder = ModelBuilder().template("P").location("Init", initial=True).end()
>>> isinstance(builder, ModelBuilder)
True

location(name: str, *, initial: bool = False, invariant: str = '', urgent: bool = False, committed: bool = False) → TemplateBuilder[source]

Append one location to the current template.

Parameters:

name (str) – Location name.
initial (bool) – Whether this location is the initial location.
invariant (str) – Optional invariant text.
urgent (bool) – Whether the location is urgent.
committed (bool) – Whether the location is committed.

Returns:

The current template builder.

Return type:

TemplateBuilder

Raises:

ValueError – If the location name already exists or multiple initial locations are requested.

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> template = ModelBuilder().template("P").location("Init", initial=True)
>>> type(template).__name__
'TemplateBuilder'

remove_edge(index: object = <object object>, *, where: object = <object object>) → TemplateBuilder[source]

Remove one edge by index or where selector.

Negative indexes follow normal Python indexing rules when index is used.

Parameters:

index (object) – Optional edge index.
where (object) – Optional edge selector mapping.

Returns:

The current template builder.

Return type:

TemplateBuilder

Note

For index-based deletion, use ModelBuilder.list_edges() or ModelBuilder.inspect() to fetch current edge indexes before patching.

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> template = (
...     ModelBuilder()
...     .template("P")
...     .location("Init", initial=True)
...     .location("Done")
...     .edge("Init", "Done")
...     .remove_edge(where={"source": "Init", "target": "Done"})
... )
>>> type(template).__name__
'TemplateBuilder'

remove_location(name: str) → TemplateBuilder[source]

Remove one location by name.

Any incident edges are removed together with the location.

Parameters:: name (str) – Location name to remove.
Returns:: The current template builder.
Return type:: TemplateBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> template = (
...     ModelBuilder()
...     .template("P")
...     .location("Init", initial=True)
...     .location("Done")
...     .remove_location("Done")
... )
>>> type(template).__name__
'TemplateBuilder'

set_declarations(*texts: str) → TemplateBuilder[source]

Replace all local declaration blocks on the current template.

Passing no texts clears the current local declaration list.

Parameters:: texts (str) – Replacement declaration blocks.
Returns:: The current template builder.
Return type:: TemplateBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> template = ModelBuilder().template("P").set_declarations("int i;")
>>> type(template).__name__
'TemplateBuilder'

update_edge(index: object = <object object>, *, where: object = <object object>, source: object = <object object>, target: object = <object object>, when: object = <object object>, guard: object = <object object>, sync: object = <object object>, send: object = <object object>, recv: object = <object object>, update: object = <object object>, reset: object = <object object>) → TemplateBuilder[source]

Update one edge by index or where selector.

Negative indexes follow normal Python indexing rules when index is used.

Parameters:

index (object) – Optional edge index.
where (object) – Optional edge selector mapping.
source (object) – Optional replacement source location name.
target (object) – Optional replacement target location name.
when (object) – Optional replacement guard alias.
guard (object) – Optional replacement guard text.
sync (object) – Optional replacement synchronisation text.
send (object) – Optional replacement send-side sugar.
recv (object) – Optional replacement receive-side sugar.
update (object) – Optional replacement assignment text.
reset (object) – Optional replacement reset sugar.

Returns:

The current template builder.

Return type:

TemplateBuilder

Note

For index-based updates, obtain edge indexes from ModelBuilder.list_edges() (for the owning template) or from the template snapshot inside ModelBuilder.inspect().

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> template = (
...     ModelBuilder()
...     .template("P")
...     .location("Init", initial=True)
...     .location("Done")
...     .edge("Init", "Done")
...     .update_edge(where={"source": "Init", "target": "Done"}, when="x >= 1")
... )
>>> type(template).__name__
'TemplateBuilder'

update_location(name: str, *, new_name: object = <object object>, initial: object = <object object>, invariant: object = <object object>, urgent: object = <object object>, committed: object = <object object>) → TemplateBuilder[source]

Update one existing location by name.

Renaming a location also updates all edges that refer to it.

Parameters:

name (str) – Existing location name.
new_name (object) – Optional replacement location name.
initial (object) – Optional replacement initial-location flag.
invariant (object) – Optional replacement invariant text.
urgent (object) – Optional replacement urgent flag.
committed (object) – Optional replacement committed flag.

Returns:

The current template builder.

Return type:

TemplateBuilder

Example:

>>> from pyudbm.binding.utap_builder import ModelBuilder
>>> template = (
...     ModelBuilder()
...     .template("P")
...     .location("Init", initial=True)
...     .update_location("Init", new_name="Start")
... )
>>> type(template).__name__
'TemplateBuilder'

build_model

pyudbm.binding.utap_builder.build_model(spec: ModelSpec) → ModelDocument[source]

Build one public ModelDocument from a ModelSpec.

Parameters:: spec (ModelSpec) – Immutable model specification.
Returns:: Parsed public model document.
Return type:: ModelDocument

Example:

>>> from pyudbm.binding.utap_builder import LocationSpec, ModelSpec, TemplateSpec, build_model
>>> document = build_model(
...     ModelSpec(
...         declarations=("clock x;",),
...         templates=(TemplateSpec("P", locations=(LocationSpec("Init", initial=True),)),),
...         processes=(("P1", "P", ()),),
...         system_process_names=("P1",),
...     )
... )
>>> document.templates[0].name
'P'

pyudbm.binding.utap_builder

__all__

LocationSpec

EdgeSpec

QuerySpec

TemplateSpec

ModelSpec

ModelBuilder

TemplateBuilder

build_model

all