Fixing forward functions across files

Author: mldiego

code/nnv/engine/nn/Prob_reach/ProbReach_ImageStar.m

@@ -71,25 +71,41 @@
 
         end
 
-        function out = forward(obj, x)
-
+        function out = forward(obj, x, inputFormat)
+    
             model_source = class(obj.model);
-
+            
             switch model_source
-
+            
                 case 'SeriesNetwork'
                     out = obj.model.predict(x);
-
+            
                 case 'DAGNetwork'
                     out = obj.model.predict(x);
-
+            
                 case 'dlnetwork'
-                    dlX = dlarray(x);
+                    % dlX = dlarray(x,inputFormat);
+                    if strcmp(inputFormat, "default")
+                        if isa(obj.model.Layers(1, 1), 'nnet.cnn.layer.ImageInputLayer')
+                            dlX = dlarray(x, "SSCB");
+                        elseif isa(obj.model.Layers(1, 1), 'nnet.cnn.layer.FeatureInputLayer') || isa(model.Layers(1, 1), 'nnet.onnx.layer.FeatureInputLayer')
+                            dlX = dlarray(x, "CB");
+                        else
+                            disp(obj.model.Layers(1,1));
+                            error("Unknown input format");
+                        end
+                    else
+                        if contains(inputFormat, "U")
+                            dlX = dlarray(x, inputFormat+"U");
+                        else
+                            dlX = dlarray(x, inputFormat);
+                        end
+                    end
                     out = obj.model.predict(dlX);
-
+            
                 case 'NN'
                     out = obj.model.evaluate(x);
-
+            
                 otherwise
                     error("Unknown model source: " + model_source + ". We only cover NN, SeriesNetwork, dlnetwork and DAGNetwork.");
             end
@@ -106,6 +122,7 @@
             N = obj.params.Nt;
             N_dir = obj.params.N_dir;
             trn_batch = obj.params.trn_batch;
+            inputFormat = obj.params.inputFormat;
 
             N_perturbed = size(obj.indices , 1);
 
@@ -124,7 +141,7 @@
                 end
                 Inp = single(obj.LB + d_at);
                 X(:,i) = Rand;
-                Y(:,:,:,i) = obj.forward(Inp);
+                Y(:,:,:,i) = obj.forward(Inp,inputFormat);
             end
             %%%%%%%%%%%%%
             n1 = numel(Y(:,:,:,1));
@@ -340,7 +357,7 @@
                     end
                     Inp = obj.LB + d_at;
                     X_test_nc(:,i) = Rand;
-                    Y_test_nc(:,:,:,i) = obj.forward(Inp);
+                    Y_test_nc(:,:,:,i) = obj.forward(Inp,inputFormat);
                 end
                 %%%%%%%%%%%%%
 
@@ -455,7 +472,8 @@
                 disp(' The Image Star is large for your memory and should be presented in sparse format.')
                 disp('Unfortunately matlab does not support sparse representation for (N>2)D arrays.')
                 disp('Thus we provide the vectorized format of ImageStar() that is a Star() via sparse 2D arrays. ')
-                p = input('Do you want to continue? Yes <-- 1 / No <-- 0     ');
+                % p = input('Do you want to continue? Yes <-- 1 / No <-- 0     ');
+                p = 1;
 
                 if p==1
 

code/nnv/engine/utils/Prob_reach.m

@@ -107,6 +107,7 @@
 params.threshold_normal = threshold_normal;
 params.guarantee = coverage;
 params.py_dir = py_dir;
+params.inputFormat = inputFormat;
 
 
 obj = ProbReach_ImageStar(Net,LB, UB,indices, SizeOut, train_mode, params);

code/nnv/examples/Submission/VNN_COMP2025/run_vnncomp_instance.m

@@ -13,7 +13,7 @@
 
 % Load networks
 
-[net, nnvnet, needReshape, reachOptionsList, inputSize,inputFormat] = load_vnncomp_network(category, onnx, vnnlib);
+[net, nnvnet, needReshape, reachOptionsList, inputSize, inputFormat] = load_vnncomp_network(category, onnx, vnnlib);
 
 if isempty(inputSize)
     inputSize = net.Layers(1, 1).InputSize;
@@ -71,7 +71,7 @@
 
 vT = tic;
 
-quickRun = true;
+quickRun = false;
 % 
 % if quickRun 
 %     tTime = toc(t);
