From 817c5a218bb79feaf3ac85f6c510f9347e4c30ba Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 16 Aug 2018 18:35:33 +0200 Subject: [PATCH] making the time bound for generated gspn properties real valued --- src/storm-gspn/builder/JaniGSPNBuilder.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index 45a2a5ebc..aa8c64a4f 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -253,7 +253,7 @@ namespace storm { storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize)); standardProperties.emplace_back("MaxPrReachDeadlock", maxReachDeadlock, "The maximal probability to eventually reach a deadlock."); - auto exprTB = expressionManager->declareIntegerVariable(getUniqueVarName(*expressionManager, "TIME_BOUND")); + auto exprTB = expressionManager->declareRationalVariable(getUniqueVarName(*expressionManager, "TIME_BOUND")); auto janiTB = storm::jani::Constant(exprTB.getName(), exprTB); model->addConstant(janiTB); storm::logic::TimeBound tb(false, janiTB.getExpressionVariable().getExpression());