Add Timed Alternating-Time Temporal Logic queries

CMakeLists.txt

@@ -73,4 +73,4 @@ install(TARGETS UTAP EXPORT UTAPConfig LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDI
 install(EXPORT UTAPConfig DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/UTAP/)
 install(FILES ${CMAKE_CURRENT_BINARY_DIR}/UTAPConfigVersion.cmake DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/UTAP )
 
-# set(CMAKE_CXX_STANDARD_LIBRARIES "-static -lwsock32 -lws2_32 -lz -lmcfgthread ${CMAKE_CXX_STANDARD_LIBRARIES}")
+# set(CMAKE_CXX_STANDARD_LIBRARIES "-static -lwsock32 -lws2_32 -lz -lmcfgthread ${CMAKE_CXX_STANDARD_LIBRARIES}")

include/utap/AbstractBuilder.hpp

@@ -119,7 +119,7 @@ class AbstractBuilder : public ParserBuilder
     void proc_location_urgent(const char* name) override;                          // mark previously decl. state
     void proc_location_init(const char* name) override;                            // mark previously decl. state
     void proc_branchpoint(const char* name) override;
-    void proc_edge_begin(const char* from, const char* to, const bool control, const char* actname) override;
+    void proc_edge_begin(const char* from, const char* to, const bool control, const char* color, const char* actname) override;
     void proc_edge_end(const char* from, const char* to) override;
     // 1 epxr,1sync,1expr
     void proc_select(const char* id) override;
@@ -219,6 +219,8 @@ class AbstractBuilder : public ParserBuilder
     void expr_load_strategy() override;
     void expr_save_strategy(const char* strategy_name) override;
 
+    void expr_atl(int, Constants::kind_t) override;
+
     // MITL
     void expr_MITL_formula() override;
     void expr_MITL_until(int, int) override;

include/utap/DocumentBuilder.hpp

@@ -106,6 +106,8 @@ class DocumentBuilder : public StatementBuilder
 
     void addSelectSymbolToFrame(const std::string& name, frame_t&, position_t pos);
 
+    uint32_t parse_hex_color(const char* color);
+
 public:
     DocumentBuilder(Document&, std::vector<std::filesystem::path> paths = {});
 
@@ -124,7 +126,7 @@ class DocumentBuilder : public StatementBuilder
     void proc_location_urgent(const char* name) override;
     void proc_location_init(const char* name) override;
     void proc_branchpoint(const char* name) override;
-    void proc_edge_begin(const char* from, const char* to, const bool control, const char* actname) override;
+    void proc_edge_begin(const char* from, const char* to, const bool control, const char* color, const char* actname) override;
     void proc_edge_end(const char* from = 0, const char* to = 0) override;
     void proc_select(const char* id) override;
     void proc_guard() override;

include/utap/ExpressionBuilder.hpp

@@ -195,6 +195,8 @@ class ExpressionBuilder : public AbstractBuilder
     void expr_save_strategy(const char* strategy_name) override;
     void expr_load_strategy() override;
 
+    void expr_atl(int, Constants::kind_t) override;
+
     void expr_simulate(int nb_of_exprs, bool filter_prop = false, int max_accepting_runs = 0) override;
     void expr_MITL_formula() override;
     void expr_MITL_until(int, int) override;

include/utap/builder.h

@@ -247,7 +247,7 @@ class ParserBuilder
     virtual void proc_location_commit(const char* name) = 0;                          // mark previously decl. state
     virtual void proc_location_urgent(const char* name) = 0;                          // mark previously decl. state
     virtual void proc_location_init(const char* name) = 0;                            // mark previously decl. state
-    virtual void proc_edge_begin(const char* from, const char* to, const bool control, const char* actname = "") = 0;
+    virtual void proc_edge_begin(const char* from, const char* to, const bool control, const char* color = "#000000", const char* actname = "") = 0;
     virtual void proc_edge_end(const char* from, const char* to) = 0;
     virtual void proc_select(const char* id) = 0;                   // 1 expr
     virtual void proc_guard() = 0;                                  // 1 expr
@@ -363,6 +363,8 @@ class ParserBuilder
     virtual void expr_load_strategy() = 0;
     virtual void expr_save_strategy(const char* strategy_name) = 0;
 
+    virtual void expr_atl(int, Constants::kind_t) = 0;
+
     // MITL Extensions
     virtual void expr_MITL_formula() = 0;
     virtual void expr_MITL_until(int, int) = 0;

include/utap/common.h

@@ -44,6 +44,7 @@ enum kind_t {
     MAX,
     RATE,
     FRACTION,
+    FREEZE,
 
     /********************************************************
      * Relational operators
@@ -143,6 +144,18 @@ enum kind_t {
     ASS_LSHIFT,
     ASS_RSHIFT,
 
+    /*******************************************************
+     * ATL Quantifiers
+     */
+    ATL_ENFORCE_UNTIL,
+    ATL_DESPITE_UNTIL,
+    ATL_ENFORCE_F,
+    ATL_DESPITE_F,
+    ATL_ENFORCE_G,
+    ATL_DESPITE_G,
+    ATL_ENFORCE_NEXT,
+    ATL_DESPITE_NEXT,
+
     /*******************************************************
      * CTL Quantifiers
      */

include/utap/document.h

@@ -107,6 +107,7 @@ struct edge_t : stringify_t<edge_t>
 {
     int nr;       /**< Placement in input file */
     bool control; /**< Controllable (true/false) */
+    uint32_t color;
     std::string actname;
     location_t* src{nullptr};          /**< Pointer to source location */
     branchpoint_t* srcb{nullptr};      /**< Pointer to source branchpoint */

include/utap/expression.h

@@ -102,6 +102,9 @@ class expression_t
     /** Returns the number of subexpression. */
     size_t get_size() const;
 
+    /** Returns the number of player colors in this expression. */
+    size_t get_player_count() const;
+
     /** Returns the position of this expression. */
     const position_t& get_position() const;
 

include/utap/prettyprinter.h

@@ -117,7 +117,7 @@ class PrettyPrinter : public AbstractBuilder
     void proc_sync(Constants::synchronisation_t type) override;
     void proc_update() override;
     void proc_edge_begin(const char* source, const char* target, const bool control);
-    void proc_edge_begin(const char* source, const char* target, const bool control, const char* actname) override;
+    void proc_edge_begin(const char* source, const char* target, const bool control, const char* color, const char* actname) override;
     void proc_edge_end(const char* source, const char* target) override;
     void proc_end() override;
     void expr_identifier(const char* id) override;

include/utap/property.h

@@ -58,6 +58,9 @@ enum class quant_t {
     probaSimulateReach,  // simulate [...] { ... } : n : p
     Mitl,
 
+    /* ATL quantifiers: */
+    Atl,
+
     /* TIGA quantifiers for controller synthesis:
      * - A[ p U q ] : AUntil
      * - A[ p W q ] : AWeakUntil
@@ -241,7 +244,7 @@ class PropertyBuilder : public std::enable_shared_from_this<PropertyBuilder>, pu
     bool isSMC(UTAP::expression_t* expr = nullptr);
 };
 
-class TigaPropertyBuilder final : public PropertyBuilder
+class TigaPropertyBuilder : public PropertyBuilder
 {
 protected:
     std::map<std::string, PropInfo*> declarations{};
@@ -266,6 +269,15 @@ class TigaPropertyBuilder final : public PropertyBuilder
     */
 };
 
+class AtlPropertyBuilder final : public TigaPropertyBuilder
+{
+public:
+    AtlPropertyBuilder(const UTAP::Document& doc) : TigaPropertyBuilder{doc} {}
+
+protected:
+    void typeProperty(UTAP::expression_t expression) override;
+};
+
 }  // namespace UTAP
 
 #endif /* VERIFIER_PROPERTY */

src/DocumentBuilder.cpp

@@ -231,7 +231,7 @@ void DocumentBuilder::proc_location_init(const char* name)
     }
 }
 
