Stormpy.pomdp¶

class BeliefExplorationModelCheckerDouble(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble, model: stormpy.storage._storage.SparsePomdp, options: storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<double>)¶

check(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble, formula: stormpy.logic._logic.Formula, cutoff_values: collections.abc.Sequence[collections.abc.Sequence[collections.abc.Mapping[SupportsInt, SupportsFloat]]]) → storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<double, storm::models::sparse::StandardRewardModel<double> >, double, double>::Result¶

check_with_environment(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble, environment: stormpy._core.Environment, formula: stormpy.logic._logic.Formula, cutoff_values: collections.abc.Sequence[collections.abc.Sequence[collections.abc.Mapping[SupportsInt, SupportsFloat]]]) → storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<double, storm::models::sparse::StandardRewardModel<double> >, double, double>::Result¶

check_with_environment_and_pre_processing_environment(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble, environment: stormpy._core.Environment, formula: stormpy.logic._logic.Formula, pre_processing_environment: stormpy._core.Environment, cutoff_values: collections.abc.Sequence[collections.abc.Sequence[collections.abc.Mapping[SupportsInt, SupportsFloat]]]) → storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<double, storm::models::sparse::StandardRewardModel<double> >, double, double>::Result¶

check_with_preprocessing_environment(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble, formula: stormpy.logic._logic.Formula, pre_processing_environment: stormpy._core.Environment, cutoff_values: collections.abc.Sequence[collections.abc.Sequence[collections.abc.Mapping[SupportsInt, SupportsFloat]]]) → storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<double, storm::models::sparse::StandardRewardModel<double> >, double, double>::Result¶

continue_unfolding(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble) → None¶

get_interactive_belief_explorer(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble) → storm::builder::BeliefMdpExplorer<storm::models::sparse::Pomdp<double, storm::models::sparse::StandardRewardModel<double> >, double>¶

get_interactive_result(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble) → storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<double, storm::models::sparse::StandardRewardModel<double> >, double, double>::Result¶

get_status(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble) → int¶

has_converged(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble) → bool¶

is_exploring(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble) → bool¶

is_result_ready(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble) → bool¶

pause_unfolding(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble) → None¶

set_fsc_values(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble, value_list: collections.abc.Sequence[collections.abc.Sequence[collections.abc.Mapping[SupportsInt, SupportsFloat]]]) → None¶

terminate_unfolding(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble) → None¶

class BeliefExplorationModelCheckerOptionsDouble(self: stormpy.pomdp._pomdp.BeliefExplorationModelCheckerOptionsDouble, discretize: bool, unfold: bool)¶

property clipping_grid_res¶

property cut_zero_gap¶

property exploration_heuristic¶

property exploration_time_limit¶

property gap_threshold_init¶

property interactive_unfolding¶

property refine¶

property refine_precision¶

property refine_step_limit¶

property size_threshold_factor¶

property size_threshold_init¶

property skip_heuristic_schedulers¶

property use_clipping¶

property use_state_elimination_cutoff¶

class BeliefExplorationPomdpModelCheckerResultDouble¶

property cutoff_schedulers¶

property induced_mc_from_scheduler¶

property lower_bound¶

property upper_bound¶

class BeliefMdpExplorerDouble¶

set_fsc_values(self: stormpy.pomdp._pomdp.BeliefMdpExplorerDouble, value_list: collections.abc.Sequence[collections.abc.Sequence[collections.abc.Mapping[SupportsInt, SupportsFloat]]]) → None¶

class BeliefSupportTrackerDouble(self: stormpy.pomdp._pomdp.BeliefSupportTrackerDouble, pomdp: stormpy.storage._storage.SparsePomdp)¶

Tracker for BeliefSupports

get_current_belief_support(self: stormpy.pomdp._pomdp.BeliefSupportTrackerDouble) → stormpy.storage._storage.BitVector¶: What is the support given the trace so far

track(self: stormpy.pomdp._pomdp.BeliefSupportTrackerDouble, action: SupportsInt, observation: SupportsInt) → None¶

class BeliefSupportTrackerExact(self: stormpy.pomdp._pomdp.BeliefSupportTrackerExact, pomdp: stormpy.storage._storage.SparseExactPomdp)¶

Tracker for BeliefSupports

get_current_belief_support(self: stormpy.pomdp._pomdp.BeliefSupportTrackerExact) → stormpy.storage._storage.BitVector¶: What is the support given the trace so far

track(self: stormpy.pomdp._pomdp.BeliefSupportTrackerExact, action: SupportsInt, observation: SupportsInt) → None¶

class BeliefSupportWinningRegion¶

static load_from_file(filepath: str) → tuple[stormpy.pomdp._pomdp.BeliefSupportWinningRegion, str]¶

store_to_file(self: stormpy.pomdp._pomdp.BeliefSupportWinningRegion, filepath: str, preamble: str, append: bool = False) → None¶

