Valuations

class Valuations(
self: stormpy.models.Valuations,
class_description: stormpy.models.ValuationClassDescription,
manager=None,
num_entities: SupportsInt | SupportsIndex = 0,
)

Bases: pybind11_object

Valuations for explicit entities (states/observations)

Construct valuations from a class description, optional expression manager and entity count

entity_has_variable(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
) → bool
get_all_variables(self: stormpy.models.Valuations)

Get all variables with valuations

get_boolean_value(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
) → bool
get_boolean_values(
self: stormpy.models.Valuations,
variable,
) → stormpy.datastructures.BitVector

Values of a Boolean variable as a BitVector

get_double_value(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
) → float

Get the value of a rational variable that was declared with the double (64-bit IEEE754) storage encoding via add_double_variable, as a Python float. get_value/get_rational_value assume the exact encoding and cannot read a double-encoded variable.

get_double_values(self: stormpy.models.Valuations, variable) → list[float]

Get the value for all entities of a rational variable declared via add_double_variable.

get_int64_value(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
) → int
get_int64_values(self: stormpy.models.Valuations, variable) → list[int]

Get the integer variable value for all entities. The i-th entry is the value of entity i.

get_integer_bigint_value(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
) → stormpy.numbers.Integer

Get the value of an integer variable as an arbitrary-precision integer. Only needed for integer variables declared with arbitrary-precision bounds whose value does not fit in an int64; get_value already handles the common case.

get_number_of_entities(self: stormpy.models.Valuations) → int

Get number of entities

get_rational_value(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
) → stormpy.numbers.Rational
get_rational_values(
self: stormpy.models.Valuations,
variable,
) → list[stormpy.numbers.Rational]

Get the rational variable value for all entities. The i-th entry is the value of entity i.

get_string_value(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
) → str
get_string_values(self: stormpy.models.Valuations, variable) → list[str]
get_value(
entity: int,
variable: Variable,
) → bool | int | Rational | str

Read a variable at an entity, dispatching by its expression type.

Parameters:

  • entity – State or observation index.

  • variable – Expression variable to read.

Returns:

Boolean, integer, rational or string value.

get_values_states(
variable: Variable,
) → list[bool] | list[int] | list[Rational] | list[str]

Read a variable for every entity, returning a list in entity order.

Parameters:

variable – Expression variable to read.

Returns:

List with one value per state or observation.

property manager
select_entities(
selected_entities: stormpy.datastructures.BitVector,
) → stormpy.models.Valuations
select_entities(
selected_entities: collections.abc.Sequence[SupportsInt | SupportsIndex],
) → stormpy.models.Valuations
to_json(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
selected_variables=None,
) → stormpy.datastructures.JsonContainer[stormpy.numbers.Rational]
to_string(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
pretty: bool = True,
selected_variables=None,
) → str
write_bool_value(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
value: bool,
) → None

Write a boolean value for the given entity and variable

write_double_value(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
value: SupportsFloat | SupportsIndex,
) → None

Write the value of a rational variable that was declared with the double (64-bit IEEE754) storage encoding via add_double_variable

write_int64_value(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
value: SupportsInt | SupportsIndex,
) → None

Write an integer (int64) value for the given entity and variable

write_integer_bigint_value(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
value: stormpy.numbers.Integer,
) → None

Write an arbitrary-precision integer value for the given entity and variable. Only needed for integer variables declared with arbitrary-precision bounds whose value does not fit in an int64.

write_rational_value(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
value: stormpy.numbers.Rational,
) → None

Write a rational value for the given entity and variable

write_string_value(
self: stormpy.models.Valuations,
entity: SupportsInt | SupportsIndex,
variable,
value: str,
) → None

Write a string value for the given entity and variable

write_value(
entity: int,
variable: Variable,
value: bool | int | Rational | str,
) → None

Write a variable at an entity, dispatching by its expression type.

Parameters:

  • entity – State or observation index.

  • variable – Expression variable to write.

  • value – Value compatible with the variable’s type and storage encoding.