API Documentation

This part of the documentation covers the interfaces used to develop with strategoutil.

StrategoController

class strategoutil.StrategoController(model_template_file, model_cfg_dict, cleanup=True)

Bases: object

Controller class to interface with UPPAAL Stratego through python.

Parameters:

• model_template_file (str) – The file name of the template model.

• model_cfg_dict (dict) – Dictionary containing pairs of state variable name and its initial value. The state variable name should match the tag name in the template model.

• cleanup (bool) – Whether or not to clean up the temporarily simulation file after being used.

Variables:

• states (bool) – Dictionary containing the current state of the system, where a state is a pair of variable name and value. It is initialized with the values from model_cfg_dict.

• tagRule (str) – The rule for each tag in the template model. Currently, the rul is set to be "//TAG_{}". Therefore, tags in the template model should be "//TAG_<variable name>", where <variable name> is the global name of the variable.

debug_copy(debug_file)

Copy UPPAAL simulationfile.xml file for manual debug in Stratego.

Parameters:

debug_file (str) – The file name of the debug file.

get_state(key)

Get the current value of the provided state variable.

Parameters:

key (str) – The state variable name.

Returns:

The currently stored value of the state variable.

Return type:

int or float

get_state_as_string()

Print the values of the state variables separated by a ‘,’.

Returns:

All the variable values joined together with a ‘,’.

Return type:

str

get_states()

Get the current states.

Returns:

The current state dictionary.

Return type:

dict

get_var_names_as_string()

Print the names of the state variables separated by a ‘,’.

Returns:

All the variable names joined together with a ‘,’.

Return type:

str

init_simfile()

Make a copy of a template file where data of specific variables is inserted.

insert_state()

Insert the current state values of the variables at the appropriate position in the simulation *.xml file indicated by the tagRule.

remove_simfile()

Clean created temporary files after the simulation is finished.

run(query_file='', learning_args=None, verifyta_command='verifyta')

Runs verifyta with requested queries and parameters that are either part of the *.xml model file or explicitly specified.

Parameters:

• query_file (str) – The file name of the query file where the queries are written to.

• learning_args (dict) – Dictionary containing the learning parameters and their values. The learning parameter names should be those used in the command line interface of Uppaal Stratego. You can also include non-learning command line parameters in this dictionary. If a non-learning command line parameter does not take any value, include the empty string "" as value.

• verifyta_command (str) – The command name for running Uppaal Stratego at the user’s machine.

Returns:

The output generated by Uppaal Stratego.

Return type:

str

update_state(new_values)

Update the state of the MPC controller.

Parameters:

new_values (dict) – Dictionary containing new values for the state variables.

MPCsetup

class strategoutil.MPCsetup(model_template_file, output_file_path=None, query_file='', model_cfg_dict=None, learning_args=None, verifyta_command='verifyta', external_simulator=False, action_variable=None, debug=False)

Bases: object

Class that performs the basic MPC scheme for Uppaal Stratego.

The class parameters are also available as attributes.

Parameters:

• model_template_file (str) – The file name of the template model.

• output_file_path (str) – The file name of the output file where the results are printed to.

• query_file (str) – The file name of the query file where the queries are written to.

• model_cfg_dict (dict) – Dictionary containing pairs of state variable name and its initial value. The state variable name should match the tag name in the template model.

• learning_args (dict) – Dictionary containing the learning parameters and their values. The learning parameter names should be those used in the command line interface of Uppaal Stratego. You can also include non-learning command line parameters in this dictionary. If a non-learning command line parameter does not take any value, include the empty string "" as value.

• verifyta_command (str) – The command name for running Uppaal Stratego at the user’s machine.

• external_simulator (bool) – Whether an external simulator is used to obtain the true state after applying the synthesized control strategy for a single control period.

• action_variable (str) – Name of the variable in the model that captures the control actions to choose from. Only relevant if an external simulator is used, as we need to get the chosen control action from Uppaal Stratego and pass it on to the external simulator. It should be a variable in model_cfg_dict.

• debug (bool) – Whether or not to run in debug mode.

Variables:

controller (StrategoController) – The controller object used for interacting with Uppaal Stratego.

create_query_file(horizon, period, final)

Create a basic query file for each step of the MPC scheme. Current content will be overwritten.

You might want to override this method for specific models.

Parameters:

• horizon (int) – The interval duration for which Uppaal stratego synthesizes a control strategy each MPC step. Is given in the number of periods.

• period (int) – The interval duration after which the controller can change the control setting, given in Uppaal Stratego time units.

• final (int) – The time that should be reached by the synthesized strategy, given in Uppaal Stratego time units. Most likely this will be current time + horizon x period.

