diff --git a/include/utap/AbstractBuilder.hpp b/include/utap/AbstractBuilder.hpp
index 1bea181..5e22250 100644
--- a/include/utap/AbstractBuilder.hpp
+++ b/include/utap/AbstractBuilder.hpp
@@ -108,7 +108,7 @@ class AbstractBuilder : public ParserBuilder
      * Process declarations
      */
     void proc_begin(std::string_view name, const bool isTA = true, std::string_view type = "",
-                    std::string_view mode = "") override;
+                    std::string_view mode = {}) override;
     void proc_end() override;                                                           // 1 ProcBody
     void proc_location(std::string_view name, bool hasInvariant, bool hasER) override;  // 1 expr
     void proc_location_commit(std::string_view name) override;                          // mark previously decl. state
@@ -177,6 +177,7 @@ class AbstractBuilder : public ParserBuilder
     void expr_false() override;
     void expr_double(double) override;
     void expr_string(std::string_view) override;
+    void expr_location(std::string_view) override;
     void expr_location() override;
     void expr_identifier(std::string_view varName) override;
     void expr_nat(int32_t) override;  // natural number
@@ -281,6 +282,11 @@ class AbstractBuilder : public ParserBuilder
     void expr_MITL_exists_dynamic_begin(std::string_view, std::string_view) override;
     void expr_MITL_exists_dynamic_end(std::string_view name) override;
 
+    /** Coshy */
+    void expr_acontrol() override;
+    void expr_discrete_interval() override;
+    void expr_interval(int32_t divisions) override;
+
     /** Verification queries */
     void model_option(std::string_view key, std::string_view value) override;
     void query_begin() override;
diff --git a/include/utap/DocumentBuilder.hpp b/include/utap/DocumentBuilder.hpp
index 1df120c..a4d3a9a 100644
--- a/include/utap/DocumentBuilder.hpp
+++ b/include/utap/DocumentBuilder.hpp
@@ -26,6 +26,7 @@
 #include "utap/utap.hpp"
 
 #include <vector>
