Merge pull request #18 from verivital/master

merge recent changes for CAV submission

code/nnv/engine/nn/fnn/FFNN.m

@@ -152,7 +152,9 @@
                     rt = obj.reachTime(i-1);
 
                     estimatedTime = rt*(nP/nP1)*(obj.Layers(i).N / obj.Layers(i-1).N);
-
+                    if isnan(estimatedTime)
+                        estimatedTime = 0.0;
+                    end
                     fprintf('\nEstimated computation time: ~ %.5f seconds', estimatedTime);
                 end
 

code/nnv/engine/nn/fnn/FFNNS.m

@@ -263,7 +263,9 @@ function start_pool(obj)
                     rt = obj.reachTime(i-1);
 
                     estimatedTime = rt*(nP/nP1)*(obj.Layers(i).N / obj.Layers(i-1).N);
-
+                    if isnan(estimatedTime)
+                        estimatedTime = 0.0;
+                    end
                     fprintf('\nEstimated computation time: ~ %.5f seconds', estimatedTime);
                 end
 

code/nnv/examples/Submission/CAV2020/ACC/config_parallelism.m

@@ -0,0 +1,17 @@
+function [out] = config_parallelism(max_cores)
+    % set number of cores to use in parallel computations
+    % if system executed on has fewer, set lower
+    physical_cores = feature('numcores'); % physical cores
+
+    % use at most the number of logical cores available
+    core_info = evalc('feature(''numcores'')'); % string with all core info, including logical cores
+    core_info_logical = regexpi(core_info, '(?<num>\d+)\s+logical\s+cores', 'names');
+    available_cores = physical_cores;
+    for i = 1 : length(core_info_logical)
+        available_cores = max(available_cores, str2num(core_info_logical(i).num));
+    end
+
+    numCores = min(available_cores, max_cores); % use at most max_cores cores if available, else fewer
+
+    out = numCores;
+end

code/nnv/examples/Submission/CAV2020_Tool/ACC/linear_ACC.txt → code/nnv/examples/Submission/CAV2020/ACC/linear_ACC.txt

@@ -4,11 +4,11 @@ VERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL
 ======================================================
 v_lead(0)                 approx-star    
                        safety  |  VT   
-[29 30]                SAFE  |  32.494   
-[28 29]                SAFE  |  28.727   
-[27 28]                SAFE  |  34.981   
-[26 27]                UNSAFE  |  63.688   
-[25 26]                UNSAFE  |  75.012   
-[24 25]                UNSAFE  |  75.623   
+[29 30]                SAFE  |  30.970   
+[28 29]                SAFE  |  29.016   
+[27 28]                SAFE  |  34.900   
+[26 27]                UNSAFE  |  68.679   
+[25 26]                UNSAFE  |  72.621   
+[24 25]                UNSAFE  |  73.469   
 -------------------------------------------------------
-Total verification time:      310.524
+Total verification time:      309.656

code/nnv/examples/Submission/CAV2020_Tool/ACC/nonlinear_ACC.txt → code/nnv/examples/Submission/CAV2020/ACC/nonlinear_ACC.txt

@@ -4,11 +4,11 @@ VERIFICATION RESULTS FOR ACC WITH NONLINEAR PLANT MODEL
 =======================================================
 v_lead(0)                 approx-star    
                        safety  |  VT   
-[29 30]              UNSAFE  |  346.615   
-[28 29]              UNSAFE  |  277.501   
-[27 28]              UNSAFE  |  289.704   
-[26 27]              UNSAFE  |  315.603   
-[25 26]              UNSAFE  |  305.560   
-[24 25]              UNSAFE  |  372.003   
+[29 30]              UNSAFE  |  512.111   
+[28 29]              UNSAFE  |  550.162   
+[27 28]              UNSAFE  |  497.645   
+[26 27]              UNSAFE  |  529.117   
+[25 26]              UNSAFE  |  521.827   
+[24 25]              UNSAFE  |  518.838   
 -------------------------------------------------------
-Total verification time:      1906.986
+Total verification time:      3129.700

code/nnv/examples/Submission/CAV2020_Tool/ACC/plot_linear_ACC_reachSets.m → code/nnv/examples/Submission/CAV2020/ACC/plot_linear_ACC_reachSets.m

@@ -1,6 +1,7 @@
 % Plot reachable sets for Discrete Linear ACC model
 % Dung Tran: 10/22/2019
 
