diff --git a/code/nnv/engine/set/Star.m b/code/nnv/engine/set/Star.m index 50297dfe3d..ff7603821d 100644 --- a/code/nnv/engine/set/Star.m +++ b/code/nnv/engine/set/Star.m @@ -609,7 +609,8 @@ function plot(obj) if isempty(obj.C) || isempty(obj.d) % star set is just a vector (one point) lb = obj.V(:, 1); - ub = obj.V(:, 1); + ub = obj.V(:, 1); + B = Box(lb, ub); else % star set is a set diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/discrete_ACC_verification_results.mat b/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/discrete_ACC_verification_results.mat deleted file mode 100644 index ed523c8d0a..0000000000 Binary files a/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/discrete_ACC_verification_results.mat and /dev/null differ diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/discrete_ACC_verification_results.txt b/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/discrete_ACC_verification_results.txt deleted file mode 100644 index 655dd46094..0000000000 --- a/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/discrete_ACC_verification_results.txt +++ /dev/null @@ -1,7 +0,0 @@ - -====================================================== -VERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL -====================================================== -x_lead(0) exact-star approx-star - safety | VT safety | VT -[29 30] | 0.000 SAFE | 19.608 \ No newline at end of file diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/plot_discrete_ACC_reachSets.m b/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/plot_discrete_ACC_reachSets.m deleted file mode 100644 index 1a19845717..0000000000 --- a/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/plot_discrete_ACC_reachSets.m +++ /dev/null @@ -1,33 +0,0 @@ -% Plot reachable sets for Discrete Linear ACC model -% Dung Tran: 10/22/2019 - - - -%% Load verification results - -load discrete_ACC_verification_results.mat; - - -%% Plot output reach sets: actual distance vs. safe distance - -% plot reachable set of the distance between two cars d = x1 - x4 vs. ego -% car's velocity -ncs = dis_ACC_approx{1}; -figure; -map_mat = [1 0 0 -1 0 0 0]; -map_vec = []; -ncs.plotOutputReachSets('blue', map_mat, map_vec); - -hold on; - -% plot safe distance between two cars: d_safe = D_default + t_gap * v_ego; -% D_default = 10; t_gap = 1.4 -% d_safe = 10 + 1.4 * x5; - -map_mat = [0 0 0 0 1.4 0 0]; -map_vec = [10]; - -ncs.plotOutputReachSets('red', map_mat, map_vec); -title('Actual Distance versus. Safe Distance'); - -%% END OF SCRIPT \ No newline at end of file diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/How to run ACC case study.txt b/code/nnv/examples/Submission/HSCC2020/ACC/How to run ACC case study.txt new file mode 100644 index 0000000000..817dd3e8eb --- /dev/null +++ b/code/nnv/examples/Submission/HSCC2020/ACC/How to run ACC case study.txt @@ -0,0 +1,32 @@ + +NOTE***: To run ACC case study, we need to have CORA installed. + +1) Install NNV: + + a) git clone --recursive https://github.com/verivital/nnv.git + + b) go to ..code/nnv/ folder to run install.m + +2) Run ACC case study: + + a) Run ACC with discrete linear plant model: + + a1) using exact analysis: run verify_discrete_ACC_exact_star.m + + total runtime is about 5.5 hours + + a2) using approximate analysis: run verify_discrete_ACC_approx_star.m + + total runtime is about 4 minutes + + b) Run ACC with nonlinear plant model using approx-star method + + run verify_nonlinear_ACC.m + + total runtime is about 30 minutes + +NOTE***: + +We use 4 cores for computation. If your computer does not have >= 4 cores + +Set numCores (or n_cores) parameter (default = 4) in the script to a suitable number \ No newline at end of file diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/car_dynamics.m b/code/nnv/examples/Submission/HSCC2020/ACC/car_dynamics.m new file mode 100644 index 0000000000..86cc73e422 --- /dev/null +++ b/code/nnv/examples/Submission/HSCC2020/ACC/car_dynamics.m @@ -0,0 +1,21 @@ +function [dx]=car_dynamics(t,x,a_ego) + +mu=0.0001; % friction parameter + +% x1 = lead_car position +% x2 = lead_car velocity +% x3 = lead_car internal state + +% x4 = ego_car position +% x5 = ego_car velocity +% x6 = ego_car internal state + +% lead car dynamics +a_lead = -5; +dx(1,1)=x(2); +dx(2,1) = x(3); +dx(3,1) = -2 * x(3) + 2 * a_lead - mu*x(2)^2; +% ego car dyanmics +dx(4,1)= x(5); +dx(5,1) = x(6); +dx(6,1) = -2 * x(6) + 2 * a_ego - mu*x(5)^2; diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/controller_5_20.mat b/code/nnv/examples/Submission/HSCC2020/ACC/controller_5_20.mat similarity index 100% rename from code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/controller_5_20.mat rename to code/nnv/examples/Submission/HSCC2020/ACC/controller_5_20.mat diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/counterExample.fig b/code/nnv/examples/Submission/HSCC2020/ACC/counterExample.fig new file mode 100644 index 0000000000..290218a3e3 Binary files /dev/null and b/code/nnv/examples/Submission/HSCC2020/ACC/counterExample.fig differ diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/counterExample.pdf b/code/nnv/examples/Submission/HSCC2020/ACC/counterExample.pdf new file mode 100644 index 0000000000..2cb51828c1 Binary files /dev/null and b/code/nnv/examples/Submission/HSCC2020/ACC/counterExample.pdf differ diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/dis_ACC_ncs_1.mat b/code/nnv/examples/Submission/HSCC2020/ACC/dis_ACC_ncs_1.mat new file mode 100644 index 0000000000..230ead4c85 Binary files /dev/null and b/code/nnv/examples/Submission/HSCC2020/ACC/dis_ACC_ncs_1.mat differ diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/dis_ACC_ncs_6.mat b/code/nnv/examples/Submission/HSCC2020/ACC/dis_ACC_ncs_6.mat new file mode 100644 index 0000000000..38ce35747e Binary files /dev/null and b/code/nnv/examples/Submission/HSCC2020/ACC/dis_ACC_ncs_6.mat differ diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_approx_star.mat b/code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_approx_star.mat new file mode 100644 index 0000000000..d1fbb18444 Binary files /dev/null and b/code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_approx_star.mat differ diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_approx_star.txt b/code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_approx_star.txt new file mode 100644 index 0000000000..a7db4640f5 --- /dev/null +++ b/code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_approx_star.txt @@ -0,0 +1,14 @@ + +====================================================== +VERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL +====================================================== +v_lead(0) approx-star + safety | VT +[29 30] SAFE | 15.764 +[28 29] SAFE | 14.479 +[27 28] SAFE | 17.387 +[26 27] UNSAFE | 31.844 +[25 26] UNSAFE | 41.238 +[24 25] UNSAFE | 43.326 +------------------------------------------------------- +Total verification time: 164.038 \ No newline at end of file diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_verification_results.mat b/code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_verification_results.mat new file mode 100644 index 0000000000..bf2a8da9fc Binary files /dev/null and b/code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_verification_results.mat differ diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_verification_results.txt b/code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_verification_results.txt new file mode 100644 index 0000000000..b3e84f5502 --- /dev/null +++ b/code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_verification_results.txt @@ -0,0 +1,16 @@ + +====================================================== +VERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL +====================================================== +x_lead(0) exact-star approx-star + safety | VT safety | VT +[29 30] | 0.000 | 0.000 +[28 29] | 0.000 | 0.000 +[27 28] | 0.000 | 0.000 +[26 27] | 0.000 | 0.000 +[25 26] | 0.000 | 0.000 +[24 25] | 0.000 UNSAFE | 49.589 +[23 24] | 0.000 | 0.000 +[22 23] | 0.000 | 0.000 +[21 22] | 0.000 | 0.000 +[20 21] | 0.000 | 0.000 \ No newline at end of file diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/nonlinear_ACC.txt b/code/nnv/examples/Submission/HSCC2020/ACC/nonlinear_ACC.txt new file mode 100644 index 0000000000..a3ee54ff83 --- /dev/null +++ b/code/nnv/examples/Submission/HSCC2020/ACC/nonlinear_ACC.txt @@ -0,0 +1,14 @@ + +======================================================= +VERIFICATION RESULTS FOR ACC WITH NONLINEAR PLANT MODEL +======================================================= +v_lead(0) approx-star + safety | VT +[29 30] UNSAFE | 265.006 +[28 29] UNSAFE | 283.954 +[27 28] UNSAFE | 292.673 +[26 27] UNSAFE | 294.249 +[25 26] UNSAFE | 300.120 +[24 25] UNSAFE | 276.630 +------------------------------------------------------- +Total verification time: 1712.633 \ No newline at end of file diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/plot_discrete_ACC_reachSets.m b/code/nnv/examples/Submission/HSCC2020/ACC/plot_discrete_ACC_reachSets.m new file mode 100644 index 0000000000..afbfcf1db4 --- /dev/null +++ b/code/nnv/examples/Submission/HSCC2020/ACC/plot_discrete_ACC_reachSets.m @@ -0,0 +1,49 @@ +% Plot reachable sets for Discrete Linear ACC model +% Dung Tran: 10/22/2019 + + + +%% Plot output reach sets: actual distance vs. safe distance + +% plot reachable set of the distance between two cars d = x1 - x4 vs. ego +% car's velocity + +figure; +h1 = subplot(2,1,1); +load dis_ACC_ncs_1.mat; +map_mat = [1 0 0 -1 0 0 0]; +map_vec = []; +ncs.plotOutputReachSets('blue', map_mat, map_vec); +hold on; +% plot safe distance between two cars: d_safe = D_default + t_gap * v_ego; +% D_default = 10; t_gap = 1.4 +% d_safe = 10 + 1.4 * x5; + +map_mat = [0 0 0 0 1.4 0 0]; +map_vec = [10]; +ncs.plotOutputReachSets('red', map_mat, map_vec); +title(h1,'Actual Distance (blue) vs. Safe Distance (red)'); +xlabel(h1, 'Control Time Steps'); +ylabel(h1, 'Distance'); +xticks(h1, [0:5:50]) + +h2 = subplot(2,1,2); +load dis_ACC_ncs_6.mat; +map_mat = [1 0 0 -1 0 0 0]; +map_vec = []; +ncs.plotOutputReachSets('blue', map_mat, map_vec); +hold on; +% plot safe distance between two cars: d_safe = D_default + t_gap * v_ego; +% D_default = 10; t_gap = 1.4 +% d_safe = 10 + 1.4 * x5; + +map_mat = [0 0 0 0 1.4 0 0]; +map_vec = [10]; +ncs.plotOutputReachSets('red', map_mat, map_vec); +title(h2,'Actual Distance (blue) vs. Safe Distance (red)'); +xlabel(h2, 'Control Time Steps'); +ylabel(h2, 'Distance'); +xticks(h2, [0:5:50]) + + +%% END OF SCRIPT \ No newline at end of file diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/plot_nonlinear_ACC_counterExamples.m b/code/nnv/examples/Submission/HSCC2020/ACC/plot_nonlinear_ACC_counterExamples.m new file mode 100644 index 0000000000..a5a76d1002 --- /dev/null +++ b/code/nnv/examples/Submission/HSCC2020/ACC/plot_nonlinear_ACC_counterExamples.m @@ -0,0 +1,17 @@ +cI = counterExamples{1}; +cI = cell2mat(cI); +d_rel = [1 0 0 -1 0 0]*cI; +d_safe = [0 0 0 1.4 0 0]*cI + 10; + +figure; +T = 0:1:50; +plot(T, d_rel, 'blue'); +hold on; +plot(T, d_safe, 'red'); + +xlabel('Control Time Steps', 'FontSize', 13); +ylabel('Distance', 'FontSize', 13); +xticks([0:5:50]); +a = get(gca,'XTickLabel'); +set(gca,'XTickLabel',a,'FontName','Times','fontsize',13) +title('Actual Distance (blue) vs. Safe Distance (red)'); diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/reachSet.fig b/code/nnv/examples/Submission/HSCC2020/ACC/reachSet.fig new file mode 100644 index 0000000000..38fd03b6b6 Binary files /dev/null and b/code/nnv/examples/Submission/HSCC2020/ACC/reachSet.fig differ diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/reachSet.pdf b/code/nnv/examples/Submission/HSCC2020/ACC/reachSet.pdf new file mode 100644 index 0000000000..006dc2a3ee Binary files /dev/null and b/code/nnv/examples/Submission/HSCC2020/ACC/reachSet.pdf differ diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/verify_discrete_ACC.m b/code/nnv/examples/Submission/HSCC2020/ACC/verify_discrete_ACC.m similarity index 94% rename from code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/verify_discrete_ACC.m rename to code/nnv/examples/Submission/HSCC2020/ACC/verify_discrete_ACC.m index a5502c4ef2..96baa5839b 100644 --- a/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/verify_discrete_ACC.m +++ b/code/nnv/examples/Submission/HSCC2020/ACC/verify_discrete_ACC.m @@ -72,7 +72,7 @@ % initial condition of the plant % initial position of lead car x_lead -x_lead = [90 100]; +x_lead = [90 92]; % initial condition of v_lead v_lead = cell(10, 1); v_lead{1, 1} = [29 30]; @@ -99,7 +99,7 @@ % initial condition for new introduced variable x7_0 = [2*a_lead 2*a_lead]; % x7 = -2*x(3) + 2 * a_lead -> x7(0) = -2*x(3)(0) + 2*alead = -2*0 + 2*-2 = -4 -N = length(x1); +N = length(v_lead); for i=1:N lb = [x_lead(1); v_lead{i}(1); internal_acc_lead(1); x_ego(1); v_ego(1); internal_acc_ego(1); x7_0(1)]; ub = [x_lead(2); v_lead{i}(2); internal_acc_lead(2); x_ego(2); v_ego(2); internal_acc_ego(2); x7_0(2)]; @@ -118,17 +118,17 @@ unsafe_mat = [1 0 0 -1 -alpha*1.4 0 0]; unsafe_vec = alpha*10; -N = 1; % just for testing - +% N = 1; % just for testing safe_exact = cell(1,N); VT_exact = zeros(1, N); counterExamples_exact = cell(1, N); dis_ACC_exact = cell(1,N); -% for i=1:N -% [safe_exact{i}, counterExamples_exact{i}, VT_exact(i)] = ncs.verify(init_set(i), ref_input, numSteps, 'exact-star', numCores, unsafe_mat, unsafe_vec); -% dis_ACC_exact{i} = ncs; %store for plotting reachable sets -% end +for i=1:N + [safe_exact{i}, counterExamples_exact{i}, VT_exact(i)] = ncs.verify(init_set(i), ref_input, numSteps, 'exact-star', numCores, unsafe_mat, unsafe_vec); + dis_ACC_exact{i} = ncs; %store for plotting reachable sets +end + safe_approx = cell(1, N); VT_approx = zeros(1, N); diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/verify_discrete_ACC.asv b/code/nnv/examples/Submission/HSCC2020/ACC/verify_discrete_ACC_approx_star.m similarity index 64% rename from code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/verify_discrete_ACC.asv rename to code/nnv/examples/Submission/HSCC2020/ACC/verify_discrete_ACC_approx_star.m index 43b37f1179..6a5819bc7d 100644 --- a/code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/verify_discrete_ACC.asv +++ b/code/nnv/examples/Submission/HSCC2020/ACC/verify_discrete_ACC_approx_star.m @@ -72,20 +72,16 @@ % initial condition of the plant % initial position of lead car x_lead -x_lead = [90 100]; -v_lead = cell(10, 1); +x_lead = [90 92]; +% initial condition of v_lead +v_lead = cell(6, 1); v_lead{1, 1} = [29 30]; v_lead{2, 1} = [28 29]; v_lead{3, 1} = [27 28]; v_lead{4, 1} = [26 27]; v_lead{5, 1} = [25 26]; v_lead{6, 1} = [24 25]; -v_lead{7, 1} = [23 24]; -v_lead{8, 1} = [22 23]; -v_lead{9, 1} = [21 22]; -v_lead{10, 1} = [ 21]; -% initial condition of v_lead -v_lead = [23 24]; + % initial condition of x_internal_lead internal_acc_lead = [0 0]; % initial condition of x_ego @@ -99,11 +95,10 @@ % initial condition for new introduced variable x7_0 = [2*a_lead 2*a_lead]; % x7 = -2*x(3) + 2 * a_lead -> x7(0) = -2*x(3)(0) + 2*alead = -2*0 + 2*-2 = -4 -x1 = x_lead; -N = length(x1); +N = length(v_lead); for i=1:N - lb = [x1{i}(1); v_lead(1); internal_acc_lead(1); x_ego(1); v_ego(1); internal_acc_ego(1); x7_0(1)]; - ub = [x1{i}(2); v_lead(2); internal_acc_lead(2); x_ego(2); v_ego(2); internal_acc_ego(2); x7_0(2)]; + lb = [x_lead(1); v_lead{i}(1); internal_acc_lead(1); x_ego(1); v_ego(1); internal_acc_ego(1); x7_0(1)]; + ub = [x_lead(2); v_lead{i}(2); internal_acc_lead(2); x_ego(2); v_ego(2); internal_acc_ego(2); x7_0(2)]; init_set(i) = Star(lb, ub); end @@ -119,17 +114,7 @@ unsafe_mat = [1 0 0 -1 -alpha*1.4 0 0]; unsafe_vec = alpha*10; -N = 1; % just for testing - -safe_exact = cell(1,N); -VT_exact = zeros(1, N); -counterExamples_exact = cell(1, N); -dis_ACC_exact = cell(1,N); - -% for i=1:N -% [safe_exact{i}, counterExamples_exact{i}, VT_exact(i)] = ncs.verify(init_set(i), ref_input, numSteps, 'exact-star', numCores, unsafe_mat, unsafe_vec); -% dis_ACC_exact{i} = ncs; %store for plotting reachable sets -% end +% N = 1; % just for testing safe_approx = cell(1, N); VT_approx = zeros(1, N); @@ -138,37 +123,39 @@ for i=1:N [safe_approx{i}, counterExamples_approx{i}, VT_approx(i)] = ncs.verify(init_set(i), ref_input, numSteps, 'approx-star', numCores, unsafe_mat, unsafe_vec); - dis_ACC_approx{i} = ncs; % store for plotting reachable sets end %% Safe verification results -save discrete_ACC_verification_results.mat safe_exact VT_exact counterExamples_exact safe_approx VT_approx counterExamples_approx dis_ACC_exact dis_ACC_approx; +save discrete_ACC_approx_star.mat safe_approx VT_approx counterExamples_approx; %% Print verification results to screen fprintf('\n======================================================'); fprintf('\nVERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL'); fprintf('\n======================================================'); -fprintf('\nx_lead(0) exact-star approx-star '); -fprintf('\n safety | VT safety | VT '); -fprintf('\n[%d %d] %s | %3.3f %s | %3.3f ', x_lead{1}(1), x_lead{1}(2), safe_exact{1}, VT_exact(1), safe_approx{1}, VT_approx(1)); -for i=2:N -fprintf('\n[%d %d] %s | %3.3f %s | %3.3f ', x_lead{i}(1), x_lead{i}(2), safe_exact{i}, VT_exact(i), safe_approx{i}, VT_approx(i)); +fprintf('\nv_lead(0) approx-star '); +fprintf('\n safety | VT '); +for i=1:N +fprintf('\n[%d %d] %s %3.3f ', v_lead{i}(1), v_lead{i}(2), safe_approx{i}, VT_approx(i)); end +fprintf('\n-------------------------------------------------------'); +fprintf('\nTotal verification time: %3.3f', sum(VT_approx)); %% Print verification results to a file -fid = fopen('discrete_ACC_verification_results.txt', 'wt'); +fid = fopen('discrete_ACC_approx_star.txt', 'wt'); + fprintf(fid,'\n======================================================'); fprintf(fid,'\nVERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL'); fprintf(fid,'\n======================================================'); -fprintf(fid,'\nx_lead(0) exact-star approx-star '); -fprintf(fid,'\n safety | VT safety | VT '); -fprintf(fid,'\n[%d %d] %s | %3.3f %s | %3.3f ', x_lead{1}(1), x_lead{1}(2), safe_exact{1}, VT_exact(1), safe_approx{1}, VT_approx(1)); -for i=2:N -fprintf(fid,'\n[%d %d] %s | %3.3f %s | %3.3f ', x_lead{i}(1), x_lead{i}(2), safe_exact{i}, VT_exact(i), safe_approx{i}, VT_approx(i)); +fprintf(fid,'\nv_lead(0) approx-star '); +fprintf(fid,'\n safety | VT '); +for i=1:N +fprintf(fid,'\n[%d %d] %s | %3.3f ', v_lead{i}(1), v_lead{i}(2), safe_approx{i}, VT_approx(i)); end +fprintf(fid,'\n-------------------------------------------------------'); +fprintf(fid,'\nTotal verification time: %3.3f', sum(VT_approx)); fclose(fid); %% END diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/verify_discrete_ACC_exact_star.m b/code/nnv/examples/Submission/HSCC2020/ACC/verify_discrete_ACC_exact_star.m new file mode 100644 index 0000000000..51ba7c8e8e --- /dev/null +++ b/code/nnv/examples/Submission/HSCC2020/ACC/verify_discrete_ACC_exact_star.m @@ -0,0 +1,161 @@ +% Reachability analysis for Discrete Linear ACC model +% Dung Tran: 9/30/2019 + + + +%% System model +% x1 = lead_car position +% x2 = lead_car velocity +% x3 = lead_car internal state + +% x4 = ego_car position +% x5 = ego_car velocity +% x6 = ego_car internal state + +% lead_car dynamics +%dx(1,1)=x(2); +%dx(2,1) = x(3); +%dx(3,1) = -2 * x(3) + 2 * a_lead - mu*x(2)^2; + +% ego car dynamics +%dx(4,1)= x(5); +%dx(5,1) = x(6); +%dx(6,1) = -2 * x(6) + 2 * a_ego - mu*x(5)^2; + + +% let x7 = -2*x(3) + 2 * a_lead -> x7(0) = -2*x(3)(0) + 2*alead +% -> dx7 = -2dx3 + + +A = [0 1 0 0 0 0 0; 0 0 1 0 0 0 0; 0 0 0 0 0 0 1; 0 0 0 0 1 0 0; 0 0 0 0 0 1 0; 0 0 0 0 0 -2 0; 0 0 -2 0 0 0 0]; +B = [0; 0; 0; 0; 0; 2; 0]; +C = [1 0 0 -1 0 0 0; 0 1 0 0 -1 0 0; 0 0 0 0 1 0 0]; % feedback relative distance, relative velocity, longitudinal velocity +D = [0; 0; 0]; + +plant = LinearODE(A, B, C, D); % continuous plant model + +plantd = plant.c2d(0.1); % discrete plant model + +% the neural network provides a_ego control input to the plant +% a_lead = -5 + + +%% Controller +load controller_5_20.mat; + +weights = network.weights; +bias = network.bias; +n = length(weights); +n = length(weights); +Layers = []; +for i=1:n - 1 + L = LayerS(weights{1, i}, bias{i, 1}, 'poslin'); + Layers = [Layers L]; +end +L = LayerS(weights{1, n}, bias{n, 1}, 'purelin'); +Layers = [Layers L]; +Controller = FFNNS(Layers); % feedforward neural network controller + + +%% NNCS + +ncs = DLinearNNCS(Controller, plantd); % a discrete linear neural network control system + + +%% Initial Set of states and reference inputs + +% reference input for neural network controller +% t_gap = 1.4; v_set = 30; + +ref_input = [30; 1.4]; + +% initial condition of the plant + +% initial position of lead car x_lead +x_lead = [90 92]; +% initial condition of v_lead +v_lead = cell(6, 1); +v_lead{1, 1} = [29 30]; +v_lead{2, 1} = [28 29]; +v_lead{3, 1} = [27 28]; +v_lead{4, 1} = [26 27]; +v_lead{5, 1} = [25 26]; +v_lead{6, 1} = [24 25]; + +% initial condition of x_internal_lead +internal_acc_lead = [0 0]; +% initial condition of x_ego +x_ego = [30 31]; +% initial condition of v_ego +v_ego = [30 30.5]; +% initial condition of x_internal_ego +internal_acc_ego = [0 0]; + +a_lead = -5; +% initial condition for new introduced variable +x7_0 = [2*a_lead 2*a_lead]; % x7 = -2*x(3) + 2 * a_lead -> x7(0) = -2*x(3)(0) + 2*alead = -2*0 + 2*-2 = -4 + +N = length(v_lead); +for i=1:N + lb = [x_lead(1); v_lead{i}(1); internal_acc_lead(1); x_ego(1); v_ego(1); internal_acc_ego(1); x7_0(1)]; + ub = [x_lead(2); v_lead{i}(2); internal_acc_lead(2); x_ego(2); v_ego(2); internal_acc_ego(2); x7_0(2)]; + init_set(i) = Star(lb, ub); +end + + + +%% Reachability Analysis && Verification +numSteps = 50; +numCores = 4; +% safety property: actual distance > alpha * safe distance <=> d = x1 - x4 > alpha * d_safe = alpha * (1.4 * v_ego + 10) + +% usafe region: x1 - x4 <= alpha * (1.4 * v_ego + 10) +alpha = 1; +unsafe_mat = [1 0 0 -1 -alpha*1.4 0 0]; +unsafe_vec = alpha*10; + +% N = 1; % just for testing + +safe_exact = cell(1,N); +VT_exact = zeros(1, N); +counterExamples_exact = cell(1, N); +dis_ACC_exact = cell(1,N); + +for i=1:N + [safe_exact{i}, counterExamples_exact{i}, VT_exact(i)] = ncs.verify(init_set(i), ref_input, numSteps, 'exact-star', numCores, unsafe_mat, unsafe_vec); + dis_ACC_exact{i} = ncs; %store for plotting reachable sets +end + +%% Safe verification results + +save discrete_ACC_exact_star.mat safe_exact VT_exact counterExamples_exact; + +%% Print verification results to screen +fprintf('\n======================================================'); +fprintf('\nVERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL'); +fprintf('\n======================================================'); +fprintf('\nv_lead(0) exact-star '); +fprintf('\n safety | VT '); +for i=1:N +fprintf('\n[%d %d] %s %3.3f ', v_lead{i}(1), v_lead{i}(2), safe_exact{i}, VT_exact(i)); +end +fprintf('\n-------------------------------------------------------'); +fprintf('\nTotal verification time: %3.3f', sum(VT_approx)); + +%% Print verification results to a file + +fid = fopen('discrete_ACC_exact_star.txt', 'wt'); + +fprintf(fid,'\n======================================================'); +fprintf(fid,'\nVERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL'); +fprintf(fid,'\n======================================================'); +fprintf(fid,'\nv_lead(0) exact-star '); +fprintf(fid,'\n safety | VT '); +for i=1:N +fprintf(fid,'\n[%d %d] %s | %3.3f ', v_lead{i}(1), v_lead{i}(2), safe_exact{i}, VT_exact(i)); +end +fprintf(fid,'\n-------------------------------------------------------'); +fprintf(fid,'\nTotal verification time: %3.3f', sum(VT_exact)); +fclose(fid); + +%% END diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/verify_nonlinear_ACC.m b/code/nnv/examples/Submission/HSCC2020/ACC/verify_nonlinear_ACC.m new file mode 100644 index 0000000000..d9871a27d1 --- /dev/null +++ b/code/nnv/examples/Submission/HSCC2020/ACC/verify_nonlinear_ACC.m @@ -0,0 +1,161 @@ +load controller_5_20.mat; + +weights = network.weights; +bias = network.bias; +n = length(weights); +Layers = []; +for i=1:n - 1 + L = Layer(weights{1, i}, bias{i, 1}, 'ReLU'); + Layers = [Layers L]; +end + +L = Layer(weights{1, n}, bias{n, 1}, 'Linear'); + +Layers = [Layers L]; + +Controller = FFNN(Layers); % feedforward neural network controller +Plant = NonLinearODE(6, 1, @car_dynamics); +Plant.set_timeStep(0.01); % time step for reachability analysis of the plant +Plant.set_tFinal(0.1); % Ts = 0.1, sampling time for control signal from neural network controller +output_mat = [0 0 0 0 1 0;1 0 0 -1 0 0; 0 1 0 0 -1 0]; % feedback: relative distance, relative velocity and ego-car velocity +Plant.set_output_mat(output_mat); % Define the outputs that is feedback to the controller + +feedbackMap = [0]; % feedback map, y[k] + +ncs = NNCS(Controller, Plant, feedbackMap); % the neural network control system + +%% Construct initial conditions +% initial condition of the Plant + +% x = [x_lead v_lead internal_acc_lead x_ego v_ego internal_acc_ego]' + +% initial position of lead car x_lead +x_lead = [90 92]; +% initial condition of v_lead +v_lead = cell(6, 1); +v_lead{1, 1} = [29 30]; +v_lead{2, 1} = [28 29]; +v_lead{3, 1} = [27 28]; +v_lead{4, 1} = [26 27]; +v_lead{5, 1} = [25 26]; +v_lead{6, 1} = [24 25]; + + +% initial condition of x_internal_lead +internal_acc_lead = [0 0]; +% initial condition of x_ego +x_ego = [10 11]; +% initial condition of v_ego +v_ego = [30 30.2]; +% initial condition of x_internal_ego +internal_acc_ego = [0 0]; + +n = length(v_lead); + +init_set(n) = Star(); + +for i=1:n + lb = [x_lead(1); v_lead{i}(1); internal_acc_lead(1); x_ego(1); v_ego(1); internal_acc_ego(1)]; + ub = [x_lead(2); v_lead{i}(2); internal_acc_lead(2); x_ego(2); v_ego(2); internal_acc_ego(2)]; + init_set(i) = Star(lb, ub); +end + +% reference input for neural network controller +% t_gap = 1.4; v_set = 30; + +lb = [30; 1.4]; +ub = [30; 1.4]; + +input_ref = Star(lb, ub); % input reference set + +%% Verification + +N = 50; % number of control steps + +n_cores = 4; % number of cores + +% safety specification: relative distance > safe distance +% dis = x_lead - x_ego +% safe distance between two cars, see here +% https://www.mathworks.com/help/mpc/examples/design-an-adaptive-cruise-control-system-using-model-predictive-control.html +% dis_safe = D_default + t_gap * v_ego; + +t_gap = 1.4; +D_default = 10; + +% safety specification: x_lead - x_ego - t_gap * v_ego - D_default > 0 +% unsafe region: x_lead - x_ego - t_gap * v_ego <= D_default + +unsafe_mat = [1 0 0 -1 -t_gap 0]; +unsafe_vec = [D_default]; + +safe = cell(1, n); % safety status +VT = zeros(1,n); % verification time +counterExamples = cell(1,n); % counter examples +for i=1:n + t = tic; + ncs.reach('approx-star', init_set(i), input_ref, n_cores, N); + [safe1, ~] = ncs.check_safety(unsafe_mat, unsafe_vec, n_cores); + if safe1 == 1 + safe{i} = 'SAFE'; + else + Bi = init_set(i).getBox; + Br = input_ref.getBox; + [rs, ~, counterExamples, ~, ~, ~] = ncs.falsify(0.1, N, Bi, Br, unsafe_mat, unsafe_vec, 1000); + + if rs == 1 + safe{i} = 'UNSAFE'; + else + safe{i} = 'UNKNOWN'; + end + end + VT(i) = toc(t); +end + +%% Safe verification results +save verify_nonlinear_ACC.mat safe VT counterExamples; + + +%% Print verification results to screen +fprintf('\n======================================================='); +fprintf('\nVERIFICATION RESULTS FOR ACC WITH NONLINEAR PLANT MODEL'); +fprintf('\n======================================================='); +fprintf('\nv_lead(0) approx-star '); +fprintf('\n safety | VT '); +for i=1:n +fprintf('\n[%d %d] %s | %3.3f ', v_lead{i}(1), v_lead{i}(2), safe{i}, VT(i)); +end +fprintf('\n-------------------------------------------------------'); +fprintf('\nTotal verification time: %3.3f', sum(VT)); + +%% Print verification results to a file + +fid = fopen('nonlinear_ACC.txt', 'wt'); +fprintf(fid,'\n======================================================='); +fprintf(fid,'\nVERIFICATION RESULTS FOR ACC WITH NONLINEAR PLANT MODEL'); +fprintf(fid,'\n======================================================='); +fprintf(fid,'\nv_lead(0) approx-star '); +fprintf(fid,'\n safety | VT '); +for i=1:n +fprintf(fid,'\n[%d %d] %s | %3.3f ', v_lead{i}(1), v_lead{i}(2), safe{i}, VT(i)); +end +fprintf(fid,'\n-------------------------------------------------------'); +fprintf(fid,'\nTotal verification time: %3.3f', sum(VT)); +fclose(fid); + +%% Plot counter examples +cI = counterExamples{1}; +cI = cell2mat(cI); +d_rel = [1 0 0 -1 0 0]*cI; +d_safe = [0 0 0 1.4 0 0]*cI + 10; + +figure; +T = 0:1:50; +plot(T, d_rel, 'blue'); +hold on; +plot(T, d_safe, 'red'); + +xlabel('Control Time Steps', 'FontSize', 13); +ylabel('Distance', 'FontSize', 13); +xticks([0:5:50]); +title('Actual Distance (blue) vs. Safe Distance (red)'); \ No newline at end of file diff --git a/code/nnv/examples/Submission/HSCC2020/ACC/verify_nonlinear_ACC.mat b/code/nnv/examples/Submission/HSCC2020/ACC/verify_nonlinear_ACC.mat new file mode 100644 index 0000000000..716767a87e Binary files /dev/null and b/code/nnv/examples/Submission/HSCC2020/ACC/verify_nonlinear_ACC.mat differ