From 790c62a48abac0f581e860fd31ebe6c7f709b727 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 7 Apr 2017 13:49:34 +0200
Subject: [PATCH] Check if DFT support was built

---
 lib/.gitignore              |  1 +
 lib/stormpy/dft/__init__.py |  5 +++++
 setup.py                    | 12 ++++++++----
 tests/dft/test_build.py     | 12 ++++++++++--
 4 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/lib/.gitignore b/lib/.gitignore
index c70bcf8..f40fdce 100644
--- a/lib/.gitignore
+++ b/lib/.gitignore
@@ -1,3 +1,4 @@
 *.so
 __pycache__/
 stormpy.egg-info/
+stormpy/dft/_config.py
diff --git a/lib/stormpy/dft/__init__.py b/lib/stormpy/dft/__init__.py
index ae53cc2..0cd0541 100644
--- a/lib/stormpy/dft/__init__.py
+++ b/lib/stormpy/dft/__init__.py
@@ -1,3 +1,8 @@
+from . import _config
+
+if not _config.has_storm_dft:
+    raise ImportError("No support for DFTs was built in Storm.")
+
 from . import dft
 from .dft import *
 
diff --git a/setup.py b/setup.py
index c855010..f8e92d2 100755
--- a/setup.py
+++ b/setup.py
@@ -30,11 +30,11 @@ class CMakeBuild(build_ext):
         except OSError:
             raise RuntimeError("CMake must be installed to build the following extensions: " +
                                ", ".join(e.name for e in self.extensions))
-        
+
         build_temp_version = self.build_temp + "-version"
         if not os.path.exists(build_temp_version):
             os.makedirs(build_temp_version)
-        
+
         # Check cmake variable values
         cmake_args = []
         if self.storm_dir is not None:
@@ -47,8 +47,11 @@ class CMakeBuild(build_ext):
         match = re.search(r"HAVE-STORM-DFT: (.*)", output)
         assert(match)
         self.have_storm_dft = True if match.group(1) == "TRUE" else False
-        
-        
+        # Set variable in _config.py
+        with open(os.path.join("lib", "stormpy", "dft", "_config.py"), "w") as f:
+            f.write("# Generated from setup.py\n")
+            f.write("has_storm_dft = {}".format(self.have_storm_dft))
+
         for ext in self.extensions:
             if ext.name == "dft":
                 if self.have_storm_dft:
@@ -58,6 +61,7 @@ class CMakeBuild(build_ext):
             else:
                 self.build_extension(ext)
 
+
     def initialize_options(self):
         build_ext.initialize_options(self)
         self.storm_dir = None
diff --git a/tests/dft/test_build.py b/tests/dft/test_build.py
index df32062..93b6cf2 100644
--- a/tests/dft/test_build.py
+++ b/tests/dft/test_build.py
@@ -1,12 +1,21 @@
 import stormpy
-import stormpy.dft
 import stormpy.logic
 from helpers.helper import get_example_path
 
 import math
 
 class TestBuild:
+
+    def test_import(self):
+        import stormpy.dft
+
     def test_build_dft(self):
+        try:
+            import stormpy.dft
+        except ImportError:
+            # No support for DFTs
+            return
+
         model = stormpy.dft.build_sparse_model_from_json_dft(get_example_path("dft", "and.json"))
         formulas = stormpy.parse_properties("T=? [ F \"failed\" ]")
         assert model.nr_states == 4
@@ -16,4 +25,3 @@ class TestBuild:
         assert initial_state == 1
         result = stormpy.model_checking(model, formulas[0])
         assert math.isclose(result.at(initial_state), 3)
-