Merge pull request #326 from JuliaReach/schillic/models

Update models and add new patch version

Project.toml

@@ -1,6 +1,6 @@
 name = "ClosedLoopReachability"
 uuid = "73c0b437-a350-4e9b-97ac-9adb151c271b"
-version = "0.2.3"
+version = "0.2.4"
 
 [deps]
 CommonSolve = "38540f10-b2f7-11e9-35d8-d573e4eb0ff2"

models/AttitudeControl/AttitudeControl.jl

@@ -115,6 +115,7 @@ print_timed(res);
 # Finally we plot the results:
 
 using Plots
+import DisplayAs
 
 function plot_helper(fig, vars; show_simulation::Bool=true)
     plot!(fig, sol, vars=vars, color=:yellow, lab="")
@@ -124,13 +125,13 @@ function plot_helper(fig, vars; show_simulation::Bool=true)
     if show_simulation
         plot_simulation!(fig, sim; vars=vars, color=:black, lab="")
     end
+    fig = DisplayAs.Text(DisplayAs.PNG(fig))
 end
 
 vars = (1, 2)
 fig = plot(xlab="ω₁", ylab="ω₂")
 plot_helper(fig, vars)
-
-savefig("AttitudeControl-x1-x2.png")
+# savefig("AttitudeControl-x1-x2.png")
 
 #-
 

models/Quadrotor/Quadrotor.jl

@@ -229,6 +229,7 @@ print_timed(res);
 # Finally we plot the results:
 
 using Plots
+import DisplayAs
 
 function plot_helper(fig, vars; show_simulation::Bool=true)
     plot!(fig, sol, vars=vars, color=:white, lab="")  # to set the plot limits
@@ -237,13 +238,13 @@ function plot_helper(fig, vars; show_simulation::Bool=true)
     if show_simulation
         plot_simulation!(fig, sim; vars=vars, color=:black, lab="")
     end
+    fig = DisplayAs.Text(DisplayAs.PNG(fig))
 end
 
 vars = (0, 3)
 fig = plot(xlab="t", ylab="x₃")
 plot_helper(fig, vars)
-
-savefig("Quadrotor-t-x3.png")
+# savefig("Quadrotor-t-x3.png")
 
 end  #jl
 nothing  #jl

models/Sherlock-Benchmark-9-TORA/Sherlock-Benchmark-9-TORA-ReluTanh.jl

@@ -5,7 +5,7 @@
 module TORA_ReluTanh  #jl
 
 using ClosedLoopReachability, MAT
-using ClosedLoopReachability: UniformAdditivePostprocessing
+using ClosedLoopReachability: LinearMapPostprocessing
 
 # This model consists of a cart attached to a wall with a spring. The cart is
 # free to move on a friction-less surface. The car has a weight attached to an
