diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Attitude Control/reach.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Attitude Control/reach.m index f223997b83..55731c0cd8 100644 --- a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Attitude Control/reach.m +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Attitude Control/reach.m @@ -1,4 +1,4 @@ -% function t = reach() +function t = reach() %% Reachability analysis of the aircarft attitude benchmark @@ -97,7 +97,7 @@ exportgraphics(f,'attitude_5v6.pdf','ContentType', 'vector'); end -% end +end %% Helper function function init_set = plantReach(plant,init_set,input_set,algoC) diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Benchmark10-Unicycle/reach.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Benchmark10-Unicycle/reach.m index f31ab25431..5c1dccea3b 100644 --- a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Benchmark10-Unicycle/reach.m +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Benchmark10-Unicycle/reach.m @@ -1,4 +1,4 @@ -% function t = reach() +function t = reach() %% Reachability analysis of the Unicycle (benchmark 10) @@ -33,8 +33,8 @@ % Store all reachable sets reachAll = init_set; % Execute reachabilty analysis -% steps = 25; - steps = 50; + steps = 25; + % steps = 50; reachOptions.reachMethod ='approx-star'; t = tic; for i=1:steps @@ -80,7 +80,7 @@ exportgraphics(f1,'unicycle_3v4.pdf', 'ContentType', 'vector'); end -% end +end %% Helper function function init_set = plantReach(plant,init_set,input_set,algoC) diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/reach.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/reach.m index f89c5c7fba..73cc6671af 100644 --- a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/reach.m +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/reach.m @@ -1,4 +1,4 @@ -% function t = reach() +function t = reach() %% Reachability analysis of Cartpole Benchmark @@ -13,6 +13,7 @@ plant = NonLinearODE(4,1,@dynamics, reachStep, controlPeriod, eye(4)); plant.set_tensorOrder(2); + t = tic; %% Reachability analysis @@ -28,17 +29,25 @@ reachAll = init_set; num_steps = 500; reachOptions.reachMethod = 'approx-star'; - t = tic; + % t = tic; for i=1:num_steps disp(i); % Compute controller output set input_set = net.reach(init_set,reachOptions); % Compute plant reachable set - init_set = plant.stepReachStar(init_set, input_set,'lin'); + init_set = plantReach(plant,init_set,input_set,'lin'); reachAll = [reachAll init_set]; - toc(t); + % toc(t); end - t = toc(t); + % t = toc(t); + end + t = toc(t); + + % Save results + if is_codeocean + save('/results/logs/cartpole.mat', 'reachAll','t','-v7.3'); + else + save('cartpole.mat', 'reachAll','t','-v7.3'); end %% Visualize results @@ -56,11 +65,22 @@ % ylabel('\theta'); % xlim([0 0.6]) % ylim([0.95 1.25]) + % Save figure - % if is_codeocean - % exportgraphics(f,'/results/logs/cartpole.pdf', 'ContentType', 'vector'); - % else - % exportgraphics(f,'cartpole.pdf','ContentType', 'vector'); - % end + if is_codeocean + exportgraphics(f,'/results/logs/cartpole.pdf', 'ContentType', 'vector'); + else + exportgraphics(f,'cartpole.pdf','ContentType', 'vector'); + end + +end -% end \ No newline at end of file +%% Helper function +function init_set = plantReach(plant,init_set,input_set,algoC) + nS = length(init_set); % based on approx-star, number of sets should be equal + ss = []; + for k=1:nS + ss =[ss plant.stepReachStar(init_set(k), input_set(k),algoC)]; + end + init_set = ss; +end \ No newline at end of file diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Docking/reach.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Docking/reach.m index 846d3b62f0..ecd29a897c 100644 --- a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Docking/reach.m +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Docking/reach.m @@ -1,64 +1,80 @@ -% function t = reach() +function t = reach() -%% Reachability analysis of the Docking benchmark - -%% Load components - -net = load_NN_from_mat('model.mat'); -controlPeriod = 1; -reachstep = 0.05; -plant = NonLinearODE(4,2,@dynamics, reachstep, controlPeriod, eye(4)); -plant.set_taylorTerms(4); -plant.set_zonotopeOrder(50); -plant.set_tensorOrder(2); -% plant.set_intermediateOrder(50); -% plant.set_polytopeOrder(50);% error = 0.001; -% error = 0.0005; -% plant.options.maxError = [error; error; error; error]; - -%% Reachability analysis + %% Reachability analysis of the Docking benchmark + + %% Load components + + net = load_NN_from_mat('model.mat'); + controlPeriod = 1; + reachstep = 0.05; + plant = NonLinearODE(4,2,@dynamics, reachstep, controlPeriod, eye(4)); + plant.set_taylorTerms(4); + plant.set_zonotopeOrder(50); + plant.set_tensorOrder(2); + % plant.set_intermediateOrder(50); + % plant.set_polytopeOrder(50);% error = 0.001; + % error = 0.0005; + % plant.options.maxError = [error; error; error; error]; + + %% Reachability analysis + + % Initial set + lb = [87; 87 ; -0.01; -0.01]; + % ub = [106; 106; 0.28; 0.28]; + ub = [89; 89; 0.01; 0.01]; + init_set = Star(lb,ub); + % Store all reachable sets + reachAll = init_set; + reachOptions.reachMethod = 'approx-star'; + % Execute reachabilty analysis + steps = 4; + i = 1; + prop = true; + t = tic; + while prop && i < steps + % Compute controller output set + input_set = net.reach(init_set,reachOptions); + % Compute plant reachable set + init_set = plantReach(plant,init_set,input_set,'lin'); + reachAll = [reachAll init_set]; + prop = verify_spec(init_set); + i = i+1; + end + t = toc(t); + + % Save results + if is_codeocean + save('/results/logs/docking.mat', 'reachAll','t','-v7.3'); + else + save('docking.mat', 'reachAll','t','-v7.3'); + end + + + %% Visualize results + f = figure; + hold on; + Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,1,2,'b'); + grid; + xlabel('x1'); + ylabel('x2'); + + f1 = figure; + hold on; + Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,3,4,'b'); + grid; + xlabel('x1'); + ylabel('x2'); + + % Save figure + if is_codeocean + exportgraphics(f,'/results/logs/docking1v2.pdf', 'ContentType', 'vector'); + exportgraphics(f1,'/results/logs/docking3v4.pdf', 'ContentType', 'vector'); + else + exportgraphics(f,'docking1v2.pdf','ContentType', 'vector'); + exportgraphics(f1,'docking3v4.pdf', 'ContentType', 'vector'); + end -% Initial set -lb = [87; 87 ; -0.01; -0.01]; -% ub = [106; 106; 0.28; 0.28]; -ub = [89; 89; 0.01; 0.01]; -init_set = Star(lb,ub); -% Store all reachable sets -reachAll = init_set; -reachOptions.reachMethod = 'approx-star'; -% Execute reachabilty analysis -steps = 4; -i = 1; -prop = true; -t = tic; -while prop && i < steps - % Compute controller output set - input_set = net.reach(init_set,reachOptions); - % Compute plant reachable set - init_set = plantReach(plant,init_set,input_set,'lin'); - reachAll = [reachAll init_set]; - prop = verify_spec(init_set); - i = i+1; end -t = toc(t); - - -%% Visualize results -f = figure; -hold on; -Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,1,2,'b'); -grid; -xlabel('x1'); -ylabel('x2'); -% saveas(f,[path_out, 'reach1v2.pdf']); - -f1 = figure; -hold on; -Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,3,4,'b'); -grid; -xlabel('x1'); -ylabel('x2'); -% saveas(f1,[path_out, 'reach3v4.pdf']); %% Helper function function init_set = plantReach(plant,init_set,input_set,algoC) diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Double_Pendulum/reach_more.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Double_Pendulum/reach_more.m index 0c1aceba88..6ce2a9010d 100644 --- a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Double_Pendulum/reach_more.m +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Double_Pendulum/reach_more.m @@ -1,4 +1,4 @@ -% function t = reach_more() +function t = reach_more() %% Reachability analysis of Double Pendulum Benchmark @@ -79,7 +79,7 @@ exportgraphics(f1,'double_pendulum_more_3v4.pdf','ContentType', 'vector'); end -% end +end %% Helper function function init_set = plantReach(plant,init_set,input_set,algoC) diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_point.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_point.m index 725ec4c9c9..6344506b45 100644 --- a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_point.m +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_point.m @@ -1,4 +1,4 @@ -% function rT = reach_point() +function rT = reach_point() %% Reachability analysis of NAV Benchmark @@ -118,4 +118,4 @@ exportgraphics(f,'nav-point.pdf','ContentType', 'vector'); end - % end \ No newline at end of file +end \ No newline at end of file diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_set.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_set.m index 20de7d8755..78af57cf7b 100644 --- a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_set.m +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_set.m @@ -1,4 +1,4 @@ -% function rT = reach_set() +function rT = reach_set() %% Reachability analysis of NAV Benchmark @@ -92,4 +92,4 @@ % end -% end \ No newline at end of file +end \ No newline at end of file diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/run_all.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/run_all.m index 2c84abfe79..011404a8a8 100644 --- a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/run_all.m +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/run_all.m @@ -6,68 +6,86 @@ function run_all() % Turn off figure display set(0,'DefaultFigureVisible','off'); - % Let's compare how things look after almost a year with the recently updated CORA -% %% Begin benchmark evaluation +%% Begin benchmark evaluation % ACC + cd ACC; + try acc = reach(); % verified (~ 15 seconds) catch acc = -1; end - cd ..; + cd ..; % Benchmark-9 (Tora) cd Tora_Heterogeneous; + try tora_relutanh = reachTora_reluTanh(); % verified w/ input partition (~ 38 mins) catch tora_relutanh = -1; end + try tora_sigmoid = reachTora_sigmoid(); % verified w/ input partition (~ 1 hour) catch tora_sigmoid = -1; end + cd ..; cd Benchmark9-Tora; + try tora_relu = reach(); % verified (~25 seconds) catch tora_relu = -1; end - cd ..; + cd ..; % Benchmark-10 (Unicycle) - % unicycle = '-'; % overapprox -> unknown + + cd Benchmark10-Unicycle/; + + try + unicycle = reach(); % overapprox -> unknown + catch + unicycle = -1; + end % VCAS + cd VCAS; + try - vcas = run_vcas(); % verified (~20 seconds) + vcas = run_vcas(); % verified (~20 seconds total) catch - vcas - 1; + vcas = -1; end - cd ..; + cd ..; % Single Pendulum + cd Single_Pendulum; + try sp = reach(); % falsified (reach sets ~3 seconds) catch sp = -1; end - cd ..; + cd ..; % Double Pendulum + cd Double_Pendulum; + try dp_more = reach_more(); % falsified (reach sets ~ 30 seconds) catch @@ -79,90 +97,158 @@ function run_all() catch dp_less = -1; end - cd ..; + cd ..; % Airplane + cd Airplane; + try airplane = reach(); % Falsified (reach sets ~ 7 seconds) catch airplane = -1; end + cd ..; % Attitude Control - % attitude = '-'; % sigmoid controller -> overapprox -> unknown + + cd('Attitude Control'); + + try + attitude = reach(); % sigmoid controller -> overapprox -> unknown + catch + attitude = -1; + end + + cd ..; % Quad - % quad = '-'; % sigmoid controller -> overapprox -> unknown + + cd QUAD; + + try + quad = reach(); + % quad = '-'; % sigmoid controller -> overapprox -> unknown + catch + quad = -1; + end + + cd ..; % Spacecraft Docking - % spacecraft = '-'; % overapproximation -> unknown - -% %% Save results in CSV file for submission - - % % Create results variable - % resultsCSV = cell(21, 4); % column names + # of benchmarks (including instances) - % resultsCSV(1, :) = {'benchmark','instance','result','time'}; % columns names - % - % % ACC - % acc_csv = {'ACC', 'relu', 'verified', acc}; - % resultsCSV(2,:) = acc_csv; - % - % % Benchmark-9 (Tora) - % tora_csv(1,:) = {'TORA', 'relu', 'verified', tora_relu}; - % tora_csv(2,:) = {'TORA', 'relutanh', 'verified', tora_relutanh}; - % tora_csv(3,:) = {'TORA', 'sigmoid', 'verified', tora_sigmoid}; - % resultsCSV(3:5,:) = tora_csv; - % - % % Benchmark-10 (Unicycle) - % unicycle_csv = {'Unicycle', '', 'unknown', unicycle}; - % resultsCSV(6,:) = unicycle_csv; - % - % % VCAS - % vcas_m19 = {'VCAS', 'middle19', 'verified', vcas(1,1)}; - % vcas_m22 = {'VCAS', 'middle22', 'verified', vcas(2,1)}; - % vcas_m25 = {'VCAS', 'middle25', 'violated', vcas(3,1)}; - % vcas_m28 = {'VCAS', 'middle28', 'violated', vcas(4,1)}; - % vcas_w19 = {'VCAS', 'worst19', 'verified', vcas(1,2)}; - % vcas_w22 = {'VCAS', 'worst22', 'violated', vcas(2,2)}; - % vcas_w25 = {'VCAS', 'worst25', 'violated', vcas(3,2)}; - % vcas_w28 = {'VCAS', 'worst28', 'violated', vcas(4,2)}; - % resultsCSV(7:14,:) = [vcas_m19; vcas_m22; vcas_m25; vcas_m28; vcas_w19; vcas_w22; vcas_w25; vcas_w28]; - % - % % Single Pendulum - % sp_csv = {'SinglePendulum', '', 'violated', sp}; - % resultsCSV(15,:) = sp_csv; - % - % % Double Pendulum - % dp_csv(1,:) = {'DoublePendulum', 'more', 'violated', dp_more}; - % dp_csv(2,:) = {'DoublePendulum', 'less', 'violated', dp_less}; - % resultsCSV(16:17, :) = dp_csv; - % - % % Airplane - % airplane_csv = {'Airplane', '', 'violated', airplane}; - % resultsCSV(18,:) = airplane_csv; - % - % % Attitude Control - % attitude_csv = {'AttitudeControl','','unknown',attitude}; - % resultsCSV(19,:) = attitude_csv; - % - % % Quad - % quad_csv = {'Quadrotor', '', 'unknown', quad}; - % resultsCSV(20,:) = quad_csv; - % - % % Spacecraft Docking - % spacecraft_csv = {'Spacecraft', '','unknown',spacecraft}; - % resultsCSV(21,:) = spacecraft_csv; - % - % - % - % % Create and save csv files with results - % if is_codeocean - % writecell(resultsCSV, '/results/results.csv'); % ARCH repeatability specific - % else - % writecell(resultsCSV, 'results.csv'); - % end + + cd Docking; + + try + spacecraft = reach(); % overapproximation -> unknown + catch + spacecraft = -1; + end + + cd ..; + + %%%%%%%%% New from 2024 %%%%%%%%%%% + + % NAV + + cd NAV/; + + try + navPoint = reach_point(); + catch + navPoint = -1; + end + + try + navSet = reach_set(); + catch + navSet = -1; + end + + % Cartpole + + cd Cartpole; + + try + cartpole = reach(); + catch + cartpole = -1; + end + +%% Save results in CSV file for submission + + % Create results variable + resultsCSV = cell(24, 4); % column names + # of benchmarks (including instances) + resultsCSV(1, :) = {'benchmark','instance','result','time'}; % columns names + + % ACC + acc_csv = {'ACC', 'safety', 'verified', acc}; + resultsCSV(2,:) = acc_csv; + + % Airplane + airplane_csv = {'Airplane', 'continuous', 'violated', airplane}; + resultsCSV(3,:) = airplane_csv; + + + % Attitude Control + attitude_csv = {'AttitudeControl','avoid','unknown',attitude}; + resultsCSV(4,:) = attitude_csv; + + % Cartpole + cartpole_csv = {'Cartpole', 'reach', 'unknown', cartpole}; + resultsCSV(5,:) = cartpole_csv; + + % Spacecraft Docking + docking_csv = {'Docking', 'constraint', 'unknown', spacecraft}; + resultsCSV(6,:) = docking_csv; + + % Double Pendulum + dp_csv(1,:) = {'DoublePendulum', 'more robust', 'violated', dp_more}; + dp_csv(2,:) = {'DoublePendulum', 'less robust', 'violated', dp_less}; + resultsCSV(7:8, :) = dp_csv; + + % NAV + dp_csv(1,:) = {'NAV', 'standard', '?', navPoint}; + dp_csv(2,:) = {'NAV', 'robust', '?', navSet}; + resultsCSV(9:10, :) = dp_csv; + + % Quad + quad_csv = {'QUAD', 'reach', 'unknown', quad}; + resultsCSV(11,:) = quad_csv; + + % Single Pendulum + sp_csv = {'SinglePendulum', 'reach', 'violated', sp}; + resultsCSV(12,:) = sp_csv; + + % Benchmark-9 (Tora) + tora_csv(1,:) = {'TORA', 'remain', 'verified', tora_relu}; + tora_csv(2,:) = {'TORA', 'reach-tanh', 'verified', tora_relutanh}; + tora_csv(3,:) = {'TORA', 'reach-sigmoid', 'verified', tora_sigmoid}; + resultsCSV(13:15,:) = tora_csv; + + % Benchmark-10 (Unicycle) + unicycle_csv = {'Unicycle', 'reach', 'unknown', unicycle}; + resultsCSV(16,:) = unicycle_csv; + + % VCAS + vcas_m19 = {'VCAS', 'middle19', 'verified', vcas(1,1)}; + vcas_m22 = {'VCAS', 'middle22', 'verified', vcas(2,1)}; + vcas_m25 = {'VCAS', 'middle25', 'violated', vcas(3,1)}; + vcas_m28 = {'VCAS', 'middle28', 'violated', vcas(4,1)}; + vcas_w19 = {'VCAS', 'worst19', 'verified', vcas(1,2)}; + vcas_w22 = {'VCAS', 'worst22', 'violated', vcas(2,2)}; + vcas_w25 = {'VCAS', 'worst25', 'violated', vcas(3,2)}; + vcas_w28 = {'VCAS', 'worst28', 'violated', vcas(4,2)}; + resultsCSV(17:24,:) = [vcas_m19; vcas_m22; vcas_m25; vcas_m28; vcas_w19; vcas_w22; vcas_w25; vcas_w28]; + + + % Create and save csv files with results + if is_codeocean + writecell(resultsCSV, '/results/results.csv'); % ARCH repeatability specific + else + writecell(resultsCSV, 'results.csv'); + end end \ No newline at end of file