Changes POPL25

guberger · Jul 12, 2024 · a80bdce · a80bdce
1 parent 8016514
commit a80bdce
Show file tree

Hide file tree

Showing 6 changed files with 23 additions and 105 deletions.
diff --git a/examples/exa_ICE_Consensus_2D/boogie_prog.txt b/examples/exa_ICE_Consensus_2D/boogie_prog.txt
@@ -7,7 +7,7 @@ procedure main()
     var x : int;
     var y : int;
     t := 0;
-    assume -3 <= x && x <= 3 && -3 <= y && y <= 3;
+    assume -10 <= x && x <= 10 && -10 <= y && y <= 10;
 
     while (*)
     invariant my_inv(t, x, y);
@@ -23,7 +23,7 @@ procedure main()
         }
     }
 
-    assert (-3 <= x && x <= 3 && -3 <= y && y <= 3) && (t < 6 || x == y);
+    assert (-10 <= x && x <= 10 && -10 <= y && y <= 10) && (t < 20 || x == y);
 }
 
 // Times out with bound put on 10
diff --git a/examples/exa_ICE_Consensus_2D/main.jl b/examples/exa_ICE_Consensus_2D/main.jl
@@ -87,9 +87,9 @@ prob = BarrierProblem(
 )
 
 iter_max = Inf
-status, gen_prob, rec = CPB.find_barrier(prob, iter_max,
-                                         solver, print_period=10,
-                                         int_gen=true, int_verif=true)
+status, gen_prob, rec = @time CPB.find_barrier(prob, iter_max,
+                                               solver, print_period=10,
+                                               int_gen=true, int_verif=true)
 @assert status == CPB.BARRIER_FOUND
 
 # Illustration

diff --git a/examples/exa_liu22/main.jl b/examples/exa_liu22/main.jl
@@ -1,5 +1,5 @@
 # To do
 # Should be easy
-# Linear disjunctive invariant generation with Farkas’ lemma
+# Linear disjunctive invariant generation with Farkas' lemma
 # Figure 1
 # https://jhc.sjtu.edu.cn/~hongfeifu/manuscripta.pdf