+path_out = [path_results(), filesep, 'ACC', filesep];
 
 %% System model
 % x1 = lead_car position
@@ -116,17 +117,12 @@
 end
 
 ncs.reach(init_set(1), ref_input, numSteps, 'approx-star', numCores);
-if is_codeocean()
-    path_results = '/results/';
-else
-    path_results = '';
-end
 
-save([path_results, 'linear_ACC_ncs_1.mat'], 'ncs');
+save([path_out, 'linear_ACC_ncs_1.mat'], 'ncs');
 
 ncs.reach(init_set(6), ref_input, numSteps, 'approx-star', numCores);
 
-save([path_results, 'linear_ACC_ncs_6.mat'], 'ncs');
+save([path_out, 'linear_ACC_ncs_6.mat'], 'ncs');
 
 %% Plot output reach sets: actual distance vs. safe distance
 
@@ -135,7 +131,7 @@
 
 figure;
 h1 = subplot(2,1,1);
-load([path_results, 'linear_ACC_ncs_1.mat']);
+load([path_out, 'linear_ACC_ncs_1.mat']);
 map_mat = [1 0 0 -1 0 0 0];
 map_vec = [];
 ncs.plotOutputReachSets('blue', map_mat, map_vec);
@@ -153,7 +149,7 @@
 xticks(h1, [0:5:50])
 
 h2 = subplot(2,1,2);
-load([path_results, 'linear_ACC_ncs_6.mat']);
+load([path_out, 'linear_ACC_ncs_6.mat']);
 map_mat = [1 0 0 -1 0 0 0];
 map_vec = [];
 ncs.plotOutputReachSets('blue', map_mat, map_vec);
@@ -170,6 +166,6 @@
 ylabel(h2, 'Distance');
 xticks(h2, [0:5:50])
 
-saveas(gcf, [path_results, 'plot_linear_ACC_reachSets.png']);
+saveas(gcf, [path_out, 'figure4_plot_linear_ACC_reachSets.png']);
 
 %% END OF SCRIPT

code/nnv/examples/Submission/CAV2020/ACC/reproduce.m

@@ -0,0 +1,38 @@
+path_reproduce = pwd();
+%path_nnv_root = ['..', filesep, '..', filesep, '..', filesep]; % in main folder
+
+path_nnv_root = ['..', filesep, '..', filesep, '..', filesep, '..', filesep]; % in acc subfolder
+
+cd(path_nnv_root);
+% run installation if not on codeocean / not already set up
+try
+    is_codeocean();
+catch
+    install;
+end
+
+% check if CORA is set up, if submodules are not pulled recursively, it won't be
+% so ensure you've pulled with: 
+% git clone --recursive https://github.com/verivital/nnv.git
+try
+    coraroot();
+catch
+    'ERROR: CORA not detected, ensure submodules have been pulled, CORA is required for nonlinear plant analysis'
+    return;
+end
+
+cd(path_reproduce);
+
+mkdir([path_results(), filesep, 'ACC']);
+
+% set number of cores based on system availability, up to a maximum of 16
+config_parallelism(16);
+
+'Figure 4: Generating ACC with linear plant model reachable sets'
+plot_linear_ACC_reachSets;
+
+'Table 3 (linear plant): Generating ACC results for linear plant model'
+verify_linear_ACC;
+
+'Table 3 (nonlinear plant): Generating ACC results for nonlinear plant model'
+verify_nonlinear_ACC;

code/nnv/examples/Submission/CAV2020_Tool/ACC/verify_linear_ACC.m → code/nnv/examples/Submission/CAV2020/ACC/verify_linear_ACC.m

@@ -1,6 +1,7 @@
 % Reachability analysis for Discrete Linear ACC model
 % Dung Tran: 9/30/2019
 
+path_out = [path_results(), filesep, 'ACC', filesep];
 
 
 %% System model
@@ -131,12 +132,7 @@
 
 
 %% Save verification results
-if is_codeocean()
-    path_results = '/results/';
-else
-    path_results = '';
-end
-save([path_results, 'linear_ACC.mat'], 'safe_approx', 'VT_approx', 'counterExamples_approx');
+save([path_out, 'linear_ACC.mat'], 'safe_approx', 'VT_approx', 'counterExamples_approx');
 
 %% Print verification results to screen
 fprintf('\n======================================================');
@@ -152,7 +148,7 @@
 
 %% Print verification results to a file
 
