Coshy

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;

include/utap/DocumentBuilder.hpp

@@ -26,6 +26,7 @@
 #include "utap/utap.hpp"
 
 #include <vector>
+
 #include <cinttypes>
 
 namespace UTAP {

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;

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);

include/utap/StatementBuilder.hpp

@@ -27,6 +27,7 @@
 
 #include <filesystem>
 #include <vector>
+
 #include <cinttypes>
 
 namespace UTAP {

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;

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,

include/utap/position.hpp

@@ -28,6 +28,7 @@
 #include <memory>
 #include <string>
 #include <vector>
+
 #include <cstdint>
 
 namespace UTAP {

include/utap/property.hpp

@@ -109,7 +109,10 @@ enum class quant_t {
     PMax,
 
     /* LSC scenario property */
-    scenario
+    scenario,
+
+    /* HYPA: acontrol: A[] ... {} -> {} */
+    acontrol,
 };
 
 /** property status */

include/utap/statement.hpp

@@ -29,6 +29,7 @@
 #include <memory>
 #include <string>
 #include <utility>
+
 #include <cstdint>
 
 namespace UTAP {

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 {

include/utap/type.hpp

@@ -29,6 +29,7 @@
 #include <memory>  // shared_ptr
 #include <optional>
 #include <string>
+
 #include <cstdint>
 
 namespace UTAP {

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; }

src/DocumentBuilder.cpp

@@ -24,8 +24,8 @@
 #include "print.hpp"
 
 #include <sstream>
-#include <stdexcept>
 #include <vector>
+
 #include <cassert>
 
 using namespace UTAP;

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())

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;
     }
 }

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)
 {}