Skip to content

Commit aa67a1f

Browse files
authored
Merge pull request #291 from sammsaski/master
SoSym journal submission Extension of formalise 2025 video classification verification paper
2 parents ba36d3a + ccdfe6b commit aa67a1f

File tree

57 files changed

+6136
-421
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

57 files changed

+6136
-421
lines changed

.gitignore

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,3 +20,5 @@ code/nnv/tests/attacks/shuttle_images/**
2020
**/shuttle_images/**
2121
**/tbxmanager/
2222
**/tbxmanager/**
23+
24+
.DS_Store

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -147,7 +147,12 @@
147147
elseif length(n) == 4
148148
image = permute(image, [3 2 1 4]);
149149
flatten_im = reshape(image, [1 1 n(1)*n(2)*n(3)*n(4)]);
150+
elseif length(n) == 5
151+
% image = permute(image, [3 2 1 4 5]);
152+
image = permute(image, [1, 5, 4, 3, 2]);
153+
flatten_im = reshape(image, [1 1 n(1)*n(2)*n(3)*n(4)*n(5)]);
150154
else
155+
disp(n);
151156
fprintf("Invalid input image with size %d", length(n));
152157
error('Invalid input image');
153158
end
Lines changed: 215 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,215 @@
1+
classdef GlobalAveragePooling3DLayer < handle
2+
% GlobalAveragePooling 3D Layer object
3+
% downsamples the input by computing the mean of the height and width dimensions
4+
%
5+
% Author: Samuel Sasaki
6+
% Date: 08/27/2025
7+
8+
properties
9+
Name = 'GlobalAvgPoolingLayer'; % default
10+
NumInputs = 1; % default
11+
InputNames = {'in1'}; % default
12+
NumOutputs = 1; % default
13+
OutputNames = {'out'}; % default
14+
end
15+
16+
methods % constructor
17+
18+
% create layer
19+
function obj = GlobalAveragePooling3DLayer(varargin)
20+
% @name: name of the layer
21+
% @NumInputs: number of inputs
22+
% @NumOutputs: number of outputs,
23+
% @InputNames: input names
24+
% @OutputNames: output names
25+
26+
switch nargin
27+
28+
case 5
29+
name = varargin{1};
30+
numInputs = varargin{2};
31+
numOutputs = varargin{3};
32+
inputNames = varargin{4};
33+
outputNames = varargin{5};
34+
case 1
35+
name = varargin{1};
36+
numInputs = 1;
37+
numOutputs = 1;
38+
inputNames = {'in1'};
39+
outputNames = {'out'};
40+
case 0
41+
name = 'global_average_pooling_3d';
42+
numInputs = 1;
43+
numOutputs = 1;
44+
inputNames = {'in1'};
45+
outputNames = {'out'};
46+
otherwise
47+
error('Invalid number of input arguments, should be 0, 1 or 5');
48+
end
49+
50+
if ~ischar(name)
51+
error('Invalid name, should be a charracter array');
52+
end
53+
54+
if numInputs < 1
55+
error('Invalid number of inputs');
56+
end
57+
58+
if numOutputs < 1
59+
error('Invalid number of outputs');
60+
end
61+
62+
if ~iscell(inputNames)
63+
error('Invalid input names, should be a cell');
64+
end
65+
66+
if ~iscell(outputNames)
67+
error('num of inputs do not match with num of input names');
68+
end
69+
70+
obj.Name = name;
71+
obj.NumInputs = numInputs;
72+
obj.NumOutputs = numOutputs;
73+
obj.InputNames = inputNames;
74+
obj.OutputNames = outputNames;
75+
end
76+
77+
% change params to gpuArrays
78+
function obj = toGPU(obj)
79+
% nothing to change in here (no params)
80+
end
81+
82+
% Change params precision
83+
function obj = changeParamsPrecision(obj, ~)
84+
85+
end
86+
87+
end
88+
89+
90+
methods % main methods
91+
92+
% evaluate
93+
function output = evaluate(obj, input)
94+
% addition layer takes usually two inputs, but allows many (N)
95+
%
96+
input = dlarray(input, "SSSCB");
97+
output = extractdata(avgpool(input,'global'));
98+
end
99+
100+
% reach (TODO)
101+
function output = reach_single_input(obj, input)
102+
% @in_image: input volumestar
103+
% @image: output set
104+
105+
if ~isa(input, 'VolumeStar')
106+
error('The input is not an VolumeStar object');
107+
end
108+
Y = obj.evaluate(input.V);
109+
output = VolumeStar(Y, input.C, input.d, input.pred_lb, input.pred_ub);
110+
111+
end
112+
113+
% handle multiple inputs
114+
function S = reach_multipleInputs(obj, inputs, option)
115+
% @inputs: an array of ImageStars
116+
% @option: = 'parallel' or 'single'
117+
% @S: output VolumeStar
118+
119+
n = length(inputs);
120+
if isa(inputs(1), 'VolumeStar')
121+
S(n) = VolumeStar;
122+
else
123+
error('Unknown input data set');
124+
end
125+
126+
if strcmp(option, 'parallel')
127+
parfor i=1:n
128+
S(i) = obj.reach_single_input(inputs(i));
129+
end
130+
elseif strcmp(option, 'single') || isempty(option)
131+
for i=1:n
132+
S(i) = obj.reach_single_input(inputs(i));
133+
end
134+
else
135+
error('Unknown computation option, should be parallel or single');
136+
end
137+
138+
end
139+
140+
% reachability analysis with multiple inputs
141+
function VS = reach(varargin)
142+
% @in_image: an input imagestar
143+
% @image: output set
144+
% @option: = 'single' or 'parallel'
145+
146+
switch nargin
147+
148+
case 7
149+
obj = varargin{1};
150+
in_images = varargin{2};
151+
method = varargin{3};
152+
option = varargin{4};
153+
% relaxFactor = varargin{5}; do not use
154+
% dis_opt = varargin{6}; do not use
155+
% lp_solver = varargin{7}; do not use
156+
157+
case 6
158+
obj = varargin{1};
159+
in_images = varargin{2};
160+
method = varargin{3};
161+
option = varargin{4};
162+
%relaxFactor = varargin{5}; do not use
163+
% dis_opt = varargin{6}; do not use
164+
165+
case 5
166+
obj = varargin{1};
167+
in_images = varargin{2};
168+
method = varargin{3};
169+
option = varargin{4};
170+
%relaxFactor = varargin{5}; do not use
171+
172+
case 4
173+
obj = varargin{1};
174+
in_images = varargin{2};
175+
method = varargin{3};
176+
option = varargin{4}; % computation option
177+
178+
case 3
179+
obj = varargin{1};
180+
in_images = varargin{2}; % don't care the rest inputs
181+
method = varargin{3};
182+
option = [];
183+
otherwise
184+
error('Invalid number of input arguments (should be 2, 3, 4, 5 or 6)');
185+
end
186+
187+
if strcmp(method, 'approx-star') || strcmp(method, 'exact-star') || strcmp(method, 'abs-dom') || strcmp(method, 'approx-zono') || contains(method, "relax-star")
188+
VS = obj.reach_multipleInputs(in_images, option);
189+
else
190+
error('Unknown reachability method');
191+
end
192+
193+
end
194+
195+
function VS = reachSequence(varargin)
196+
obj = varargin{1};
197+
VS = obj.reach(varargin{2:end});
198+
end
199+
end
200+
201+
202+
methods(Static)
203+
204+
% parsing method
205+
function L = parse(layer)
206+
% create NNV layer from matlab
207+
208+
if ~isa(layer, 'nnet.cnn.layer.GlobalAveragePooling3DLayer')
209+
error('Input is not a GlobalAveragePooling3DLayer layer');
210+
end
211+
L = GlobalAveragePooling3DLayer(layer.Name, layer.NumInputs, layer.NumOutputs, layer.InputNames, layer.OutputNames);
212+
end
213+
214+
end
215+
end

code/nnv/engine/utils/matlab2nnv.m

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,10 @@
114114
elseif isa(L, 'nnet.cnn.layer.AveragePooling3DLayer')
115115
Li = AveragePooling3DLayer.parse(L);
116116

117+
% Global Average Pooling 3D Layer
118+
elseif isa(L, 'nnet.cnn.layer.GlobalAveragePooling3DLayer')
119+
Li = GlobalAveragePooling3DLayer.parse(L);
120+
117121
% Global Average Pooling 2D Layer
118122
elseif isa(L, 'nnet.cnn.layer.GlobalAveragePooling2DLayer')
119123
Li = GlobalAveragePooling2DLayer.parse(L);
Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,4 @@
1-
NNV_PATH='' # replace with '/path/to/nnv'
2-
NPY_MATLAB_PATH='' # replace with '/path/to/npy-matlab/npy-matlab'
1+
# Docker container paths (used when running inside NNV Docker container)
2+
# See README.md for container setup instructions
3+
NNV_PATH='/nnv'
4+
NPY_MATLAB_PATH='/nnv/code/nnv/examples/Submission/FORMALISE2025/npy-matlab/npy-matlab'

code/nnv/examples/Submission/FORMALISE2025/.gitignore

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,9 @@
55
*data/ZoomOut*
66
*data/GTSRB*
77
*data/STMNIST*
8+
*data/UCF11*
9+
*data/KTHActions*
10+
*data.zip*
811

912
# matlab stuff
1013
*.asv

0 commit comments

Comments
 (0)