-fid = fopen([path_results, 'linear_ACC.txt'], 'wt');
+fid = fopen([path_out, 'table3_linear_ACC.txt'], 'wt');
 
 fprintf(fid,'\n======================================================');
 fprintf(fid,'\nVERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL');

code/nnv/examples/Submission/CAV2020_Tool/ACC/verify_nonlinear_ACC.m → code/nnv/examples/Submission/CAV2020/ACC/verify_nonlinear_ACC.m

@@ -1,5 +1,7 @@
 load controller_5_20.mat;
 
+path_out = [path_results(), filesep, 'ACC', filesep];
+
 weights = network.weights;
 bias = network.bias;
 n = length(weights);
@@ -115,13 +117,7 @@
     VT(i) = toc(t);
 end
 
-%% Safe verification results
-if is_codeocean()
-    path_results = '/results/';
-else
-    path_results = '';
-end
-save([path_results, 'verify_nonlinear_ACC.mat'], 'safe', 'VT', 'counterExamples');
+save([path_out, 'verify_nonlinear_ACC.mat'], 'safe', 'VT', 'counterExamples');
 
 
 %% Print verification results to screen
@@ -138,7 +134,7 @@
 
 %% Print verification results to a file
 
-fid = fopen([path_results, 'nonlinear_ACC.txt'], 'wt');
+fid = fopen([path_out, 'table3_nonlinear_ACC.txt'], 'wt');
 fprintf(fid,'\n=======================================================');
 fprintf(fid,'\nVERIFICATION RESULTS FOR ACC WITH NONLINEAR PLANT MODEL');
 fprintf(fid,'\n=======================================================');
@@ -168,4 +164,4 @@
 xticks([0:5:50]);
 title('Actual Distance (blue) vs. Safe Distance (red)');
 
-saveas(gcf, [path_results, 'verify_nonlinear_acc_cex.png']);
+saveas(gcf, [path_out, 'verify_nonlinear_acc_cex.png']);

code/nnv/examples/Submission/CAV2020/verify_P0_N00_abs.m

@@ -67,7 +67,7 @@
 
 fileID = fopen(filename,'w');
 if safe
-    fprintf(fileID, 'UNSAT\n');
+    fprintf(fileID, 'UNKNOWN\n');
 else
     fprintf(fileID, 'SAT\n');
 end

code/nnv/examples/Submission/CAV2020/verify_P0_N00_star_appr.m

@@ -69,7 +69,7 @@
 filename = [path_results(), 'logs_nnv_star_appr/P',num2str(P0),'_N',num2str(N1),num2str(N2),'_star_appr.txt'];
 fileID = fopen(filename,'w');
 if safe
-    fprintf(fileID, 'UNSAT\n');
+    fprintf(fileID, 'UNKNOWN\n');
 else
     fprintf(fileID, 'SAT\n');
 end

code/nnv/examples/Submission/CAV2020/verify_P0_N00_zono.m

@@ -68,7 +68,7 @@
 filename = [path_results(), 'logs_nnv_zono/P',num2str(P0),'_N',num2str(N1),num2str(N2),'_zono.txt'];
 fileID = fopen(filename,'w');
 if safe
-    fprintf(fileID, 'UNSAT\n');
+    fprintf(fileID, 'UNKNOWN\n');
 else
     fprintf(fileID, 'SAT\n');
 end

code/run

@@ -3,6 +3,15 @@ set -ex
 
 pwd
 
+# unfortunately, the git files do not exist when running the capsule, so this cannot be done to pull in the submodules
+#cd /root/capsule
+#pwd
+#ls -la
+
+# add submodules (CORA, HyST, NNMT)
+#git submodule init
+#git submodule update
+
 # This is the master script for the capsule. When you click "Reproducible Run", the code in this file will execute.
 ls
 
@@ -13,9 +22,10 @@ ls
 cd /deps/run_nnv_comparison
 
 chmod +x run_tools.sh
-# run tool comparisons, this will take some time
-#./run_tools.sh > /results/run_nnv_comparison_log.txt 2>/results/run_nnv_comparison_err.txt
+# run tool comparisons, this will take some time (~20-40 minutes or so, depends on codeocean load as this is run on shared resources)
+./run_tools.sh > /results/run_nnv_comparison_log.txt 2>/results/run_nnv_comparison_err.txt
 
+# start up matlab and run
 cd ~/
 
 matlab -nodisplay -r "addpath(genpath('/deps')); addpath(genpath('/code')); startup_nnv; savepath; run_codeocean;"