@@ -100,7 +100,7 @@
                 if ~strcmp(reachOptions.reachMethod, "cp-star")
                     ySet = nnvnet.reach(IS, reachOptions);
                 else
-                    ySet = Prob_reach(net, IS, []);
+                    ySet = Prob_reach(net, IS, reachOptions);
                 end
 
                 % Verify property
@@ -143,7 +143,7 @@
                     if ~strcmp(reachOptions.reachMethod, "cp-star")
                         ySet = nnvnet.reach(IS, reachOptions);
                     else
-                        ySet = Prob_reach(net, IS, []);
+                        ySet = Prob_reach(net, IS, reachOptions);
                     end
 
                     % Verify property
@@ -203,7 +203,7 @@
                     if ~strcmp(reachOptions.reachMethod, "cp-star")
                         ySet = nnvnet.reach(IS, reachOptions);
                     else
-                        ySet = Prob_reach(net, IS, []);
+                        ySet = Prob_reach(net, IS, reachOptions);
                     end
 
                     % Add verification status
@@ -320,6 +320,7 @@
 function [net,nnvnet,needReshape,reachOptionsList,inputSize,inputFormat] = load_vnncomp_network(category, onnx, vnnlib)
 % load participating vnncomp 2025 benchmark NNs 
 % Not yet supported:
+% - cctsdb (some errrors when forward propagating)
 % - lsnc_relu
 % - ml4acopf
 % - traffic_signs_recognition
@@ -350,15 +351,17 @@
         end
 
     elseif contains(category, "cctsdb_yolo")
-        net = importNetworkFromONNX(onnx);
-        nnvnet = "";
-        inputSize = [12296, 1];
-        inputFormat = "UU";
-        X = dlarray(rand(12296, 1), inputFormat);
-        net = initialize(net, X);
-        reachOptions = struct;
-        reachOptions.reachMethod = 'cp-star';
-        reachOptionsList{1} = reachOptions;
+        % net = importNetworkFromONNX(onnx);
+        % nnvnet = "";
+        % inputSize = [12296, 1];
+        % inputFormat = "UU";
+        % X = dlarray(rand(12296, 1), inputFormat);
+        % net = initialize(net, X);
+        % reachOptions = struct;
+        % reachOptions.reachMethod = 'cp-star';
+        % reachOptions.inputFormat = inputFormat;
+        % reachOptionsList{1} = reachOptions;
+        error("Working on supporting this one");
 
     elseif contains(category, "cersyve")
         net = importNetworkFromONNX(onnx, "InputDataFormats", "BC");
@@ -520,6 +523,7 @@
         % net = initialize(net, X);
         % nnvnet = "";
         % reachOptions = struct;
+        % reachOptions.inputFormat = inputFormat;
         % reachOptions.reachMethod = 'cp-star';
         % reachOptionsList{1} = reachOptions;
         error("Not supported");
@@ -562,6 +566,7 @@
             net = initialize(net, X);
             nnvnet = "";
             reachOptions = struct;
+            reachOptions.inputFormat = inputFormat;
             reachOptions.reachMethod = 'cp-star'; % default parameters
             reachOptionsList{1} = reachOptions;
         end
@@ -586,6 +591,7 @@
         reachOptions = struct;
         reachOptions.reachMethod = 'relax-star-area';
         reachOptions.relaxFactor = 1;
+        reachOptions.inputFormat = inputFormat;
         reachOptionsList{1} = reachOptions;
         % reachOptions.reachMethod = 'relax-star-area';
         % reachOptions.relaxFactor = 0.5;
@@ -660,6 +666,7 @@
         % % needReshape = 1; % 1 is wrong
         % reachOptions = struct;
         % % inputFormat = "BSSC";
+        % reachOptions.inputFormat = inputFormat;
         % reachOptions.reachMethod = 'cp-star';
         % reachOptionsList{1} = reachOptions;
         error("IR and opset not yet supported in MATLAB")

code/nnv/examples/Submission/VNN_COMP2025/test_instances.m

@@ -66,8 +66,10 @@
     end
 end
 
-% Errors on both? None of them finished...
-% Let's test this again
+% There are errors in some of the forward prediction (gather to multlayer)
+% There seems to be some assertion that fails sometimes when randomly
+% executing
+% Let's test this again in the future
 
 %% cersyve