Merge pull request #351 from JuliaReach/schillic/outsource

Outsource code to NeuralNetworkReachability.jl
JuliaReach · Dec 25, 2023 · 85741d4 · 85741d4 · schillic · Dec 25, 2023
2 parents 41946c0 + 7d4fcd5
commit 85741d4
Show file tree

Hide file tree

Showing 14 changed files with 36 additions and 618 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
diff --git a/.github/workflows/ci_PR.yml b/.github/workflows/ci_PR.yml
diff --git a/Project.toml b/Project.toml
@@ -1,11 +1,12 @@
 name = "ClosedLoopReachability"
 uuid = "73c0b437-a350-4e9b-97ac-9adb151c271b"
-version = "0.3.0"
+version = "0.4.0"
 
 [deps]
 CommonSolve = "38540f10-b2f7-11e9-35d8-d573e4eb0ff2"
 ControllerFormats = "02ac4b2c-022a-44aa-84a5-ea45a5754bcc"
 LazySets = "b4f0291d-fe17-52bc-9479-3d1a343d9043"
+NeuralNetworkReachability = "5de1e908-2f08-45bf-a571-ac88a54f7e7f"
 Parameters = "d96e819e-fc66-5662-9728-84c9c7592b0a"
 ReachabilityAnalysis = "1e97bd63-91d1-579d-8e8d-501d2b57c93f"
 ReachabilityBase = "379f33d0-9447-4353-bd03-d664070e549f"
@@ -15,10 +16,11 @@ Requires = "ae029012-a4dd-5104-9daa-d747884805df"
 [compat]
 CommonSolve = "0.1 - 0.2"
 ControllerFormats = "0.1 - 0.2"
-LazySets = "2.7.6"
+LazySets = "2.11.1"
+NeuralNetworkReachability = "0.1"
 Parameters = "0.12"
 ReachabilityAnalysis = "0.14.5 - 0.22"
-ReachabilityBase = "0.1.1 - 0.2"
+ReachabilityBase = "0.2.1"
 Reexport = "0.2, 1"
 Requires = "0.5, 1"
 julia = "1.6"
diff --git a/models/VertCAS/VertCAS.jl b/models/VertCAS/VertCAS.jl
@@ -181,7 +181,7 @@ end
 function forward_adv(X::Singleton, τ, adv; alg=nothing)
     v = vcat(element(X), τ)
     v = normalize(v)
-    u = forward(CONTROLLERS[adv], v)
+    u = forward(v, CONTROLLERS[adv])
     imax = argmax(u)
     return CTRL_IDX[imax]
 end
@@ -191,7 +191,7 @@ function forward_adv(X::AbstractZonotope, τ, adv; alg=DeepZ())
     Y = cartesian_product(X, Singleton([τ]))
 
     Y = normalize(Y)
-    out = forward(alg, CONTROLLERS[adv], Y)
+    out = forward(Y, CONTROLLERS[adv], alg)
 
     imax = argmax(high(out))
     return CTRL_IDX[imax]

diff --git a/src/ClosedLoopReachability.jl b/src/ClosedLoopReachability.jl
@@ -2,7 +2,6 @@ module ClosedLoopReachability
 
 include("init.jl")
 include("problem.jl")
-include("nnops.jl")
 include("setops.jl")
 include("split.jl")
 include("utils.jl")
@@ -14,19 +13,16 @@ export ControlledPlant,
        BlackBoxController
 
 # splitters
-export BoxSplitter, ZonotopeSplitter,
+export BoxSplitter,
+       ZonotopeSplitter,
        IndexedSplitter,
        SignSplitter
 
 # solvers
-export solve, forward, simulate,
-       DeepZ, SampledApprox, VertexSolver, BoxSolver, SplitSolver, BlackBoxSolver
+export solve, simulate
 
 # utility functions
 export @modelpath,
        print_timed
 
-# parsers
-@reexport using ControllerFormats.FileFormats
-
 end
diff --git a/src/init.jl b/src/init.jl
@@ -3,6 +3,11 @@ using Requires, Reexport
 using ControllerFormats
 # namespace conflict
 using ControllerFormats: Id
+# parsers
+@reexport using ControllerFormats.FileFormats
+
+@reexport using NeuralNetworkReachability.ForwardAlgorithms
+using NeuralNetworkReachability.ForwardAlgorithms: ForwardAlgorithm
 
 @reexport using ReachabilityAnalysis
 # namespace conflict
@@ -15,16 +20,15 @@ using ReachabilityAnalysis: _check_dim, _get_tspan, _get_cpost, _default_cpost,
 
 using ReachabilityBase.Timing,
       ReachabilityBase.Require
+using ReachabilityBase.Arrays: SingleEntryVector
+using ReachabilityBase.Comparison: isapproxzero
 
 using Parameters: @with_kw
 
 # aliases
 const RA = ReachabilityAnalysis
 const IA = IntervalArithmetic
 
-using LazySets: _leq, _geq, isapproxzero, _isapprox, array,
-                remove_zero_generators, remove_zero_columns, subtypes, SingleEntryVector
-
 import CommonSolve: solve
 
 # optional dependencies