From 90ade051c2fe7ff19160250f34a77621e697826c Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 28 May 2020 14:24:09 +0200
Subject: [PATCH] Added CMAKE option STORM_LOAD_QVBS to automatically download
 the quantitative verification benchmark set

---
 CHANGELOG.md                      |  1 +
 CMakeLists.txt                    |  4 +++-
 resources/3rdparty/CMakeLists.txt | 32 ++++++++++++++++++++++++-------
 3 files changed, 29 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 643ee03bf..4b48c742d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,6 +12,7 @@ Version 1.5.x
 - Scheduler export: Properly handle models with end components. Added export in `.json` format.
 - CMake: Search for Gurobi prefers new versions
 - CMake: We no longer ship xerces-c. If xerces-c is not found on the system, storm-gspn will not be able to parse xml-based GSPN formats 
+- CMake: Added option `STORM_LOAD_QVBS` to automatically download the quantitative verification benchmark set.
 - Eigen library: The source code of Eigen is no longer included but downloaded from an external repository instead. Incremented Eigen version to 3.3.7 which fixes a compilation issue with recent XCode versions.
 - Tests: Enabled tests for permissive schedulers
 - `storm-counterexamples`: fix when computing multiple counterexamples in debug mode
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 134b6577a..a522e67ff 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -66,7 +66,9 @@ set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optiona
 set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).")
 set(CUDA_ROOT "" CACHE STRING "The hint to the root directory of CUDA (optional).")
 set(MSAT_ROOT "" CACHE STRING "The hint to the root directory of MathSAT (optional).")
-set(STORM_QVBS_ROOT "" CACHE STRING "The hint to the root directory of the Quantitative Verification Benchmark Set (QVBS) (optional).")
+option(STORM_LOAD_QVBS "Sets whether the Quantitative Verification Benchmark Set (QVBS) should be downloaded." OFF)
+set(STORM_QVBS_ROOT "" CACHE STRING "The root directory of the Quantitative Verification Benchmark Set (QVBS) in case it should not be downloaded (optional).")
+MARK_AS_ADVANCED(STORM_QVBS_ROOT)
 set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.")
 set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.")
 set(USE_XERCESC ${XML_SUPPORT})
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 3833ca950..d939ab369 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -450,13 +450,31 @@ endif(ENABLE_MSAT)
 #############################################################
 
 set(STORM_HAVE_QVBS OFF)
-if (NOT "${STORM_QVBS_ROOT}" STREQUAL "")
-	if( EXISTS "${STORM_QVBS_ROOT}/index.json")
-       set(STORM_HAVE_QVBS ON)
-       message (STATUS "Storm - Enabled inputs from QVBS located at ${STORM_QVBS_ROOT}")
-	else()
-   		message(FATAL_ERROR "No file 'index.json' in provided QVBS root directory ${STORM_QVBS_ROOT}")
-	endif()
+if (STORM_LOAD_QVBS)
+    ExternalProject_Add(
+            download_qvbs
+            GIT_REPOSITORY https://github.com/ahartmanns/qcomp.git
+            GIT_SHALLOW 1
+            PREFIX ${PROJECT_BINARY_DIR}/qvbs
+            UPDATE_COMMAND ""
+            CONFIGURE_COMMAND ""
+            BUILD_COMMAND ""
+            INSTALL_COMMAND ""
+            LOG_INSTALL ON
+    )
+    add_dependencies(resources download_qvbs)
+    set(STORM_HAVE_QVBS ON)
+    ExternalProject_Get_Property(download_qvbs source_dir)
+    set(STORM_QVBS_ROOT "${source_dir}/benchmarks")
+elseif (NOT "${STORM_QVBS_ROOT}" STREQUAL "")
+    if( EXISTS "${STORM_QVBS_ROOT}/index.json")
+        set(STORM_HAVE_QVBS ON)
+    else()
+        message(FATAL_ERROR "No file 'index.json' in provided QVBS root directory ${STORM_QVBS_ROOT}")
+    endif()
+endif()
+if (STORM_HAVE_QVBS)
+    message (STATUS "Storm - Enabled inputs from QVBS located at ${STORM_QVBS_ROOT}")
 endif()