Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ code/nnv/UUV/
code/nnv/tbxmanager/
code/nnv/tests/io/models/*.caffemodel
.venv
*.asv


data/vgg16_cache.mat
Expand Down
59 changes: 54 additions & 5 deletions code/nnv/engine/nn/NN.m
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@
input_sets = {}; % input set values for each layer (cell array of cells of layer input sets)
dis_opt = []; % display option = 'display' or []
lp_solver = 'linprog'; % choose linprog as default LP solver for constructing reachable set user can choose 'glpk' or 'linprog' as an LP solver
matlabnet = []; % the matlab network this NN was created from

% To facilitate graph computation flow
name2indx = []; % Match name to index in nnvLayers list
Expand Down Expand Up @@ -440,21 +441,57 @@
methods % secondary methods (verification, safety, robustness...)

% Verify a VNN-LIB specification
function result = verify_vnnlib(obj, propertyFile, reachOptions)
function [result, X] = verify_vnnlib(obj, propertyFile, reachOptions, needReshape)

arguments
obj
propertyFile
reachOptions
needReshape = 0;
end

% Load specification to verify
property = load_vnnlib(propertyFile);
lb = property.lb;
ub = property.ub;


if isfield(reachOptions, 'single_average_input') && reachOptions.single_average_input
if ~isa(lb, 'cell')
lb = (lb + ub)/2;
ub = lb;
else
lb = (lb{1} + ub{1})/2;
ub = lb;
end
end

if needReshape > 0.1
Copy link

Copilot AI Dec 1, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[nitpick] Unclear conditional check: Using needReshape > 0.1 is an unusual way to check if reshaping is needed. Since needReshape has a default value of 0 and can be 1 or 2, it would be clearer to use needReshape > 0 or needReshape ~= 0 instead of > 0.1. The current threshold of 0.1 seems arbitrary and could be confusing.

Suggested change
if needReshape > 0.1
if needReshape > 0

Copilot uses AI. Check for mistakes.
% Format bounds into correct dimensions
% (using code from run_vnncomp2024_instance.m)

first_layer = obj.Layers(1, 1);
inputSize = first_layer{1}.InputSize;
if needReshape == 1
lb = permute(lb, [2 1 3]);
ub = permute(ub, [2 1 3]);
elseif needReshape == 2
newSize = [inputSize(2) inputSize(1) inputSize(3:end)];
lb = reshape(lb, newSize);
lb = permute(lb, [2 1 3 4]);
ub = reshape(ub, newSize);
ub = permute(ub, [2 1 3 4]);
else
error("Unsupported value for needReshape")
end
end

% Create reachability parameters and options
if contains(reachOptions.reachMethod, "zono")
X = ImageZono(lb, ub);
else
X = ImageStar(lb,ub);
X = ImageStar(lb, ub);
end

% Compute reachability

Y = obj.reach(X, reachOptions); % Seems to be working
result = verify_specification(Y, property.prop);

Expand Down Expand Up @@ -1468,6 +1505,18 @@ function start_pool(obj)
end
end

% return the indices of layers of the specified types
function layers = get_layer_indices(obj, layer_types)
layers = [];
for l = 1:length(obj.Layers)
for n = 1:length(layer_types)
if isa(obj.Layers{l}, layer_types(n))
layers = [layers l];
end
end
end
end

end % end helper functions


Expand Down
Loading