diff --git a/docs/MTLFormula_8h_source.html b/docs/MTLFormula_8h_source.html
index f94929df..a1e350b6 100644
--- a/docs/MTLFormula_8h_source.html
+++ b/docs/MTLFormula_8h_source.html
@@ -385,7 +385,7 @@
-
+
@@ -400,11 +400,11 @@
-
+
-
-
+
+
diff --git a/docs/MTLFormula_8hpp_source.html b/docs/MTLFormula_8hpp_source.html
index 62752129..81a01ff1 100644
--- a/docs/MTLFormula_8hpp_source.html
+++ b/docs/MTLFormula_8hpp_source.html
@@ -322,161 +322,157 @@
-
-
- 248 assert(this->get_operands().size() == rhs.
get_operands().size());
-
-
- 251 if (operator_ == LOP::LUNTIL || operator_ == LOP::LDUNTIL) {
- 252 if (duration_ < rhs.duration_) {
-
-
- 255 if (rhs.duration_ < duration_) {
-
-
-
-
- 260 return std::lexicographical_compare(this->get_operands().begin(),
- 261 this->get_operands().end(),
-
-
-
- 265template <
typename APType>
-
-
-
-
-
-
- 272 case LOP::AP:
return *
this;
break;
-
- 274 switch (operands_.front().get_operator()) {
-
-
- 277 case LOP::AP:
return *
this;
break;
-
- 279 return MTLFormula(operands_.front().get_operands().front())
-
-
-
-
- 284 std::vector<MTLFormula<APType>> normalized;
- 285 for (
const auto &op : operands_.front().get_operands()) {
- 286 normalized.push_back(
MTLFormula(LOP::LNEG, {op}).to_positive_normal_form());
-
-
- 289 std::begin(normalized),
- 290 std::end(normalized));
-
-
-
-
-
- 296 MTLFormula(LOP::LNEG, {operands_.front().get_operands().front()}).to_positive_normal_form();
-
- 298 MTLFormula(LOP::LNEG, {operands_.front().get_operands().back()}).to_positive_normal_form();
- 299 return MTLFormula(
dual(operands_.front().get_operator()),
-
- 301 operands_.front().get_interval());
-
-
-
-
-
-
-
- 309 std::vector<MTLFormula<APType>> normalized;
- 310 for (
const auto &op : operands_) {
- 311 normalized.push_back(op.to_positive_normal_form());
-
- 313 auto res = MTLFormula(operator_, std::begin(normalized), std::end(normalized));
- 314 res.duration_ = duration_;
-
-
-
- 318 throw std::logic_error(
"Error in to_positive_normal_form: should have returned.");
-
-
- 321template <
typename APType>
- 322std::set<AtomicProposition<APType>>
-
-
- 325 std::set<MTLFormula> aps = get_subformulas_of_type(LOP::AP);
- 326 std::set<logic::AtomicProposition<APType>> res;
-
- 328 for (
const auto &sf : aps) {
- 329 res.insert(sf.get_atomicProposition());
-
-
-
-
- 334template <
typename APType>
- 335std::set<MTLFormula<APType>>
-
-
- 338 std::set<MTLFormula> res;
+
+ 247 if (operator_ == LOP::LUNTIL || operator_ == LOP::LDUNTIL) {
+ 248 if (duration_ < rhs.duration_) {
+
+
+ 251 if (rhs.duration_ < duration_) {
+
+
+
+
+ 256 return std::lexicographical_compare(this->get_operands().begin(),
+ 257 this->get_operands().end(),
+
+
+
+ 261template <
typename APType>
+
+
+
+
+
+
+ 268 case LOP::AP:
return *
this;
break;
+
+ 270 switch (operands_.front().get_operator()) {
+
+
+ 273 case LOP::AP:
return *
this;
break;
+
+ 275 return MTLFormula(operands_.front().get_operands().front())
+
+
+
+
+ 280 std::vector<MTLFormula<APType>> normalized;
+ 281 for (
const auto &op : operands_.front().get_operands()) {
+ 282 normalized.push_back(
MTLFormula(LOP::LNEG, {op}).to_positive_normal_form());
+
+
+ 285 std::begin(normalized),
+ 286 std::end(normalized));
+
+
+
+
+
+ 292 MTLFormula(LOP::LNEG, {operands_.front().get_operands().front()}).to_positive_normal_form();
+
+ 294 MTLFormula(LOP::LNEG, {operands_.front().get_operands().back()}).to_positive_normal_form();
+
+
+ 297 operands_.front().get_interval());
+
+
+
+
+
+
+
+ 305 std::vector<MTLFormula<APType>> normalized;
+ 306 for (
const auto &op : operands_) {
+ 307 normalized.push_back(op.to_positive_normal_form());
+
+ 309 auto res = MTLFormula(operator_, std::begin(normalized), std::end(normalized));
+ 310 res.duration_ = duration_;
+
+
+
+ 314 throw std::logic_error(
"Error in to_positive_normal_form: should have returned.");
+
+
+ 317template <
typename APType>
+ 318std::set<AtomicProposition<APType>>
+
+
+ 321 std::set<MTLFormula> aps = get_subformulas_of_type(LOP::AP);
+ 322 std::set<logic::AtomicProposition<APType>> res;
+
+ 324 for (
const auto &sf : aps) {
+ 325 res.insert(sf.get_atomicProposition());
+
+
+
+
+ 330template <
typename APType>
+ 331std::set<MTLFormula<APType>>
+
+
+ 334 std::set<MTLFormula> res;
+
+ 336 if (get_operator() == op) {
+
+
- 340 if (get_operator() == op) {
-
-
-
- 344 std::for_each(operands_.begin(), operands_.end(), [&res, op](
const MTLFormula &o) {
- 345 auto tmp = o.get_subformulas_of_type(op);
- 346 res.insert(tmp.begin(), tmp.end());
-
-
-
-
-
- 352template <
typename APType>
-
-
-
- 356 Endpoint largest_constant = 0;
-
-
-
- 360 case LOP::FALSE: largest_constant = 0;
break;
- 361 case LOP::LNEG: largest_constant = operands_[0].get_largest_constant();
break;
-
-
- 364 for (
const auto &sub_formula : operands_) {
- 365 largest_constant = std::max(0u, sub_formula.get_largest_constant());
-
-
-
-
-
-
- 372 largest_constant = std::max(largest_constant, duration_->upper());
-
-
- 375 largest_constant = std::max(largest_constant, duration_->lower());
-
-
- 378 largest_constant = std::max(
- 379 {largest_constant, operands_[0].get_largest_constant(), operands_[1].get_largest_constant()});
-
-
-
- 383 return largest_constant;
-
-
-
+ 340 std::for_each(operands_.begin(), operands_.end(), [&res, op](
const MTLFormula &o) {
+ 341 auto tmp = o.get_subformulas_of_type(op);
+ 342 res.insert(tmp.begin(), tmp.end());
+
+
+
+
+
+ 348template <
typename APType>
+
+
+
+ 352 Endpoint largest_constant = 0;
+
+
+
+ 356 case LOP::FALSE: largest_constant = 0;
break;
+ 357 case LOP::LNEG: largest_constant = operands_[0].get_largest_constant();
break;
+
+
+ 360 for (
const auto &sub_formula : operands_) {
+ 361 largest_constant = std::max(0u, sub_formula.get_largest_constant());
+
+
+
+
+
+
+ 368 largest_constant = std::max(largest_constant, duration_->upper());
+
+
+ 371 largest_constant = std::max(largest_constant, duration_->lower());
+
+
+ 374 largest_constant = std::max(
+ 375 {largest_constant, operands_[0].get_largest_constant(), operands_[1].get_largest_constant()});
+
+
+
+ 379 return largest_constant;
+
+
+
-
+
-
+
-
-
+
+
bool satisfies(const MTLFormula< APType > &phi) const
Checks satisfaction at pos 0.
Definition: MTLFormula.hpp:180
bool satisfies_at(const MTLFormula< APType > &phi, std::size_t i) const
Checks satisfaction at a certain position.
Definition: MTLFormula.hpp:111
std::unique_ptr< Formula< LocationT > > create_disjunction(std::unique_ptr< Formula< LocationT > > disjunct1, std::unique_ptr< Formula< LocationT > > disjunct2)
Create a disjunction of two formulas. If possible, the formula will be immediately simplified.
Definition: ata_formula.hpp:317
std::unique_ptr< Formula< LocationT > > create_conjunction(std::unique_ptr< Formula< LocationT > > conjunct1, std::unique_ptr< Formula< LocationT > > conjunct2)
Create a conjunction of two formulas. If possible, the formula will be immediately simplified.
Definition: ata_formula.hpp:299
utilities::arithmetic::Interval< Endpoint > TimeInterval
An interval used for constrained until and dual until operators.
Definition: MTLFormula.h:30