-void DocumentBuilder::proc_edge_begin(const char* from, const char* to, const bool control, const char* actname)
+void DocumentBuilder::proc_edge_begin(const char* from, const char* to, const bool control, const char* color, const char* actname)
 {
     symbol_t fid, tid;
 
@@ -243,6 +243,7 @@ void DocumentBuilder::proc_edge_begin(const char* from, const char* to, const bo
         push_frame(frame_t::create(frames.top()));  // dummy frame for upcoming popFrame
     } else {
         currentEdge = &currentTemplate->add_edge(fid, tid, control, actname);
+        currentEdge->color = parse_hex_color(color);
         currentEdge->guard = make_constant(1);
         currentEdge->assign = make_constant(1);
         // default "probability" weight is 1.
@@ -754,3 +755,8 @@ void DocumentBuilder::model_option(const char* key, const char* value)
     }
     document.get_options().emplace_back(key, value == nullptr ? "" : value);
 }
+
+uint32_t DocumentBuilder::parse_hex_color(const char* color)
+{
+    return std::stoul(color + 1 /* Skip the '#' */, nullptr, 16);
+}

src/ExpressionBuilder.cpp

@@ -810,6 +810,24 @@ void ExpressionBuilder::expr_proba_expected(const char* aggregatingOp)
     fragments.push(expression_t::create_nary(PROBA_EXP, std::move(args), position));
 }
 
