Class JaniParserExtended

• Defined in File jani_parser_extended.hpp

Inheritance Relationships

Base Type

• public storm::parser::JaniParser< double >

Class Documentation

class JaniParserExtended : public storm::parser::JaniParser<double>

Public Functions

JaniParserExtended(const std::filesystem::path &path, const std::vector<std::filesystem::path> &plugin_paths)

Constructor for the Jani file parser.

Parameters:

• path – The path to the Jani file.

• plugin_paths – The paths to the plugin libraries, to load at runtime.

~JaniParserExtended() = default

Public Static Functions

static JaniModelPropertiesPlugins parseModelPropertiesAndPlugins(const std::filesystem::path &path, const std::vector<std::filesystem::path> &plugin_paths)

Load the JANI model, the properties and the plugins description from a JANI file.

Parameters:

• path – The path to the JANI file containing the model description.

• plugin_paths – The paths where to search the required plugins from the JANI file.

Returns:

A triple, containing the loaded JANI model instance, its properties and its plugins descriptions.

Protected Functions

JaniModelPropertiesPlugins parseModelPropertiesAndPlugins()

The method parsing the JANI file from the constructor.

Returns:

A triple, containing the loaded JANI model instance, its properties and its plugins descriptions.

std::vector<model_checker::SmcPluginInstance> loadPlugins(const storm::jani::Model &jani_model)

Generate the plugin instance descriptions from the loaded JANI model.

Parameters:

jani_model – The JANI model the loaded plugins will refer to.

Returns:

A vector of plugin instance descriptions.

void generateGlobalScope(const storm::jani::Model &jani_model)

Generate the maps of global constants and variables from the loaded JANI model instance.

Parameters:

jani_model – The JANI model to use for extracting the constants and variables.

VariablesMap extractVariablesAutomatonScope(const storm::jani::Automaton &plugin_automaton) const

Extract the local variables from the automaton.

Parameters:

plugin_automaton – The JANI automaton instance to get the local variables from.

Returns:

A VariablesMap instance with the automaton’s local variables.

Protected Attributes

storm::json<double> _jani_json

std::reference_wrapper<const std::vector<std::filesystem::path>> _plugin_paths

ConstantsMap _constants_map

VariablesMap _global_vars_map