class BeliefSupportWinningRegionQueryInterfaceDouble(self: stormpy.pomdp._pomdp.BeliefSupportWinningRegionQueryInterfaceDouble, pomdp: stormpy.storage._storage.SparsePomdp, BeliefSupportWinningRegion: storm::pomdp::WinningRegion)¶

query_action(self: stormpy.pomdp._pomdp.BeliefSupportWinningRegionQueryInterfaceDouble, current_belief: stormpy.storage._storage.BitVector, action: SupportsInt) → bool¶

query_current_belief(self: stormpy.pomdp._pomdp.BeliefSupportWinningRegionQueryInterfaceDouble, current_belief: stormpy.storage._storage.BitVector) → bool¶

class IterativeQualitativeSearchOptions(self: stormpy.pomdp._pomdp.IterativeQualitativeSearchOptions)¶: Options for the IterativeQualitativeSearch

class IterativeQualitativeSearchSolverDouble¶

Solver for POMDPs that solves qualitative queries

compute_winning_policy_for_initial_states(self: stormpy.pomdp._pomdp.IterativeQualitativeSearchSolverDouble, lookahead: SupportsInt) → bool¶

compute_winning_region(self: stormpy.pomdp._pomdp.IterativeQualitativeSearchSolverDouble, lookahead: SupportsInt) → None¶

property last_winning_region¶: get the last computed winning region

class NondeterministicBeliefTrackerDoubleSparse(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparse, pomdp: stormpy.storage._storage.SparsePomdp, options: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparseOptions)¶

Tracker for belief states and uncontrollable actions

dimension(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparse) → int¶

obtain_beliefs(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparse) → set[stormpy.pomdp._pomdp.SparseBeliefStateDouble]¶

obtain_current_risk(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparse, max: bool = True) → float¶

obtain_last_observation(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparse) → int¶

reduce(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparse) → int¶

reduction_timed_out(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparse) → bool¶

reset(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparse, arg0: SupportsInt) → bool¶

set_risk(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparse, risk: collections.abc.Sequence[SupportsFloat]) → None¶

size(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparse) → int¶

track(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparse, observation: SupportsInt) → bool¶

class NondeterministicBeliefTrackerDoubleSparseOptions(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerDoubleSparseOptions)¶

Options for the corresponding tracker

property reduction_timeout¶

property reduction_wiggle¶

property track_timeout¶

class NondeterministicBeliefTrackerExactSparse(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparse, pomdp: stormpy.storage._storage.SparseExactPomdp, options: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparseOptions)¶

Tracker for belief states and uncontrollable actions

dimension(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparse) → int¶

obtain_beliefs(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparse) → set[stormpy.pomdp._pomdp.SparseBeliefStateExact]¶

obtain_current_risk(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparse, max: bool = True) → stormpy.pycarl.gmp.Rational¶

obtain_last_observation(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparse) → int¶

reduce(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparse) → int¶

reduction_timed_out(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparse) → bool¶

reset(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparse, arg0: SupportsInt) → bool¶

set_risk(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparse, risk: collections.abc.Sequence[stormpy.pycarl.gmp.Rational]) → None¶

size(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparse) → int¶

track(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparse, observation: SupportsInt) → bool¶

class NondeterministicBeliefTrackerExactSparseOptions(self: stormpy.pomdp._pomdp.NondeterministicBeliefTrackerExactSparseOptions)¶

Options for the corresponding tracker

property reduction_timeout¶

property reduction_wiggle¶

property track_timeout¶

class ObservationTraceUnfolderDouble(self: stormpy.pomdp._pomdp.ObservationTraceUnfolderDouble, model: stormpy.storage._storage.SparsePomdp, risk: collections.abc.Sequence[SupportsFloat], expression_manager: stormpy.storage._storage.ExpressionManager)¶

Unfolds observation traces in models

extend(self: stormpy.pomdp._pomdp.ObservationTraceUnfolderDouble, new_observation: SupportsInt) → stormpy.storage._storage.SparseMdp¶

reset(self: stormpy.pomdp._pomdp.ObservationTraceUnfolderDouble, new_observation: SupportsInt) → None¶

transform(self: stormpy.pomdp._pomdp.ObservationTraceUnfolderDouble, trace: collections.abc.Sequence[SupportsInt]) → stormpy.storage._storage.SparseMdp¶

class ObservationTraceUnfolderExact(self: stormpy.pomdp._pomdp.ObservationTraceUnfolderExact, model: stormpy.storage._storage.SparseExactPomdp, risk: collections.abc.Sequence[stormpy.pycarl.gmp.Rational], expression_manager: stormpy.storage._storage.ExpressionManager)¶

Unfolds observation traces in models

extend(self: stormpy.pomdp._pomdp.ObservationTraceUnfolderExact, new_observation: SupportsInt) → stormpy.storage._storage.SparseExactMdp¶

reset(self: stormpy.pomdp._pomdp.ObservationTraceUnfolderExact, new_observation: SupportsInt) → None¶

transform(self: stormpy.pomdp._pomdp.ObservationTraceUnfolderExact, trace: collections.abc.Sequence[SupportsInt]) → stormpy.storage._storage.SparseExactMdp¶