+
 #include <cinttypes>
 
 namespace UTAP {
diff --git a/include/utap/ExpressionBuilder.hpp b/include/utap/ExpressionBuilder.hpp
index 6b7a460..5170a69 100644
--- a/include/utap/ExpressionBuilder.hpp
+++ b/include/utap/ExpressionBuilder.hpp
@@ -27,6 +27,7 @@
 
 #include <stack>
 #include <vector>
+
 #include <cassert>
 
 namespace UTAP {
@@ -90,7 +91,6 @@ T pop_back(std::vector<T>& vec)
     vec.pop_back();
     return res;
 }
-
 /**
  * Partial implementation of the builder interface: The
  * ExpressionBuilder implements all expression related
@@ -190,6 +190,7 @@ class ExpressionBuilder : public AbstractBuilder
     void expr_double(double) override;
     void expr_string(std::string_view name) override;
     void expr_identifier(std::string_view varName) override;
+    void expr_location(std::string_view name) override;
     void expr_location() override;
     void expr_nat(int32_t) override;
     void expr_call_begin() override;
@@ -239,6 +240,11 @@ class ExpressionBuilder : public AbstractBuilder
     void expr_MITL_diamond(int, int) override;
     void expr_MITL_box(int, int) override;
 
+    /** Coshy */
+    void expr_acontrol() override;
+    void expr_discrete_interval() override;
+    void expr_interval(int32_t divisions) override;
+
     /* Dynamic process creation */
     void expr_spawn(int params) override;
     void expr_exit() override;
diff --git a/include/utap/PrettyPrinter.hpp b/include/utap/PrettyPrinter.hpp
index fc5b2f7..2c435e7 100644
--- a/include/utap/PrettyPrinter.hpp
+++ b/include/utap/PrettyPrinter.hpp
@@ -44,10 +44,10 @@ class PrettyPrinter : public AbstractBuilder
     std::string committed;
     std::string param;
     std::string templateset;
-    int select{}, guard{}, sync{}, update{}, probability{};
+    int select{-1}, guard{-1}, sync{-1}, update{-1}, probability{-1};
 
-    bool first{};
-    uint32_t level{};
+    bool first{true};
+    uint32_t level{0};
 
     void indent();
     void indent(std::string& s);
diff --git a/include/utap/StatementBuilder.hpp b/include/utap/StatementBuilder.hpp
index 5d6abec..e030dd1 100644
--- a/include/utap/StatementBuilder.hpp
+++ b/include/utap/StatementBuilder.hpp
@@ -27,6 +27,7 @@
 
 #include <filesystem>
 #include <vector>
+
 #include <cinttypes>
 
 namespace UTAP {
diff --git a/include/utap/builder.hpp b/include/utap/builder.hpp
index c79b691..ca8f8bc 100644
--- a/include/utap/builder.hpp
+++ b/include/utap/builder.hpp
@@ -321,6 +321,7 @@ class ParserBuilder
     virtual void expr_double(double) = 0;
     virtual void expr_string(std::string_view name) = 0;
     virtual void expr_identifier(std::string_view varName) = 0;
+    virtual void expr_location(std::string_view name) = 0;
     virtual void expr_location() = 0;
     virtual void expr_nat(int32_t) = 0;  // natural number
     virtual void expr_call_begin() = 0;
@@ -433,6 +434,11 @@ class ParserBuilder
     virtual void expr_MITL_exists_dynamic_end(std::string_view name) = 0;
     virtual void expr_dynamic_process_expr(std::string_view) = 0;
 
+    /** Coshy */
+    virtual void expr_acontrol() = 0;
+    virtual void expr_discrete_interval() = 0;
+    virtual void expr_interval(int32_t divisions) = 0;
+
     /** Verification queries */
     virtual void model_option(std::string_view key, std::string_view value) = 0;
     virtual void query_begin() = 0;
diff --git a/include/utap/common.hpp b/include/utap/common.hpp
index 41eb2b0..64ecae5 100644
--- a/include/utap/common.hpp
+++ b/include/utap/common.hpp
@@ -278,6 +278,15 @@ enum Kind {
     MITL_ATOM,
     MITL_EXISTS,
     MITL_FORALL,
+
+    /******************************************************
+     * HYPA
+     */
+    ACONTROL,
+    DISCRETE_INTERVAL,
+    INTERVAL,
+    INTERVAL_LIST,
+
     /*Dynamic */
     SPAWN,
     EXIT,
diff --git a/include/utap/position.hpp b/include/utap/position.hpp
index 8f28df5..0e8fb13 100644
--- a/include/utap/position.hpp
+++ b/include/utap/position.hpp
@@ -28,6 +28,7 @@
 #include <memory>
 #include <string>
 #include <vector>
+
 #include <cstdint>
 
 namespace UTAP {
diff --git a/include/utap/property.hpp b/include/utap/property.hpp
index 06ab036..daca0b4 100644
--- a/include/utap/property.hpp
+++ b/include/utap/property.hpp
@@ -109,7 +109,10 @@ enum class quant_t {
     PMax,
 
     /* LSC scenario property */
-    scenario
+    scenario,
+
+    /* HYPA: acontrol: A[] ... {} -> {} */
+    acontrol,
 };
 
 /** property status */
diff --git a/include/utap/statement.hpp b/include/utap/statement.hpp
index 0af80e3..2aadfc9 100644
--- a/include/utap/statement.hpp
+++ b/include/utap/statement.hpp
@@ -29,6 +29,7 @@
 #include <memory>
 #include <string>
 #include <utility>
+
 #include <cstdint>
 
 namespace UTAP {
diff --git a/include/utap/symbols.hpp b/include/utap/symbols.hpp
index 0abc848..ed79f3b 100644
--- a/include/utap/symbols.hpp
+++ b/include/utap/symbols.hpp
@@ -23,12 +23,12 @@
 #ifndef UTAP_SYMBOLS_HH
 #define UTAP_SYMBOLS_HH
 
-#include "common.hpp"
 #include "position.hpp"
 #include "type.hpp"
 
 #include <exception>
 #include <optional>
+
 #include <cstdint>
 
 namespace UTAP {
diff --git a/include/utap/type.hpp b/include/utap/type.hpp
index bb84614..cc305c5 100644
--- a/include/utap/type.hpp
+++ b/include/utap/type.hpp
@@ -29,6 +29,7 @@
 #include <memory>  // shared_ptr
 #include <optional>
 #include <string>
+
 #include <cstdint>
 
 namespace UTAP {
diff --git a/src/AbstractBuilder.cpp b/src/AbstractBuilder.cpp
index fbb76c7..049736c 100644
--- a/src/AbstractBuilder.cpp
+++ b/src/AbstractBuilder.cpp
@@ -22,9 +22,8 @@
 #include "utap/AbstractBuilder.hpp"
 
 #include <vector>
+
 #include <cinttypes>
-#include <cstdarg>
-#include <cstdio>
 
 using namespace UTAP;
 
@@ -202,6 +201,7 @@ void AbstractBuilder::expr_scenario(std::string_view name) { UNSUPPORTED; }
 void AbstractBuilder::expr_ternary(Constants::Kind ternaryop, bool firstMissing) { UNSUPPORTED; }
 void AbstractBuilder::expr_inline_if() { UNSUPPORTED; }
 void AbstractBuilder::expr_comma() { UNSUPPORTED; }
+void AbstractBuilder::expr_location(std::string_view) { UNSUPPORTED; }
 void AbstractBuilder::expr_location() { UNSUPPORTED; }
 void AbstractBuilder::expr_dot(std::string_view) { UNSUPPORTED; }
 void AbstractBuilder::expr_deadlock() { UNSUPPORTED; }
@@ -280,6 +280,10 @@ void AbstractBuilder::expr_MITL_forall_dynamic_end(std::string_view name) { UNSU
 void AbstractBuilder::expr_MITL_exists_dynamic_begin(std::string_view, std::string_view) { UNSUPPORTED; }
 void AbstractBuilder::expr_MITL_exists_dynamic_end(std::string_view name) { UNSUPPORTED; }
 
+void AbstractBuilder::expr_acontrol() { UNSUPPORTED; }
+void AbstractBuilder::expr_discrete_interval() { UNSUPPORTED; }
+void AbstractBuilder::expr_interval(int32_t divisions) { UNSUPPORTED; }
+
 void AbstractBuilder::query_begin() { UNSUPPORTED; }
 void AbstractBuilder::query_end() { UNSUPPORTED; }
 void AbstractBuilder::query_formula(std::string_view, std::string_view) { UNSUPPORTED; }
diff --git a/src/DocumentBuilder.cpp b/src/DocumentBuilder.cpp
index 7bea49f..0b667c5 100644
--- a/src/DocumentBuilder.cpp
+++ b/src/DocumentBuilder.cpp
@@ -24,8 +24,8 @@
 #include "print.hpp"
 
 #include <sstream>
-#include <stdexcept>
 #include <vector>
+
 #include <cassert>
 
 using namespace UTAP;
diff --git a/src/ExpressionBuilder.cpp b/src/ExpressionBuilder.cpp
index bf1b13a..757be6f 100644
--- a/src/ExpressionBuilder.cpp
+++ b/src/ExpressionBuilder.cpp
@@ -435,9 +435,7 @@ void ExpressionBuilder::expr_unary(Kind unaryop)  // 1 expr
     case PLUS:
         /* Unary plus can be ignored */
         break;
-    case MINUS:
-        unaryop = UNARY_MINUS;
-        [[fallthrough]];
+    case MINUS: unaryop = UNARY_MINUS; [[fallthrough]];
     default: fragments[0] = Expression::create_unary(unaryop, fragments[0], position, fragments[0].get_type());
     }
 }
@@ -532,6 +530,17 @@ void ExpressionBuilder::expr_comma()
     fragments.push(Expression::create_binary(COMMA, e1, e2, position, e2.get_type()));
 }
 
+void ExpressionBuilder::expr_location(std::string_view name)
+{
+    Symbol uid;
+    if (!resolve(name, uid)) {
+        expr_false();
+        throw unknown_identifier_error(name);
+    }
+    fragments.push(Expression::create_identifier(uid, position));
+    expr_location();
+}
+
 void ExpressionBuilder::expr_location()
 {
     Expression expr = fragments[0];
@@ -725,7 +734,7 @@ void ExpressionBuilder::expr_load_strategy()
 
 void ExpressionBuilder::expr_save_strategy(std::string_view strategy_name)
 {
-    assert(fragments.size() == 1);
+    // assert(fragments.size() == 1);
     fragments[0] = Expression::create_binary(SAVE_STRAT, fragments[0], make_constant(strategy_name), position);
 }
 
@@ -892,6 +901,38 @@ void ExpressionBuilder::expr_MITL_box(int low, int high)
     fragments.push(form);
 }
 
+void ExpressionBuilder::expr_acontrol()
+{
+    const auto partition = fragments[0];
+    assert(partition.get_kind() == INTERVAL_LIST);
+    const auto to_enforce = fragments[1];
+    fragments.pop(2);
+    fragments.push(Expression::create_binary(ACONTROL, to_enforce, partition, position));
+}
+
+void ExpressionBuilder::expr_discrete_interval()
+{
+    const auto identifier = fragments[0];
+    const auto upper = fragments[1];
+    const auto lower = fragments[2];
+    fragments.pop(3);
+    auto args = std::vector{identifier, lower, upper};
+    const auto discrete_interval = Expression::create_nary(DISCRETE_INTERVAL, std::move(args), position);
+    fragments.push(discrete_interval);
+}
+
+void ExpressionBuilder::expr_interval(int32_t divisions)
+{
+    const auto identifier = fragments[0];
+    const auto upper = fragments[1];
+    const auto lower = fragments[2];
+    fragments.pop(3);
+    const auto divisions2 = Expression::create_constant(divisions, position);
+    auto args = std::vector{identifier, lower, upper, divisions2};
+    const auto interval = Expression::create_nary(INTERVAL, std::move(args), position);
+    fragments.push(interval);
+}
+
 void ExpressionBuilder::expr_MITL_disj()
 {
     auto& left = fragments[1];
@@ -1065,7 +1106,6 @@ void ExpressionBuilder::push_dynamic_frame_of(Template* t, std::string_view name
         throw TypeException("Template referenced before used");
     dynamicFrames.emplace(std::string{name}, t->frame);
 }
-
 void ExpressionBuilder::pop_dynamic_frame_of(std::string_view name)
 {
     if (auto it = dynamicFrames.find(name); it != dynamicFrames.end())
diff --git a/src/FeatureChecker.cpp b/src/FeatureChecker.cpp
index b9cf7f8..cdaf182 100644
--- a/src/FeatureChecker.cpp
+++ b/src/FeatureChecker.cpp
@@ -69,7 +69,7 @@ void FeatureChecker::visit_guard(Expression& guard)
             if (guard.get(i).uses_fp())
                 supported_methods.symbolic = false;
         }
-		[[fallthrough]];
+        [[fallthrough]];
     default: break;
     }
 }
diff --git a/src/PrettyPrinter.cpp b/src/PrettyPrinter.cpp
index f68f815..dbbbed5 100644
--- a/src/PrettyPrinter.cpp
+++ b/src/PrettyPrinter.cpp
@@ -71,14 +71,7 @@ void PrettyPrinter::indent(std::string& s)
     }
 }
 
-PrettyPrinter::PrettyPrinter(std::ostream& stream)
-{
-    o.push(&stream);
-
-    first = true;
-    level = 0;
-    select = guard = sync = update = probability = -1;
-}
+PrettyPrinter::PrettyPrinter(std::ostream& stream) { o.push(&stream); }
 
 void PrettyPrinter::add_position(uint32_t position, uint32_t offset, uint32_t line, std::shared_ptr<std::string> path)
 {}
diff --git a/src/TypeChecker.cpp b/src/TypeChecker.cpp
index 5d11633..a2ff41d 100644
--- a/src/TypeChecker.cpp
+++ b/src/TypeChecker.cpp
@@ -37,6 +37,7 @@
 #include <string>
 #include <tuple>
 #include <vector>
+
 #include <cassert>
 #include <cstddef>  // size_t
 #include <cstdint>  // uint32_t
@@ -208,6 +209,18 @@ bool is_assignable(const Type& type)
     }
 }
 
+static bool is_interval_list(Expression& expression)
+{
+    const auto n_expressions = expression.get_size();
+    for (auto i = 0u; i < n_expressions; ++i) {
+        auto e = expression[i];
+        if (!(e.get_type().is(INTERVAL) || e.get_type().is(DISCRETE_INTERVAL) || e.get_type().is(LOCATION_EXPR)))
+            return false;
+    }
+
+    return true;
+}
+
 using Error = TypeChecker::TypeError;
 
 Error expression_has_no_effect(const Expression& expr) { return {expr, "$Expression_does_not_have_any_effect"}; }
