Template Class JaniSmcStatesExpansion

• Defined in File jani_smc_states_expansion.hpp

Nested Relationships

Nested Types

• Struct JaniSmcStatesExpansion::ActionDescription

• Struct JaniSmcStatesExpansion::ComputedDestinations

• Struct JaniSmcStatesExpansion::PairHash

Class Documentation

template<typename ValueType>
class JaniSmcStatesExpansion

Public Functions

JaniSmcStatesExpansion(const storm::jani::Model &jani_model, const std::optional<std::string> &reward_name, const std::vector<model_checker::SmcPluginInstance> &external_plugins, std::default_random_engine &random_generator)

Initiate the state generator class.

Parameters:

• jani_model – The model to generate the states from

• reward_name – The reward to generate from the model (zero or one reward)

• external_plugins – Dummy placeholder for the external plugins. To be done!!!

~JaniSmcStatesExpansion() = default

inline const state_properties::StateVariableInformation<ValueType> &getVariableInformation() const

Getter for the variable information: needed to introspect the CompressedState.

Returns:

A const reference to the Variable information

inline const state_properties::StateVariableData<ValueType> &getCurrentState() const

Getter for the current state of the expanded model.

Returns:

A const reference to the current state

const state_properties::StateVariableData<ValueType> &setInitialState()

Generate the initial state and set it as the current one.

Returns:

The generated initial state

std::pair<std::reference_wrapper<const state_properties::StateVariableData<ValueType>>, ValueType> setNextState(const ActionId action_id, const DestinationId destination_id)

Advance the automaton to the next state selecting a specific action and related destination.

Parameters:

• action_id – The ID of the action to execute. Use getAvailableActions to get the Action IDs available from the current state.

• destination_id – The ID of the destination to take. Use getDestinationsFromAction to compute the available ones.

Returns:

The new current_state, obtained by moving to the requested destination, together with the destination reward.

bool satisfies(const storm::expressions::Expression &expression) const

Check if the current state satisfies a specific expression.

Parameters:

expression – the expression to evaluate on the current state

Returns:

true if the expression holds, false otherwise

inline const ValueType getStateReward() const

Get the reward associated to the current state (TODO)

Returns:

A reward value

inline const ValueType getActionReward() const

Get the reward associated to the current state (TODO)

Returns:

A reward value

inline const ValueType getTransitionReward() const

AvailableActions<ValueType> getAvailableActions()

Get the actions that can be taken from the current state.

Returns:

A vector of pairs indicating the action ID and the associated reward

ActionDestinations getDestinationsFromAction(const ActionId action_id)

Get the destinations that can be reached from the current state by taking a specific action.

Returns:

A vector of pairs indicating the destination ID and the associated probability of being selected

Public Members

AutomatonAndActionToPluginId automaton_and_action_to_plugin_ids

std::vector<std::reference_wrapper<const storm::jani::Automaton>> parallel_automata

std::vector<SyncIdxAndEdges> composite_edges

storm::builder::RewardModelInformation information

storm::expressions::Expression expression

ValueType current_state_reward