|
40 | 40 | input_sets = {}; % input set values for each layer (cell array of cells of layer input sets) |
41 | 41 | dis_opt = []; % display option = 'display' or [] |
42 | 42 | lp_solver = 'linprog'; % choose linprog as default LP solver for constructing reachable set user can choose 'glpk' or 'linprog' as an LP solver |
| 43 | + matlabnet = []; % the matlab network this NN was created from |
43 | 44 |
|
44 | 45 | % To facilitate graph computation flow |
45 | 46 | name2indx = []; % Match name to index in nnvLayers list |
|
440 | 441 | methods % secondary methods (verification, safety, robustness...) |
441 | 442 |
|
442 | 443 | % Verify a VNN-LIB specification |
443 | | - function result = verify_vnnlib(obj, propertyFile, reachOptions) |
| 444 | + function [result, X] = verify_vnnlib(obj, propertyFile, reachOptions, needReshape) |
| 445 | + |
| 446 | + arguments |
| 447 | + obj |
| 448 | + propertyFile |
| 449 | + reachOptions |
| 450 | + needReshape = 0; |
| 451 | + end |
444 | 452 |
|
445 | 453 | % Load specification to verify |
446 | 454 | property = load_vnnlib(propertyFile); |
447 | 455 | lb = property.lb; |
448 | 456 | ub = property.ub; |
449 | | - |
| 457 | + |
| 458 | + if isfield(reachOptions, 'single_average_input') && reachOptions.single_average_input |
| 459 | + if ~isa(lb, 'cell') |
| 460 | + lb = (lb + ub)/2; |
| 461 | + ub = lb; |
| 462 | + else |
| 463 | + lb = (lb{1} + ub{1})/2; |
| 464 | + ub = lb; |
| 465 | + end |
| 466 | + end |
| 467 | + |
| 468 | + if needReshape > 0.1 |
| 469 | + % Format bounds into correct dimensions |
| 470 | + % (using code from run_vnncomp2024_instance.m) |
| 471 | + |
| 472 | + first_layer = obj.Layers(1, 1); |
| 473 | + inputSize = first_layer{1}.InputSize; |
| 474 | + if needReshape == 1 |
| 475 | + lb = permute(lb, [2 1 3]); |
| 476 | + ub = permute(ub, [2 1 3]); |
| 477 | + elseif needReshape == 2 |
| 478 | + newSize = [inputSize(2) inputSize(1) inputSize(3:end)]; |
| 479 | + lb = reshape(lb, newSize); |
| 480 | + lb = permute(lb, [2 1 3 4]); |
| 481 | + ub = reshape(ub, newSize); |
| 482 | + ub = permute(ub, [2 1 3 4]); |
| 483 | + else |
| 484 | + error("Unsupported value for needReshape") |
| 485 | + end |
| 486 | + end |
| 487 | + |
450 | 488 | % Create reachability parameters and options |
451 | 489 | if contains(reachOptions.reachMethod, "zono") |
452 | 490 | X = ImageZono(lb, ub); |
453 | 491 | else |
454 | | - X = ImageStar(lb,ub); |
| 492 | + X = ImageStar(lb, ub); |
455 | 493 | end |
456 | | - |
457 | | - % Compute reachability |
| 494 | + |
458 | 495 | Y = obj.reach(X, reachOptions); % Seems to be working |
459 | 496 | result = verify_specification(Y, property.prop); |
460 | 497 |
|
@@ -1473,6 +1510,18 @@ function start_pool(obj) |
1473 | 1510 | end |
1474 | 1511 | end |
1475 | 1512 |
|
| 1513 | + % return the indices of layers of the specified types |
| 1514 | + function layers = get_layer_indices(obj, layer_types) |
| 1515 | + layers = []; |
| 1516 | + for l = 1:length(obj.Layers) |
| 1517 | + for n = 1:length(layer_types) |
| 1518 | + if isa(obj.Layers{l}, layer_types(n)) |
| 1519 | + layers = [layers l]; |
| 1520 | + end |
| 1521 | + end |
| 1522 | + end |
| 1523 | + end |
| 1524 | + |
1476 | 1525 | end % end helper functions |
1477 | 1526 |
|
1478 | 1527 |
|
|
0 commit comments