Benchmark Generator for Stratified Controllers of Tank Networks
Contents
Overview
In this work, we present a benchmark generator that constructs benchmark instances in SpaceEx' format [2] of switched buffer networks with stratified controllers.
Features
The generator allows one to scale and tweak the generated benchmark instances in the following ways:
- Number of tanks
- Connections between tanks, i.e., which tanks are connected by channels
- Capacity of each tank
- Minimum and maximum throughput of each channel
- Inflow rate of liquid into the system
- Outflow rate of liquid out of the system
- Usage of three types of dynamics:
- No dynamics: Channels are opened instantaneously with a flow rate in a defined minimum and maximum interval.
- Constant dynamics of the form rate_min' = c1, rate_max'=c2, where c1 and c2 are constants: The minimum and maximum flow rates of channels are increased according to the differential equation provided above.
- Affine dynamics: The minimum and maximum flow rates of channels are increased according to the differential equation v' = c(v_target - v), where v_target is some target velocity and c is a constant.
- Number of controller phases
- Actions in each controller phase, i.e., opening or closing a channel
- Multiple options per controller phase, i.e., the possibility to add non-deterministic choices to each phase
- Specification of the duration in time for each option
- Cyclic or non-cyclic behavior of the controller
Generator Input File
Each benchmark instance is generated from a so-called benchdef file. This file contains a description of the tank network and of the controller with all its phases.
The typical benchdef file looks as follows:
# TANKS:
define tank "MainTank" capacity=10
define tank "SubTank1" capacity=10
define tank "LastTank" capacity=100 sink="true" output=0.5
# CHANNELS:
define channel "RootChannel" root="true" gen_flow=2
define channel "channel1"
define channel "channel2"
# CONNECTIONS:
define connection "RootChannel" target="MainTank"
define connection "channel1" source="MainTank" target="SubTank1"
define connection "channel2" source="SubTank1" target="LastTank"
# PHASES:
define phase "openphase"
define option "option1" duration=40
define option "option1" "RootChannel" action="open"
define option "option1" "channel1" action="open" dynamics="none" \
lowest_throughput=1 highest_throughput=1
define option "option1" "channel2" action="open" dynamics="none" \
lowest_throughput=1 highest_throughput=1
define option "option2" duration=40 condition="fill_LastTank<=10"
define option "option2" "RootChannel" action="open"
define option "option2" "channel1" action="open" dynamics="const" \
min_speed=0.1 max_speed=0.1
define option "option2" "channel2" action="open" dynamics="const" \
min_speed=0.1 max_speed=0.1
define option "option3" duration=40
define option "option3" "channel1" action="open" dynamics="affine" \
coeff=1 min_target=0.6 max_target=0.6
define option "option3" "channel2" action="open" dynamics="affine" \
coeff=1 min_target=0.8 max_target=0.8
define phase "closephase"
define option "option1" duration=20
define option "option1" "RootChannel" action="close"
define option "option1" "channel1" action="close"
define option "option1" "channel2" action="close"
(Note that for style reasons, we split some lines into two parts, indicated with "\". In the correct benchdef format, however, lines must not be split.)
First, the number and names of tanks and their capacities are defined. Note that for the last tank in the network, where the liquid flows out of the system, a outflow rate has to be specified. This last tank is marked with the expression sink="true".
Second, the number and names of the channels occurring in the system are defined. The channel that is supposed to let liquid flow into the system is marked with root="true". For this channel, the rate at which new liquid flows into the system is specified. This inflow rate cannot be changed by the controller as it is constant for a particular system.
The # CONNECTIONS part defines how tanks and channels are connected to each other. For each channel, a source tank identifier and a target tank identifier is provided. Note that in case of the channel that allows liquid to flow into the system, a source tank must not be specified.
The definition of the controller is done in the # PHASES section. First, a phase is defined with a unique identifier. Then, options for each phase are specified. If there is only one option specified, the controller behaves deterministically. If there are multiple options specified, the controller chooses non-deterministically between possible options.
For each option, a maximum duration can be specified. This is the time the controller should wait until further phases are executed. Additionally, it is possible to specify conditions for each option, when it can be executed by the controller. The full set of variables that can be used in the conditional expression can be extracted from the generated SpaceEx XML file. The most important variable, however, is "fill_<TankID>" which can be used to obtain the fill state of tank "<TankID>".
Within each option, one of two actions can be performed: open or close. The "open" action indicates the controller to open the specified channel, the "close" action closes the channel. While the "close" action closes a channel instantaneously, there are two different forms of dynamics that can be specified when a channel should be opened:
dynamics="none": This leads to the instantaneous opening of a channel with specified lower and upper bound for the flow rate, or throughput.dynamics="const": This opens the channel according to the differential equation x' = c, where c is a constant. In other words, c can be seen as the "speed" at which either the minimum or the maximum throughput increases.dynamics="affine": This setting opens the channel according to the differential equation v' = c((target + epsilon) - v), where c is a constant, target is the target velocity, and epsilon is the global precision.
Note that since closing a channel happens instantaneously, no minimum and maximum throughput or speed needs to be specified when the action "close" is chosen.
Be aware that it is only allowed to open or close channels within one option. It is not allowed to mix opening and closing up. In this case, we advise to use a designated phase to close certain channels, if needed.
Usage
The benchmark generator uses Java. To run the generator, use
$ java -jar BenchGenerator.jar
This will generate a new directory that has the same name as the benchdef file in which the generated SpaceEx model file, config file and run script are stored. When you execute the run script, SpaceEx's output and a plot will be generated. Note that the config file that is generated always tells SpaceEx to plot the fill state of the output tank of the system vs. the passed time. This can be altered by changing the value of the variable output-variables.
The following command line switches can be used to further tweak the output:
-t <num>-- Specifies the maximum time frame for the analysis with SpaceEx. When the specified time is reached, SpaceEx will terminate. Default: 1000
-i <num>-- Specifies the maximum number of iterations that SpaceEx should perform. When the specified iteration count is reached, SpaceEx will terminate. Default: 200
-c-- If this flag is used, the controller will be acyclic, meaning that the controller phases are only executed once, instead of starting again with the first phase after the last phase has been executed.
-e <num>,--epsilon <num>-- Specifies the global value for epsilon. In other words, this is the precision with which SpaceEx calculates the target values for affine dynamics.
-h-- Displays the help.
Example 1
The example benchdef file shown above without options "option2" and "option3" in the open phase can be downloaded in the Downloads section of this page. When you generate and run this sample for 10000 iterations with SpaceEx, you obtain the plot shown in Fig. 1.
Fig. 1: The plot from the sample with only the first option.
What you can see in Fig. 1 is that each open phase takes 40 time units and each close phase takes 20 time units, as specified in the benchdef file. Additionally, the fill state of the last tank increases with a constant rate when the channels are open. For example, in the first 40 time units, the fill state reaches 20, since 40sec * 1 unit/sec = 40 units and since the outflow of the system is 0.5 units/sec. What you can also see is that in each close phase, the fill state decreases by 10 units, since 0.5 units/sec flow out of the system and the close phase has the duration of 20 sec.
Example 2
In our work [1], we introduce another example with no dynamics and two options that can be executed by the controller in each open phase of the channels. The close phase, again, has just one option. The controller also behaves in a cyclic manner.
When the controller has the choice between multiple options, SpaceEx analyzes all of the resulting paths. Fig. 2 provides an intuition for this fact. Since the controller is behaving cyclically, every time after closing the channels, there are two new possible traces for the open phase.
Fig. 2: Example plot from the example in [1].
The benchdef file and the resulting SpaceEx models can be downloaded in the Downloads section.
Experimental Option
There is one experimental option for the usage of the benchmark generator. Be advised that SpaceEx may have problems to analyze certain systems or that the produced output may consist of a too coarse over-approximation when this experimental option is used.
Generator Option
The following experimental command line option for the benchmark generator exists:
-l,--lgg-- Specifies to use SpaceEx's LGG scenario. In this case, the generated dynamics are treated differently. All differential equations will have a lower and an upper bound.
Note that this option has only been tested under specialized conditions.
Downloads
- Benchmark generator for switched buffer networks in hybrid systems
- Benchdef and output files of Example 1
- Example from "Benchmark: Stratified Controllers of Tank Networks" paper (Example 2)
- Benchmark suite generated with the benchmark generator including some benchdef files from the paper
For more information, please contact Sergiy Bogomolov or Marius Greitschus.
References
- Stanley Bak, Sergiy Bogomolov, Marius Greitschus, and Taylor T. Johnson. "Benchmark: Stratified Controllers of Tank Networks". Submitted to ARCH 2015. [pdf].
- G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler. "SpaceEx: Scalable Verification of Hybrid Systems". In Computer Aided Verification, pages 379-395, 2011 [bib | Springer].