Specifications#

class staliro.specifications.Specification#

Class that represents a requirement to be evaluated using simulation data.

A specification should accept the trajectories and timestamps generated by a model and return a value which represents the “goodness” of the model results with respect to some criteria.

abstract evaluate(_Specification__trace)#

Evaluate trajectories and timestamps with respect to some requirement.

Parameters:

  • trajectories – Matrix of states where each row represents a state variable.

  • timestamps – Vector of time values corresponding to each column of the trajectories matrix.

  • _Specification__trace (Trace[S]) –

Returns:

A value indicating the “goodness” of the trajectories according to the requirement.

Return type:

Result[C, E]

staliro.specifications.specification(func: Callable[[Trace[S]], Result[C, E]]) → UserSpecification[S, C, E]#
staliro.specifications.specification(func: Callable[[Trace[S]], R]) → UserSpecification[S, R, None]
staliro.specifications.specification(func: None = None) → Decorator

Create a specification from a function.

If no function is provided, then a decorator is returned that can be called with the function to create the specification. The function must accept a Trace as an argument and return either a cost value or a staliro.Result containing the cost value and additional annotation data. If only a cost value is returned, a staliro.Result will be constructed with the annotation set to None.

Parameters:

func – The function to use to construct the specification

Returns:

A Specification or a a decorator to construct a Specification

RTAMT#

staliro.specifications.rtamt.parse_discrete(formula: str, columns: Mapping[str, int]) → DiscreteMapped#
staliro.specifications.rtamt.parse_discrete(formula: str, columns: None = None) → DiscreteNamed

Create a discrete-time requirement from a formula and an optional variable-column mapping.

If a variable-column mapping is provided, the created specification will expect states in the system trace to be a Sequence[float]. If the mapping is omitted then the specification will expect the states to be dict[str, float]. The discrete-time specification also imposes the following constraints on any Trace it evaluates:

  • The amount of time between each state must be equal

  • There must be at least two states in the trace

Parameters:

  • requirement – The requirement to use to evaluate the Trace

  • columns – The optional variable-column mapping

Returns:

A dense time specification

staliro.specifications.rtamt.parse_dense(requirement: str, columns: Mapping[str, int]) → DenseMapped#
staliro.specifications.rtamt.parse_dense(requirement: str, columns: None = None) → DenseNamed

Create a dense-time requirement from a formula and an optional variable-column mapping.

If a variable-column mapping is provided, the created specification will expect states in the system trace to be a Sequence[float]. If the mapping is omitted then the specification will expect the states to be dict[str, float].

Parameters:

  • requirement – The requirement to use to evaluate the Trace

  • columns – The optional variable-column mapping

Returns:

A dense time specification