|
@ -329,11 +329,11 @@ namespace storm { |
|
|
std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds; |
|
|
std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds; |
|
|
std::vector<storm::logic::TimeBoundReference> timeBoundReferences; |
|
|
std::vector<storm::logic::TimeBoundReference> timeBoundReferences; |
|
|
for (auto const& timeBound : timeBounds.get()) { |
|
|
for (auto const& timeBound : timeBounds.get()) { |
|
|
|
|
|
STORM_LOG_ASSERT(!std::get<0>(timeBound), "Lower bounds are not implemented for globally formulas."); |
|
|
lowerBounds.push_back(std::get<0>(timeBound)); |
|
|
lowerBounds.push_back(std::get<0>(timeBound)); |
|
|
upperBounds.push_back(std::get<1>(timeBound)); |
|
|
upperBounds.push_back(std::get<1>(timeBound)); |
|
|
timeBoundReferences.emplace_back(*std::get<2>(timeBound)); |
|
|
timeBoundReferences.emplace_back(*std::get<2>(timeBound)); |
|
|
} |
|
|
} |
|
|
STORM_LOG_ASSERT(lowerBounds.size() == 0, "Lower bounds are not implemented for globally formulas."); |
|
|
|
|
|
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedGloballyFormula(subformula, lowerBounds, upperBounds, timeBoundReferences)); |
|
|
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedGloballyFormula(subformula, lowerBounds, upperBounds, timeBoundReferences)); |
|
|
} else { |
|
|
} else { |
|
|
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GloballyFormula(subformula)); |
|
|
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GloballyFormula(subformula)); |
|
|