@@ -487,7 +500,7 @@ Error clock_difference_is_not_supported(const Expression& expr)
     return {expr, "$Clock_differences_are_not_supported"};
 }
 
-bool is_game_property(const Expression& expr)
+static bool is_game_property(const Expression& expr)
 {
     switch (expr.get_kind()) {
     case CONTROL:
@@ -496,7 +509,8 @@ bool is_game_property(const Expression& expr)
     case CONTROL_TOPT:
     case PO_CONTROL:
     case CONTROL_TOPT_DEF1:
-    case CONTROL_TOPT_DEF2: return true;
+    case CONTROL_TOPT_DEF2:
+    case ACONTROL: return true;
     default: return false;
     }
 }
@@ -512,7 +526,7 @@ bool has_MITL_in_quantified_sub(const Expression& expr)
     return hasIt;
 }
 
-bool has_spawn_or_exit(const Expression& expr)
+static bool has_spawn_or_exit(const Expression& expr)
 {
     bool hasIt = (expr.get_kind() == SPAWN || expr.get_kind() == EXIT);
     if (!hasIt) {
@@ -556,7 +570,6 @@ void static_analysis(Document& doc)
     }
 }
 }  // anonymous namespace
-
 ///////////////////////////////////////////////////////////////////////////
 
 void CompileTimeComputableValues::visit_variable(Variable& variable)
@@ -809,7 +822,7 @@ void TypeChecker::checkType(const Type& type, bool initialisable, bool inStruct)
     case Constants::STRING:
         if (inStruct)
             handleError(cannot_be_inside_struct(type));
-		break;
+        break;
     case Constants::CLOCK: break;
     case Constants::DOUBLE: break;
     case Constants::INT: break;
@@ -1211,6 +1224,7 @@ void TypeChecker::visit_progress(Progress& progress)
 {
     checkExpression(progress.guard);
     checkExpression(progress.measure);
+
     if (!progress.guard.empty() && !is_integral(progress.guard))
         handleError(progress_guard_must_evaluate_to_boolean(progress.guard));
     if (!is_integral(progress.measure))
@@ -1276,6 +1290,17 @@ void TypeChecker::visit_instance(Instance& instance)
     }
 }
 
+static bool hasMITLInQuantifiedSub(Expression& expr)
+{
+    bool hasIt = (expr.get_kind() == MITL_FORALL || expr.get_kind() == MITL_EXISTS);
+    if (!hasIt) {
+        for (uint32_t i = 0; i < expr.get_size(); i++) {
+            hasIt |= hasMITLInQuantifiedSub(expr.get(i));
+        }
+    }
+    return hasIt;
+}
+
 void TypeChecker::visitProperty(Expression& expr)
 {
     if (checkExpression(expr)) {
@@ -1653,16 +1678,20 @@ Expression TypeChecker::checkInitialiser(const Type& type, const Expression& ini
                     current = *index;
                 }
             }
+
             if (current >= type.get_record_size()) {
                 handleError(too_many_elements_in_initializer(init[i]));
                 break;
             }
+
             if (!result[current].empty()) {
                 handleError(multiple_initializers_for_field(init[i]));
                 continue;
             }
+
             result[current] = checkInitialiser(type.get_sub(current), init[i]);
         }
+
         // Check that all fields do have an initializer.
         for (const auto& res : result) {
             if (res.empty()) {
@@ -1670,6 +1699,7 @@ Expression TypeChecker::checkInitialiser(const Type& type, const Expression& ini
                 break;
             }
         }
+
         return Expression::create_nary(LIST, result, init.get_position(), type);
     }
     handleError(invalid_initializer(init));
@@ -2299,6 +2329,36 @@ bool TypeChecker::checkExpression(Expression& expr)
         }
         break;
 
+    case INTERVAL_LIST:
+        if (is_interval_list(expr)) {
+            type = Type::create_primitive(INTERVAL_LIST);
+        }
+        break;
+
+    case INTERVAL: {
+        const auto ident = expr[0].get_type();
+        const auto lower = expr[1].get_type();
+        const auto upper = expr[2].get_type();
+        const auto divisions = expr[3].get_type();
+        if ((ident.is_integer() || ident.is_double() || ident.is_clock()) &&
+            (lower.is_integer() || lower.is_double() || lower.is_clock()) &&
+            (upper.is_integer() || upper.is_double() || upper.is_clock()) && divisions.is_integer()) {
+            type = Type::create_primitive(INTERVAL);
+        }
+    } break;
+
+    case DISCRETE_INTERVAL:
+        if (expr[0].get_type().is_integer() && expr[1].get_type().is_integer()) {
+            type = Type::create_primitive(DISCRETE_INTERVAL);
+        }
+        break;
+
+    case ACONTROL:
+        if (expr[0].get_type().is_guard() && is_interval_list(expr[1])) {
+            type = Type::create_primitive(FORMULA);
+        }
+        break;
+
     case LEADS_TO:
     case SCENARIO2:
     case A_UNTIL:
@@ -2674,7 +2734,9 @@ int32_t parse_XML_buffer(const char* buffer, Document& doc, bool newxta,
     auto builder = DocumentBuilder{doc, paths};
     if (const auto err = parse_XML_buffer(buffer, builder, newxta); err != 0)
         return err;
+
     static_analysis(doc);
+
     return 0;
 }
 
@@ -2685,6 +2747,7 @@ int32_t parse_XML_file(const std::filesystem::path& file, Document& doc, bool ne
     if (const auto err = parse_XML_file(file, builder, newxta); err != 0)
         return err;
     static_analysis(doc);
+
     return 0;
 }
 
@@ -2694,6 +2757,7 @@ int32_t parse_XML_fd(int fd, Document& doc, bool newxta, const std::vector<std::
     if (const auto err = parse_XML_fd(fd, builder, newxta); err != 0)
         return err;
     static_analysis(doc);
+
     return 0;
 }
 
diff --git a/src/expression.cpp b/src/expression.cpp
index 4da1b43..88965fa 100644
--- a/src/expression.cpp
+++ b/src/expression.cpp
@@ -434,6 +434,7 @@ uint32_t Expression::get_size() const
     case FUN_CALL:
     case FUN_CALL_EXT:
     case LIST:
+    case INTERVAL_LIST:
     case SIMULATE:
     case SIMULATEREACH:
     case SPAWN: return std::get<int32_t>(data->value);
@@ -486,6 +487,9 @@ uint32_t Expression::get_size() const
     case MITL_FORALL:
     case FOREACH_DYNAMIC: assert(data->sub.size() == 3); return 3;
     case DYNAMIC_EVAL: assert(data->sub.size() == 2); return 2;
+    case ACONTROL: assert(data->sub.size() == 2); return 2;
+    case DISCRETE_INTERVAL: assert(data->sub.size() == 3); return 3;
+    case INTERVAL: assert(data->sub.size() == 4); return 4;
     default: assert(0); return 0;
     }
 }
@@ -1628,6 +1632,42 @@ std::ostream& Expression::print(std::ostream& os, bool old) const
         break;
     case TYPEDEF: os << "typedef"; break;
 
+    case ACONTROL:
+        os << "acontrol: A[] ";
+        get(0).print(os, old);
+        get(1).print(os, old);
+        break;
+
+    case INTERVAL_LIST:
+        os << " { ";
+        for (auto i = 0u; i < get_size(); ++i) {
+            get(i).print(os, old);
+            if (i + 1 < get_size()) {
+                os << ", ";
+            }
+        }
+        os << " }";
+        break;
+
+    case INTERVAL:
+        get(0).print(os, old);
+        os << "[";
+        get(1).print(os, old);
+        os << ", ";
+        get(2).print(os, old);
+        os << "]:";
+        get(3).print(os, old);
+        break;
+
+    case DISCRETE_INTERVAL:
+        get(0).print(os, old);
+        os << "[";
+        get(1).print(os, old);
+        os << ", ";
+        get(2).print(os, old);
+        os << "]";
+        break;
+
     // Types - Not applicable in expression printing
     case RANGE:
     case RECORD:
