juliareach / closedloopreachability.jl Goto Github PK

using NeuralNetworkAnalysis

controller = read_nnet(@modelpath("Single-Pendulum", "controller_single_pendulum.nnet"));

const m = 0.5;
const L = 0.5;
const c = 0.0;
const g = 1.0;
const gL = g/L;
const mL = 1/(m*L^2);

function single_pendulum!(dx, x, params, t)
    dx[1] = x[2]
    dx[2] = gL * sin(x[1]) + mL*(x[3] - c*x[2])
    dx[3] = zero(x[1])
    return dx
end

# X0 = Hyperrectangle([1.1, 0.1], [0.1, 0.1]);  # full initial states
X0 = Singleton([1.2, 0.2]);  # subset of initial states
U0 = ZeroSet(1);
ivp = @ivp(x' = single_pendulum!(x), dim: 3, x(0) ∈ X0 × U0);
vars_idx = Dict(:state_vars=>1:2, :control_vars=>3);
period = 0.05;
T = 0.1;
prob = ControlledPlant(ivp, controller, vars_idx, period);

alg = TMJets(abs_tol=1e-10, orderT=10, orderQ=3);
alg_nn = BoxSolver();
@time sol = NeuralNetworkAnalysis.solve(prob, T=T, alg_nn=alg_nn, alg=alg);
solz = overapproximate(sol, Zonotope);

using DifferentialEquations
sim = simulate(prob, T=T; trajectories=1)

using Plots
vars = (0, 1)
plot()
plot!(solz, vars=vars, lab="")
xl = xlims()
yl = ylims()
for simulation in trajectories(sim)
    for piece in simulation
        plot!(piece, vars=vars, color=:red, lab="")
    end
end
xlims!(xl)
ylims!(yl)
plot!()

julia> @taylorize function test!(dx, x, p, t)
           A = [1.0 0.0; 0.0 1.0]  # not supported
           dx = A * x
       end
ERROR: LoadError: MethodError: no method matching parse!(::Espresso.ExGraph, ::Espresso.ExH{:vcat})

$ julia --color=yes docs/make.jl

┌ Warning: ignoring ACC
└ @ Main ~/.julia/dev/NeuralNetworkAnalysis/docs/generate.jl:18
┌ Warning: ignoring Non-linear Cart-Pole
└ @ Main ~/.julia/dev/NeuralNetworkAnalysis/docs/generate.jl:18
┌ Warning: ignoring Sherlock-Benchmark-10
└ @ Main ~/.julia/dev/NeuralNetworkAnalysis/docs/generate.jl:18
┌ Warning: ignoring Sherlock-Benchmark-7
└ @ Main ~/.julia/dev/NeuralNetworkAnalysis/docs/generate.jl:18
┌ Warning: ignoring Sherlock-Benchmark-9
└ @ Main ~/.julia/dev/NeuralNetworkAnalysis/docs/generate.jl:18
[ Info: generating plain script file from `~/.julia/dev/NeuralNetworkAnalysis/models/mat2NV.jl`
[ Info: writing result to `~/.julia/dev/NeuralNetworkAnalysis/docs/src/models/mat2NV.jl`
[ Info: generating markdown page from `~/.julia/dev/NeuralNetworkAnalysis/models/mat2NV.jl`
[ Info: writing result to `~/.julia/dev/NeuralNetworkAnalysis/docs/src/models/mat2NV.md`
[ Info: generating notebook from `~/.julia/dev/NeuralNetworkAnalysis/models/mat2NV.jl`
[ Info: executing notebook `mat2NV.ipynb`
[ Info: writing result to `~/.julia/dev/NeuralNetworkAnalysis/docs/src/models/mat2NV.ipynb`
[ Info: SetupBuildDirectory: setting up build directory.
ERROR: LoadError: 'models/Sherlock-Benchmark-7.md' is not an existing page!
Stacktrace:
 [1] error(::String) at ./error.jl:33
 [2] walk_navpages(::Bool, ::String, ::String, ::Array{Any,1}, ::Documenter.Documents.NavNode, ::Documenter.Documents.Doc
ument) at /home/mforets/.julia/packages/Documenter/QQWIJ/src/Builder.jl:176
 [3] walk_navpages at /home/mforets/.julia/packages/Documenter/QQWIJ/src/Builder.jl:191 [inlined]
 [4] walk_navpages at /home/mforets/.julia/packages/Documenter/QQWIJ/src/Builder.jl:193 [inlined]
 [5] (::Documenter.Builder.var"#1#2"{Documenter.Documents.NavNode,Documenter.Documents.Document})(::Pair{String,String})
at ./none:0
 [6] iterate at ./generator.jl:47 [inlined]
 [7] collect(::Base.Generator{Array{Any,1},Documenter.Builder.var"#1#2"{Documenter.Documents.NavNode,Documenter.Documents
.Document}}) at ./array.jl:665
 [8] walk_navpages at /home/mforets/.julia/packages/Documenter/QQWIJ/src/Builder.jl:194 [inlined]
 [9] walk_navpages at /home/mforets/.julia/packages/Documenter/QQWIJ/src/Builder.jl:181 [inlined]
 [10] walk_navpages(::String, ::Array{Any,1}, ::Nothing, ::Documenter.Documents.Document) at /home/mforets/.julia/package
s/Documenter/QQWIJ/src/Builder.jl:190
 [11] walk_navpages(::Pair{String,Any}, ::Nothing, ::Documenter.Documents.Document) at /home/mforets/.julia/packages/Docu
menter/QQWIJ/src/Builder.jl:193
 [12] (::Documenter.Builder.var"#1#2"{Nothing,Documenter.Documents.Document})(::Pair{String,Any}) at ./none:0
 [13] iterate at ./generator.jl:47 [inlined]
 [14] collect_to!(::Array{Documenter.Documents.NavNode,1}, ::Base.Generator{Array{Any,1},Documenter.Builder.var"#1#2"{Not
hing,Documenter.Documents.Document}}, ::Int64, ::Int64) at ./array.jl:711
 [15] collect_to_with_first! at ./array.jl:689 [inlined]
 [16] collect(::Base.Generator{Array{Any,1},Documenter.Builder.var"#1#2"{Nothing,Documenter.Documents.Document}}) at ./ar
ray.jl:670
 [17] walk_navpages at /home/mforets/.julia/packages/Documenter/QQWIJ/src/Builder.jl:194 [inlined]
 [18] runner(::Type{Documenter.Builder.SetupBuildDirectory}, ::Documenter.Documents.Document) at /home/mforets/.julia/pac
kages/Documenter/QQWIJ/src/Builder.jl:146
 [19] dispatch(::Type{Documenter.Builder.DocumentPipeline}, ::Documenter.Documents.Document) at /home/mforets/.julia/pack
ages/Documenter/QQWIJ/src/Utilities/Selectors.jl:167
 [20] #2 at /home/mforets/.julia/packages/Documenter/QQWIJ/src/Documenter.jl:237 [inlined]
 [21] cd(::Documenter.var"#2#3"{Documenter.Documents.Document}, ::String) at ./file.jl:104
 [22] #makedocs#1 at /home/mforets/.julia/packages/Documenter/QQWIJ/src/Documenter.jl:236 [inlined]
 [23] top-level scope at /home/mforets/.julia/dev/NeuralNetworkAnalysis/docs/make.jl:9
 [24] include(::Module, ::String) at ./Base.jl:377
 [25] exec_options(::Base.JLOptions) at ./client.jl:288
 [26] _start() at ./client.jl:484
in expression starting at /home/mforets/.julia/dev/NeuralNetworkAnalysis/docs/make.jl:9

A
for i = 1:NSAMPLES
    B
    if i < NSAMPLES
        A
    end
end

for i = 1:NSAMPLES
    A
    B
end

import sys
sys.path.append('/home/mforets/Tools/NNet')
from NNet.python.nnet import *

from NNet.converters.onnx2nnet import onnx2nnet
from onnx import *

## Script showing how to run onnx2nnet
# Min and max values used to bound the inputs
inputMins  = [0.0,-3.141593,-3.141593,100.0,0.0]
inputMaxes = [60760.0,3.141593,3.141593,1200.0,1200.0]

# Mean and range values for normalizing the inputs and outputs. All outputs are normalized with the same value
means  = [1.9791091e+04,0.0,0.0,650.0,600.0,7.5188840201005975]
ranges = [60261.0,6.28318530718,6.28318530718,1100.0,1200.0,373.94992]

# ONNX file to convert to .nnet file
onnxFile = '/home/mforets/Tools/NNet/nnet/TestNetwork2.onnx'

# Convert the file
onnx2nnet(onnxFile, inputMins, inputMaxes, means, ranges)

julia> X0 = Hyperrectangle([1.0, 0.1], [0.0, 0.1]);

controls 1 solve: [-0.67564, -0.543037]
controls 1 simulate: [-0.668787, -0.54751]
controls 2 solve: [-0.609227, -0.42013]
controls 2 simulate: [-0.550897, -0.458256]

solver = Ai2();
split_fun = X -> split(box_approximation(X), 4 * ones(Int, dim(X)));

merge_fun1 = X -> convert(Interval, box_approximation(X));  # takes the box around all results
alg_nn1 = SplitSolver(solver=solver, split_fun=split_fun, merge_fun=merge_fun1);
sol1 = solve(prob, T=T, alg_nn=alg_nn1, alg=alg);

merge_fun2 = X -> convert(Interval, X.array[1]);  # only takes the first result
alg_nn2 = SplitSolver(solver=solver, split_fun=split_fun, merge_fun=merge_fun2);
sol2 = solve(prob, T=T, alg_nn=alg_nn2, alg=alg);