+void ExpressionBuilder::expr_atl(int nbPlayers, Constants::kind_t kind)
+{
+    int nbSubExprs = (kind == ATL_ENFORCE_UNTIL || kind == ATL_DESPITE_UNTIL) ? 2 : 1;
+    std::vector<expression_t> parts;
+    parts.reserve(nbPlayers + nbSubExprs);
+
+    for (int i = 0; i < nbPlayers; ++i) {
+        parts.push_back(fragments[nbPlayers + nbSubExprs - 1 - i]);
+    }
+
+    for (int i = 0; i < nbSubExprs; ++i) {
+        parts.push_back(fragments[nbSubExprs - 1 - i]);
+    }
+
+    fragments.pop(parts.size());
+    fragments.push(expression_t::create_nary(kind, parts, position));
+}
+
 void ExpressionBuilder::expr_simulate(int nbExpr, bool hasReach, int numberOfAcceptingRuns)
 {
     // Stack:

src/abstractbuilder.cpp

@@ -109,7 +109,7 @@ void AbstractBuilder::proc_location_commit(const char* name) { UNSUPPORTED; }
 void AbstractBuilder::proc_location_urgent(const char* name) { UNSUPPORTED; }
 void AbstractBuilder::proc_location_init(const char* name) { UNSUPPORTED; }
 void AbstractBuilder::proc_branchpoint(const char* name) { UNSUPPORTED; }
-void AbstractBuilder::proc_edge_begin(const char* from, const char* to, const bool control, const char* actname)
+void AbstractBuilder::proc_edge_begin(const char* from, const char* to, const bool control, const char* color, const char* actname)
 {
     UNSUPPORTED;
 }
@@ -271,6 +271,8 @@ void AbstractBuilder::expr_foreach_dynamic_begin(const char*, const char*) { UNS
 void AbstractBuilder::expr_foreach_dynamic_end(const char* name) { UNSUPPORTED; }
 void AbstractBuilder::expr_dynamic_process_expr(const char*) { UNSUPPORTED; }
 
+void AbstractBuilder::expr_atl(int, Constants::kind_t) { UNSUPPORTED; }
+
 void AbstractBuilder::expr_MITL_forall_dynamic_begin(const char*, const char*) { UNSUPPORTED; }
 void AbstractBuilder::expr_MITL_forall_dynamic_end(const char* name) { UNSUPPORTED; }
 void AbstractBuilder::expr_MITL_exists_dynamic_begin(const char*, const char*) { UNSUPPORTED; }

src/document.cpp

@@ -315,6 +315,7 @@ edge_t& template_t::add_edge(symbol_t src, symbol_t dst, bool control, string ac
     }
 
     edge.control = control;
+    edge.color = 0x000000;
     edge.actname = std::move(actname);
     edge.nr = nr;
     return edge;

src/expression.cpp

@@ -327,6 +327,7 @@ size_t expression_t::get_size() const
     case BIT_XOR:
     case BIT_LSHIFT:
     case BIT_RSHIFT:
+    case FREEZE:
     case AND:
     case OR:
     case XOR:
@@ -444,6 +445,15 @@ size_t expression_t::get_size() const
     case SIMULATEREACH:
     case SPAWN: return std::get<int32_t>(data->value);
 
+    case ATL_ENFORCE_UNTIL:
+    case ATL_DESPITE_UNTIL: assert(data->sub.size() >= 2); return std::get<int32_t>(data->value);
+    case ATL_ENFORCE_F:
+    case ATL_DESPITE_F:
+    case ATL_ENFORCE_G:
+    case ATL_DESPITE_G:
+    case ATL_ENFORCE_NEXT:
+    case ATL_DESPITE_NEXT: assert(data->sub.size() >= 1); return std::get<int32_t>(data->value);
+
     case EG:
     case AG:
     case EF:
@@ -496,6 +506,27 @@ size_t expression_t::get_size() const
     }
 }
 