extract_control_action_from_stratego(stratego_output)

Extract the chosen control action for the first control period from the simulation output of Stratego.

Parameters:

stratego_output (str) – The output as generated by Uppaal Stratego.

Returns:

The control action chosen for the first control period.

Return type:

float

extract_states_from_stratego(result, control_period)

Extract the new state values from the simulation output of Stratego.

The extracted values are directly saved in the controller.

Parameters:

• result (str) – The output as generated by Uppaal Stratego.

• control_period (int) – The interval duration after which the controller can change the control setting, given in Uppaal Stratego time units.

perform_at_start_iteration(*args, **kwargs)

Perform some customizable preprocessing steps at the start of each MPC iteration. This method can be overwritten for specific models.

print_state()

Print the current state to output file if provided. Otherwise, it will be printed to the standard output.

print_state_vars()

Print the names of the state variables to output file if provided. Otherwise, it will be printed to the standard output.

run(control_period, horizon, duration, **kwargs)

Run the basic MPC scheme where the controller can changes its strategy once every period, where the strategy synthesis looks the horizon ahead, and continues for the duration of the experiment.

The control period is in Uppaal Stratego time units. Both horizon and duration have control period as time unit.

Parameters:

• control_period (int) – The interval duration after which the controller can change the control setting, given in Uppaal Stratego time units.

• horizon (int) – The interval duration for which Uppaal stratego synthesizes a control strategy each MPC step. Is given in the number of control periods.

• duration (int) – The number of times (steps) the MPC scheme should be performed, given as the number of control periods.

• **kwargs – Any additional parameters are forwarded to perform_at_start_iteration().

run_external_simulator(chosen_action, *args, **kwargs)

Run an external simulator to obtain the ‘true’ state after applying the synthesized control action for a single control period.

This method should be overridden by the user. The method should return the new ‘true’ state as a dictionary containing pairs where the key is a variable name and the value is its new value.

Parameters:

chosen_action (int or float) – The synthesized control action for the first control period.

Returns:

The ‘true’ state of the system after simulation a single control period. The dictionary containings pairs of state variable name and their values. The state variable name should match the tag name in the template model.

Return type:

dict

run_single(control_period, horizon, **kwargs)

Run the basic MPC scheme a single step where a single controller strategy is calculated, where the strategy synthesis looks the horizon ahead, and continues for the duration of the experiment.

The control period is in Uppaal Stratego time units. Horizon have control period as time unit.

Parameters:

• control_period (int) – The interval duration after which the controller can change the control setting, given in Uppaal Stratego time units.

• horizon (int) – The interval duration for which Uppaal stratego synthesizes a control strategy each MPC step. Is given in the number of control periods.

• **kwargs – Any additional parameters are forwarded to perform_at_start_iteration().

Returns:

The control action chosen for the first control period.

run_verifyta(*args, **kwargs)

Run verifyta with the current data stored in this class.

Parameters:

• *args – Is not used in this method; it is used in the overriding method run_verifyta() in SafeMPCSetup.

• **kwargs – Is not used in this method; it is used in the overriding method run_verifyta() in SafeMPCSetup.

Returns:

The output generated by Uppaal Stratego.

Return type:

str

step_without_sim(control_period, horizon, duration, step, **kwargs)

Perform a step in the basic MPC scheme without the simulation of the synthesized strategy.

Parameters:

• control_period (int) – The interval duration after which the controller can change the control setting, given in Uppaal Stratego time units.

• horizon (int) – The interval duration for which Uppaal stratego synthesizes a control strategy each MPC step. Is given in the number of control periods.

• duration (int) – The number of times (steps) the MPC scheme should be performed, given as the number of control periods. Is only forwarded to perform_at_start_iteration().

• step (int) – The current iteration step in the basic MPC loop.

• kwargs – Any additional parameters are forwarded to perform_at_start_iteration().

Returns:

The output generated by Uppaal Stratego.

Return type:

str

SafeMPCSetup

class strategoutil.SafeMPCSetup(model_template_file, output_file_path=None, query_file='', model_cfg_dict=None, learning_args=None, verifyta_command='verifyta', external_simulator=False, action_variable=None, debug=False)

Bases: MPCsetup

Class that performs the basic MPC scheme for Uppaal Stratego.

The class monitors and detects whether Uppaal Stratego has sucessfully synthesized a strategy. If not, it will run Uppaal Stratego with an alternative query, which has to be specified by the user, as it depends on the model what a safe query would be.

create_alternative_query_file(horizon, period, final)

Create an alternative query file in case the original query could not be satisfied by Stratego, i.e., it could not find a strategy.

Parameters:

