GomX-3: Supplementary Material

Battery-Aware Scheduling tool Demo

This page contains the sources and input data for the GomX-3 scheduling tool. Download the zip bundle here.

Note

The tool was developed and carefully tested under a Linux Operating System. It is untested w.r.t. any other operating system.
Windows users may be able to run the tool by providing Windows-style paths to the following options:

  • --tables
  • --export
  • --binaries
  • --model_file
  • --query_file
  • --model_tmpl
  • --query_tmpl

These command line options have reasonable defaults that are Unix-style paths.

Dependencies

  • Python 3
  • Numpy for Python 3
  • Pandas for Python 3
  • MatPlotLib for Python 3
  • Uppaal Cora executable (verifyta)
  • KiBaM validation tool executable (KibamScheduleRunner). [Included]

Uppaal Cora can be downloaded here. After extraction, please put the verifyta binary into the binaries folder of this tool

Usage

The file to execute is schedule.py with your Python3 executable (referred to as python).
Use the --help option to see which options to pass.

python schedule.py --help
usage: schedule.py [-h] [--start START] [--end END] [--tables TABLES]
                   [--export EXPORT] [--binaries BINARIES]
                   [--model-file MODEL_FILE] [--query-file QUERY_FILE]
                   [--model-tmpl MODEL_TMPL] [--query-tmpl QUERY_TMPL]
                   [--capacity CAPACITY] [--init-soc INIT_SOC]
                   [--cora-safe-mode CORA_SAFE_MODE] [--rem-soc REM_SOC]
                   [--soc-penalty-factor SOC_PENALTY_FACTOR] [--no-ratios]
                   [--no-force-take] [--ratio-X RATIO_X] [--ratio-L RATIO_L]
                   [--max-load MAX_LOAD] [--kibam-safe-mode KIBAM_SAFE_MODE]
                   [--discretization DISCRETIZATION] [--c {0.5}] [--p P]
                   [--depl-thresh DEPL_THRESH] [--temporary]

A Demo of the GomX-3 scheduling tool

optional arguments:
  -h, --help            show this help message and exit
  --start START         The starting point of the scheduling interval in UTC
                        of the form 'DD/MM/YYYY hh:mm:ss'. >>> Mind the quotes
                        <<< (default: 20/03/2016 07:00:00)
  --end END             The end point of the scheduling interval in UTC of the
                        form 'DD/MM/YYYY hh:mm:ss'. >>> Mind the quotes <<<
                        (default: 21/03/2016 07:00:00)
  --tables TABLES       Directory of the operational window CSV tables
                        (default: ./tables/)
  --export EXPORT       Directory of where the filled out CSV tables and the
                        plots are saved to (default: ./output/)
  --binaries BINARIES   The tool will search for the Uppaal Cora executable
                        (verifyta) as well as the StoKiBaM tool executable
                        (KibamScheduleRunner) in this directory. (default:
                        ./binaries/)
  --model-file MODEL_FILE
                        Path to the model instance file. If --temporary is
                        set, this will ignored (default: ./models/gomx3.xta)
  --query-file QUERY_FILE
                        Path to the query instance file. If --temporary is
                        set, this will ignored (default: ./models/gomx3.q)
  --model-tmpl MODEL_TMPL
                        Path to the model template file (default:
                        ./templates/gomx3.mtmpl)
  --query-tmpl QUERY_TMPL
                        Path to the query template file (default:
                        ./templates/gomx3.qtmpl)
  --capacity CAPACITY   The capacity of the battery in mJ/s (default:
                        149760000)
  --init-soc INIT_SOC   The initial SoC factor. Initial SoC will be capacity *
                        init-soc (default: 0.9)
  --cora-safe-mode CORA_SAFE_MODE
                        The safe mode threshold factor used in Uppaal Cora.
                        Safe Mode threshold will be capacity * cora-safe-mode
                        (default: 0.55)
  --rem-soc REM_SOC     The factor dictating how much charge should remain at
                        the end of the scheduling horizon. Remaining SoC at
                        the end of the scheduling horizon will be at least
                        capacity * rem-soc (default: 0.6)
  --soc-penalty-factor SOC_PENALTY_FACTOR
                        In the last model checking step, penalize a low SoC
                        level with penalty (capacity - soc) / soc-penalty-
                        factor. Set to 0 to disable. (default: 0)
  --no-ratios           Disables the ratio-heuristic. If set, --ratio-L and
                        --ratio-X will have no effect. (default: False)
  --no-force-take       Disables the take-if-almost-full heuristic. (default:
                        False)
  --ratio-X RATIO_X     X-Band part of the heuristic guiding the ratio between
                        X-Band and L-Band jobs. (default: 2)
  --ratio-L RATIO_L     L-Band part of the heuristic guiding the ratio between
                        X-Band and L-Band jobs. (default: 1)
  --max-load MAX_LOAD   Heuristic limiting the maximal load on the battery
                        allowed. To 'disable' this, set to a high value, like
                        50000 mJ/s (default: 15000)
  --kibam-safe-mode KIBAM_SAFE_MODE
                        The safe mode threshold factor used in the StoKiBaM
                        validation. Safe Mode threshold will be capacity *
                        kibam-safe-mode (default: 0.4)
  --discretization DISCRETIZATION
                        The discretization rate of the StoKiBaM tool. The tool
                        will use matrices of the size discretization X
                        discretization. Thus higher is more precise, but also
                        slower and more memory-heavy. (default: 1000)
  --c {0.5}             Width of the available charge well (default: 0.5)
  --p P                 Diffusion constant of the KiBaM (default: 2e-05)
  --depl-thresh DEPL_THRESH
                        The acceptance threshold of the validation step. Set
                        to value greater than 1 to always pass. (default: 0.1)
  --temporary           A flag saying the instantiated models and intermediate
                        file should be stored in memory to reduce disk-IO
                        (default: False)

The tool does some rudimentary sanity checks when all parameters have been parsed, to ensure suitable operation.

Defaults

Simply running python schedule.py will generate a schedule from 20/03/2016 07:00:00 to 21/03/2016 07:00:00.
All command line options have sensible defaults such that extracting and running the tool should produce schedules.

Input

The tool needs .csv files providing operational windows for each job type.
Such tables are provided in the tables folder, ranging from 20/03/2016 07:00:00 to 22/03/2016 19:00:00

Output after successful excecution

The tool will generate filled-out .csv files ending in Access.csv as well as plots visualising the synthesized schedule and the final SoC distribution as computed by the validation step. These files will be put wherever --export points to.
In addition there will be lots of console output. Among it are some aggregated information regarding the schedule and the validation step, as well as some runtime information.

Possible Uppaal error messages

  • If Uppaal terminates saying -- Property is not satisfied, it means that no schedule could be computed using the given parameters. This could mean that every path leads to depletion.
  • If Uppaal terminates saying Aborted, then you have possibly found a bug.

Model Templates

The model templates are in the templates directory.
The tool will fill them accordingly, such that they can be processed by Uppaal Cora.

Model Instances

Instantiated models will be put into the models folder by default, if --temporary is not set.
The folder already contains filled out models for the range 20/03/2016 07:00:00 to 21/03/2016 07:00:00, for the sake of completeness.

Recommended scheduling horizon length

The tool will most likely be able to synthesize schedules of length up to 36 hours.
Anything much larger will probably fail, due to the limits of Uppaal Cora.