diff --git a/src/keywords.cpp b/src/keywords.cpp
index 2078f24..838adc0 100644
--- a/src/keywords.cpp
+++ b/src/keywords.cpp
@@ -149,6 +149,7 @@ namespace UTAP {
             {"foreach",       Keyword{T_FOREACH, Syntax::PROPERTY}},
             {"query",         Keyword{T_QUERY, Syntax::NEW}},
             {"location",      Keyword{T_LOCATION, Syntax::NEW}},
+            {"acontrol",      Keyword{T_ACONTROL, Syntax::NEW_PROPERTY}},
     };
 // clang-format on
 
diff --git a/src/keywords.hpp b/src/keywords.hpp
index ed2ccf7..31945ca 100644
--- a/src/keywords.hpp
+++ b/src/keywords.hpp
@@ -25,7 +25,6 @@
 #include "libparser.hpp"
 
 #include <string_view>
-#include <cinttypes>  // uint32_t
 
 namespace UTAP {
 struct Keyword
diff --git a/src/parser.y b/src/parser.y
index 37908e0..a4b38ab 100644
--- a/src/parser.y
+++ b/src/parser.y
@@ -2,22 +2,22 @@
 
  /* libutap - Uppaal Timed Automata Parser.
     Copyright (C) 2011-2024 Aalborg University.
-    Copyright (C) 2002-2011 Uppsala University and Aalborg University.
-
-    This library is free software; you can redistribute it and/or
-    modify it under the terms of the GNU Lesser General Public License
-    as published by the Free Software Foundation; either version 2.1 of
-    the License, or (at your option) any later version.
-
-    This library is distributed in the hope that it will be useful, but
-    WITHOUT ANY WARRANTY; without even the implied warranty of
-    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-    Lesser General Public License for more details.
-
-    You should have received a copy of the GNU Lesser General Public
-    License along with this library; if not, write to the Free Software
-    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
-    USA
+	Copyright (C) 2002-2011 Uppsala University and Aalborg University.
+
+	This library is free software; you can redistribute it and/or
+	modify it under the terms of the GNU Lesser General Public License
+	as published by the Free Software Foundation; either version 2.1 of
+	the License, or (at your option) any later version.
+
+	This library is distributed in the hope that it will be useful, but
+	WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+	Lesser General Public License for more details.
+
+	You should have received a copy of the GNU Lesser General Public
+	License along with this library; if not, write to the Free Software
+	Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
+	USA
  */
 
  /*********************************************************************
@@ -37,7 +37,6 @@
   * appear continuous error reports on the same code as no recovery is
   * made. Please report it, this might be corrected.
   */
-
 %code top {
 //NOLINTBEGIN
 }
@@ -54,15 +53,15 @@
 using namespace UTAP;
 using namespace Constants;
 
-#define YYLLOC_DEFAULT(Current, Rhs, N)    \
-    do                                     \
+#define YYLLOC_DEFAULT(Current, Rhs, N)        		  	        \
+	 do        								\
         if (N) {                           \
-            (Current).start = YYRHSLOC (Rhs, 1).start; \
-            (Current).end   = YYRHSLOC (Rhs, N).end;   \
+		   (Current).start        = YYRHSLOC (Rhs, 1).start;	        \
+		   (Current).end          = YYRHSLOC (Rhs, N).end;	        \
         } else {                           \
             (Current).start = (Current).end = YYRHSLOC (Rhs, 0).end; \
-        }                                  \
-    while (0)
+		 }								\
+	 while (0)
 
 #define YYLTYPE position_t
 }
@@ -78,13 +77,13 @@ static int lexer_flex();
 
 static int utap_lex()
 {
-    int old;
+   int old;
     if (syntax_token != 0) {
-       old = syntax_token;
-       syntax_token = 0;
-       return old;
-    }
-    return lexer_flex();
+	 old = syntax_token;
+	 syntax_token = 0;
+	 return old;
+   }
+   return lexer_flex();
 }
 
 static char rootTransId[MAXLEN];
@@ -92,11 +91,12 @@ static char rootTransId[MAXLEN];
 /* Counter used during array parsing. */
 static int types = 0;
 
+
 struct str_entry_t
 {
     size_t len;
-    const char* from;
-    const char* to;
+	const char* from;
+	const char* to;
 };
 
 const char* utap_msg(const char *msg)
@@ -115,30 +115,29 @@ const char* utap_msg(const char *msg)
             "$syntax_error: $unexpected %s, $expecting %s $or %s $or %s" },
         { 59, "syntax error, unexpected %s, expecting %s or %s or %s or %s",
             "$syntax_error: $unexpected %s, $expecting %s $or %s $or %s $or %s" }
-    };
+		};
     const auto len = std::strlen(msg);
     auto i = NB_STR / 2;
     while (i < NB_STR) {
         if (len < table[i].len) {
-            if (i == 0) return msg;
-            i = i/2;
-            continue;
-        }
+			if (i == 0) return msg;
+			i = i/2;
+			continue;
+		}
         if (len > table[i].len) {
-            if (i == NB_STR-1) return msg;
-            i = (i+NB_STR)/2;
-            continue;
-        }
+			if (i == NB_STR-1) return msg;
+			i = (i+NB_STR)/2;
+			continue;
+		}
         for(;i < NB_STR && len <= table[i].len; ++i) {
             if (strcmp(msg, table[i].from) == 0) {
-                return table[i].to;
-            }
-        }
-        break;
-    }
+				return table[i].to;
+			}
+		}
+		break;
+	}
     return msg;
 }
-
 #define CALL(first,last,call) do { ch->set_position(first.start, last.end); try { ch->call; } catch (TypeException &te) { ch->handle_error(te); } } while (0)
 
 #define YY_(msg) utap_msg(msg)
@@ -213,6 +212,9 @@ const char* utap_msg(const char *msg)
 /* Control Synthesis */
 %token T_CONTROL T_CONTROL_T T_SIMULATION
 
+/* HYPA */
+%token T_ACONTROL
+
 /* ExpectationKind optimization */
 %token T_MINEXP T_MAXEXP T_MINPR T_MAXPR T_STRATEGY T_LOAD_STRAT T_SAVE_STRAT
 
@@ -267,6 +269,7 @@ const char* utap_msg(const char *msg)
 %type <number> ArgList FieldDeclList FieldDeclIdList FieldDecl
 %type <number> ParameterList FieldInitList
 %type <number> OptionalInstanceParameterList ExpressionList NonEmptyExpressionList
+%type <number> IntervalList NonEmptyIntervalList
 %type <prefix> Type TypePrefix
 %type <string> Id NonTypeId
 %type <kind> UnaryOp AssignOp
@@ -377,10 +380,10 @@ InstanceLineExpression:
 OptionalInstanceParameterList:
         /* empty */ { $$ = 0; }
         | '(' ')' {
-            $$ = 0;
+        	$$ = 0;
         }
         | '(' ParameterList ')' {
-            $$ = $2;
+        	$$ = $2;
         };
 
 System: SysDecl Progress GanttDecl;
@@ -443,8 +446,8 @@ GanttDef:
         /* empty */
         | GanttDef NonTypeId              { CALL(@2, @2, gantt_decl_begin($2)); }
           GanttArgs ':' GanttExprList ';' { CALL(@2, @6, gantt_decl_end());
-    }
-    ;
+	}
+	;
 
 GanttArgs:
         /* empty */
@@ -463,12 +466,12 @@ GanttDeclSelect:
 GanttExprList:
         GanttExpr
         | GanttExprList ',' GanttExpr
-    ;
+	;
 
 GanttExpr:
         Expression T_ARROW Expression {
-        CALL(@1, @3, gantt_entry_begin());
-        CALL(@1, @3, gantt_entry_end());
+	    CALL(@1, @3, gantt_entry_begin());
+	    CALL(@1, @3, gantt_entry_end());
         }
         | T_FOR                                                  { CALL(@1, @1, gantt_entry_begin()); }
           '(' GanttEntrySelect ')' Expression T_ARROW Expression { CALL(@1, @7, gantt_entry_end()); }