+size_t expression_t::get_player_count() const
+{
+    assert(data);
+    switch (data->kind) {
+    case ATL_ENFORCE_UNTIL:
+    case ATL_DESPITE_UNTIL:
+        assert(get_size() >= 2);
+        return get_size() - 2;
+    case ATL_ENFORCE_F:
+    case ATL_DESPITE_F:
+    case ATL_ENFORCE_G:
+    case ATL_DESPITE_G:
+    case ATL_ENFORCE_NEXT:
+    case ATL_DESPITE_NEXT:
+        assert(get_size() >= 1);
+        return get_size() - 1;
+    default:
+        return 0;
+    }
+}
+
 type_t expression_t::get_type() const
 {
     assert(data);
@@ -837,10 +868,18 @@ int expression_t::get_precedence(kind_t kind)
     case EXISTS:
     case SUM: return 8;
 
+    case ATL_ENFORCE_UNTIL:
+    case ATL_DESPITE_UNTIL:
     case A_UNTIL:
     case A_WEAK_UNTIL:
     case A_BUCHI: return 7;
 
+    case ATL_ENFORCE_F:
+    case ATL_DESPITE_F:
+    case ATL_ENFORCE_G:
+    case ATL_DESPITE_G:
+    case ATL_ENFORCE_NEXT:
+    case ATL_DESPITE_NEXT:
     case EF:
     case EG:
     case AF:
@@ -1425,6 +1464,70 @@ std::ostream& expression_t::print(std::ostream& os, bool old) const
 
     case RATE: get(0).print(os, old) << '\''; break;
 
+    case FREEZE: os << get(0) << " @ " << get(1); break;
+
+    case ATL_ENFORCE_UNTIL:
+    case ATL_ENFORCE_F:
+    case ATL_ENFORCE_G:
+    case ATL_ENFORCE_NEXT: {
+        os << "<<";
+        size_t n = get_player_count();
+        for (int i = 0; i < n; ++i) {
+            get(i).print(os << "#" << std::setfill('0') << std::setw(6) << std::hex, old);
+            if (i < n - 1) os << ", ";
+        }
+        os << std::dec << ">> ";
+        switch (data->kind) {
+        case Constants::ATL_ENFORCE_UNTIL:
+            get(n).print(os << "[", old) << " U ";
+            get(n + 1).print(os, old) << "] ";
+            break;
+        case Constants::ATL_ENFORCE_F:
+            get(n).print(os << "<> ");
+            break;
+        case Constants::ATL_ENFORCE_G:
+            get(n).print(os << "[] ");
+            break;
+        case Constants::ATL_ENFORCE_NEXT:
+            get(n).print(os << "X ");
+            break;
+        default:
+            assert(false);
+        }
+        break;
+    }
+
+    case ATL_DESPITE_UNTIL:
+    case ATL_DESPITE_F:
+    case ATL_DESPITE_G:
+    case ATL_DESPITE_NEXT: {
+        os << "[[";
+        size_t n = get_player_count();
+        for (int i = 0; i < n; ++i) {
+            get(i).print(os << "#" << std::setfill('0') << std::setw(6) << std::hex, old);
+            if (i < n - 1) os << ", ";
+        }
+        os << "]] ";
+        switch (data->kind) {
+        case Constants::ATL_DESPITE_UNTIL:
+            get(n).print(os << "[", old) << " U ";
+            get(n + 1).print(os, old) << "] ";
+            break;
+        case Constants::ATL_DESPITE_F:
+            get(n).print(os << "<> ");
+            break;
+        case Constants::ATL_DESPITE_G:
+            get(n).print(os << "[] ");
+            break;
+        case Constants::ATL_DESPITE_NEXT:
+            get(n).print(os << "X ");
+            break;
+        default:
+            assert(false);
+        }
+        break;
+    }
+
     case EF:
         os << "E<> ";
         get(0).print(os, old);

src/lexer.l

@@ -150,15 +150,17 @@ idchr        [a-zA-Z0-9_$#]
 ">"        	{ return T_GT; }
 "=="        	{ return T_EQ; }
 "!="        	{ return T_NEQ; }
-
 "++"            { return T_INCREMENT; }
 "--"            { return T_DECREMENT; }
 
+"@"             { return T_FREEZE; }
+
 "A"             { return 'A'; }
 "U"             { return 'U'; }
 "R"             { return 'R'; }
 "W"             { return 'W'; }
 "E"             { return 'E'; }
+"X"             { return 'X'; }
 
 "A<>"           { return T_AF; }
 "A[]"           { return T_AG; }