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.

abstractmethod evaluate(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.

  • trace (Trace[S])

Returns:

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

Return type:

Result[C, E]

@staliro.specification(f: Callable[[Trace[T]], Result[C, E]]) → Specification[T, C, E]
@staliro.specification(f: Callable[[Trace[T]], C]) → Specification[T, C, None]

Create a specification from a function.

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

  • f (Callable[[Trace[T]], Result[C, E] | C])

Returns:

A Specification implementation wrapping the provided function

Return type:

Specification[T, C, E | None]

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 (Mapping[str, int] | None) – The optional variable-column mapping

  • formula (str)

Returns:

A dense time specification

Return type:

DiscreteMapped | DiscreteNamed

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 (str) – The requirement to use to evaluate the Trace

  • columns (Mapping[str, int] | None) – The optional variable-column mapping

Returns:

A dense time specification

Return type:

DenseMapped | DenseNamed