Update Sherlock benchmarks

verivital · Jun 19, 2020 · f8d91e7 · f8d91e7
1 parent 5fac990
commit f8d91e7
Show file tree

Hide file tree

Showing 7 changed files with 9 additions and 3 deletions.
diff --git a/benchmarks/ACC/Specifications.txt b/benchmarks/ACC/Specifications.txt
@@ -1,7 +1,6 @@
 Parameters:
 
 a_lead = -2
-t = 5 seconds
 T_gap = 1.4
 D_default = 10
 
@@ -13,6 +12,9 @@ x_ego  = x(4) = [10, 11]
 v_ego  = x(5) = [30, 30.2]
 γ_ego  = x(6) = 0
 
+t = 5 seconds
+control period = 0.1 s
+
 Safety Property:
 
 x_lead - x_ego >= D_safe, where D_safe = D_default + T_gap * v_ego;

diff --git a/benchmarks/Benchmark10-Unicycle/Specifications.txt b/benchmarks/Benchmark10-Unicycle/Specifications.txt
@@ -6,11 +6,12 @@ x3 = [2.1, 2.11]
 x4 = [1.5, 1.51]
 
 t = 10 seconds
+control period = 0.2 s
 
 Property:
 
 Prove that the system reaches the states:
 x1 = [-0.6, 0.6]
 x2 = [-0.2, 0.2]
 x3 = [-0.06, 0.06]
-x4 = [-0.3, 0.3]
+x4 = [-0.3, 0.3]
diff --git a/benchmarks/Benchmark10-Unicycle/controllerB.onnx b/benchmarks/Benchmark10-Unicycle/controllerB.onnx
diff --git a/benchmarks/Benchmark10-Unicycle/controllerB_nnv.mat b/benchmarks/Benchmark10-Unicycle/controllerB_nnv.mat
diff --git a/benchmarks/Benchmark9-Tora/Specifications.txt b/benchmarks/Benchmark9-Tora/Specifications.txt
@@ -6,7 +6,10 @@ x3 = [-0.4, -0.3]
 x4 = [0.5, 0.6]
 
 t = 20 seconds
+control period = 1s
 
 Property:
 
-The system, states 1 to 3, always stays within the box x ∈ [-1,1]
+The system, states 1 to 3, always stays within the box x ∈ [-1,1]
+
+
diff --git a/benchmarks/Benchmark9-Tora/controllerTora.onnx b/benchmarks/Benchmark9-Tora/controllerTora.onnx
diff --git a/benchmarks/Benchmark9-Tora/controllerTora_nnv.mat b/benchmarks/Benchmark9-Tora/controllerTora_nnv.mat