Commit 76b1008b authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain
Browse files

Merge branch 'hotfix/dreal'

parents 2b239d53 77373bd6
......@@ -8,7 +8,7 @@
about/0
]).
version('4.1.8').
version('4.1.9').
copyright(
'Copyright (C) 2003-2018 Inria, EPI Lifeware, Saclay-Île de France, France'
......
%% Cell type:markdown id: tags:
 
# Bouncing ball example
 
classical example of the hybrid system community
classical example of the hybrid system community (https://github.com/dreal/dreal2/tree/master/benchmarks/hybrid_systems/bouncing_ball)
 
implemented here with reactions and events
 
%% Cell type:code id: tags:
 
```
load(ball.bc).
```
 
%% Cell type:code id: tags:
 
```
list_model.
```
 
%%%% Output: execute_result
 
MA(c)for _=[v]=>x.
g/c for v=>_.
MA(D*c)for v=[v]=>_.
present(x,x0).
present(y,3.5).
parameter(
x0 = 8.725,
D = -0.05,
K = 0.75,
g = 9.8,
c = 1.0
).
add_event(x<=0, c = -K*c).
 
%% Cell type:code id: tags:
 
```
list_ode.
```
 
%%%% Output: execute_result
 
[0] d(v)/dt= -1*g/c-D*c*v^2
[1] d(x)/dt=c*v
[2] d(y)/dt=0
 
%% Cell type:markdown id: tags:
 
# Numerical simulation
 
In a hybrid system numerical simulations are relatively time consuming due to the necessity of precisely checking the satisfaction time of events
 
%% Cell type:code id: tags:
 
```
numerical_simulation. plot.
```
 
%%%% Output: display_data
 
 
%% Cell type:markdown id: tags:
 
# Model robustness to parameter perturbations
 
Statistical evaluation by sampling the parameter space
 
This is time consuming since it involves making one simulation for each parameter set
 
The FO-LTL formula defines the amplitude range of x in the domain of the free variable h
The FO-LTL formula defines the height of the first bounce of x in the domain of the free variable h
 
The amplitude 3.96 exceeds here the objective of 3.5, the satisfaction degree is thus greater than one showing some formula robustness
The height 3.96 exceeds here the objective of 3.5, the satisfaction degree is thus greater than one showing some formula robustness
 
However the model robustness w.r.t. (default) parameter perturbations is below one (0.88) showing that some parameter perturbations destroy the amplitude objective.
However the model robustness w.r.t. (default) parameter perturbations is below one (0.88) showing that some parameter perturbations destroy the height objective.
 
%% Cell type:code id: tags:
 
```
%timeout 180
```
 
%%%% Output: execute_result
 
Timeout set to 180
 
%% Cell type:code id: tags:
 
```
validity_domain(F(x < h /\ F(x > h))).
```
 
%%%% Output: execute_result
 
h<3.96646/\h> -1.0e-6
 
%% Cell type:code id: tags:
 
```
satisfaction_degree(F(x < h /\ F(x > h)), [h -> 3.5]).
```
 
%%%% Output: execute_result
 
1.466440
 
%% Cell type:code id: tags:
 
```
seed(0).
robustness(F(x < h /\ F(x > h)), [x0, K, D], [h -> 3.5]).
```
 
%%%% Output: execute_result
 
Time: 158.027 s
Robustness degree: 0.88414
 
%% Cell type:markdown id: tags:
 
# Formula robustness
With a satisfaction degree greater than 1 the formula is already satisfied with some margin
 
Formula robustness can be further optimized by parameter optimization with formula robustness as objective function with no extra cost and much faster computation time than for estimating model robustness
 
It gives an amplitude of 4.84 which obviously improves the satisfaction degree of the formula
It gives a height of 4.84 which obviously improves the satisfaction degree of the formula
 
This is shown to also improve the model robustness (0.93) to parameter perturbations as expected in many examples
 
%% Cell type:code id: tags:
 
```
seed(0).
search_parameters(F(x < h /\ F(x > h)), [5 <= x0 <= 10, 0.5 <= K <= 1.0 , -0.1 <= D <= 0.0], [h -> 3.5], cmaes_stop_fitness: -0.5).
```
 
%%%% Output: execute_result
 
Time: 27.491 s
Stopping reason: Fitness: function value -5.72e-01 <= stopFitness (-5.00e-01)
Best satisfaction degree: 2.339136
[0] parameter(x0=9.555198250463423)
[1] parameter(K=0.8014006370116868)
[2] parameter(D= -0.058468364144163905)
 
%% Cell type:code id: tags:
 
```
numerical_simulation. plot.
```
 
%%%% Output: display_data
 
 
%% Cell type:code id: tags:
 
```
validity_domain(F(x < h /\ F(x > h))).
```
 
%%%% Output: execute_result
 
h<4.83916/\h> -1.0e-6
 
%% Cell type:code id: tags:
 
```
satisfaction_degree(F(x < h /\ F(x > h)), [h -> 3.5]).
```
 
%%%% Output: execute_result
 
2.339120
 
%% Cell type:code id: tags:
 
```
seed(0).
robustness(F(x < h /\ F(x > h)), [x0, K, D], [h -> 3.5]).
```
 
%%%% Output: execute_result
 
Time: 100.736 s
Robustness degree: 0.930547
 
%% Cell type:code id: tags:
 
```
```
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment