Browse Source

making the time bound for generated gspn properties real valued

tempestpy_adaptions
TimQu 6 years ago
parent
commit
817c5a218b
  1. 2
      src/storm-gspn/builder/JaniGSPNBuilder.cpp

2
src/storm-gspn/builder/JaniGSPNBuilder.cpp

@ -253,7 +253,7 @@ namespace storm {
storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize)); storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize));
standardProperties.emplace_back("MaxPrReachDeadlock", maxReachDeadlock, "The maximal probability to eventually reach a deadlock."); 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); auto janiTB = storm::jani::Constant(exprTB.getName(), exprTB);
model->addConstant(janiTB); model->addConstant(janiTB);
storm::logic::TimeBound tb(false, janiTB.getExpressionVariable().getExpression()); storm::logic::TimeBound tb(false, janiTB.getExpressionVariable().getExpression());

Loading…
Cancel
Save