Preparing ARCH-COMP24 RE package

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)

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)

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
+%% 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

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)

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)

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
+end

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
+end