diff --git a/examples/exa_saturation/main_sat.jl b/examples/exa_saturation/main_sat.jl
@@ -19,22 +19,23 @@ A = [
 b = [1, 0, -0.064, -12.8]
 c = [0, 0, 1, 0]
 urange = (-0.5, 0.0, 0.5)
-xmax = 50
+xmaxs = (2, 1, 1, 25)
+α = 1.0 # parameter [0,1] to tune: the closer to 0, the easier
 
 gfs_safe = GenForm[]
-for i = 1:N
+for (i, xmax) in enumerate(xmaxs)
     push!(gfs_safe, GenForm(1, AffForm(-hot(i, N), -xmax)))
     push!(gfs_safe, GenForm(1, AffForm(+hot(i, N), -xmax)))
 end
 
 pieces = Piece[]
 for u in urange
     afs_dom = [AffForm(+c, -u + 1)] # C*x - u < -1 => -1
-    push!(pieces, Piece(afs_dom, 1, A, -b, 1))
+    push!(pieces, Piece(afs_dom, 1, α*A, -α*b, 1))
     afs_dom = [AffForm(-c, +u - 1), AffForm(+c, -u - 1)] # -1 ≤ C*x - u ≤ 1
-    push!(pieces, Piece(afs_dom, 1, A + b*c', -b*u, 1))
+    push!(pieces, Piece(afs_dom, 1, α*A + α*b*c', -α*b*u, 1))
     afs_dom = [AffForm(-c, +u + 1)] # C*x - u > +1 => +1
-    push!(pieces, Piece(afs_dom, 1, A, +b, 1))
+    push!(pieces, Piece(afs_dom, 1, α*A, +α*b, 1))
 end
 
 # simulation
@@ -47,7 +48,7 @@ ax_ = fig.subplots(
 nstep = 300
 tol_dom = 1e-8
 
-for i = 1:N
+for (i, xmax) in enumerate(xmaxs)
     ax_[i].set_xlim((0, nstep))
     ax_[i].set_xlabel("step")
     ax_[i].set_ylim(-xmax, +xmax)
@@ -82,7 +83,7 @@ prob = BarrierProblem(
     GenForm[], # gfs_inv
     gfs_safe,
     [State(1, zeros(N))], # states_init
-    0.25, # ϵ
+    0.01, # ϵ
     1e-8 # δ
 )
 
@@ -92,48 +93,6 @@ status, gen_prob, rec = @time CPB.find_barrier(prob, iter_max,
 display(status)
 @assert status == CPB.BARRIER_FOUND
 
-# Illustration
-fig = figure(1, figsize=(15, 8))
-ax_ = fig.subplots(
-    nrows=2, ncols=2,
-    gridspec_kw=Dict("wspace"=>0.2, "hspace"=>0.1)
-)
-
-xlims = (Tlo - 0.05*DT, Tup + 0.05*DT)
-ylims = (-5*dt, Tstab + 5*dt)
-lims = ([Tlo - 2*DT, -Tstab - 5*dt], [Tup + 2*DT, 2*Tstab + 5*dt])
-
-for ax in ax_
-    ax.set_xlim(xlims...)
-    ax.set_ylim(ylims...)
-    ax.tick_params(axis="both", labelsize=15)
-end
-
-for loc = 1:4
-    plot_level2D!(ax_[loc], prob.gfs_safe, loc, lims,
-                  fc="none", fa=0, ec="red", ew=1.5)
-end
-
-for loc = 1:4
-    plot_level2D!(ax_[loc], gen_prob.gfs, loc, lims,
-                  fc="gold", ec="gold", fa=0.5, ew=2.5)
-end
-
-for state in gen_prob.states_inside
-    plot_point!(ax_[state.loc], state.x, mc="blue")
-end
-
-for state in gen_prob.states_image
-    plot_point!(ax_[state.loc], state.x, mc="purple")
-end
-
-for link in gen_prob.links_unknown
-    state = link.src
-    plot_point!(ax_[state.loc], state.x, mc="orange")
-end
-
-@assert isempty(gen_prob.states_outside)
-
 ## Algo illustration
 fig = figure(2, figsize=(10, 5))
 ax = fig.add_subplot()

diff --git a/examples/exa_saturation/main_unsat.jl b/examples/exa_saturation/main_unsat.jl
@@ -18,18 +18,19 @@ A = [
 ]
 b = [-1, 0, 0.064, 12.8]
 urange = (-0.5, 0.0, 0.5)
-xmax = 50
+xmaxs = (2, 1, 1, 25)
+α = 0.9 # parameter [0,1] to tune: the closer to 0, the easier
 
 gfs_safe = GenForm[]
-for i = 1:N
+for (i, xmax) in enumerate(xmaxs)
     push!(gfs_safe, GenForm(1, AffForm(-hot(i, N), -xmax)))
     push!(gfs_safe, GenForm(1, AffForm(+hot(i, N), -xmax)))
 end
 
 afs_dom = AffForm[]
 pieces = Piece[]
 for u in urange
-    push!(pieces, Piece(afs_dom, 1, A, b*u, 1))
+    push!(pieces, Piece(afs_dom, 1,α*A, α*b*u, 1))
 end
 
 # simulation
@@ -41,7 +42,7 @@ ax_ = fig.subplots(
 
 nstep = 300
 
-for i = 1:N
+for (i, xmax) in enumerate(xmaxs)
     ax_[i].set_xlim((0, nstep))
     ax_[i].set_xlabel("step")
     ax_[i].set_ylim(-xmax, +xmax)
@@ -53,7 +54,6 @@ end
 for _ = 1:10
     xs = Vector{Float64}[]
     x = zeros(N)
-    x[end] = xmax * 0.8
     push!(xs, x)
     for istep = 1:nstep
         piece = rand(pieces)
@@ -70,7 +70,7 @@ prob = BarrierProblem(
     GenForm[], # gfs_inv
     gfs_safe,
     [State(1, zeros(N))], # states_init
-    0.125, # ϵ
+    0.05, # ϵ
     1e-8 # δ
 )
 
@@ -80,48 +80,6 @@ status, gen_prob, rec = @time CPB.find_barrier(prob, iter_max,
 display(status)
 @assert status == CPB.BARRIER_FOUND
 
-# Illustration
-fig = figure(1, figsize=(15, 8))
-ax_ = fig.subplots(
-    nrows=2, ncols=2,
-    gridspec_kw=Dict("wspace"=>0.2, "hspace"=>0.1)
-)
-
-xlims = (Tlo - 0.05*DT, Tup + 0.05*DT)
-ylims = (-5*dt, Tstab + 5*dt)
-lims = ([Tlo - 2*DT, -Tstab - 5*dt], [Tup + 2*DT, 2*Tstab + 5*dt])
-
-for ax in ax_
-    ax.set_xlim(xlims...)
-    ax.set_ylim(ylims...)
-    ax.tick_params(axis="both", labelsize=15)
-end
-
-for loc = 1:4
-    plot_level2D!(ax_[loc], prob.gfs_safe, loc, lims,
-                  fc="none", fa=0, ec="red", ew=1.5)
-end
-
-for loc = 1:4
-    plot_level2D!(ax_[loc], gen_prob.gfs, loc, lims,
-                  fc="gold", ec="gold", fa=0.5, ew=2.5)
-end
-
-for state in gen_prob.states_inside
-    plot_point!(ax_[state.loc], state.x, mc="blue")
-end
-
-for state in gen_prob.states_image
-    plot_point!(ax_[state.loc], state.x, mc="purple")
-end
-
-for link in gen_prob.links_unknown
-    state = link.src
-    plot_point!(ax_[state.loc], state.x, mc="orange")
-end
-
-@assert isempty(gen_prob.states_outside)
-
 ## Algo illustration
 fig = figure(2, figsize=(10, 5))
 ax = fig.add_subplot()

diff --git a/examples/exa_trains/main_distance.jl b/examples/exa_trains/main_distance.jl
@@ -60,13 +60,14 @@ end
 iter_max = Inf
 # iter_max = 5
 
-for Nt = 1:3
+for Nt = 4:5
+    println("Nt: ", Nt)
     prob = build_problem(Nt, α, β, lim_lo, lim_up, vinit,
                          xsafe_lo, xsafe_up, vsafe)
     println("# pieces: ", length(prob.pieces))
     println("# initial states: ", length(prob.states_init))
     status, gen_prob, rec = @time CPB.find_barrier(prob, iter_max, solver,
-                                                   print_period=10)
+                                                   print_period=100)
     display(status)
     @assert Int(status) ∈ (1, 3)
     ## Algo illustration