Tutorial DSN 2024

code/nnv/engine/nn/layers/Conv1DLayer.m

@@ -521,10 +521,10 @@ function set_name(obj, name)
 
     end
 
-    % reachability analysis using star set
-    methods
-        % reachability analysis method using Stars
-        % a star represent a set of images (2D matrix of h x w)
+
+    methods % reachability analysis using Stars
+
+        % reachability analysis using star set
         function S = reach_star_single_input(obj, input)
             % @inputs: an ImageStar input set
             % @S: an ImageStar with number of channels = obj.NumFilters
@@ -555,30 +555,6 @@ function set_name(obj, name)
 
         end
 
-        % reachability analysis using ImageZonos
-        function Z = reach_zono(obj, input)
-            % @input: an ImageZono input set
-            % @Z: an ImageZono with number of channels = obj.NumFilters
-
-            if ~isa(input, 'ImageZono')
-                error('The input is not an ImageZono object');
-            end
-
-            if input.numChannels ~= obj.NumChannels
-                error("Input set contains %d channels while the convolutional layers has %d channels", input.numChannels, obj.NumChannels);
-            end
-
-            % compute output sets
-            c = vl_nnconv1d(input.V(:,:,:,1), obj.Weights, obj.Bias', obj.Stride, obj.PaddingSize, obj.DilationFactor);
-            n = size(input.V(:,:,:,2:input.numPred + 1),4);
-            for i = 1:n
-                V(:,:,1,i) = vl_nnconv1d(input.V(:,:,:,i+1), obj.Weights, 0, obj.Stride, obj.PaddingSize, obj.DilationFactor);         
-            end
-            Y = cat(4, c, V);
-            Z = ImageZono(Y);
-
-        end
-
         % hangle multiple inputs
         function images = reach_star_multipleInputs(obj, in_signals, option)
             % @in_images: an array of ImageStars input set
@@ -602,27 +578,6 @@ function set_name(obj, name)
             end
 
         end
-
-        function images = reach_zono_multipleInputs(obj, in_images, option)
-            % @in_images: an array of ImageZonos input set
-            % @option: = 'parallel' or 'single' or empty
-
-            n = length(in_images);
-            images(n) = ImageZono; 
-
-            if strcmp(option, 'parallel')
-                parfor i=1:n
-                    images(i) = obj.reach_zono(in_images(i));
-                end
-            elseif strcmp(option, 'single') || isempty(option)
-                for i=1:n
-                    images(i) = obj.reach_zono(in_images(i));
-                end
-            else
-                error('Unknown computation option');
-            end
-
-        end
 
         % reach star with multiple inputs
         function images = reachSequence(varargin)

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