From 344ba353e05c22737ce651576f2c516064b050f6 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 25 Jan 2021 20:50:48 +0100
Subject: [PATCH] Use template for DFTTraceSimulator

---
 src/storm-dft/simulator/DFTTraceSimulator.cpp | 14 +++++++++++++-
 src/storm-dft/simulator/DFTTraceSimulator.h   |  2 +-
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/storm-dft/simulator/DFTTraceSimulator.cpp b/src/storm-dft/simulator/DFTTraceSimulator.cpp
index fd0af4b14..eae3a004c 100644
--- a/src/storm-dft/simulator/DFTTraceSimulator.cpp
+++ b/src/storm-dft/simulator/DFTTraceSimulator.cpp
@@ -67,12 +67,18 @@ namespace storm {
                             smallestTimebound = timebound;
                         }
                     }
-                    STORM_LOG_TRACE("Let BE " << *nextFail.getFailBE(dft).first << "fail after time " << smallestTimebound);
+                    STORM_LOG_TRACE("Let BE " << *nextFail.getFailBE(dft).first << " fail after time " << smallestTimebound);
                     bool res = step(nextFail);
                     return res ? smallestTimebound : -1;
                 }
             }
 
+            template<>
+            double DFTTraceSimulator<storm::RationalFunction>::randomStep() {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs.");
+            }
+
+
             template<typename ValueType>
             bool DFTTraceSimulator<ValueType>::step(storm::dft::storage::FailableElements::const_iterator nextFailElement) {
                 if (nextFailElement == state->getFailableElements().end()) {
@@ -116,9 +122,15 @@ namespace storm {
                 }
                 // Time is up
                 return false;
+            }
+
+            template<>
+            bool DFTTraceSimulator<storm::RationalFunction>::simulateCompleteTrace(double timebound) {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs.");
             } 
 
             template class DFTTraceSimulator<double>;
+            template class DFTTraceSimulator<storm::RationalFunction>;
         }
     }
 }
diff --git a/src/storm-dft/simulator/DFTTraceSimulator.h b/src/storm-dft/simulator/DFTTraceSimulator.h
index ac54d87a4..7f9203207 100644
--- a/src/storm-dft/simulator/DFTTraceSimulator.h
+++ b/src/storm-dft/simulator/DFTTraceSimulator.h
@@ -83,7 +83,7 @@ namespace storm {
                 storm::storage::DFTStateGenerationInfo const& stateGenerationInfo;
 
                 // Generator for creating next state in DFT
-                storm::generator::DftNextStateGenerator<double> generator;
+                storm::generator::DftNextStateGenerator<ValueType> generator;
 
                 // Current state
                 DFTStatePointer state;