Script for SLICOT benchmarks

[mforets]

We used to have a script to run all SLICOT benchmarks. This shall now be more automatic by calling such models from ReachabilityModels.jl.

In this issue we can track the progress for each model.

Tables:

• First table: runtime (in seconds) for different algorithms in ReachabilityAnalysis.jl, and the reference runtime in HSCC'18 article (TAC).
• Second table: width of the final reach-set for the variables computed.

Motor

Settings: step-size: 1e-3, dim: 8, property: x5 < 0.45 || x5 > 0.6.

Runtime:

Vars	LGG09	HSCC18
x5, -x5		0.5
box		3.85

Accuracy:

Vars	LGG09	HSCC18
x5, -x5		-

Building

Settings: step-size: 1e-3, dim: 48, property: x25 < 6e-3.

Runtime:

Vars	LGG09	HSCC18
x25		1.71
box		66.5

Accuracy:

Vars	LGG09	HSCC18
x25, -x25
box

PDE

Settings: step-size: 1e-3, dim: 84, property: y1 < 12.

Runtime:

Vars	LGG09	HSCC18
y1		3.56
box		197

Accuracy:

Vars	LGG09	HSCC18
y1, -y1
box

Heat

Settings: step-size: 1e-3, dim: 200, property: x133 < 0.1.

Runtime:

Vars	LGG09	HSCC18
x133	0.47	8.28
box	98	1050

Accuracy:

Vars	LGG09	HSCC18
x133, -x133	[-0.056793, 0.056862]

ISS

Settings: step-size: 1e-3, dim: 270, property: -7e-4 <= y3 <= 7e-4.

Runtime:

Vars	LGG09	HSCC18
y3		0.95
box		126

Accuracy:

Vars	LGG09	HSCC18
y3, -y3
box

Beam

Settings: step-size: 1e-3, dim: 348, property: x89 < 2100.

Runtime:

Vars	LGG09	HSCC18
x89		26.7
box		2960

Accuracy:

Vars	LGG09	HSCC18
x89, -x89
box

MNA1

Settings: step-size: 1e-3, dim: 578, property: x1 < 0.5.

Runtime:

Vars	LGG09	HSCC18
x1		90
box		580

Accuracy:

Vars	LGG09	HSCC18
x1. -x1
box

FOM

Settings: step-size: 1e-3, dim: 1006, property: y1 < 185.

Runtime:

Vars	LGG09	HSCC18
y1		3.67
box		1060

Accuracy:

Vars	LGG09	HSCC18
y1, -y1
box

MNA5

Settings: step-size: 1e-3, dim: 10913, property: x1 < 0.2 & x2 < 0.15.

Runtime:

Vars	LGG09	HSCC18
x1, x2		1220
box		TO

Accuracy:

Vars	LGG09	HSCC18
x1, -x1, x2, -x2
box