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::randomStep() { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs."); + } + + template bool DFTTraceSimulator::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::simulateCompleteTrace(double timebound) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs."); } template class DFTTraceSimulator; + template class DFTTraceSimulator; } } } 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 generator; + storm::generator::DftNextStateGenerator generator; // Current state DFTStatePointer state;