Class JaniSmcModelBuild

Class Documentation

class JaniSmcModelBuild

Public Types

using LocationEdges = std::vector<std::reference_wrapper<const storm::jani::Edge>>
using AutomatonAction = std::vector<LocationEdges>
using AutomatonActionsSet = std::vector<AutomatonAction>
using AutomatonToActionId = std::pair<uint64_t, uint64_t>
using CompositeEdge = std::pair<uint64_t, std::vector<AutomatonToActionId>>
using EdgeToPluginId = std::pair<uint64_t, uint64_t>
using AutomatonEdgesWithPlugin = std::vector<EdgeToPluginId>

Public Functions

JaniSmcModelBuild(const storm::jani::Model &jani_model, const std::vector<model_checker::SmcPluginInstance> &external_plugins)

Build an internal model from the provided JANI object.

Parameters:

  • jani_model – The model we are building from.

  • external_plugins – All plugin instances loaded in the model.

uint64_t getPluginFromAutomatonAction(const uint64_t automaton_id, const uint64_t action_id) const

Get the plugin ID associated to a provided automaton and action ID pair.

Parameters:

  • automaton_id – The ID of the automaton associated to the plugin.

  • action_id – The action ID associated to the automaton, that might or not have an associated plugin ID.

Returns:

The ID of the plugin to execute. If non found, it returns the NO_PLUGIN_ID constant.

inline const std::vector<std::reference_wrapper<const storm::jani::Automaton>> &getAutomata() const

Get all the automata instances loaded from the provided model.

Returns:

An array of references to Jani Automata.

inline uint64_t getAutomataCount() const

Get the amount of automata loaded from the model.

Returns:

A count of the loaded automata.

inline const storm::jani::Automaton &getAutomaton(const uint64_t automaton_id) const

Get a specific automaton instance.

Parameters:

automaton_id – The ID of the automaton to retrieve.

Returns:

The retrieved automaton.

inline const std::vector<CompositeEdge> &getCompositeEdges() const

Retrieve all the composite edges (aka the actions defined in the system composition).

Returns:

An array of possible (composite) actions.

inline const std::vector<std::reference_wrapper<const storm::jani::Edge>> &getAutomatonActionEdgesAtLocation(const uint64_t automaton_id, const uint64_t action_id, const uint64_t location_id) const

Given an automaton, the selected action and its location, retrieve all edges associated to it.

Parameters:

  • automaton_id – The ID of the automaton we extract the edge from.

  • action_id – The action ID associated to the edge.

  • location_id – The location the edge leaves from.

Returns:

An array of edges matching with the provided arguments (could be empty).

Public Static Attributes

static constexpr uint64_t SILENT_ACTION_ID = std::numeric_limits<uint64_t>::max()
static constexpr uint64_t NO_PLUGIN_ID = std::numeric_limits<uint64_t>::max()