class ObservationTraceUnfolderRf(self: stormpy.pomdp._pomdp.ObservationTraceUnfolderRf, model: stormpy.storage._storage.SparseParametricPomdp, risk: collections.abc.Sequence[stormpy.pycarl.cln.FactorizedRationalFunction], expression_manager: stormpy.storage._storage.ExpressionManager)¶

Unfolds observation traces in models

extend(self: stormpy.pomdp._pomdp.ObservationTraceUnfolderRf, new_observation: SupportsInt) → stormpy.storage._storage.SparseParametricMdp¶

reset(self: stormpy.pomdp._pomdp.ObservationTraceUnfolderRf, new_observation: SupportsInt) → None¶

transform(self: stormpy.pomdp._pomdp.ObservationTraceUnfolderRf, trace: collections.abc.Sequence[SupportsInt]) → stormpy.storage._storage.SparseParametricMdp¶

class PomdpFscApplicationMode(self: stormpy.pomdp._pomdp.PomdpFscApplicationMode, value: SupportsInt)¶

Members:

standard

simple_linear

simple_linear_inverse

simple_log

full

full = <PomdpFscApplicationMode.full: 4>¶

property name¶

simple_linear = <PomdpFscApplicationMode.simple_linear: 1>¶

simple_linear_inverse = <PomdpFscApplicationMode.simple_linear_inverse: 2>¶

simple_log = <PomdpFscApplicationMode.simple_log: 3>¶

standard = <PomdpFscApplicationMode.standard: 0>¶

property value¶

class PomdpMemory¶

Memory for POMDP policies

property nr_states¶: How many states does the memory structure have

class PomdpMemoryBuilder(self: stormpy.pomdp._pomdp.PomdpMemoryBuilder)¶

MemoryBuilder for POMDP policies

build(self: stormpy.pomdp._pomdp.PomdpMemoryBuilder, pattern: stormpy.pomdp._pomdp.PomdpMemoryPattern, nr_states: SupportsInt) → stormpy.pomdp._pomdp.PomdpMemory¶

class PomdpMemoryPattern(self: stormpy.pomdp._pomdp.PomdpMemoryPattern, value: SupportsInt)¶

Memory pattern for POMDP memory

Members:

trivial

fixed_counter

selective_counter

fixed_ring

selective_ring

settable_bits

full

fixed_counter = <PomdpMemoryPattern.fixed_counter: 1>¶

fixed_ring = <PomdpMemoryPattern.fixed_ring: 3>¶

full = <PomdpMemoryPattern.full: 6>¶

property name¶

selective_counter = <PomdpMemoryPattern.selective_counter: 2>¶

selective_ring = <PomdpMemoryPattern.selective_ring: 4>¶

settable_bits = <PomdpMemoryPattern.settable_bits: 5>¶

trivial = <PomdpMemoryPattern.trivial: 0>¶

property value¶

class SparseBeliefStateDouble¶

Belief state in sparse format

get(self: stormpy.pomdp._pomdp.SparseBeliefStateDouble, state: SupportsInt) → float¶

property is_valid¶

property risk¶

class SparseBeliefStateExact¶

Belief state in sparse format

get(self: stormpy.pomdp._pomdp.SparseBeliefStateExact, state: SupportsInt) → stormpy.pycarl.gmp.Rational¶

property is_valid¶

property risk¶

apply_unknown_fsc(model, mode)¶

create_interactive_mc(env: stormpy._core.Environment, pomdp: stormpy.storage._storage.SparsePomdp, use_clipping: bool) → stormpy.pomdp._pomdp.BeliefExplorationModelCheckerDouble¶

create_iterative_qualitative_search_solver_Double(pomdp: stormpy.storage._storage.SparsePomdp, formula: stormpy.logic._logic.Formula, options: storm::pomdp::MemlessSearchOptions) → storm::pomdp::IterativePolicySearch<double>¶: Create solver

create_nondeterminstic_belief_tracker(model, reduction_timeout, track_timeout)¶

Parameters:

model – A POMDP
reduction_timeout – timeout in milliseconds for the reduction algorithm, 0 for no timeout.

Returns:

create_observation_trace_unfolder(model, risk_assessment, expr_manager)¶

Parameters:

model
risk_assessment
expr_manager

Returns:

make_canonic(model)¶: Make the POMDP canonic :param model: :return:

make_simple(model, keep_state_valuations=False)¶

Make the POMDP simple (aka alternating), i.e., each state has at most two actions, and if there is nondeterminism, then there is no probabilistic branching,

Parameters:: model
Returns:

prepare_pomdp_for_qualitative_search_Double(pomdp: stormpy.storage._storage.SparsePomdp, formula: stormpy.logic._logic.Formula) → stormpy.storage._storage.SparsePomdp¶: Preprocess POMDP

unfold_memory(model, memory, add_memory_labels=False, keep_state_valuations=False)¶

Unfold the memory for an FSC into the POMDP

Parameters:

model – A pomdp
memory – A memory structure

Returns:

A pomdp that contains states from the product of the original POMDP and the FSC Memory