• horizon (int) – The interval duration for which Uppaal stratego synthesizes a control strategy each MPC step. Is given in the number of periods.

• period (int) – The interval duration after which the controller can change the control setting, given in Uppaal Stratego time units.

• final (int) – The time that should be reached by the synthesized strategy, given in Uppaal Stratego time units. Most likely this will be current time + horizon x period.

run_verifyta(horizon, control_period, final, *args, **kwargs)

Run verifyta with the current data stored in this class.

It verifies whether Stratego has successfully synthesized a strategy. If not, it will create an alternative query file and run Stratego again.

Overrides run_verifyta() in MPCsetup.

Parameters:

• horizon (int) – The interval duration for which Uppaal stratego synthesizes a control strategy each MPC step. Is given in the number of periods.

• control_period (int) – The interval duration after which the controller can change the control setting, given in Uppaal Stratego time units.

• final (int) – The time that should be reached by the synthesized strategy, given in Uppaal Stratego time units. Most likely this will be current time + horizon x period.

• *args – Is not used in this method; it is included here to safely override the original method.

• **kwargs – Is not used in this method; it is included here to safely override the original method.

Static methods

The folowing static methods are available.

strategoutil.array_to_stratego(arr)

Convert python array string to C style array used in UPPAAL Stratego. NB, does not include ‘;’ in the end.

Parameters:

arr (str) – The array string to convert.

Returns:

An array string where "[" and "]" are replaced by "{" and "}", respectively.

Return type:

str

strategoutil.check_tool_existence(name)

Check whether ‘name’ is on PATH and marked executable.

From https://stackoverflow.com/questions/11210104/check-if-a-program-exists-from-a-python-script.

Parameters:

name (str) – the name of the tool.

Returns:

True when the tool is found and executable, false otherwise.

Return type:

bool

strategoutil.extract_state(text, var, control_period)

Extract the state from the Uppaal Stratego output at the end of the simulated control period.

Parameters:

• text (str) – The input string containing the Uppaal Stratego output.

• var (str) – The variable name.

• control_period (int) – The interval duration after which the controller can change the control setting, given in Uppaal Stratego time units.

Returns:

The value of the variable at the end of control_period.

Return type:

float

strategoutil.get_duration_action(tuples, max_time=None)

Get tuples (duration, action) from tuples (time, variable) resulted from simulate query.

strategoutil.get_float_tuples(text)

Convert Stratego simulation output to list of tuples (float, float).

Parameters:

text (str) – The input string containing the Uppaal Stratego output.

Returns:

A list of tuples (float, float).

Return type:

list

strategoutil.get_int_tuples(text)

Convert Stratego simulation output to list of tuples (int, int).

Parameters:

text (str) – The input string containing the Uppaal Stratego output.

Returns:

A list of tuples (int, int).

Return type:

list

strategoutil.insert_to_modelfile(model_file, tag, inserted)

Replace tag in model file by the desired text.

Parameters:

• model_file (str) – The file name of the model.

• tag (str) – The tag to replace.

• inserted (str) – The value to replace the tag with.

strategoutil.merge_verifyta_args(cfg_dict)

Concatenate and format a string of verifyta arguments given by the configuration dictionary.

Parameters:

cfg_dict (dict) – The configuration dictionary.

Returns:

String containing all arguments from the configuration dictionary.

Return type:

str

strategoutil.print_progress_bar(i, max, post_text)

Print a progress bar to sys.stdout.

Subsequent calls will override the previous progress bar (given that nothing else has been written to sys.stdout).

From https://stackoverflow.com/a/58602365.

Parameters:

• i (int) – The number of steps already completed.

• max (int) – The maximum number of steps for process to be completed.

• post_text (str) – The text to display after the progress bar.

strategoutil.run_stratego(model_file, query_file='', learning_args=None, verifyta_command='verifyta')

Run command line version of Uppaal Stratego.

Parameters:

• model_file (str) – The file name of the model.

• query_file (str) – The file name of the query.

• learning_args (dict) – Dictionary containing the learning parameters and their values. The learning parameter names should be those used in the command line interface of Uppaal Stratego. You can also include non-learning command line parameters in this dictionary. If a non-learning command line parameter does not take any value, include the empty string "" as value.

• verifyta_command (str) – The command name for running Uppaal Stratego at the user’s machine.

Returns:

The output as produced by Uppaal Stratego.

Return type:

str

strategoutil.successful_result(text)

Verify whether the stratego output is based on the successful synthesis of a strategy.

Parameters:

text (str) – The output generated by Uppaal Stratego.

Returns:

Whether Uppaal Stratego has successfuly ran all queries.

Return type:

bool