@@ -55,7 +55,7 @@ vars_idx = Dict(:states=>1:4, :controls=>5)
 ivp = @ivp(x' = TORA!(x), dim: 5, x(0) ∈ X₀ × U)
 
 period = 0.5  # control period
-control_postprocessing = UniformAdditivePostprocessing(-10.0)  # control postprocessing
+control_postprocessing = LinearMapPostprocessing(11.0)  # control postprocessing
 
 prob = ControlledPlant(ivp, controller, vars_idx, period;
                        postprocessing=control_postprocessing)
@@ -66,8 +66,7 @@ T_warmup = 2 * period  # shorter time horizon for dry run
 
 goal_states_x1x2 = Hyperrectangle(low=[-0.1, -0.9], high=[0.2, -0.6])
 goal_states = cartesian_product(goal_states_x1x2, Universe(3))
-predicate =
-    sol -> all(isdisjoint(project(R, [1, 2]), goal_states_x1x2) for F in sol for R in F);
+predicate = sol -> project(sol[end][end], [1, 2]) ⊆ goal_states_x1x2;
 
 # ## Results
 
@@ -88,9 +87,9 @@ function benchmark(; T=T, silent::Bool=false)
     silent || print_timed(res_pred)
 
     if res_pred.value
-        silent || println("The property is violated.")
+        silent || println("The property is satisfied.")
     else
-        silent || println("The property may be satisfied.")
+        silent || println("The property may be violated.")
     end
     return solz
 end
@@ -125,6 +124,7 @@ function plot_helper(fig, vars)
     plot!(fig, goal_states_projected, color=:cyan, lab="goal states")
     plot!(fig, sol, vars=vars, color=:yellow, lab="")
     plot_simulation!(fig, sim; vars=vars, color=:black, lab="")
+    lens!(fig, [0.0, 0.25], [-0.85, -0.7], inset = (1, bbox(0.4, 0.4, 0.3, 0.3)), lc=:black)
     fig = DisplayAs.Text(DisplayAs.PNG(fig))
 end
 

models/Sherlock-Benchmark-9-TORA/Sherlock-Benchmark-9-TORA-Sigmoid.jl

@@ -5,7 +5,7 @@
 module TORA_Sigmoid  #jl
 
 using ClosedLoopReachability, MAT
-using ClosedLoopReachability: UniformAdditivePostprocessing
+using ClosedLoopReachability: LinearMapPostprocessing
 
 # This model consists of a cart attached to a wall with a spring. The cart is
 # free to move on a friction-less surface. The car has a weight attached to an
@@ -55,7 +55,7 @@ vars_idx = Dict(:states=>1:4, :controls=>5)
 ivp = @ivp(x' = TORA!(x), dim: 5, x(0) ∈ X₀ × U)
 
 period = 0.5  # control period
-control_postprocessing = UniformAdditivePostprocessing(-10.0)  # control postprocessing
+control_postprocessing = LinearMapPostprocessing(11.0)  # control postprocessing
 
 prob = ControlledPlant(ivp, controller, vars_idx, period;
                        postprocessing=control_postprocessing)
@@ -67,8 +67,7 @@ T_warmup = 2 * period  # shorter time horizon for dry run
 ## The property for falsifying:
 goal_states_x1x2 = Hyperrectangle(low=[-0.1, -0.9], high=[0.2, -0.6])
 goal_states = cartesian_product(goal_states_x1x2, Universe(3))
-predicate =
-    sol -> all(isdisjoint(project(R, [1, 2]), goal_states_x1x2) for F in sol for R in F);
+predicate = sol -> project(sol[end][end], [1, 2]) ⊆ goal_states_x1x2;
 
 # ## Results
 
@@ -89,9 +88,9 @@ function benchmark(; T=T, silent::Bool=false)
     silent || print_timed(res_pred)
 
     if res_pred.value
-        silent || println("The property is violated.")
+        silent || println("The property is satisfied.")
     else
-        silent || println("The property may be satisfied.")
+        silent || println("The property may be violated.")
     end
     return solz
 end
@@ -126,6 +125,7 @@ function plot_helper(fig, vars)
     plot!(fig, goal_states_projected, color=:cyan, lab="goal states")
     plot!(fig, sol, vars=vars, color=:yellow, lab="")
     plot_simulation!(fig, sim; vars=vars, color=:black, lab="")
+    lens!(fig, [0.1, 0.25], [-0.9, -0.8], inset = (1, bbox(0.4, 0.4, 0.3, 0.3)), lc=:black)
     fig = DisplayAs.Text(DisplayAs.PNG(fig))
 end
 

models/Spacecraft/Spacecraft.jl

@@ -107,7 +107,7 @@ function benchmark(; silent::Bool=false)
     sol = res_sol.value
     silent || print_timed(res_sol)
 
-    ## Next we check the property for an overapproximated flowpipe:
+    ## Next we check the property:
     silent || println("property checking")
     res_pred = @timed predicate_sol(sol)
     silent || print_timed(res_pred)
@@ -130,7 +130,7 @@ print_timed(res);
 import DifferentialEquations
 
 println("simulation")
-res = @timed simulate(prob, T=T, trajectories=10, include_vertices=true)
+res = @timed simulate(prob, T=T, trajectories=1, include_vertices=true)
 sim = res.value
 print_timed(res);
 
@@ -153,27 +153,27 @@ print_timed(res);
 # Finally we plot the results:
 
 using Plots
+import DisplayAs
 
 function plot_helper(fig, vars; show_simulation::Bool=true)
     plot!(fig, sol, vars=vars, color=:yellow, lab="")
     if show_simulation
         plot_simulation!(fig, sim; vars=vars, color=:black, lab="")
     end
+    fig = DisplayAs.Text(DisplayAs.PNG(fig))
 end
 
 vars = (1, 2)
 fig = plot(xlab="x", ylab="y")
 plot_helper(fig, vars)
-
-savefig("Spacecraft-x-y.png")
+# savefig("Spacecraft-x-y.png")
 
 #-
 
 vars = (3, 4)
 fig = plot(xlab="x'", ylab="y'")
 plot_helper(fig, vars)
-
-savefig("Spacecraft-x'-y'.png")
+# savefig("Spacecraft-x'-y'.png")
 
 #-