stormvogel.transformations.eliminate_transition_rewards

Transformation: rewrite transition rewards into state rewards.

Functions

eliminate_transition_rewards(...)

Rewrite transition rewards into state rewards via auxiliary entry states.

Module Contents

stormvogel.transformations.eliminate_transition_rewards.eliminate_transition_rewards(model: stormvogel.model.model.Model) → stormvogel.model.model.Model

Rewrite transition rewards into state rewards via auxiliary entry states.

For each transition (s, a, s’) carrying reward r in any reward model, inserts an auxiliary state e and reroutes:

s --a, p--> s'   =>   s --a, p--> e --τ, 1--> s'

with state_reward(e) = r.

Returns a new model with only state rewards. If no transition rewards are present, returns model unchanged. Note that step-bounded properties are not preserved by this transformation.

Models with observations are not supported as the observed information changes

and there is currently no silent steps in stormvogel.

State valuations are currently dropped; support for them may be added later.

Parameters:

model – The source model.

Returns:

A new model with only state rewards, or model if it had none.