From bf2d49dcc543519fac6d4343faf7767825b66dff Mon Sep 17 00:00:00 2001
From: Elena Botoeva <e.botoeva@imperial.ac.uk>
Date: Tue, 7 Jul 2020 12:12:30 +0100
Subject: [PATCH] fixes to Sherlock benchmark specifications (safety box in
 Tora and shifting and scaling in Tora and Unicycle)

---
 benchmarks/Benchmark10-Unicycle/dynamics10.m  | 42 ++++++++++---------
 benchmarks/Benchmark9-Tora/Specifications.txt |  2 +-
 benchmarks/Benchmark9-Tora/dynamics9.m        | 22 ++++++----
 3 files changed, 37 insertions(+), 29 deletions(-)

diff --git a/benchmarks/Benchmark10-Unicycle/dynamics10.m b/benchmarks/Benchmark10-Unicycle/dynamics10.m
index b014c06..b71b346 100644
--- a/benchmarks/Benchmark10-Unicycle/dynamics10.m
+++ b/benchmarks/Benchmark10-Unicycle/dynamics10.m
@@ -1,20 +1,24 @@
-function [dx] = dynamics10(t,x,u,w)
-% Ex_car_model
-  %vehicleODE Bicycle model of a vehicle with
-  % states
-  %       x(1), x(2): x,y positions
-  %       x(3): Yaw angle (\psi)
-  %       x(4): velocity
-  % control inputs
-  %       u(1): acceleration m/s^2
-  %       u(2): steering angle of front wheel
-  % disturbance input
-  %       w: disturbance with a range (-10^-4,10^4)
-  % Initial state range [9.5, 9.55] × [-4.5, -4.45] × [2.1, 2.11] × [1.5, 1.51]
-  
-dx(1,1) = x(4) * cos(x(3));
-dx(2,1) = x(4) * sin(x(3));
-dx(3,1) = u(2);
-dx(4,1) = u(1) + w;
-
+function [dx] = dynamics10(t,x,u,w)
+% Ex_car_model
+  %vehicleODE Bicycle model of a vehicle with
+  % states
+  %       x(1), x(2): x,y positions
+  %       x(3): Yaw angle (\psi)
+  %       x(4): velocity
+  % control inputs
+  %       u(1): acceleration m/s^2
+  %       u(2): steering angle of front wheel
+  % disturbance input
+  %       w: disturbance with a range (-10^-4,10^4)
+  % Initial state range [9.5, 9.55] × [-4.5, -4.45] × [2.1, 2.11] × [1.5, 1.51]
+%
+% The output of the neural network f(x) needs to be normalized 
+% in order to obtain u(1) and u(2).
+% Namely, u(i) = f(x)(i) - 20 
+%
+dx(1,1) = x(4) * cos(x(3));
+dx(2,1) = x(4) * sin(x(3));
+dx(3,1) = u(2);
+dx(4,1) = u(1) + w;
+
 end
\ No newline at end of file
diff --git a/benchmarks/Benchmark9-Tora/Specifications.txt b/benchmarks/Benchmark9-Tora/Specifications.txt
index d862bc7..c69f00f 100644
--- a/benchmarks/Benchmark9-Tora/Specifications.txt
+++ b/benchmarks/Benchmark9-Tora/Specifications.txt
@@ -10,6 +10,6 @@ control period = 1s
 
 Property:
 
-The system, states 1 to 3, always stays within the box x ∈ [-1,1]
+The system states always stays within the box x ∈ [-2,2]
 
 
diff --git a/benchmarks/Benchmark9-Tora/dynamics9.m b/benchmarks/Benchmark9-Tora/dynamics9.m
index 7924785..5ed69f4 100644
--- a/benchmarks/Benchmark9-Tora/dynamics9.m
+++ b/benchmarks/Benchmark9-Tora/dynamics9.m
@@ -1,11 +1,15 @@
-function [dx] = dynamics9(t,x,u)
-% Ex_tora
-% Initial state range:
+function [dx] = dynamics9(t,x,u)
+% Ex_tora
+% Initial state range:
 % [0.6, 0.7] × [-0.7, -0.6] × [-0.4, -0.3] × [0.5, 0.6]
-  
-dx(1,1) = x(2);
-dx(2,1) = - x(1) + 0.1*sin(x(3));
-dx(3,1) = x(4);
-dx(4,1) = u;
-
+%
+% The output of the neural network f(x) needs to be normalized 
+% in order to obtain u.
+% Namely, u = f(x) - 10 
+%
+dx(1,1) = x(2);
+dx(2,1) = - x(1) + 0.1*sin(x(3));
+dx(3,1) = x(4);
+dx(4,1) = u;
+
 end
\ No newline at end of file