Commit 77373bd6 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain
Browse files

text in ball.ipynb

parent 2b239d53
...@@ -8,7 +8,7 @@ ...@@ -8,7 +8,7 @@
about/0 about/0
]). ]).
version('4.1.8'). version('4.1.9').
copyright( copyright(
'Copyright (C) 2003-2018 Inria, EPI Lifeware, Saclay-Île de France, France' 'Copyright (C) 2003-2018 Inria, EPI Lifeware, Saclay-Île de France, France'
......
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
   
# Bouncing ball example # 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 implemented here with reactions and events
   
%% Cell type:code id: tags: %% Cell type:code id: tags:
   
``` ```
load(ball.bc). load(ball.bc).
``` ```
   
%% Cell type:code id: tags: %% Cell type:code id: tags:
   
``` ```
list_model. list_model.
``` ```
   
%%%% Output: execute_result %%%% Output: execute_result
   
MA(c)for _=[v]=>x. MA(c)for _=[v]=>x.
g/c for v=>_. g/c for v=>_.
MA(D*c)for v=[v]=>_. MA(D*c)for v=[v]=>_.
present(x,x0). present(x,x0).
present(y,3.5). present(y,3.5).
parameter( parameter(
x0 = 8.725, x0 = 8.725,
D = -0.05, D = -0.05,
K = 0.75, K = 0.75,
g = 9.8, g = 9.8,
c = 1.0 c = 1.0
). ).
add_event(x<=0, c = -K*c). add_event(x<=0, c = -K*c).
   
%% Cell type:code id: tags: %% Cell type:code id: tags:
   
``` ```
list_ode. list_ode.
``` ```
   
%%%% Output: execute_result %%%% Output: execute_result
   
[0] d(v)/dt= -1*g/c-D*c*v^2 [0] d(v)/dt= -1*g/c-D*c*v^2
[1] d(x)/dt=c*v [1] d(x)/dt=c*v
[2] d(y)/dt=0 [2] d(y)/dt=0
   
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
   
# Numerical simulation # Numerical simulation
   
In a hybrid system numerical simulations are relatively time consuming due to the necessity of precisely checking the satisfaction time of events 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: %% Cell type:code id: tags:
   
``` ```
numerical_simulation. plot. numerical_simulation. plot.
``` ```
   
%%%% Output: display_data %%%% Output: display_data
   
   
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
   
# Model robustness to parameter perturbations # Model robustness to parameter perturbations
   
Statistical evaluation by sampling the parameter space Statistical evaluation by sampling the parameter space
   
This is time consuming since it involves making one simulation for each parameter set 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: %% Cell type:code id: tags:
   
``` ```
%timeout 180 %timeout 180
``` ```
   
%%%% Output: execute_result %%%% Output: execute_result
   
Timeout set to 180 Timeout set to 180
   
%% Cell type:code id: tags: %% Cell type:code id: tags:
   
``` ```
validity_domain(F(x < h /\ F(x > h))). validity_domain(F(x < h /\ F(x > h))).
``` ```
   
%%%% Output: execute_result %%%% Output: execute_result
   
h<3.96646/\h> -1.0e-6 h<3.96646/\h> -1.0e-6
   
%% Cell type:code id: tags: %% Cell type:code id: tags:
   
``` ```
satisfaction_degree(F(x < h /\ F(x > h)), [h -> 3.5]). satisfaction_degree(F(x < h /\ F(x > h)), [h -> 3.5]).
``` ```
   
%%%% Output: execute_result %%%% Output: execute_result
   
1.466440 1.466440
   
%% Cell type:code id: tags: %% Cell type:code id: tags:
   
``` ```
seed(0). seed(0).
robustness(F(x < h /\ F(x > h)), [x0, K, D], [h -> 3.5]). robustness(F(x < h /\ F(x > h)), [x0, K, D], [h -> 3.5]).
``` ```
   
%%%% Output: execute_result %%%% Output: execute_result
   
Time: 158.027 s Time: 158.027 s
Robustness degree: 0.88414 Robustness degree: 0.88414
   
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
   
# Formula robustness # Formula robustness
With a satisfaction degree greater than 1 the formula is already satisfied with some margin 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 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 This is shown to also improve the model robustness (0.93) to parameter perturbations as expected in many examples
   
%% Cell type:code id: tags: %% Cell type:code id: tags:
   
``` ```
seed(0). 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). 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 %%%% Output: execute_result
   
Time: 27.491 s Time: 27.491 s
Stopping reason: Fitness: function value -5.72e-01 <= stopFitness (-5.00e-01) Stopping reason: Fitness: function value -5.72e-01 <= stopFitness (-5.00e-01)
Best satisfaction degree: 2.339136 Best satisfaction degree: 2.339136
[0] parameter(x0=9.555198250463423) [0] parameter(x0=9.555198250463423)
[1] parameter(K=0.8014006370116868) [1] parameter(K=0.8014006370116868)
[2] parameter(D= -0.058468364144163905) [2] parameter(D= -0.058468364144163905)
   
%% Cell type:code id: tags: %% Cell type:code id: tags:
   
``` ```
numerical_simulation. plot. numerical_simulation. plot.
``` ```
   
%%%% Output: display_data %%%% Output: display_data
   
   
%% Cell type:code id: tags: %% Cell type:code id: tags:
   
``` ```
validity_domain(F(x < h /\ F(x > h))). validity_domain(F(x < h /\ F(x > h))).
``` ```
   
%%%% Output: execute_result %%%% Output: execute_result
   
h<4.83916/\h> -1.0e-6 h<4.83916/\h> -1.0e-6
   
%% Cell type:code id: tags: %% Cell type:code id: tags:
   
``` ```
satisfaction_degree(F(x < h /\ F(x > h)), [h -> 3.5]). satisfaction_degree(F(x < h /\ F(x > h)), [h -> 3.5]).
``` ```
   
%%%% Output: execute_result %%%% Output: execute_result
   
2.339120 2.339120
   
%% Cell type:code id: tags: %% Cell type:code id: tags:
   
``` ```
seed(0). seed(0).
robustness(F(x < h /\ F(x > h)), [x0, K, D], [h -> 3.5]). robustness(F(x < h /\ F(x > h)), [x0, K, D], [h -> 3.5]).
``` ```
   
%%%% Output: execute_result %%%% Output: execute_result
   
Time: 100.736 s Time: 100.736 s
Robustness degree: 0.930547 Robustness degree: 0.930547
   
%% Cell type:code id: tags: %% 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