instantiate_constants

instantiate_constants(
model: PrismProgram | JaniModel | SymbolicModelDescription,
constants: str | Mapping[str | Variable, bool | int | float | Rational | Expression],
properties: Property | Iterable[Property] | None = None,
) → tuple[PrismProgram | JaniModel | SymbolicModelDescription, list[Property]]

Instantiate undefined constants in a symbolic model and the corresponding properties.

Parameters:

  • model – Symbolic model (Prism program, Jani model or symbolic model description).

  • constants – Constant definitions, either as comma-separated string, e.g. "N=3,p=0.5", or as mapping from constants (given by name or variable) to values, e.g. {"N": 3, "p": 0.5}. Values can be Booleans, integers, floats, rationals or expressions.

  • properties – (optional) Property or properties in which the constants are instantiated as well.

Returns:

Tuple of the instantiated model (of the same kind as the given model) and the list of instantiated properties.