diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 61959158a..f246438fe 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -157,9 +157,12 @@ int main(const int argc, const char** argv) { auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, 0.0, 10.0); auto tbUntil = std::make_shared(tbFormula); + auto evFormula = std::make_shared(evtlFormula, storm::logic::FormulaContext::Time); + auto rewFormula = std::make_shared(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation); + storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule(); if (janiSettings.isJaniFileSet()) { - storm::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil)}, janiSettings.getJaniFilename()); + storm::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}, janiSettings.getJaniFilename()); } delete model;