rename package

JuliaReach · May 27, 2022 · a72d8b3 · a72d8b3
1 parent 39c72c8
commit a72d8b3
Show file tree

Hide file tree

Showing 23 changed files with 45 additions and 72 deletions.
diff --git a/LICENSE b/LICENSE
@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2020 Marcelo Forets
+Copyright (c) 2020 Marcelo Forets and Christian Schilling
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

diff --git a/Project.toml b/Project.toml
@@ -1,4 +1,4 @@
-name = "NeuralNetworkAnalysis"
+name = "ClosedLoopReachability"
 uuid = "73c0b437-a350-4e9b-97ac-9adb151c271b"
 version = "0.1.0"
 

diff --git a/README.md b/README.md
@@ -1,38 +1,11 @@
-# NeuralNetworkAnalysis.jl
+# ClosedLoopReachability.jl
 
-[![Build Status](https://github.com/JuliaReach/NeuralNetworkAnalysis.jl/actions/workflows/ci.yml/badge.svg?branch=master)](https://github.com/JuliaReach/NeuralNetworkAnalysis.jl/actions/workflows/ci.yml?query=branch%3Amaster)
-[![Documentation](https://img.shields.io/badge/docs-latest-blue.svg)](https://juliareach.github.io/NeuralNetworkAnalysis.jl/dev/)
-[![license](https://img.shields.io/github/license/mashape/apistatus.svg?maxAge=2592000)](https://github.com/juliareach/NeuralNetworkAnalysis.jl/blob/master/LICENSE)
-[![Code coverage](http://codecov.io/github/JuliaReach/NeuralNetworkAnalysis.jl/coverage.svg?branch=master)](https://codecov.io/github/JuliaReach/NeuralNetworkAnalysis.jl?branch=master)
+[![Build Status](https://github.com/JuliaReach/ClosedLoopReachability.jl/actions/workflows/ci.yml/badge.svg?branch=master)](https://github.com/JuliaReach/ClosedLoopReachability.jl/actions/workflows/ci.yml?query=branch%3Amaster)
+[![Documentation](https://img.shields.io/badge/docs-latest-blue.svg)](https://juliareach.github.io/ClosedLoopReachability.jl/dev/)
+[![license](https://img.shields.io/github/license/mashape/apistatus.svg?maxAge=2592000)](https://github.com/juliareach/ClosedLoopReachability.jl/blob/master/LICENSE)
+[![Code coverage](http://codecov.io/github/JuliaReach/ClosedLoopReachability.jl/coverage.svg?branch=master)](https://codecov.io/github/JuliaReach/ClosedLoopReachability.jl?branch=master)
 [![Join the chat at https://gitter.im/JuliaReach/Lobby](https://badges.gitter.im/JuliaReach/Lobby.svg)](https://gitter.im/JuliaReach/Lobby?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge)
 
-Methods to verify neural network control systems using reachability analysis
-
-## Links
-
-- [Proceedings of ARCH-COMP20 Category Report:
-Artificial Intelligence and Neural Network Control Systems
-(AINNCS) for Continuous and Hybrid Systems Plants](https://easychair.org/publications/open/Jvwg)
-- https://github.com/verivital/nnv/tree/master/code/nnv/examples/Submission/ARCH_COMP2020
-- [Repo with benchmark models (2020)](https://github.com/verivital/ARCH-COMP2020)
-- [Proceedings of ARCH-COMP 2019 AI-NNCS](https://easychair.org/publications/open/BFKs)
-- [Repo with benchmark models (2019)](https://github.com/verivital/ARCH-COMP19-AINNCS)
-
-## Related tools
-
-- see also the [wiki entry](https://github.com/JuliaReach/NeuralNetworkAnalysis.jl/wiki#related-tools) on related tools
-
-- [NeuralVerification.jl](https://github.com/sisl/NeuralVerification.jl) -- Methods to soundly verify deep neural networks
-
-- [ReachNNStar](https://github.com/JmfanBU/ReachNNStar) -- Reachability Analysis Tool of Neural Network Controlled Systems (NNCSs)
-
-- [NeuralOptimization.jl
-](https://github.com/castrong/NeuralOptimization.jl) -- A compilation of ReLU network optimization algorithms.
-
-- [sherlock](https://github.com/souradeep-111/sherlock) -- Sherlock is a tool for output range anaylsis of Deep Neural Networks with ReLU activation units.
-
-- [NeuralVerifier.jl](https://github.com/jaypmorgan/NeuralVerifier.jl) -- Formal Verification of Deep Neural Networks in Julia
-
-- [Adversarial.jl](https://github.com/jaypmorgan/Adversarial.jl) -- Adversarial attacks for Neural Networks written with FluxML
-
+This package implements methods to analyze closed-loop control systems using reachability analysis.
 
+Currently we support neural-network controllers.
diff --git a/docs/generate.jl b/docs/generate.jl
@@ -1,6 +1,6 @@
 # generate examples
 import Literate
-import NeuralNetworkAnalysis: @modelpath
+import ClosedLoopReachability: @modelpath
 
 MODELS = [
     joinpath(@__DIR__, "..", "models", "ACC"),

diff --git a/docs/make.jl b/docs/make.jl
@@ -1,14 +1,14 @@
-using Documenter, NeuralNetworkAnalysis
+using Documenter, ClosedLoopReachability
 
-DocMeta.setdocmeta!(NeuralNetworkAnalysis, :DocTestSetup,
-                    :(using NeuralNetworkAnalysis); recursive=true)
+DocMeta.setdocmeta!(ClosedLoopReachability, :DocTestSetup,
+                    :(using ClosedLoopReachability); recursive=true)
 
 # generate models
 include("generate.jl")
 
 makedocs(
-    sitename = "NeuralNetworkAnalysis.jl",
-    modules = [NeuralNetworkAnalysis],
+    sitename = "ClosedLoopReachability.jl",
+    modules = [ClosedLoopReachability],
     format = Documenter.HTML(prettyurls = get(ENV, "CI", nothing) == "true",
                              collapselevel = 1,
                              assets = ["assets/aligned.css"]),
@@ -33,6 +33,6 @@ makedocs(
 )
 
 deploydocs(
-    repo = "github.com/JuliaReach/NeuralNetworkAnalysis.jl.git",
+    repo = "github.com/JuliaReach/ClosedLoopReachability.jl.git",
     push_preview=true
 )
diff --git a/docs/src/lib/problems.md b/docs/src/lib/problems.md
@@ -1,6 +1,6 @@
 ```@meta
-DocTestSetup = :(using NeuralNetworkAnalysis)
-CurrentModule = NeuralNetworkAnalysis
+DocTestSetup = :(using ClosedLoopReachability)
+CurrentModule = ClosedLoopReachability
 ```
 
 # Problem types

diff --git a/docs/src/lib/solvers.md b/docs/src/lib/solvers.md
@@ -1,6 +1,6 @@
 ```@meta
-DocTestSetup = :(using NeuralNetworkAnalysis)
-CurrentModule = NeuralNetworkAnalysis
+DocTestSetup = :(using ClosedLoopReachability)
+CurrentModule = ClosedLoopReachability
 ```
 
 # Solvers

diff --git a/docs/src/lib/utils.md b/docs/src/lib/utils.md
@@ -1,6 +1,6 @@
 ```@meta
-DocTestSetup = :(using NeuralNetworkAnalysis)
-CurrentModule = NeuralNetworkAnalysis
+DocTestSetup = :(using ClosedLoopReachability)
+CurrentModule = ClosedLoopReachability
 ```
 
 # Utility functions

diff --git a/models/ACC/ACC.jl b/models/ACC/ACC.jl
@@ -10,8 +10,8 @@
 
 module ACC  #jl
 
-using NeuralNetworkAnalysis, MAT
-using NeuralNetworkAnalysis: FunctionPreprocessing
+using ClosedLoopReachability, MAT
+using ClosedLoopReachability: FunctionPreprocessing
 
 # ## Model
 #

diff --git a/models/Airplane/Airplane.jl b/models/Airplane/Airplane.jl
@@ -20,7 +20,7 @@
 
 module Airplane  #jl
 
-using NeuralNetworkAnalysis
+using ClosedLoopReachability
 
 # The following option determines whether the falsification settings should be
 # used or not. The falsification settings are sufficient to show that the safety

diff --git a/models/Cart-Pole/Cart-Pole.jl b/models/Cart-Pole/Cart-Pole.jl
@@ -30,7 +30,7 @@
 # to the plant is 10.  However if ``\textrm{output}_1 < \textrm{output}_2`` then the input supplied
 # to the plant is -10.
 
-using NeuralNetworkAnalysis
+using ClosedLoopReachability
 
 @taylorize function cartpole!(du, u, p, t)
     local f, m, l, mt, g = 10, 0.1, 0.5, 1.1, 9.8

diff --git a/models/Double-Pendulum/Double-Pendulum.jl b/models/Double-Pendulum/Double-Pendulum.jl
@@ -9,8 +9,8 @@
 
 module DoublePendulum  #jl
 
-using NeuralNetworkAnalysis
-using NeuralNetworkAnalysis: Specification
+using ClosedLoopReachability
+using ClosedLoopReachability: Specification
 
 # The following option determines whether the falsification settings should be
 # used or not. The falsification settings are sufficient to show that the safety

diff --git a/models/Sherlock-Benchmark-10-Unicycle/Sherlock-Benchmark-10-Unicycle.jl b/models/Sherlock-Benchmark-10-Unicycle/Sherlock-Benchmark-10-Unicycle.jl
@@ -4,8 +4,8 @@
 
 module Unicycle  #jl
 
-using NeuralNetworkAnalysis, MAT
-using NeuralNetworkAnalysis: UniformAdditivePostprocessing
+using ClosedLoopReachability, MAT
+using ClosedLoopReachability: UniformAdditivePostprocessing
 
 # This benchmark is that of a unicycle model of a car [^DCS19] taken from Benchmark
 # 10 of the Sherlock tool. It models the dynamics of a car involving 4

diff --git a/models/Sherlock-Benchmark-7/Sherlock-Benchmark-7.jl b/models/Sherlock-Benchmark-7/Sherlock-Benchmark-7.jl
@@ -21,7 +21,7 @@
 # The trained network had 2 hidden layers, with 300 neurons in the first layer,
 # and 200 in the second layer. The sampling time for this controller was 0.5s.
 
-using NeuralNetworkAnalysis
+using ClosedLoopReachability
 
 # The spatial variables are aguemte
 @taylorize function f!(dx, x, p, t)

diff --git a/models/Sherlock-Benchmark-9-TORA/Sherlock-Benchmark-9-TORA-ReluTanh.jl b/models/Sherlock-Benchmark-9-TORA/Sherlock-Benchmark-9-TORA-ReluTanh.jl
@@ -4,8 +4,8 @@
 
 module TORA_ReluTanh  #jl
 
-using NeuralNetworkAnalysis, MAT
-using NeuralNetworkAnalysis: UniformAdditivePostprocessing, NoSplitter
+using ClosedLoopReachability, MAT
+using ClosedLoopReachability: UniformAdditivePostprocessing, NoSplitter
 
 # 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

diff --git a/models/Sherlock-Benchmark-9-TORA/Sherlock-Benchmark-9-TORA-Sigmoid.jl b/models/Sherlock-Benchmark-9-TORA/Sherlock-Benchmark-9-TORA-Sigmoid.jl
@@ -4,8 +4,8 @@
 
 module TORA_Sigmoid  #jl
 
-using NeuralNetworkAnalysis, MAT
-using NeuralNetworkAnalysis: UniformAdditivePostprocessing, NoSplitter
+using ClosedLoopReachability, MAT
+using ClosedLoopReachability: UniformAdditivePostprocessing, NoSplitter
 
 # The following option determines whether the verification settings should be
 # used or not. The verification settings are chosen to show that the safety

diff --git a/models/Sherlock-Benchmark-9-TORA/Sherlock-Benchmark-9-TORA.jl b/models/Sherlock-Benchmark-9-TORA/Sherlock-Benchmark-9-TORA.jl
@@ -4,8 +4,8 @@
 
 module TORA  #jl
 
-using NeuralNetworkAnalysis, MAT
-using NeuralNetworkAnalysis: UniformAdditivePostprocessing, NoSplitter
+using ClosedLoopReachability, MAT
+using ClosedLoopReachability: UniformAdditivePostprocessing, NoSplitter
 
 # The following option determines whether the verification settings should be
 # used or not. The verification settings are chosen to show that the safety

diff --git a/models/Single-Pendulum/Single-Pendulum.jl b/models/Single-Pendulum/Single-Pendulum.jl
@@ -8,8 +8,8 @@
 
 module SinglePendulum  #jl
 
-using NeuralNetworkAnalysis
-using NeuralNetworkAnalysis: SingleEntryVector
+using ClosedLoopReachability
+using ClosedLoopReachability: SingleEntryVector
 
 # The following option determines whether the falsification settings should be
 # used or not. The falsification settings are sufficient to show that the safety

diff --git a/models/VertCAS/VertCAS.jl b/models/VertCAS/VertCAS.jl
@@ -9,7 +9,7 @@
 
 module VertCAS  #jl
 
-using NeuralNetworkAnalysis, LinearAlgebra
+using ClosedLoopReachability, LinearAlgebra
 
 # ## Model
 #
@@ -23,7 +23,7 @@ using NeuralNetworkAnalysis, LinearAlgebra
 # to have a constant horizontal speed, and the intruder (red) is assumed to
 # follow a constant horizontal trajectory towards ownship, see the figure below.
 #
-# ![](https://raw.githubusercontent.com/JuliaReach/NeuralNetworkAnalysis.jl/master/models/VertCAS/nmac.png)
+# ![](https://raw.githubusercontent.com/JuliaReach/ClosedLoopReachability.jl/master/models/VertCAS/nmac.png)
 #
 # The current geometry of the system is described by:
 #

diff --git a/src/NeuralNetworkAnalysis.jl → src/ClosedLoopReachability.jl b/src/NeuralNetworkAnalysis.jl → src/ClosedLoopReachability.jl
@@ -1,4 +1,4 @@
-module NeuralNetworkAnalysis
+module ClosedLoopReachability
 
 include("init.jl")
 include("activation.jl")

diff --git a/src/utils.jl b/src/utils.jl
@@ -210,7 +210,7 @@ A `Network` struct.
 ### Notes
 
 The following activation functions are supported: identity, relu, sigmoid and tanh;
-see `NeuralNetworkAnalysis.ACT_YAML`.
+see `ClosedLoopReachability.ACT_YAML`.
 """
 function read_nnet_yaml(data::Dict)
     NLAYERS = length(data["offsets"])

diff --git a/test/black_box_toy_model.jl b/test/black_box_toy_model.jl
@@ -1,4 +1,4 @@
-using NeuralNetworkAnalysis
+using ClosedLoopReachability
 
 @taylorize function sys!(dx, x, p, t)
     dx[1] = x[2]

diff --git a/test/runtests.jl b/test/runtests.jl
@@ -1,4 +1,4 @@
-using NeuralNetworkAnalysis
+using ClosedLoopReachability
 using Test
 
 @time @testset "Toy model (black-box network)" begin include("black_box_toy_model.jl") end