Property verification EMBrake

EMBrake_verif.md

no pv, no jitter, delta = 1e-7, GLGM06

first_in = findfirst((X->begin
                #= In[14]:11 =#
                set(X) ⊆ P
            end), vsol.Xk) = 888783
all((X->begin
            #= In[14]:14 =#
            set(X) ⊆ P
        end), vsol.Xk[first_in:end]) = true
tspan(vsol[first_in]) = [0.0887895, 0.0887897]
max values of x
ρ([1.0, 0.0], Flowpipe(vsol.Xk[first_in:first_in])) = 0.04850572743425879
ρ([1.0, 0.0], Flowpipe(vsol.Xk[first_in:end])) = 0.0492794261847055
ρ([1.0, 0.0], Flowpipe(vsol.Xk[end:end])) = 0.0492794261847055
min values of x
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[first_in:first_in]))) = 0.048000002027475806
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[first_in:end]))) = 0.048000002027475806
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[end:end]))) = 0.04854423385309506
max values of v
ρ([0.0, 1.0], Flowpipe(vsol.Xk[first_in:first_in])) = 0.0007994567734929507
ρ([0.0, 1.0], Flowpipe(vsol.Xk[first_in:end])) = 0.0007994567734929507
ρ([0.0, 1.0], Flowpipe(vsol.Xk[end:end])) = 0.0005874379912341613
min values of v
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[first_in:first_in]))) = 0.0006327526764030105
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[first_in:end]))) = 0.0003450783028747313
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[end:end]))) = 0.0003450783028747313
0.0003450783028747313

no pv, no jitter, delta = 1e-8, GLGM06

prob = embrake_no_pv(ζ=0.0, Tsample=1e-4);
# GLGM06, order 1, static
#@time sol = solve(prob, alg=GLGM06(δ=1e-8, max_order=1, static=true, dim=4, ngens=4), max_jumps=2);
@time sol = solve(prob, alg=GLGM06(δ=1e-8, max_order=1, static=true, dim=4, ngens=4), max_jumps=1000);
final_diams(sol)
  0.414480 seconds (271.44 k allocations: 1.691 GiB, 1.54% gc time)
final diameter of current I = 17.746604024816392
final diameter of position x = 0.0009518262957221718

safety_property(sol)
first_in = findfirst((X->begin
                #= In[56]:11 =#
                set(X) ⊆ P
            end), vsol.Xk) = 9015845
all((X->begin
            #= In[56]:14 =#
            set(X) ⊆ P
        end), vsol.Xk[first_in:end]) = true
tspan(vsol[first_in]) = [0.0900594, 0.0900595]
max values of x
ρ([1.0, 0.0], Flowpipe(vsol.Xk[first_in:first_in])) = 0.04868287562433759
ρ([1.0, 0.0], Flowpipe(vsol.Xk[first_in:end])) = 0.04938757641401575
ρ([1.0, 0.0], Flowpipe(vsol.Xk[end:end])) = 0.04938757641401575
min values of x
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[first_in:first_in]))) = 0.04800000018332063
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[first_in:end]))) = 0.04800000018332063
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[end:end]))) = 0.048435750118293576
max values of v
ρ([0.0, 1.0], Flowpipe(vsol.Xk[first_in:first_in])) = 0.0007950689857855407
ρ([0.0, 1.0], Flowpipe(vsol.Xk[first_in:end])) = 0.0007950689857855407
ρ([0.0, 1.0], Flowpipe(vsol.Xk[end:end])) = 0.0006232115341202552
min values of v
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[first_in:first_in]))) = 0.0005699644062819035
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[first_in:end]))) = 0.00030943639703057016
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[end:end]))) = 0.00030943639703057016
0.00030943639703057016

no pv, no jitter, delta = 1e-9, GLGM06

no pv, with jitter, delta = 1e-8, ASB07

prob = embrake_no_pv(ζ=[-1e-8, 1e-7], Tsample=1e-4);
# GLGM06, order 1, static
@time sol = solve(prob, alg=GLGM06(δ=1e-8, max_order=1, static=true, dim=4, ngens=4), max_jumps=1000);
final_diams(sol)

  2.109413 seconds (795.14 k allocations: 1.716 GiB, 0.67% gc time)
final diameter of current I = 17.746604024816392
final diameter of position x = 0.0009518262957221718

safety_property(sol, ngens=4)

first_in = findfirst((X->begin
                #= In[56]:11 =#
                set(X) ⊆ P
            end), vsol.Xk) = 9015845
all((X->begin
            #= In[56]:14 =#
            set(X) ⊆ P
        end), vsol.Xk[first_in:end]) = true
