GenerateMonitorVerifier

Warning

The stormpy developer API is internal and can be subject to change.

class GenerateMonitorVerifier[ValueType](

mc: stormpy.models.SparseDtmc[ValueType],

monitor: stormpy.models.SparseMdp[ValueType],

expr_manager: stormpy.expressions.ExpressionManager,

options: stormpy.pomdp.developer.GenerateMonitorVerifierOptions[ValueType],

)

Generator of POMDP used in verifying monitors against Markov chains

Template arguments:

• ValueType (type)

Available specializations:

• GenerateMonitorVerifier[float]

• GenerateMonitorVerifier[stormpy.numbers.Rational]

Construction

The specialization can be inferred from the first positional constructor argument (alternatively, the mc keyword argument).

Members

GenerateMonitorVerifier.create_product(

self: stormpy.pomdp.developer.GenerateMonitorVerifier[ValueType],

) → stormpy.pomdp.MonitorVerifier[ValueType]

Create the verification POMDP

GenerateMonitorVerifier.set_risk()

For GenerateMonitorVerifier[float]:

set_risk(self: stormpy.pomdp.developer.GenerateMonitorVerifier[ValueType], risk: collections.abc.Sequence[typing.SupportsFloat | typing.SupportsIndex]) -> None

Set the risk of each state of the Markov chain

For GenerateMonitorVerifier[stormpy.numbers.Rational]:

set_risk(self: stormpy.pomdp.developer.GenerateMonitorVerifier[ValueType], risk: collections.abc.Sequence[ValueType]) -> None

Set the risk of each state of the Markov chain