@@ -509,13 +512,13 @@ FunctionDecl:
         /* Notice that StatementList will catch all errors. Hence we
          * should be able to guarantee, that once declFuncBegin() has
          * been called, we will also call declFuncEnd().
-         * Correction: No it won't.
-         * int f() { if (cond) { return 0; }
-         * will generate an error, not call declFuncEnd, and the builder
-         * will be left in an inconsistent state. EndBlock fixes that.
-         *
-         * Correction^2: It did not fix it. Discussion continued at
-         * StatementBuilder::declFuncBegin definition
+	 * Correction: No it won't.
+	 * int f() { if (cond) { return 0; }
+	 * will generate an error, not call declFuncEnd, and the builder
+	 * will be left in an inconsistent state. EndBlock fixes that.
+     *
+     * Correction^2: It did not fix it. Discussion continued at
+     * StatementBuilder::declFuncBegin definition
          */
         Type Id OptionalParameterList '{' {
           CALL(@1, @2, decl_func_begin($2));
@@ -771,8 +774,8 @@ ProcDecl:
 
 ProcBody:
         ProcLocalDeclList States LocFlags Init Transitions
-        | ProcLocalDeclList States Branchpoints LocFlags Init Transitions
-        | /* empty */
+	| ProcLocalDeclList States Branchpoints LocFlags Init Transitions
+	| /* empty */
         ;
 
 ProcLocalDeclList:
@@ -795,17 +798,17 @@ StateDeclList:
 StateDecl:
           NonTypeId { CALL(@1, @1, proc_location($1, false, false)); }
         | NonTypeId '{' ';' ExpRate '}' {
-        CALL(@1, @5, proc_location($1, false, true));
-    }
+	    CALL(@1, @5, proc_location($1, false, true));
+	}
         | NonTypeId '{' Expression '}' {
-        CALL(@1, @4, proc_location($1, true, false));
+	    CALL(@1, @4, proc_location($1, true, false));
         }
         | NonTypeId '{' Expression ';' ExpRate '}' {
-        CALL(@1, @6, proc_location($1, true, true));
-    }
+	    CALL(@1, @6, proc_location($1, true, true));
+	}
         | NonTypeId '{' error '}' {
-        CALL(@1, @4, proc_location($1, false, false));
-    }
+	    CALL(@1, @4, proc_location($1, false, false));
+	}
         ;
 
 Branchpoints:
@@ -820,7 +823,7 @@ BranchpointDeclList:
 
 BranchpointDecl:
         NonTypeId {
-        CALL(@1, @1, proc_branchpoint($1));
+	    CALL(@1, @1, proc_branchpoint($1));
         };
 
 Init:
@@ -903,7 +906,7 @@ Sync:
 
 SyncExpr:
         Expression {
-        CALL(@1, @1, proc_sync(SYNC_CSP));
+	    CALL(@1, @1, proc_sync(SYNC_CSP));
         }
         | Expression T_EXCLAM {
           CALL(@1, @2, proc_sync(SYNC_BANG));
@@ -980,9 +983,9 @@ UStateList:
 
 ExpRate:
         Expression
-    | Expression ':' Expression {
-        CALL(@1,@3, expr_binary(FRACTION));
-    };
+	| Expression ':' Expression {
+	    CALL(@1,@3, expr_binary(FRACTION));
+	};
 
 /**********************************************************************
  * Uppaal C grammar
@@ -1020,18 +1023,18 @@ IfCondition: T_IF '(' { CALL(@1, @2, if_begin()); } ExprList ')' { CALL(@3, @3,
 IfConditionThenMatched: IfCondition MatchedStatement T_ELSE { CALL(@1, @3, if_then()); };
 
 MatchedStatement: IfConditionThenMatched MatchedStatement {
-        CALL(@1, @2, if_end(true));
-    }
+	    CALL(@1, @2, if_end(true));
+	}
         | OtherStatement
-    ;
+	;
 
 UnmatchedStatement: IfCondition Statement {
             CALL(@2, @2, if_then());
             CALL(@1, @2, if_end(false));
-    }
+	}
         | IfConditionThenMatched UnmatchedStatement {
-        CALL(@1, @2, if_end(true));
-    }
+	    CALL(@1, @2, if_end(true));
+	}
         ;
 
 OtherStatement:
@@ -1043,7 +1046,7 @@ OtherStatement:
           CALL(@1, @2, expr_statement());
         }
         | ForStatement
-    | WhileStatement
+	| WhileStatement
         | T_BREAK ';' {
             CALL(@1, @2, break_statement());
           }
@@ -1063,8 +1066,8 @@ OtherStatement:
           CALL(@1, @2, return_statement(false));
         }
         | T_ASSERT Expression ';' {
-        CALL(@1, @2, assert_statement());
-    }
+	    CALL(@1, @2, assert_statement());
+	}
         ;
 
 ForStatement: T_FOR '(' ExprList ';' ExprList ';' ExprList ')' {
@@ -1080,18 +1083,18 @@ ForStatement: T_FOR '(' ExprList ';' ExprList ';' ExprList ')' {
             CALL(@7, @7, iteration_end($3));
         }
         | T_FOR '(' error ')' Statement
-    ;
+	;
 
 WhileStatement: T_WHILE '(' {
             CALL(@1, @2, while_begin());
         }
         ExprList ')' Statement {
             CALL(@3, @4, while_end());
-    }
+	}
         | T_WHILE '(' error ')' Statement
         | T_DO {
             CALL(@1, @1, do_while_begin());
-    }
+	}
           Statement T_WHILE '(' ExprList ')' ';' {
             CALL(@2, @7, do_while_end());
         }
@@ -1103,11 +1106,11 @@ SwitchCaseList: SwitchCase
 
 SwitchCase:
         T_CASE Expression ':' {
-        CALL(@1, @3, case_begin());
+	    CALL(@1, @3, case_begin());
         }
         StatementList {
             CALL(@4, @4, case_end());
-    }
+	}
         | T_DEFAULT ':' {
             CALL(@1, @2, default_begin());
         }
@@ -1124,32 +1127,32 @@ ExprList:
 
 Expression:
         T_FALSE {
-        CALL(@1, @1, expr_false());
+	    CALL(@1, @1, expr_false());
         }
         | T_TRUE {
-        CALL(@1, @1, expr_true());
+	    CALL(@1, @1, expr_true());
         }
         | T_NAT  {
-        CALL(@1, @1, expr_nat($1));
+	    CALL(@1, @1, expr_nat($1));
         }
         | T_FLOATING {
-        CALL(@1, @1, expr_double($1));
-    }
+	    CALL(@1, @1, expr_double($1));
+	}
         | T_CHARARR
         {
             CALL(@1, @1, expr_string($1));
         }
         | BuiltinFunction1 '(' Expression ')' {
-        CALL(@1, @4, expr_builtin_function1($1));
-    }
+	    CALL(@1, @4, expr_builtin_function1($1));
+	}
         | BuiltinFunction2 '(' Expression ',' Expression ')' {
-        CALL(@1, @6, expr_builtin_function2($1));
-    }
+	    CALL(@1, @6, expr_builtin_function2($1));
+	}
         | BuiltinFunction3 '(' Expression ',' Expression ',' Expression ')' {
-        CALL(@1, @8, expr_builtin_function3($1));
-    }
+	    CALL(@1, @8, expr_builtin_function3($1));
+	}
         | NonTypeId {
-        CALL(@1, @1, expr_identifier($1));
+	    CALL(@1, @1, expr_identifier($1));
         }
         | Expression '(' {
             CALL(@1, @2, expr_call_begin());
@@ -1184,8 +1187,8 @@ Expression:
           CALL(@1, @2, expr_pre_decrement());
         }
         | T_MINUS T_POS_NEG_MAX {
-      CALL(@1, @2, expr_nat(std::numeric_limits<int>::min()));
-    }
+	  CALL(@1, @2, expr_nat(std::numeric_limits<int>::min()));
+	}
         | UnaryOp Expression {
           CALL(@1, @2, expr_unary($1));
         } %prec UOPERATOR
@@ -1273,8 +1276,8 @@ Expression:
           CALL(@1, @3, expr_binary(OR));
         }
         | Expression T_KW_XOR Expression {
-        CALL(@1, @3, expr_binary(XOR));
-    }
+	    CALL(@1, @3, expr_binary(XOR));
+	}
         | Expression T_MIN Expression {
             CALL(@1, @3, expr_binary(MIN));
         }
@@ -1286,7 +1289,7 @@ Expression:
         } Expression {
             CALL(@1, @8, expr_sum_end($3));
         } %prec T_SUM
-        | T_FORALL '(' Id ':' Type ')' {
+	    | T_FORALL '(' Id ':' Type ')' {
             CALL(@1, @6, expr_forall_begin($3));
         } Expression {
             CALL(@1, @8, expr_forall_end($3));
@@ -1296,48 +1299,48 @@ Expression:
         } Expression {
             CALL(@1, @8, expr_exists_end($3));
         } %prec T_EXISTS
-    | DynamicExpression
-    | MITLExpression
+	| DynamicExpression
+	| MITLExpression
         | Assignment
         ;
 
 DynamicExpression:
         T_SPAWN NonTypeId {
-        CALL(@1,@2, expr_identifier($2));
-    } '(' ArgList ')' {
-        CALL(@1,@6, expr_spawn($5));
-    }
+	    CALL(@1,@2, expr_identifier($2));
+	} '(' ArgList ')' {
+	    CALL(@1,@6, expr_spawn($5));
+	}
         | T_EXIT '(' ')' {
-        CALL(@1,@3, expr_exit());
-    }
+	    CALL(@1,@3, expr_exit());
+	}
         | T_NUMOF '(' NonTypeId ')'{
-        CALL(@3,@3, expr_identifier($3));
-        CALL(@1,@4, expr_numof());
-    }
+	    CALL(@3,@3, expr_identifier($3));
+	    CALL(@1,@4, expr_numof());
+	}
         | T_FORALL '(' Id ':' NonTypeId {
-        CALL(@1,@5, expr_identifier($5));
-        CALL(@1,@5, expr_forall_dynamic_begin($3,$5));
-    } ')'  '(' Expression ')'   {
-        CALL(@1,@8, expr_forall_dynamic_end($3));
-    }
+	    CALL(@1,@5, expr_identifier($5));
+	    CALL(@1,@5, expr_forall_dynamic_begin($3,$5));
+	} ')'  '(' Expression ')'   {
+	    CALL(@1,@8, expr_forall_dynamic_end($3));
+	}
         | T_EXISTS '(' Id ':' NonTypeId {
-        CALL(@1,@5, expr_identifier($5));
-        CALL(@1,@5, expr_exists_dynamic_begin($3,$5));
-    } ')' '(' Expression ')'  {
-        CALL(@1,@8, expr_exists_dynamic_end($3));
-    }
+	    CALL(@1,@5, expr_identifier($5));
+	    CALL(@1,@5, expr_exists_dynamic_begin($3,$5));
+	} ')' '(' Expression ')'  {
+	    CALL(@1,@8, expr_exists_dynamic_end($3));
+	}
         | T_SUM '(' Id ':' NonTypeId {
-        CALL(@1,@5, expr_identifier($5));
-        CALL(@1,@5, expr_sum_dynamic_begin($3,$5));
-    } ')' Expression   {
-        CALL(@1,@8, expr_sum_dynamic_end($3));
-    }
+	    CALL(@1,@5, expr_identifier($5));
+	    CALL(@1,@5, expr_sum_dynamic_begin($3,$5));
+	} ')' Expression   {
+	    CALL(@1,@8, expr_sum_dynamic_end($3));
+	}
         | T_FOREACH '(' Id ':' NonTypeId {
-        CALL(@1,@5, expr_identifier($5));
-        CALL(@1,@5, expr_foreach_dynamic_begin($3,$5));
-    } ')' Expression   {
-        CALL(@1,@8, expr_foreach_dynamic_end($3));
-    }
+	    CALL(@1,@5, expr_identifier($5));
+	    CALL(@1,@5, expr_foreach_dynamic_begin($3,$5));
+	} ')' Expression   {
+	    CALL(@1,@8, expr_foreach_dynamic_end($3));
+	}
         ;
 
 
@@ -1586,10 +1589,10 @@ OldStateDeclList:
 
 OldStateDecl:
         NonTypeId {
-        CALL(@1, @1, proc_location($1, false, false));
+	    CALL(@1, @1, proc_location($1, false, false));
         }
         | NonTypeId '{' OldInvariant '}' {
-        CALL(@1, @4, proc_location($1, true, false));
+	    CALL(@1, @4, proc_location($1, true, false));
         }
         ;
 
@@ -1681,47 +1684,47 @@ PropertyList:
 PropertyList2:
         /* empty */
         | PropertyList2 Property '\n'
-    ;
+	;
 
 QueryList:
         /* empty */
-    | QueryList Query
-    ;
+	| QueryList Query
+	;
 
 Query:
         T_QUERY '{' Property '}'
         | T_QUERY '{' error '}'
-    ;
+	;
 
 BoolOrKWAnd:
         T_KW_AND | T_BOOL_AND;
 
 SubProperty:
         T_AF Expression {
-        CALL(@1, @2, expr_unary(AF));
-    }
+	    CALL(@1, @2, expr_unary(AF));
+	}
         | T_AG '(' Expression BoolOrKWAnd T_AF Expression ')' {
             CALL(@5, @6, expr_unary(AF));
             CALL(@3, @6, expr_binary(AND));
             CALL(@1, @7, expr_unary(AG));
         }
         | T_AG Expression {
-        CALL(@1, @2, expr_unary(AG));
+	    CALL(@1, @2, expr_unary(AG));
         }
