diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 9d0b88fed..d40597684 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -56,18 +56,21 @@ namespace storm { std::shared_ptr const& exprManager = gspn.getExpressionManager(); storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); - storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); + STORM_LOG_TRACE("Target expression: " << targetExpression); + auto evtlFormula = std::make_shared(targetExpression); auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); 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); + auto timeBoundedProperty = storm::jani::Property("time-bounded", tbUntil); + auto mttfProperty = storm::jani::Property("mttf", rewFormula); storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule(); if (janiSettings.isJaniFileSet()) { - storm::api::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}, janiSettings.getJaniFilename()); + // Currently no properties are set + storm::api::exportJaniModel(*model, {}, janiSettings.getJaniFilename()); } return model;