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.