Formal properties#

Formal properties are used to specify the properties of an operator body. They are used to define the assumptions, guarantees, and assertions of the operator.

../../../_images/formal_props.svg — Fig. 10 Formal properties class diagram#

Assume section#

class ansys.scadeone.core.swan.AssumeSection(assertions: List[Assertion])#

Bases: AssertionBase

Implements Assume section:

assume {{LUID: expr ;}}

get_full_path() → str#

Full path of the Swan construct.

This method is implemented by derived classes that correspond to a declaration at the module level (such as sensor, type, group, const, operator), or a module itself.

Returns:

str: Path within the owner and name of the Swan construct.

Raises:

ScadeOneException: If the method is not implemented for the current SwanItem type.

static set_owner(owner: SwanItem | IModel | None, children: SwanItem | Iterable[SwanItem] | None) → None#

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

Parameters:

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

property assertions: List[Assertion]#: Assertions of Assume or Assert or 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: IModel#: Return model containing the Swan item.

property module: ModuleBase | None#

Module containing the item.

Returns:: ModuleBase: module container, see ModuleBody and ModuleInterface or None if the object is itself a module.

property owner: SwanItem | IModel | None#: Owner of current Swan construct.

property pragmas: List[Pragma]#: Pragmas associated to this scope section.

Guarantee section#

class ansys.scadeone.core.swan.GuaranteeSection(assertions: List[Assertion])#

Bases: AssertionBase

Implements Guarantee section:

guarantee {{LUID: expr ;}}

get_full_path() → str#

Full path of the Swan construct.

This method is implemented by derived classes that correspond to a declaration at the module level (such as sensor, type, group, const, operator), or a module itself.

Returns:

str: Path within the owner and name of the Swan construct.

Raises:

ScadeOneException: If the method is not implemented for the current SwanItem type.

static set_owner(owner: SwanItem | IModel | None, children: SwanItem | Iterable[SwanItem] | None) → None#

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

Parameters:

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

property assertions: List[Assertion]#: Assertions of Assume or Assert or 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: IModel#: Return model containing the Swan item.

property module: ModuleBase | None#

Module containing the item.

Returns:: ModuleBase: module container, see ModuleBody and ModuleInterface or None if the object is itself a module.

property owner: SwanItem | IModel | None#: Owner of current Swan construct.

property pragmas: List[Pragma]#: Pragmas associated to this scope section.

Assert section#

class ansys.scadeone.core.swan.AssertSection(assertions: List[Assertion])#

Bases: AssertionBase

Implements Assert section:

assert {{LUID: expr ;}}

get_full_path() → str#

Full path of the Swan construct.

This method is implemented by derived classes that correspond to a declaration at the module level (such as sensor, type, group, const, operator), or a module itself.

Returns:

str: Path within the owner and name of the Swan construct.

Raises:

ScadeOneException: If the method is not implemented for the current SwanItem type.

static set_owner(owner: SwanItem | IModel | None, children: SwanItem | Iterable[SwanItem] | None) → None#

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

Parameters:

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

property assertions: List[Assertion]#: Assertions of Assume or Assert or 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: IModel#: Return model containing the Swan item.

property module: ModuleBase | None#

Module containing the item.

Returns:: ModuleBase: module container, see ModuleBody and ModuleInterface or None if the object is itself a module.

property owner: SwanItem | IModel | None#: Owner of current Swan construct.

property pragmas: List[Pragma]#: Pragmas associated to this scope section.

Assertion class#

class ansys.scadeone.core.swan.Assertion(luid: Luid, expr: Expression, pragmas: List[Pragma] | None)#

Bases: HasPragma

Assume, assert or guarantee expression.

get_full_path() → str#

Full path of the Swan construct.

This method is implemented by derived classes that correspond to a declaration at the module level (such as sensor, type, group, const, operator), or a module itself.

Returns:

str: Path within the owner and name of the Swan construct.

Raises:

ScadeOneException: If the method is not implemented for the current SwanItem type.

static set_owner(owner: SwanItem | IModel | None, children: SwanItem | Iterable[SwanItem] | None) → None#

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

Parameters:

ownerSwanItem: Owner of the items.
childrenUnion[SwanItem, Iterable[SwanItem], None]: 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: IModel#: Return model containing the Swan item.

property module: ModuleBase | None#

Module containing the item.

Returns:: ModuleBase: module container, see ModuleBody and ModuleInterface or None if the object is itself a module.

property owner: SwanItem | IModel | None#: Owner of current Swan construct.

property pragmas: List[Pragma]#: List of pragmas.