stormvogel.result¶

Classes¶

`Scheduler`	Specify what action to take in each state.
`Result`	Represent the model checking results for a given model.
`ParetoResult`	Result of a multiobjective Pareto model checking query.

Functions¶

`random_scheduler`(→ Scheduler)	Create a random scheduler for the provided model.
`plot_pareto_result`(result[, ax, labels, bbox_pad])	Plot the under- and over-approximation of a 2-objective Pareto model checking result.

Module Contents¶

class stormvogel.result.Scheduler(model: stormvogel.model.Model, taken_actions: dict[stormvogel.model.State, stormvogel.model.Action])¶

Specify what action to take in each state.

All schedulers are nondeterministic and memoryless.

Parameters:

model – Model associated with the scheduler (must support actions).
taken_actions – For each state, the action chosen in that state.

model: stormvogel.model.Model¶

taken_actions: dict[stormvogel.model.State, stormvogel.model.Action]¶

get_action_at_state(state: stormvogel.model.State) → stormvogel.model.Action¶

Return the action in the scheduler for the given state.

Parameters:: state – The state to look up.
Returns:: The action chosen for the given state.
Raises:: RuntimeError – If the state is not a part of the model.

generate_induced_dtmc(drop_unreachable: bool = True) → stormvogel.model.Model¶

Resolve the nondeterminacy of the MDP and return the scheduler-induced DTMC.

Copies the MDP (preserving state UUIDs), changes the model type to DTMC, and replaces each state’s choices with only the scheduled action’s branch.

Parameters:: drop_unreachable – When True (default), states not reachable from the initial state under the scheduler are pruned from the result. Set to False to keep the full state space.
Returns:: The induced DTMC.
Raises:: ValueError – If the model is not an MDP or POMDP.

__str__() → str¶

__eq__(other) → bool¶

stormvogel.result.random_scheduler(model: stormvogel.model.Model) → Scheduler¶

Create a random scheduler for the provided model.

Parameters:: model – The model to create a scheduler for.
Returns:: A new Scheduler with randomly chosen actions.

class stormvogel.result.Result(model: stormvogel.model.Model, values: dict[stormvogel.model.State, stormvogel.model.Value], scheduler: Scheduler | None = None)¶

Represent the model checking results for a given model.

Parameters:

model – Stormvogel representation of the model associated with the results.
values – For each state, the model checking result.
scheduler – In case the model is an MDP, optionally store a scheduler.

model: stormvogel.model.Model¶

values: dict[stormvogel.model.State, stormvogel.model.Value]¶

scheduler: Scheduler | None¶

at(state: stormvogel.model.State) → stormvogel.model.Value¶

Return the model checking result for a given state.

Parameters:: state – The state to look up.
Returns:: The model checking result value for the state.
Raises:: RuntimeError – If the state is not a part of the model.

at_init() → stormvogel.model.Value¶: Return the model checking result for the initial state.

get_result_of_state(state: stormvogel.model.State) → stormvogel.model.Value¶

filter(value_predicate: Callable[[stormvogel.model.Value], bool]) → list[stormvogel.model.State]¶

filter_true()¶: Obtain the set of states S’ where the result for each s in S’ is true.

__str__() → str¶

maximum_result() → stormvogel.model.Value¶

Return the maximum result.

Returns:: The maximum value across all states.
Raises:: RuntimeError – If the model uses interval or parametric values.

__eq__(other) → bool¶

__iter__()¶

class stormvogel.result.ParetoResult¶

Result of a multiobjective Pareto model checking query.

Holds the under- and over-approximation of the Pareto front as vertex lists. Each point is a list of floats with one entry per objective. The number of objectives is unrestricted, but plotting is limited to 2 objectives.

Parameters:

lower_points – Vertices of the under-approximation (known achievable region).
upper_points – Vertices of the over-approximation.
property_labels – One label per objective, auto-extracted from the formula.

lower_points: list[list[float]]¶

upper_points: list[list[float]]¶

property_labels: list[str] | None = None¶

plot(ax=None, labels: tuple[str, str] | None = None)¶

Plot the Pareto front. Only 2-objective results are supported.

Parameters:

ax – Target axes; creates a new figure if None.
labels – Override axis labels; defaults to property_labels.

Returns:

The populated axes.

stormvogel.result.plot_pareto_result(result: ParetoResult, ax=None, labels: tuple[str, str] | None = None, bbox_pad: float = 0.2)¶

Plot the under- and over-approximation of a 2-objective Pareto model checking result.

Renders: - Green filled polygon: under-approximation (known achievable region) - Blue dashed outline: over-approximation (upper bound on achievable region) - Black dots: vertices of the under-approximation

Parameters:

result – A ParetoResult from multiobjective model checking.
ax – Target axes; creates a new figure if None.
labels – Override axis labels; defaults to property_labels.
bbox_pad – Fractional padding around the points for axis limits.

Returns:

The populated axes.

Raises:

ValueError – If result does not contain exactly 2-dimensional points.