Assume/guarantee - emission#

Assume guarantee sections#

class ansys.scadeone.core.swan.FormalProperty(luid: Luid, expr: Expression)#

Bases: SwanItem

Assume or Guarantee expression.

get_full_path() → str#: Full path of Swan construct.

static set_owner(owner: Self, children: Self | Iterable[Self])#

Helper to set owner as the owner of each item in the Iterable items.

Parameters:

ownerSwanItem: Owner of the items.
childrenUnion[SwanItem, Iterable[SwanItem]]: Items to set owner.

property expr: Expression#: Property expression.

property is_protected: bool#: Tell if a construct item is syntactically protected with some markup and is stored as a string (without the markup).

property luid: Luid#: Property identifier.

property model: Model#: Return model containing the Swan item.

property module: ModuleBase#

Module containing the item.

Returns:: ModuleBase: module container, see ModuleBody and ModuleInterface

property owner: Self#: Owner of current Swan construct.

class ansys.scadeone.core.swan.AssumeSection(hypotheses: List[FormalProperty])#

Bases: ScopeSection

Implements Assume section:

assume {{LUID: expr ;}}

get_full_path() → str#: Full path of Swan construct.

static set_owner(owner: Self, children: Self | Iterable[Self])#

Helper to set owner as the owner of each item in the Iterable items.

Parameters:

ownerSwanItem: Owner of the items.
childrenUnion[SwanItem, Iterable[SwanItem]]: Items to set owner.

property hypotheses: List[FormalProperty]#: Hypotheses of Assume.

property is_protected: bool#: Tell if a construct item is syntactically protected with some markup and is stored as a string (without the markup).

property is_text: bool#: True when section is given from {text%…%text} markup.

property model: Model#: Return model containing the Swan item.

property module: ModuleBase#

Module containing the item.

Returns:: ModuleBase: module container, see ModuleBody and ModuleInterface

property owner: Self#: Owner of current Swan construct.

class ansys.scadeone.core.swan.GuaranteeSection(guarantees: List[FormalProperty])#

Bases: ScopeSection

Implements Guarantee section:

guarantee {{LUID: expr ;}}

get_full_path() → str#: Full path of Swan construct.

static set_owner(owner: Self, children: Self | Iterable[Self])#

Helper to set owner as the owner of each item in the Iterable items.

Parameters:

ownerSwanItem: Owner of the items.
childrenUnion[SwanItem, Iterable[SwanItem]]: Items to set owner.

property guarantees: List[FormalProperty]#: Guarantees of Guarantee.

property is_protected: bool#: Tell if a construct item is syntactically protected with some markup and is stored as a string (without the markup).

property is_text: bool#: True when section is given from {text%…%text} markup.

property model: Model#: Return model containing the Swan item.

property module: ModuleBase#

Module containing the item.

Returns:: ModuleBase: module container, see ModuleBody and ModuleInterface

property owner: Self#: Owner of current Swan construct.

Emissions#

class ansys.scadeone.core.swan.EmissionBody(flows: List[Identifier], condition: Expression | None = None, luid: Luid | None = None)#

Bases: SwanItem

Implements an emission:

emission_body ::= flow_names [[ if expr ]]

flow_names ::= NAME {{ , NAME }}

get_full_path() → str#: Full path of Swan construct.

static set_owner(owner: Self, children: Self | Iterable[Self])#

Helper to set owner as the owner of each item in the Iterable items.

Parameters:

ownerSwanItem: Owner of the items.
childrenUnion[SwanItem, Iterable[SwanItem]]: Items to set owner.

property condition: Expression | None#: Emission condition if exists, else None.

property flows: List[Identifier]#: Emitted flows.

property is_protected: bool#: Tell if a construct item is syntactically protected with some markup and is stored as a string (without the markup).

property luid: Luid | None#: Emission identifier if exists, else None.

property model: Model#: Return model containing the Swan item.

property module: ModuleBase#

Module containing the item.

Returns:: ModuleBase: module container, see ModuleBody and ModuleInterface

property owner: Self#: Owner of current Swan construct.

class ansys.scadeone.core.swan.EmitSection(emissions: List[EmissionBody])#

Bases: ScopeSection

Implements an Emit section:

emit {{emission_body ;}}

get_full_path() → str#: Full path of Swan construct.

static set_owner(owner: Self, children: Self | Iterable[Self])#

Helper to set owner as the owner of each item in the Iterable items.

Parameters:

ownerSwanItem: Owner of the items.
childrenUnion[SwanItem, Iterable[SwanItem]]: Items to set owner.

property emissions: List[EmissionBody]#: List of emissions.

property is_protected: bool#: Tell if a construct item is syntactically protected with some markup and is stored as a string (without the markup).

property is_text: bool#: True when section is given from {text%…%text} markup.

property model: Model#: Return model containing the Swan item.

property module: ModuleBase#

Module containing the item.

Returns:: ModuleBase: module container, see ModuleBody and ModuleInterface

property owner: Self#: Owner of current Swan construct.