-    | T_EF Expression {
-        CALL(@1, @2, expr_unary(EF));
+	| T_EF Expression {
+	    CALL(@1, @2, expr_unary(EF));
         }
-    | T_EG Expression {
-        CALL(@1, @2, expr_unary(EG));
+	| T_EG Expression {
+	    CALL(@1, @2, expr_unary(EG));
         }
-    | Expression T_LEADS_TO Expression {
-        CALL(@1, @3, expr_binary(LEADS_TO));
+	| Expression T_LEADS_TO Expression {
+	    CALL(@1, @3, expr_binary(LEADS_TO));
         }
-    | 'A' '[' Expression 'U' Expression ']' {
-        CALL(@1, @6, expr_binary(A_UNTIL));
+	| 'A' '[' Expression 'U' Expression ']' {
+	    CALL(@1, @6, expr_binary(A_UNTIL));
         }
-    | 'A' '[' Expression 'W' Expression ']' {
-        CALL(@1, @6, expr_binary(A_WEAK_UNTIL));
+	| 'A' '[' Expression 'W' Expression ']' {
+	    CALL(@1, @6, expr_binary(A_WEAK_UNTIL));
         }
 ;
 
@@ -1731,40 +1734,80 @@ Features: {
     }
     | BracketExprList T_ARROW BracketExprList;
 
+
+/* Binary tree inspired by BracketExprList */
+BracketIntervalList:
+	'{' IntervalList '}' {
+		CALL(@1, @3, expr_nary(INTERVAL_LIST, $2));
+	}
+	;
+
+/* $$ is number of intervals in the list. */
+IntervalList:
+	/* empty */ { $$ = 0; }
+	| NonEmptyIntervalList
+	;
+
+NonEmptyIntervalList:
+	Interval { $$ = 1; }
+	| NonEmptyIntervalList ',' Interval { $$ = $1 + 1; }
+	;
+
+Interval:
+	T_ID '[' Expression ',' Expression ']' {
+		CALL(@1, @1, expr_identifier($1));
+		CALL(@1, @6, expr_discrete_interval());
+	}
+	| T_ID '[' Expression ',' Expression ']' ':' T_NAT {
+		CALL(@1, @1, expr_identifier($1));
+		CALL(@1, @8, expr_interval($8));
+	}
+	| T_ID '.' T_LOCATION {
+		CALL(@1, @3, expr_location($1));
+	}
+	;
+
+Partition:
+	| BracketIntervalList;
+
 AssignablePropperty:
     T_CONTROL ':' SubProperty Subjection {
         CALL(@1, @3, expr_unary(CONTROL));
         CALL(@1, @3, property());
     }
     | T_CONTROL_T T_MULT '(' Expression ',' Expression ')' ':' SubProperty {
-    CALL(@1, @9, expr_ternary(CONTROL_TOPT));
-    CALL(@1, @9, property());
+	CALL(@1, @9, expr_ternary(CONTROL_TOPT));
+	CALL(@1, @9, property());
     }
     | T_CONTROL_T T_MULT '(' Expression ')' ':' SubProperty {
-    CALL(@1, @7, expr_binary(CONTROL_TOPT_DEF1));
-    CALL(@1, @7, property());
+	CALL(@1, @7, expr_binary(CONTROL_TOPT_DEF1));
+	CALL(@1, @7, property());
     }
     | T_CONTROL_T T_MULT ':' SubProperty {
-    CALL(@1, @4, expr_unary(CONTROL_TOPT_DEF2));
-    CALL(@1, @4, property());
+	CALL(@1, @4, expr_unary(CONTROL_TOPT_DEF2));
+	CALL(@1, @4, property());
     }
     | T_EF T_CONTROL ':' SubProperty Subjection {
-    CALL(@1, @4, expr_unary(EF_CONTROL));
-    CALL(@1, @4, property());
+	CALL(@1, @4, expr_unary(EF_CONTROL));
+	CALL(@1, @4, property());
+    }
+    | T_ACONTROL ':' T_AG Expression Partition {
+    	CALL(@1, @4, expr_acontrol());
+    	CALL(@1, @4, property());
     }
     | BracketExprList T_CONTROL ':' SubProperty Subjection {
         CALL(@1, @4, expr_binary(PO_CONTROL));
-    CALL(@1, @4, property());
+	CALL(@1, @4, property());
     }
     | ExpQuantifier '(' Expression ')' '[' BoundType ']' Features ':' PathType Expression Subjection Imitation
     {
         CALL(@1, @12, expr_optimize_exp($1,  ParserBuilder::EXPRPRICE, $10));
-    CALL(@1, @9, property());
+	CALL(@1, @9, property());
     }
     | ExpPrQuantifier '[' BoundType ']' Features ':' PathType Expression Subjection Imitation
     {
         CALL(@1, @9, expr_optimize_exp($1, ParserBuilder::TIMEPRICE, $7));
-    CALL(@1, @6, property());
+	CALL(@1, @6, property());
     }
     | T_LOAD_STRAT Features '(' Expression ')' {
         CALL(@1, @5, expr_load_strategy());
@@ -1781,7 +1824,7 @@ PropertyExpr:
         CALL(@1, @1, property());
     }
     | T_PMAX Expression {  // Deprecated, comes from old uppaal-prob.
-    CALL(@1, @2, expr_unary(PMAX));
+	CALL(@1, @2, expr_unary(PMAX));
         CALL(@1, @2, property());
     }
     | AssignablePropperty
@@ -1792,47 +1835,47 @@ PropertyExpr:
         CALL(@1, @3, property());
     }
     | T_PROBA SMCBounds '(' PathType Expression ')' CmpGLE T_FLOATING Subjection {
-    CALL(@1, @9, expr_proba_qualitative($4, $7, $8));
+	CALL(@1, @9, expr_proba_qualitative($4, $7, $8));
         CALL(@1, @9, property());
     }
     | T_PROBA SMCBounds '(' PathType Expression ')' Subjection {
         CALL(@6, @6, expr_true()); // push a trivial stop-predicate (see next rule)
         CALL(@1, @7, expr_proba_quantitative($4));
-    CALL(@1, @7, property());
+	CALL(@1, @7, property());
     }
     | T_PROBA SMCBounds '(' Expression 'U' Expression ')' Subjection {
         CALL(@1, @8, expr_proba_quantitative(DIAMOND));
-    CALL(@1, @8, property());
+	CALL(@1, @8, property());
     }
     | T_PROBA SMCBounds '(' PathType Expression ')' T_GEQ
       T_PROBA SMCBounds '(' PathType Expression ')' Subjection {
-    CALL(@1, @14, expr_proba_compare($4, $11));
-    CALL(@1, @14, property());
+	CALL(@1, @14, expr_proba_compare($4, $11));
+	CALL(@1, @14, property());
     }
     | T_PROBA SMCBounds '(' PathType Expression ')' T_SUBJECT SubjectionList T_GEQ
       T_PROBA SMCBounds '(' PathType Expression ')' Subjection {
-    CALL(@1, @16, expr_proba_compare($4, $13));
-    CALL(@1, @16, property());
+	CALL(@1, @16, expr_proba_compare($4, $13));
+	CALL(@1, @16, property());
     }//T_SUBJECT SubjectionList
     | T_SIMULATE SMCBounds '{' NonEmptyExpressionList '}' Subjection {
         CALL(@1, @6, expr_simulate($4));
         CALL(@1, @6, property());
     }
     | T_SIMULATE SMCBounds '{' NonEmptyExpressionList '}' ':' Expression Subjection {
-    CALL(@1, @8, expr_simulate($4, true));
-    CALL(@1, @8, property());
+	CALL(@1, @8, expr_simulate($4, true));
+	CALL(@1, @8, property());
     }
     | T_SIMULATE SMCBounds '{' NonEmptyExpressionList '}' ':' T_NAT ':' Expression Subjection {
         CALL(@1, @10, expr_simulate($4, true, $7));
-    CALL(@1, @10, property());
+	CALL(@1, @10, property());
     }
     | 'E' SMCBounds '(' Id ':' Expression ')' Subjection {
         CALL(@1, @8, expr_proba_expected($4));
-    CALL(@1, @8, property());
+	CALL(@1, @8, property());
     }
     | T_PROBA Expression Subjection {
-    CALL(@1, @3, expr_MITL_formula());
-    CALL(@1, @3, property());
+	CALL(@1, @3, expr_MITL_formula());
+	CALL(@1, @3, property());
     }
     | T_SAVE_STRAT '(' Expression ',' Id ')' {
         CALL(@1, @6, subjection($5));
@@ -1843,7 +1886,7 @@ PropertyExpr:
 
 MITLExpression :
     '(' Expression 'U' '['  T_NAT ',' T_NAT ']' Expression ')' {
-        CALL(@1,@10, expr_MITL_until($5,$7));
+	    CALL(@1,@10, expr_MITL_until($5,$7));
     }
     | '(' Expression 'R' '['  T_NAT ',' T_NAT ']' Expression ')' {
         CALL(@1,@10, expr_MITL_release($5,$7));
@@ -1852,7 +1895,7 @@ MITLExpression :
         CALL(@1,@4, expr_MITL_next());
     }
     | '(' T_DIAMOND '[' T_NAT ',' T_NAT ']' Expression ')' {
-        CALL(@1,@4, expr_MITL_diamond($4,$6));
+	    CALL(@1,@4, expr_MITL_diamond($4,$6));
     }
     | '(' T_BOX '[' T_NAT ',' T_NAT ']' Expression ')' {
         CALL(@1,@4, expr_MITL_box($4,$6));
@@ -1861,10 +1904,10 @@ MITLExpression :
 
 SMCBounds:
     '[' BoundType ']' {
-    CALL(@1, @1, expr_nat(-1));
+	CALL(@1, @1, expr_nat(-1));
     }
     | '[' BoundType ';' T_NAT ']' {
-    CALL(@1, @3, expr_nat($4));
+	CALL(@1, @3, expr_nat($4));
     };
 
 BoundType:
@@ -1879,21 +1922,21 @@ CmpGLE:
         ;
 
 PathType:
-        T_BOX { $$ = BOX; }
-        | T_DIAMOND { $$ = DIAMOND; }
-        ;
+	    T_BOX { $$ = BOX; }
+	    | T_DIAMOND { $$ = DIAMOND; }
+	    ;
 
 BracketExprList:
-    '{' ExpressionList '}' {
-        CALL(@1, @3, expr_nary(LIST,$2));
-    };
+	'{' ExpressionList '}' {
+	    CALL(@1, @3, expr_nary(LIST,$2));
+	};
 
 /* There is an ExprList but it's not a list, rather
  * a binary tree built with commas.
  */
 
 ExpressionList:
-    /* nothing */ { $$ = 0; }
+	/* nothing */ { $$ = 0; }
         | NonEmptyExpressionList
         ;
 
@@ -1904,24 +1947,24 @@ NonEmptyExpressionList:
 
 SupPrefix:
         T_SUP ':' {
-        CALL(@1, @2, expr_true());
-    }
-    | T_SUP '{' Expression '}' ':'
-    ;
+	    CALL(@1, @2, expr_true());
+	}
+	| T_SUP '{' Expression '}' ':'
+	;
 
 InfPrefix:
-    T_INF ':' {
-        CALL(@1, @2, expr_true());
-    }
-    | T_INF '{' Expression '}' ':'
-    ;
+	T_INF ':' {
+	    CALL(@1, @2, expr_true());
+	}
+	| T_INF '{' Expression '}' ':'
+	;
 
 BoundsPrefix:
-    T_BOUNDS ':' {
-        CALL(@1, @2, expr_true());
-    }
-    | T_BOUNDS '{' Expression '}' ':'
-    ;
+	T_BOUNDS ':' {
+	    CALL(@1, @2, expr_true());
+	}
+	| T_BOUNDS '{' Expression '}' ':'
+	;
 
             
 StrategyAssignment: 
@@ -1930,29 +1973,28 @@ StrategyAssignment:
         };
 
 Property:
-    /* empty */
+	/* empty */
         | StrategyAssignment
         | PropertyExpr
-    | SupPrefix NonEmptyExpressionList Subjection {
-        CALL(@1, @2, expr_nary(LIST,$2));
-        CALL(@1, @2, expr_binary(SUP_VAR));
-        CALL(@1, @2, property());
-        }
-    | InfPrefix NonEmptyExpressionList Subjection {
-        CALL(@1, @2, expr_nary(LIST,$2));
-        CALL(@1, @2, expr_binary(INF_VAR));
-        CALL(@1, @2, property());
-    }
-    | BoundsPrefix NonEmptyExpressionList Subjection {
-        CALL(@1, @2, expr_nary(LIST,$2));
-        CALL(@1, @2, expr_binary(BOUNDS_VAR));
-        CALL(@1, @2, property());
-    };
+	| SupPrefix NonEmptyExpressionList Subjection {
+	    CALL(@1, @2, expr_nary(LIST,$2));
+	    CALL(@1, @2, expr_binary(SUP_VAR));
+	    CALL(@1, @2, property());
+        }
+	| InfPrefix NonEmptyExpressionList Subjection {
+	    CALL(@1, @2, expr_nary(LIST,$2));
+	    CALL(@1, @2, expr_binary(INF_VAR));
+	    CALL(@1, @2, property());
+	}
+	| BoundsPrefix NonEmptyExpressionList Subjection {
+	    CALL(@1, @2, expr_nary(LIST,$2));
+	    CALL(@1, @2, expr_binary(BOUNDS_VAR));
+	    CALL(@1, @2, property());
+	};
 
 %%
 
 #include "lexer.cc"
-
 //NOLINTEND
 
 static void utap_error(const char* msg)
@@ -1987,8 +2029,8 @@ static void setStartToken(XTAPart part, bool newxta)
         syntax_token = newxta ? T_NEW_INVARIANT : T_OLD_INVARIANT;
         break;
     case S_EXPONENTIAL_RATE:
-    syntax_token = T_EXPONENTIAL_RATE;
-    break;
+	syntax_token = T_EXPONENTIAL_RATE;
+	break;
     case S_SELECT:
         syntax_token = T_NEW_SELECT;
         break;
diff --git a/src/property.cpp b/src/property.cpp
index 5e3d9bf..c74b804 100644
--- a/src/property.cpp
+++ b/src/property.cpp
@@ -226,6 +226,7 @@ void PropertyBuilder::typeProperty(Expression expr)  // NOLINT
         prob = true;
         break;
     case MITL_FORMULA: properties.back().type = quant_t::Mitl; break;
+    case ACONTROL: properties.back().type = quant_t::acontrol; break;
     default: throw UTAP::TypeException("$Invalid_property_type"); prob = true;
     }
 
diff --git a/src/statement.cpp b/src/statement.cpp
index ed6fa19..3ebdf5f 100644
--- a/src/statement.cpp
+++ b/src/statement.cpp
@@ -22,8 +22,8 @@
 
 #include "utap/statement.hpp"
 
-#include <iostream>
 #include <sstream>
+
 #include <cassert>
 
 using namespace UTAP;
diff --git a/src/type.cpp b/src/type.cpp
index 32e4728..f1e462d 100644
--- a/src/type.cpp
+++ b/src/type.cpp
@@ -135,6 +135,9 @@ bool Type::is_prefix() const
     case Constants::TYPEDEF:
     case Constants::LABEL:
     case Constants::RATE:
+    case Constants::INTERVAL:
+    case Constants::DISCRETE_INTERVAL:
+    case Constants::INTERVAL_LIST:
     case Constants::INSTANCE_LINE:  // LSC
     case Constants::MESSAGE:        // LSC
     case Constants::CONDITION:      // LSC
diff --git a/test/document_fixture.h b/test/document_fixture.h
index 585d7eb..595c8cb 100644
--- a/test/document_fixture.h
+++ b/test/document_fixture.h
@@ -31,6 +31,7 @@
 #include <memory>
 #include <stdexcept>
 #include <string>
+
 #include <cstring>
 
 /// Checks text containment in unit testing
diff --git a/test/pretty.cpp b/test/pretty.cpp
index ba4279c..102ae91 100644
--- a/test/pretty.cpp
+++ b/test/pretty.cpp
@@ -24,6 +24,7 @@
 #include <filesystem>
 #include <iostream>
 #include <string>
+
 #include <cstdio>
 #include <cstdlib>
 
diff --git a/test/prettyprint_test.cpp b/test/prettyprint_test.cpp
index 956fe0c..21c709e 100644
--- a/test/prettyprint_test.cpp
+++ b/test/prettyprint_test.cpp
@@ -362,4 +362,79 @@ TEST_CASE("Post incrementing an identifier should not require parenthesis")
     CHECK(expr.str() == "foo++");
 }
 
+TEST_CASE("acontrol query")
+{
+    auto f = document_fixture{}
+                 .add_default_process()
+                 .add_system_decl("bool myBool;")
+                 .add_system_decl("int myInt;")
+                 .add_system_decl("int[1, 10] myConstrainedInt;")
+                 .add_system_decl("double myDouble;")
+                 .add_system_decl("clock myClock;")
+                 .add_system_decl("chan MyChannel;")
+                 .build_query_fixture();
+
+    const auto foo = f.get_errors();
+    REQUIRE(f.get_errors().empty());
+
+    SUBCASE("Basics")
+    {
+        // NB: Whitespace is significant since it must match the pretty-printer.
+        const auto* query_string = "acontrol: A[] myDouble < 1 "
+                                   "{ "
+                                   "myInt[2 + 2, 10], "
+                                   "myConstrainedInt[1, 2 * 5], "
+                                   "myDouble[M_PI, 2.1 * 100]:100 "
+                                   "}";
+
+        const auto query1 = f.parse_query(query_string).intermediate;
+
+        REQUIRE(query1.get_kind() == UTAP::Constants::ACONTROL);
+        CHECK(query_string == query1.str());
+    }
+
+    SUBCASE("Support of locations")
+    {
+        const std::string query_string =
+            "acontrol: A[] Process.location != Process._id0 { Process.location, myClock[2, 10]:100 }";
+
+        auto query = f.parse_query(query_string.data()).intermediate;
+
+        REQUIRE(query.get_kind() == UTAP::Constants::ACONTROL);
+        CHECK(query_string == query.str());
+    }
+
+    SUBCASE("Mixing some clocks in there")
+    {
+        const std::string query_string = "acontrol: A[] myClock < 10 && myClock > 0 { myClock[-1, 10]:100 }";
+
+        auto query1 = f.parse_query(query_string.data()).intermediate;
+
+        REQUIRE(query1.get_kind() == UTAP::Constants::ACONTROL);
+        CHECK(query_string == query1.str());
+    }
+
+    SUBCASE("Invalid condition to enforce")
+    {
+        const auto query_string = "acontrol: A[] (-2.2) { }";
+        CHECK_THROWS_WITH(f.parse_query(query_string), "$Unknown_type_of_the_expression");
+
+        const auto query_string2 = "acontrol: A[] myChannel { }";
+        CHECK_THROWS_WITH(f.parse_query(query_string2), "$Unknown_type_of_the_expression");
+    }
+
+    SUBCASE("Invalid number of divisions")
+    {
+        const auto query_string = "acontrol: A[] myDouble < 1 {  myDouble[M_PI, 21 * 100]:1.5 }";
+        CHECK_THROWS_WITH(f.parse_query(query_string), "$syntax_error: $unexpected T_FLOATING, $expecting T_NAT");
+
+        // Don't know why it still says "T_FLOATING" here.
+        const auto query_string2 = "acontrol: A[] myDouble < 1 { myDouble[M_PI, 21 * 100]:myChannel }";
+        CHECK_THROWS_WITH(f.parse_query(query_string2), "$syntax_error: $unexpected T_FLOATING, $expecting T_NAT");
+
+        const auto query_string3 = "acontrol: A[] myDouble < 1 { myDouble[M_PI, 21 * 100]:myClock }";
+        CHECK_THROWS_WITH(f.parse_query(query_string3), "$syntax_error: $unexpected T_FLOATING, $expecting T_NAT");
+    }
+}
+
 TEST_SUITE_END();