"We call the *test_multiple_strategies_multiprocess* function, to initiate the experiments. It then handles the test_parameters, initiating *do_one_testrun* for each repetition of each set of parameters, and then collects the data in the end.\n",
"\n",
"*do_one_testrun* initiates the Storm Simulator based on the test_parameters, and then calls *c_strategy_whole_run*. *c_strategy_whole_run* keeps track of the restarts and steps, and calls repeatedly *c_strategy_fragment*, until a call of *c_strategy_fragment* results in reaching the step threshold.\n",
"\n",
"*c_strategy_fragment* implements one fragment of the strategy, e.g. what happens between two restarts, or after the last restart. It checks for the occurence of the Rabin labels, and executes entire blocks of steps with *simulator_step_block*."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"#Does 2*num_restart^c steps and checks for the occurence of Rabin Labels\n",
"In the following, we will define the test parameters that were used to conduct the experiments. The first entry denotes the used c. In the PRISM examples, this is followed by the path and the name of the program and property file. Then comes a list of the Rabin pairs. Every rabin pair consists of a good label and a bad label, followed by True if the presence of the label indicates the good/bad label, or False if the absence of the label indicates the good/bad label. Then we have the threshold for the number of steps. If 10num_restart^c is larger than this threshold, the program uses 10num_restart^c instead. Then we set the maximum number of restarts. Ideally, if Pgood>0, this number will never be reached. Finally, we have the type of example ['syntheticPgood','syntheticPmRm', 'normal', 'not_gridworld', 'not_gridworld_Big'].\n",
"\n",
"For the synthetic examples, the parameter sets looks slightly different because the Markov Chains will be generated directly by the Python code."
" 'not_gridworld_VG_Big.pm', 'propNotGridworld.pctl', [[['janitorrow', True], ['x', True]], [['robotrow', False], ['x', True]]], 30000000, 100000], 'not_gridworld_Big'] for i in range(3)]\n",
"testparamsNotGridWorld = [[[i+1, 'PRISM/',\n",
" 'not_gridworld_VG.pm', 'propNotGridworld.pctl', [[['(janitor_row = 1)', True], ['x', True]], [['(robot_row = 1)', False], ['x', True]]], 30000000,100000], 'not_gridworld'] for i in range(3)]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Experiments\n",
"\n",
"Now we just run the experiments. The method test_multiple_strategies_multiprocess takes two arguments: The test parameters, and the number of repetitions. You can alter the maximum number of cores used in the the function itself (Under PROCESSES). You can decide how to increment the nice-values of the individual processes in the do_one_testrun function."
We call the *test_multiple_strategies_multiprocess* function, to initiate the experiments. It then handles the test_parameters, initiating *do_one_testrun* for each repetition of each set of parameters, and then collects the data in the end.
*do_one_testrun* initiates the Storm Simulator based on the test_parameters, and then calls *c_strategy_whole_run*. *c_strategy_whole_run* keeps track of the restarts and steps, and calls repeatedly *c_strategy_fragment*, until a call of *c_strategy_fragment* results in reaching the step threshold.
*c_strategy_fragment* implements one fragment of the strategy, e.g. what happens between two restarts, or after the last restart. It checks for the occurence of the Rabin labels, and executes entire blocks of steps with *simulator_step_block*.
%% Cell type:code id: tags:
``` python
#Does 2*num_restart^c steps and checks for the occurence of Rabin Labels
In the following, we will define the test parameters that were used to conduct the experiments. The first entry denotes the used c. In the PRISM examples, this is followed by the path and the name of the program and property file. Then comes a list of the Rabin pairs. Every rabin pair consists of a good label and a bad label, followed by True if the presence of the label indicates the good/bad label, or False if the absence of the label indicates the good/bad label. Then we have the threshold for the number of steps. If 10num_restart^c is larger than this threshold, the program uses 10num_restart^c instead. Then we set the maximum number of restarts. Ideally, if Pgood>0, this number will never be reached. Finally, we have the type of example ['syntheticPgood','syntheticPmRm', 'normal', 'not_gridworld', 'not_gridworld_Big'].
For the synthetic examples, the parameter sets looks slightly different because the Markov Chains will be generated directly by the Python code.
Now we just run the experiments. The method test_multiple_strategies_multiprocess takes two arguments: The test parameters, and the number of repetitions. You can alter the maximum number of cores used in the the function itself (Under PROCESSES). You can decide how to increment the nice-values of the individual processes in the do_one_testrun function.