tspan(vsol[first_in]) = [0.0900594, 0.0900595]
max values of x
ρ([1.0, 0.0], Flowpipe(vsol.Xk[first_in:first_in])) = 0.04868287562433759
ρ([1.0, 0.0], Flowpipe(vsol.Xk[first_in:end])) = 0.04938757641401575
ρ([1.0, 0.0], Flowpipe(vsol.Xk[end:end])) = 0.04938757641401575
min values of x
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[first_in:first_in]))) = 0.04800000018332063
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[first_in:end]))) = 0.04800000018332063
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[end:end]))) = 0.048435750118293576
max values of v
ρ([0.0, 1.0], Flowpipe(vsol.Xk[first_in:first_in])) = 0.0007950689857855407
ρ([0.0, 1.0], Flowpipe(vsol.Xk[first_in:end])) = 0.0007950689857855407
ρ([0.0, 1.0], Flowpipe(vsol.Xk[end:end])) = 0.0006232115341202552
min values of v
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[first_in:first_in]))) = 0.0005699644062819035
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[first_in:end]))) = 0.00030943639703057016
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[end:end]))) = 0.00030943639703057016
0.00030943639703057016

pv1, no jitter, delta = 1e-8, ASB07

prob = embrake_pv_1(ζ=0.0, Tsample=1e-4);
# order 3
@time sol = solve(prob, alg=ASB07(δ=1e-8, max_order=3, dim=4, ngens=12, static=true), max_jumps=1_000);
final_diams(sol)
final diameter of current I = 2.9414439401694423
final diameter of position x = 0.0001229578152434907

safety_property(sol, ngens=12)
first_in = findfirst((X->begin
                #= In[56]:11 =#
                set(X) ⊆ P
            end), vsol.Xk) = 8654084
all((X->begin
            #= In[56]:14 =#
            set(X) ⊆ P
        end), vsol.Xk[first_in:end]) = true
tspan(vsol[first_in]) = [0.0865408, 0.0865409]
max values of x
ρ([1.0, 0.0], Flowpipe(vsol.Xk[first_in:first_in])) = 0.048161937383798405
ρ([1.0, 0.0], Flowpipe(vsol.Xk[first_in:end])) = 0.04897071950798819
ρ([1.0, 0.0], Flowpipe(vsol.Xk[end:end])) = 0.04897071950798819
min values of x
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[first_in:first_in]))) = 0.048000000058297514
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[first_in:end]))) = 0.048000000058297514
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[end:end]))) = 0.0488477616927447
max values of v
ρ([0.0, 1.0], Flowpipe(vsol.Xk[first_in:first_in])) = 0.0008165062857196601
ρ([0.0, 1.0], Flowpipe(vsol.Xk[first_in:end])) = 0.0008165062857196601
ρ([0.0, 1.0], Flowpipe(vsol.Xk[end:end])) = 0.0004932708432558988
min values of v
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[first_in:first_in]))) = 0.0007460799328546838
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[first_in:end]))) = 0.0004412635986992693
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[end:end]))) = 0.0004412635986992693
0.0004412635986992693

pv1, with jitter, delta = 1e-8, ASB07

prob = embrake_pv_1(ζ=[-1e-8, 1e-7], Tsample=1e-4);
@time sol = solve(prob, alg=ASB07(δ=1e-8, max_order=1, dim=4, ngens=4, static=true), max_jumps=1);
@time sol = solve(prob, alg=ASB07(δ=1e-8, max_order=1, dim=4, ngens=4, static=true), max_jumps=1000);

final_diams(sol)

  0.722996 seconds (1.23 M allocations: 71.672 MiB)
 16.972784 seconds (110.52 M allocations: 10.243 GiB, 43.87% gc time)
final diameter of current I = 154.207482098115
final diameter of position x = 0.008210036200221565

safety_property(sol, ngens=4, ε=0.005)

first_in = findfirst((X->begin
                #= In[56]:11 =#
                set(X) ⊆ P
            end), vsol.Xk) = 7251941
all((X->begin
            #= In[56]:14 =#
            set(X) ⊆ P
        end), vsol.Xk[first_in:end]) = false
tspan(vsol[first_in]) = [0.0724397, 0.0724398]
max values of x
ρ([1.0, 0.0], Flowpipe(vsol.Xk[first_in:first_in])) = 0.04825960654834148
ρ([1.0, 0.0], Flowpipe(vsol.Xk[first_in:end])) = 0.05301736140115831
ρ([1.0, 0.0], Flowpipe(vsol.Xk[end:end])) = 0.05301736140115831
min values of x
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[first_in:first_in]))) = 0.04500000058208545
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[first_in:end]))) = 0.04480732520093674
-(ρ([-1.0, 0.0], Flowpipe(vsol.Xk[end:end]))) = 0.04480732520093674
max values of v
ρ([0.0, 1.0], Flowpipe(vsol.Xk[first_in:first_in])) = 0.0018794473599369806
ρ([0.0, 1.0], Flowpipe(vsol.Xk[first_in:end])) = 0.0018794473599369806
ρ([0.0, 1.0], Flowpipe(vsol.Xk[end:end])) = 0.0018293238731492435
min values of v
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[first_in:first_in]))) = 0.0007834008334339722
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[first_in:end]))) = -0.0008971962975791285
-(ρ([0.0, -1.0], Flowpipe(vsol.Xk[end:end]))) = -0.0008971962975791285
-0.0008971962975791285