From d78c0fea054111c6c4c08b2e6e96e29e2256b2fa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Mon, 23 Sep 2024 13:52:46 +0200 Subject: [PATCH 01/16] Test --- src/document.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/document.cpp b/src/document.cpp index 6c048bac..9830c951 100644 --- a/src/document.cpp +++ b/src/document.cpp @@ -758,6 +758,7 @@ std::ostream& chan_priority_t::print(std::ostream& os) const Document::Document() { + std::cout << "TEST GETLIBS TEST %%%%" << std::endl; global.frame = frame_t::create(); #ifdef ENABLE_CORA addVariable(&global, type_t::create_primitive(COST), "cost", expression_t()); From 12ca343205d3aaedfc31a20cfe0aea854644c7bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Wed, 23 Oct 2024 11:28:42 +0200 Subject: [PATCH 02/16] Super basic ATL expression --- include/utap/common.h | 6 ++++++ src/document.cpp | 1 - src/expression.cpp | 3 +++ src/lexer.l | 2 ++ src/parser.y | 14 +++++++++++++- test/test_parser.cpp | 22 ++++++++++++++++++++++ 6 files changed, 46 insertions(+), 2 deletions(-) diff --git a/include/utap/common.h b/include/utap/common.h index 1341e605..74b8be64 100644 --- a/include/utap/common.h +++ b/include/utap/common.h @@ -143,6 +143,12 @@ enum kind_t { ASS_LSHIFT, ASS_RSHIFT, + /******************************************************* + * T-ATL Quantifiers + */ + ATL_ENFORCE_F, + ATL_DESPITE_F, + /******************************************************* * CTL Quantifiers */ diff --git a/src/document.cpp b/src/document.cpp index 9830c951..6c048bac 100644 --- a/src/document.cpp +++ b/src/document.cpp @@ -758,7 +758,6 @@ std::ostream& chan_priority_t::print(std::ostream& os) const Document::Document() { - std::cout << "TEST GETLIBS TEST %%%%" << std::endl; global.frame = frame_t::create(); #ifdef ENABLE_CORA addVariable(&global, type_t::create_primitive(COST), "cost", expression_t()); diff --git a/src/expression.cpp b/src/expression.cpp index af2e7499..8281fb4a 100644 --- a/src/expression.cpp +++ b/src/expression.cpp @@ -444,6 +444,9 @@ size_t expression_t::get_size() const case SIMULATEREACH: case SPAWN: return std::get(data->value); + case ATL_ENFORCE_F: + case ATL_DESPITE_F: assert(data->sub.size() == 1); return 1; + case EG: case AG: case EF: diff --git a/src/lexer.l b/src/lexer.l index 90c7dc79..29d52dab 100644 --- a/src/lexer.l +++ b/src/lexer.l @@ -129,6 +129,8 @@ idchr [a-zA-Z0-9_$#] "&&" { return T_BOOL_AND; } "/\\" { return T_MITL_AND; } "\\/" { return T_MITL_OR; } +"[[" { return T_LBRBR; } +"]]" { return T_RBRBR; } "<=" { return T_LEQ; } ">=" { return T_GEQ; } diff --git a/src/parser.y b/src/parser.y index 265b992e..48cffff3 100644 --- a/src/parser.y +++ b/src/parser.y @@ -283,6 +283,9 @@ const char* utap_msg(const char *msg) %token T_DYNAMIC T_HYBRID %token T_SPAWN T_EXIT T_NUMOF +/* T-ATL */ +%token T_LBRBR T_RBRBR + %type ExpQuantifier ExpPrQuantifier %type PathType %type ArgList FieldDeclList FieldDeclIdList FieldDecl @@ -1733,8 +1736,17 @@ Query: BoolOrKWAnd: T_KW_AND | T_BOOL_AND; +SubPropertyOrExpression: + SubProperty | Expression; + SubProperty: - T_AF Expression { + T_LSHIFT 'A' T_RSHIFT T_DIAMOND SubPropertyOrExpression { + CALL(@1, @5, expr_unary(ATL_ENFORCE_F)); + } + | T_LBRBR 'A' T_RBRBR T_DIAMOND SubPropertyOrExpression { + CALL(@1, @5, expr_unary(ATL_DESPITE_F)); + } + | T_AF Expression { CALL(@1, @2, expr_unary(AF)); } | T_AG '(' Expression BoolOrKWAnd T_AF Expression ')' { diff --git a/test/test_parser.cpp b/test/test_parser.cpp index 9d6a208e..dc961821 100644 --- a/test/test_parser.cpp +++ b/test/test_parser.cpp @@ -536,4 +536,26 @@ TEST_CASE("Increment with multiple array subscripting and dot accessing") .parse(); CHECK_MESSAGE(doc->get_errors().size() == 0, doc->get_errors().at(0).msg); +} + +TEST_CASE("T-ALT properties") +{ + auto doc = std::make_unique(); + auto builder = std::make_unique(*doc); + SUBCASE("Basic EnforceF property") + { + auto res = parseProperty("<< A >> <> true", builder.get()); + REQUIRE(res == 0); + auto expr = builder->getQuery(); + CHECK(expr.get_size() == 1); + CHECK(expr.get_kind() == UTAP::Constants::ATL_ENFORCE_F); + } + SUBCASE("Basic DespiteF property") + { + auto res = parseProperty("[[ A ]] <> true", builder.get()); + REQUIRE(res == 0); + auto expr = builder->getQuery(); + CHECK(expr.get_size() == 1); + CHECK(expr.get_kind() == UTAP::Constants::ATL_DESPITE_F); + } } \ No newline at end of file From 1469a597ec183a842662e870c7ebfa2f811f735b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Wed, 23 Oct 2024 15:54:40 +0200 Subject: [PATCH 03/16] Add remain ATL formula except coalition part --- include/utap/common.h | 8 ++++- include/utap/property.h | 14 ++++++++- src/expression.cpp | 8 ++++- src/lexer.l | 1 + src/parser.y | 26 ++++++++++++--- src/property.cpp | 19 ++++++++++- src/typechecker.cpp | 20 ++++++++++++ test/test_parser.cpp | 70 ++++++++++++++++++++++++++++++++++++----- 8 files changed, 151 insertions(+), 15 deletions(-) diff --git a/include/utap/common.h b/include/utap/common.h index 74b8be64..e2d1482f 100644 --- a/include/utap/common.h +++ b/include/utap/common.h @@ -144,10 +144,16 @@ enum kind_t { ASS_RSHIFT, /******************************************************* - * T-ATL Quantifiers + * 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 diff --git a/include/utap/property.h b/include/utap/property.h index dedaa79f..d50a7aa9 100644 --- a/include/utap/property.h +++ b/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, pu bool isSMC(UTAP::expression_t* expr = nullptr); }; -class TigaPropertyBuilder final : public PropertyBuilder +class TigaPropertyBuilder : public PropertyBuilder { protected: std::map 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 */ diff --git a/src/expression.cpp b/src/expression.cpp index 8281fb4a..f53821a8 100644 --- a/src/expression.cpp +++ b/src/expression.cpp @@ -444,8 +444,14 @@ size_t expression_t::get_size() const case SIMULATEREACH: case SPAWN: return std::get(data->value); + case ATL_ENFORCE_UNTIL: + case ATL_DESPITE_UNTIL: assert(data->sub.size() == 2); return 2; case ATL_ENFORCE_F: - case ATL_DESPITE_F: assert(data->sub.size() == 1); return 1; + 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 1; case EG: case AG: diff --git a/src/lexer.l b/src/lexer.l index 29d52dab..b19c9c17 100644 --- a/src/lexer.l +++ b/src/lexer.l @@ -161,6 +161,7 @@ idchr [a-zA-Z0-9_$#] "R" { return 'R'; } "W" { return 'W'; } "E" { return 'E'; } +"X" { return 'X'; } "A<>" { return T_AF; } "A[]" { return T_AG; } diff --git a/src/parser.y b/src/parser.y index 48cffff3..509501ce 100644 --- a/src/parser.y +++ b/src/parser.y @@ -283,7 +283,7 @@ const char* utap_msg(const char *msg) %token T_DYNAMIC T_HYBRID %token T_SPAWN T_EXIT T_NUMOF -/* T-ATL */ +/* ATL */ %token T_LBRBR T_RBRBR %type ExpQuantifier ExpPrQuantifier @@ -302,7 +302,7 @@ const char* utap_msg(const char *msg) %right T_AF T_AG T_EF T_EG 'A' 'M' %right T_AG_PLUS T_EF_PLUS T_AG_MULT T_EF_MULT %right T_PMAX T_SCENARIO -%left 'U' 'W' 'R' +%left 'U' 'W' 'R' 'X' %right T_FORALL T_EXISTS T_SUM %right T_ASSIGNMENT T_ASSPLUS T_ASSMINUS T_ASSMULT T_ASSDIV T_ASSMOD T_ASSAND T_ASSOR T_ASSLSHIFT T_ASSRSHIFT T_ASSXOR %right '?' ':' @@ -320,7 +320,7 @@ const char* utap_msg(const char *msg) %left T_POWOP %right T_EXCLAM T_KW_NOT UOPERATOR %right T_INCREMENT T_DECREMENT -%left '(' ')' '[' ']' '.' '\'' +%left '(' ')' '[' ']' '.' '\'' T_LBRBR T_RBRBR %union { @@ -1740,12 +1740,30 @@ SubPropertyOrExpression: SubProperty | Expression; SubProperty: - T_LSHIFT 'A' T_RSHIFT T_DIAMOND SubPropertyOrExpression { + T_LSHIFT 'A' T_RSHIFT '[' SubPropertyOrExpression 'U' SubPropertyOrExpression ']' { + CALL(@1, @8, expr_binary(ATL_ENFORCE_UNTIL)); + } + | T_LBRBR 'A' T_RBRBR '[' SubPropertyOrExpression 'U' SubPropertyOrExpression ']' { + CALL(@1, @8, expr_binary(ATL_DESPITE_UNTIL)); + } + | T_LSHIFT 'A' T_RSHIFT T_DIAMOND SubPropertyOrExpression { CALL(@1, @5, expr_unary(ATL_ENFORCE_F)); } | T_LBRBR 'A' T_RBRBR T_DIAMOND SubPropertyOrExpression { CALL(@1, @5, expr_unary(ATL_DESPITE_F)); } + | T_LSHIFT 'A' T_RSHIFT T_BOX SubPropertyOrExpression { + CALL(@1, @5, expr_unary(ATL_ENFORCE_G)); + } + | T_LBRBR 'A' T_RBRBR T_BOX SubPropertyOrExpression { + CALL(@1, @5, expr_unary(ATL_DESPITE_G)); + } + | T_LSHIFT 'A' T_RSHIFT 'X' SubPropertyOrExpression { + CALL(@1, @5, expr_unary(ATL_ENFORCE_NEXT)); + } + | T_LBRBR 'A' T_RBRBR 'X' SubPropertyOrExpression { + CALL(@1, @5, expr_unary(ATL_DESPITE_NEXT)); + } | T_AF Expression { CALL(@1, @2, expr_unary(AF)); } diff --git a/src/property.cpp b/src/property.cpp index 6f174190..7fd9a1f5 100644 --- a/src/property.cpp +++ b/src/property.cpp @@ -478,4 +478,21 @@ void TigaPropertyBuilder::imitation(const char* id) void TigaPropertyBuilder::expr_optimize(int, int, int, int) { // nothing for now -} \ No newline at end of file +} +void AtlPropertyBuilder::typeProperty(UTAP::expression_t expr) +{ + switch (expr.get_kind()) { + case ATL_ENFORCE_UNTIL: + case ATL_DESPITE_UNTIL: + case ATL_ENFORCE_F: + case ATL_DESPITE_F: + case ATL_ENFORCE_G: + case ATL_DESPITE_G: + case ATL_ENFORCE_NEXT: + case ATL_DESPITE_NEXT: + properties.back().type = quant_t::Atl; + break; + default: + TigaPropertyBuilder::typeProperty(expr); + } +} diff --git a/src/typechecker.cpp b/src/typechecker.cpp index 553f3463..a2b8117c 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -2221,6 +2221,26 @@ bool TypeChecker::checkExpression(expression_t expr) } break; + case ATL_ENFORCE_UNTIL: + case ATL_DESPITE_UNTIL: + // TODO: Check coalition + if (is_formula(expr[0]) && is_formula(expr[1])) { + type = type_t::create_primitive(FORMULA); + } + break; + + case ATL_ENFORCE_F: + case ATL_DESPITE_F: + case ATL_ENFORCE_G: + case ATL_DESPITE_G: + case ATL_ENFORCE_NEXT: + case ATL_DESPITE_NEXT: + // TODO: Check coalition + if (is_formula(expr[0])) { + type = type_t::create_primitive(FORMULA); + } + break; + case AF: case AG: case EF: diff --git a/test/test_parser.cpp b/test/test_parser.cpp index dc961821..a4748fcc 100644 --- a/test/test_parser.cpp +++ b/test/test_parser.cpp @@ -541,21 +541,77 @@ TEST_CASE("Increment with multiple array subscripting and dot accessing") TEST_CASE("T-ALT properties") { auto doc = std::make_unique(); - auto builder = std::make_unique(*doc); + auto builder = std::make_unique(*doc); + SUBCASE("Basic EnforceUntil property") + { + auto res = parseProperty("<< A >> [ true U false ]", builder.get()); + REQUIRE(res == 0); + auto expr = &builder->getProperties().front(); + CHECK(expr->intermediate.get_size() == 2); + CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_UNTIL); + CHECK(expr->type == UTAP::quant_t::Atl); + } + SUBCASE("Basic DespiteUntil property") + { + auto res = parseProperty("[[ A ]] [ true U false ]", builder.get()); + REQUIRE(res == 0); + auto expr = &builder->getProperties().front(); + CHECK(expr->intermediate.get_size() == 2); + CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_UNTIL); + CHECK(expr->type == UTAP::quant_t::Atl); + } SUBCASE("Basic EnforceF property") { auto res = parseProperty("<< A >> <> true", builder.get()); REQUIRE(res == 0); - auto expr = builder->getQuery(); - CHECK(expr.get_size() == 1); - CHECK(expr.get_kind() == UTAP::Constants::ATL_ENFORCE_F); + auto expr = &builder->getProperties().front(); + CHECK(expr->intermediate.get_size() == 1); + CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_F); + CHECK(expr->type == UTAP::quant_t::Atl); } SUBCASE("Basic DespiteF property") { auto res = parseProperty("[[ A ]] <> true", builder.get()); REQUIRE(res == 0); - auto expr = builder->getQuery(); - CHECK(expr.get_size() == 1); - CHECK(expr.get_kind() == UTAP::Constants::ATL_DESPITE_F); + auto expr = &builder->getProperties().front(); + CHECK(expr->intermediate.get_size() == 1); + CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_F); + CHECK(expr->type == UTAP::quant_t::Atl); + } + SUBCASE("Basic EnforceG property") + { + auto res = parseProperty("<< A >> [] true", builder.get()); + REQUIRE(res == 0); + auto expr = &builder->getProperties().front(); + CHECK(expr->intermediate.get_size() == 1); + CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_G); + CHECK(expr->type == UTAP::quant_t::Atl); + } + SUBCASE("Basic DespiteG property") + { + auto res = parseProperty("[[ A ]] [] true", builder.get()); + REQUIRE(res == 0); + auto expr = &builder->getProperties().front(); + CHECK(expr->intermediate.get_size() == 1); + CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_G); + CHECK(expr->type == UTAP::quant_t::Atl); + } + SUBCASE("Basic EnforceNext property") + { + auto res = parseProperty("<< A >> X true", builder.get()); + REQUIRE(res == 0); + auto expr = &builder->getProperties().front(); + CHECK(expr->intermediate.get_size() == 1); + CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_NEXT); + CHECK(expr->type == UTAP::quant_t::Atl); + } + SUBCASE("Basic DespiteNext property") + { + auto res = parseProperty("[[ A ]] X true", builder.get()); + REQUIRE(res == 0); + auto expr = &builder->getProperties().front(); + CHECK(expr->intermediate.get_size() == 1); + CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_NEXT); + CHECK(expr->type == UTAP::quant_t::Atl); } } \ No newline at end of file From d18e4c2c2a68dd03ee849a24f80ee91b3c3fc906 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Fri, 25 Oct 2024 14:28:25 +0200 Subject: [PATCH 04/16] Parse PlayerColors for ATL --- include/utap/AbstractBuilder.hpp | 2 ++ include/utap/ExpressionBuilder.hpp | 2 ++ include/utap/builder.h | 2 ++ src/ExpressionBuilder.cpp | 19 ++++++++++++ src/abstractbuilder.cpp | 2 ++ src/expression.cpp | 4 +-- src/parser.y | 49 +++++++++++++++++++----------- src/typechecker.cpp | 25 +++++++++------ test/test_parser.cpp | 32 +++++++++---------- 9 files changed, 91 insertions(+), 46 deletions(-) diff --git a/include/utap/AbstractBuilder.hpp b/include/utap/AbstractBuilder.hpp index 1b43870a..f108286a 100644 --- a/include/utap/AbstractBuilder.hpp +++ b/include/utap/AbstractBuilder.hpp @@ -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; diff --git a/include/utap/ExpressionBuilder.hpp b/include/utap/ExpressionBuilder.hpp index 88d469ec..f3857711 100644 --- a/include/utap/ExpressionBuilder.hpp +++ b/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; diff --git a/include/utap/builder.h b/include/utap/builder.h index 32f903bf..1d2bbd00 100644 --- a/include/utap/builder.h +++ b/include/utap/builder.h @@ -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; diff --git a/src/ExpressionBuilder.cpp b/src/ExpressionBuilder.cpp index e07181a9..ba20be33 100644 --- a/src/ExpressionBuilder.cpp +++ b/src/ExpressionBuilder.cpp @@ -810,6 +810,25 @@ 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 parts; + parts.reserve(nbPlayers + nbSubExprs); + + // TODO Deduplicate players + 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: diff --git a/src/abstractbuilder.cpp b/src/abstractbuilder.cpp index 08621726..82f0bee8 100644 --- a/src/abstractbuilder.cpp +++ b/src/abstractbuilder.cpp @@ -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; } diff --git a/src/expression.cpp b/src/expression.cpp index f53821a8..d5f59a5c 100644 --- a/src/expression.cpp +++ b/src/expression.cpp @@ -445,13 +445,13 @@ size_t expression_t::get_size() const case SPAWN: return std::get(data->value); case ATL_ENFORCE_UNTIL: - case ATL_DESPITE_UNTIL: assert(data->sub.size() == 2); return 2; + case ATL_DESPITE_UNTIL: assert(data->sub.size() >= 2); return std::get(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 1; + case ATL_DESPITE_NEXT: assert(data->sub.size() >= 1); return std::get(data->value); case EG: case AG: diff --git a/src/parser.y b/src/parser.y index 509501ce..b0c6e5d7 100644 --- a/src/parser.y +++ b/src/parser.y @@ -289,10 +289,10 @@ const char* utap_msg(const char *msg) %type ExpQuantifier ExpPrQuantifier %type PathType %type ArgList FieldDeclList FieldDeclIdList FieldDecl -%type ParameterList FieldInitList +%type ParameterList FieldInitList PlayerColorList %type OptionalInstanceParameterList ExpressionList NonEmptyExpressionList %type Type TypePrefix -%type Id NonTypeId +%type Id NonTypeId PlayerColor %type UnaryOp AssignOp %type VarInit %type CmpGLE @@ -757,12 +757,25 @@ NonTypeId: | 'R' { strncpy($$, "R", MAXLEN); } | 'E' { strncpy($$, "E", MAXLEN); } | 'M' { strncpy($$, "M", MAXLEN); } + | 'X' { strncpy($$, "X", MAXLEN); } | T_SUP { strncpy($$, "sup", MAXLEN); } | T_INF { strncpy($$, "inf", MAXLEN); } | T_BOUNDS { strncpy($$, "bounds", MAXLEN); } | T_SIMULATION { strncpy($$, "simulation", MAXLEN); } ; +PlayerColor: + NonTypeId { + CALL(@1, @1, expr_string($1)); + } + ; + +PlayerColorList: + /* empty */ { $$=0; } + | PlayerColor { $$=1; } + | PlayerColorList ',' PlayerColor { $$=$1+1; } + ; + FieldDeclList: FieldDecl { $$=$1; } | FieldDeclList FieldDecl { $$=$1+$2; } @@ -1740,29 +1753,29 @@ SubPropertyOrExpression: SubProperty | Expression; SubProperty: - T_LSHIFT 'A' T_RSHIFT '[' SubPropertyOrExpression 'U' SubPropertyOrExpression ']' { - CALL(@1, @8, expr_binary(ATL_ENFORCE_UNTIL)); + T_LSHIFT PlayerColorList T_RSHIFT '[' SubPropertyOrExpression 'U' SubPropertyOrExpression ']' { + CALL(@1, @8, expr_atl($2, ATL_ENFORCE_UNTIL)); } - | T_LBRBR 'A' T_RBRBR '[' SubPropertyOrExpression 'U' SubPropertyOrExpression ']' { - CALL(@1, @8, expr_binary(ATL_DESPITE_UNTIL)); + | T_LBRBR PlayerColorList T_RBRBR '[' SubPropertyOrExpression 'U' SubPropertyOrExpression ']' { + CALL(@1, @8, expr_atl($2, ATL_DESPITE_UNTIL)); } - | T_LSHIFT 'A' T_RSHIFT T_DIAMOND SubPropertyOrExpression { - CALL(@1, @5, expr_unary(ATL_ENFORCE_F)); + | T_LSHIFT PlayerColorList T_RSHIFT T_DIAMOND SubPropertyOrExpression { + CALL(@1, @5, expr_atl($2, ATL_ENFORCE_F)); } - | T_LBRBR 'A' T_RBRBR T_DIAMOND SubPropertyOrExpression { - CALL(@1, @5, expr_unary(ATL_DESPITE_F)); + | T_LBRBR PlayerColorList T_RBRBR T_DIAMOND SubPropertyOrExpression { + CALL(@1, @5, expr_atl($2, ATL_DESPITE_F)); } - | T_LSHIFT 'A' T_RSHIFT T_BOX SubPropertyOrExpression { - CALL(@1, @5, expr_unary(ATL_ENFORCE_G)); + | T_LSHIFT PlayerColorList T_RSHIFT T_BOX SubPropertyOrExpression { + CALL(@1, @5, expr_atl($2, ATL_ENFORCE_G)); } - | T_LBRBR 'A' T_RBRBR T_BOX SubPropertyOrExpression { - CALL(@1, @5, expr_unary(ATL_DESPITE_G)); + | T_LBRBR PlayerColorList T_RBRBR T_BOX SubPropertyOrExpression { + CALL(@1, @5, expr_atl($2, ATL_DESPITE_G)); } - | T_LSHIFT 'A' T_RSHIFT 'X' SubPropertyOrExpression { - CALL(@1, @5, expr_unary(ATL_ENFORCE_NEXT)); + | T_LSHIFT PlayerColorList T_RSHIFT 'X' SubPropertyOrExpression { + CALL(@1, @5, expr_atl($2, ATL_ENFORCE_NEXT)); } - | T_LBRBR 'A' T_RBRBR 'X' SubPropertyOrExpression { - CALL(@1, @5, expr_unary(ATL_DESPITE_NEXT)); + | T_LBRBR PlayerColorList T_RBRBR 'X' SubPropertyOrExpression { + CALL(@1, @5, expr_atl($2, ATL_DESPITE_NEXT)); } | T_AF Expression { CALL(@1, @2, expr_unary(AF)); diff --git a/src/typechecker.cpp b/src/typechecker.cpp index a2b8117c..8c928608 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -994,6 +994,14 @@ void TypeChecker::visitInstance(instance_t& instance) static bool isGameProperty(expression_t expr) { switch (expr.get_kind()) { + case ATL_ENFORCE_UNTIL: + case ATL_DESPITE_UNTIL: + 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 CONTROL: case SMC_CONTROL: case EF_CONTROL: @@ -2223,24 +2231,21 @@ bool TypeChecker::checkExpression(expression_t expr) case ATL_ENFORCE_UNTIL: case ATL_DESPITE_UNTIL: - // TODO: Check coalition - if (is_formula(expr[0]) && is_formula(expr[1])) { - type = type_t::create_primitive(FORMULA); - } - break; - case ATL_ENFORCE_F: case ATL_DESPITE_F: case ATL_ENFORCE_G: case ATL_DESPITE_G: case ATL_ENFORCE_NEXT: - case ATL_DESPITE_NEXT: - // TODO: Check coalition - if (is_formula(expr[0])) { + case ATL_DESPITE_NEXT: { + bool isUntil = expr.get_kind() == ATL_ENFORCE_UNTIL || expr.get_kind() == ATL_DESPITE_UNTIL; + int numPlayer = expr.get_size() - (isUntil ? 2 : 1); + for (int i = 0; i < numPlayer; ++i) { + } + if (is_formula(expr[numPlayer]) && (!isUntil || is_formula(expr[numPlayer + 1]))) { type = type_t::create_primitive(FORMULA); } break; - + } case AF: case AG: case EF: diff --git a/test/test_parser.cpp b/test/test_parser.cpp index a4748fcc..7193a4df 100644 --- a/test/test_parser.cpp +++ b/test/test_parser.cpp @@ -544,73 +544,73 @@ TEST_CASE("T-ALT properties") auto builder = std::make_unique(*doc); SUBCASE("Basic EnforceUntil property") { - auto res = parseProperty("<< A >> [ true U false ]", builder.get()); + auto res = parseProperty("<< red, green >> [ true U false ]", builder.get()); REQUIRE(res == 0); auto expr = &builder->getProperties().front(); - CHECK(expr->intermediate.get_size() == 2); + CHECK(expr->intermediate.get_size() == 4); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_UNTIL); CHECK(expr->type == UTAP::quant_t::Atl); } SUBCASE("Basic DespiteUntil property") { - auto res = parseProperty("[[ A ]] [ true U false ]", builder.get()); + auto res = parseProperty("[[red, green]] [ true U false ]", builder.get()); REQUIRE(res == 0); auto expr = &builder->getProperties().front(); - CHECK(expr->intermediate.get_size() == 2); + CHECK(expr->intermediate.get_size() == 4); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_UNTIL); CHECK(expr->type == UTAP::quant_t::Atl); } SUBCASE("Basic EnforceF property") { - auto res = parseProperty("<< A >> <> true", builder.get()); + auto res = parseProperty("<> <> true", builder.get()); REQUIRE(res == 0); auto expr = &builder->getProperties().front(); - CHECK(expr->intermediate.get_size() == 1); + CHECK(expr->intermediate.get_size() == 3); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_F); CHECK(expr->type == UTAP::quant_t::Atl); } SUBCASE("Basic DespiteF property") { - auto res = parseProperty("[[ A ]] <> true", builder.get()); + auto res = parseProperty("[[red, green]] <> true", builder.get()); REQUIRE(res == 0); auto expr = &builder->getProperties().front(); - CHECK(expr->intermediate.get_size() == 1); + CHECK(expr->intermediate.get_size() == 3); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_F); CHECK(expr->type == UTAP::quant_t::Atl); } SUBCASE("Basic EnforceG property") { - auto res = parseProperty("<< A >> [] true", builder.get()); + auto res = parseProperty("<> [] true", builder.get()); REQUIRE(res == 0); auto expr = &builder->getProperties().front(); - CHECK(expr->intermediate.get_size() == 1); + CHECK(expr->intermediate.get_size() == 3); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_G); CHECK(expr->type == UTAP::quant_t::Atl); } SUBCASE("Basic DespiteG property") { - auto res = parseProperty("[[ A ]] [] true", builder.get()); + auto res = parseProperty("[[red, green]] [] true", builder.get()); REQUIRE(res == 0); auto expr = &builder->getProperties().front(); - CHECK(expr->intermediate.get_size() == 1); + CHECK(expr->intermediate.get_size() == 3); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_G); CHECK(expr->type == UTAP::quant_t::Atl); } SUBCASE("Basic EnforceNext property") { - auto res = parseProperty("<< A >> X true", builder.get()); + auto res = parseProperty("<> X true", builder.get()); REQUIRE(res == 0); auto expr = &builder->getProperties().front(); - CHECK(expr->intermediate.get_size() == 1); + CHECK(expr->intermediate.get_size() == 3); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_NEXT); CHECK(expr->type == UTAP::quant_t::Atl); } SUBCASE("Basic DespiteNext property") { - auto res = parseProperty("[[ A ]] X true", builder.get()); + auto res = parseProperty("[[red, green]] X true", builder.get()); REQUIRE(res == 0); auto expr = &builder->getProperties().front(); - CHECK(expr->intermediate.get_size() == 1); + CHECK(expr->intermediate.get_size() == 3); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_NEXT); CHECK(expr->type == UTAP::quant_t::Atl); } From e17bd2f281a1b81c80a0510d95b2c598b5c19275 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Fri, 25 Oct 2024 15:55:37 +0200 Subject: [PATCH 05/16] Add type checking of player colors --- include/utap/AbstractBuilder.hpp | 2 +- include/utap/DocumentBuilder.hpp | 2 +- include/utap/builder.h | 2 +- include/utap/document.h | 1 + include/utap/prettyprinter.h | 2 +- src/DocumentBuilder.cpp | 3 ++- src/ExpressionBuilder.cpp | 1 - src/abstractbuilder.cpp | 2 +- src/document.cpp | 1 + src/prettyprinter.cpp | 4 ++-- src/typechecker.cpp | 31 +++++++++++++++++++++++++++++++ src/xmlreader.cpp | 6 +++++- test/test_parser.cpp | 32 ++++++++++++++++++++++++++------ 13 files changed, 73 insertions(+), 16 deletions(-) diff --git a/include/utap/AbstractBuilder.hpp b/include/utap/AbstractBuilder.hpp index f108286a..ca0cc4ab 100644 --- a/include/utap/AbstractBuilder.hpp +++ b/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; diff --git a/include/utap/DocumentBuilder.hpp b/include/utap/DocumentBuilder.hpp index d2439b8a..6a318743 100644 --- a/include/utap/DocumentBuilder.hpp +++ b/include/utap/DocumentBuilder.hpp @@ -124,7 +124,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; diff --git a/include/utap/builder.h b/include/utap/builder.h index 1d2bbd00..a609998c 100644 --- a/include/utap/builder.h +++ b/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 diff --git a/include/utap/document.h b/include/utap/document.h index 06ad2fcb..36a80f40 100644 --- a/include/utap/document.h +++ b/include/utap/document.h @@ -107,6 +107,7 @@ struct edge_t : stringify_t { int nr; /**< Placement in input file */ bool control; /**< Controllable (true/false) */ + std::string color; std::string actname; location_t* src{nullptr}; /**< Pointer to source location */ branchpoint_t* srcb{nullptr}; /**< Pointer to source branchpoint */ diff --git a/include/utap/prettyprinter.h b/include/utap/prettyprinter.h index d54ba65c..eb557f0b 100644 --- a/include/utap/prettyprinter.h +++ b/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; diff --git a/src/DocumentBuilder.cpp b/src/DocumentBuilder.cpp index 07611ec1..00e84679 100644 --- a/src/DocumentBuilder.cpp +++ b/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 = ¤tTemplate->add_edge(fid, tid, control, actname); + currentEdge->color = color; currentEdge->guard = make_constant(1); currentEdge->assign = make_constant(1); // default "probability" weight is 1. diff --git a/src/ExpressionBuilder.cpp b/src/ExpressionBuilder.cpp index ba20be33..ad950f9b 100644 --- a/src/ExpressionBuilder.cpp +++ b/src/ExpressionBuilder.cpp @@ -816,7 +816,6 @@ void ExpressionBuilder::expr_atl(int nbPlayers, Constants::kind_t kind) std::vector parts; parts.reserve(nbPlayers + nbSubExprs); - // TODO Deduplicate players for (int i = 0; i < nbPlayers; ++i) { parts.push_back(fragments[nbPlayers + nbSubExprs - 1 - i]); } diff --git a/src/abstractbuilder.cpp b/src/abstractbuilder.cpp index 82f0bee8..41ed5694 100644 --- a/src/abstractbuilder.cpp +++ b/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; } diff --git a/src/document.cpp b/src/document.cpp index 6c048bac..a6768535 100644 --- a/src/document.cpp +++ b/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 = string{"#000000"}; edge.actname = std::move(actname); edge.nr = nr; return edge; diff --git a/src/prettyprinter.cpp b/src/prettyprinter.cpp index 20f4cc05..ba4be443 100644 --- a/src/prettyprinter.cpp +++ b/src/prettyprinter.cpp @@ -540,10 +540,10 @@ void PrettyPrinter::proc_update() { update = st.size(); } void PrettyPrinter::proc_edge_begin(const char* from, const char* to, const bool control) { - proc_edge_begin(from, to, control, nullptr); + proc_edge_begin(from, to, control, nullptr, nullptr); } -void PrettyPrinter::proc_edge_begin(const char* source, const char* target, const bool control, const char* actname) +void PrettyPrinter::proc_edge_begin(const char* source, const char* target, const bool control, const char* color, const char* actname) { if (first) { // this is the first transition diff --git a/src/typechecker.cpp b/src/typechecker.cpp index 8c928608..91497a34 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -2239,7 +2239,38 @@ bool TypeChecker::checkExpression(expression_t expr) case ATL_DESPITE_NEXT: { bool isUntil = expr.get_kind() == ATL_ENFORCE_UNTIL || expr.get_kind() == ATL_DESPITE_UNTIL; int numPlayer = expr.get_size() - (isUntil ? 2 : 1); + std::array, 11> color_map {{ + {"black", "#000000"}, + {"lightgray", "#c0c0c0"}, + {"darkgray", "#a9a9a9"}, + {"red", "#ff0000"}, + {"green", "#00ff00"}, + {"blue", "#0000ff"}, + {"yellow", "#ffff00"}, + {"cyan", "#00ffff"}, + {"magenta", "#ff00ff"}, + {"orange", "#ffa500"}, + {"pink", "#ffc0cb"}, + }}; + std::array used{}; for (int i = 0; i < numPlayer; ++i) { + const auto& str = expr[i].get_string_value(); + bool found = false; + for (int j = 0; j < color_map.size(); ++j) { + auto [name, hex] = color_map[j]; + if (str == name) { + auto str_id = document.add_string(hex); + expr[i] = expression_t::create_string(str_id, expr[i].get_position()); + if (used[j]) { + handleError(expr[i], "$Atl_player_color_used_twice"); + } + used[j] = found = true; + break; + } + } + if (!found) { + handleError(expr[i], "$Atl_unknown_player_color"); + } } if (is_formula(expr[numPlayer]) && (!isUntil || is_formula(expr[numPlayer + 1]))) { type = type_t::create_primitive(FORMULA); diff --git a/src/xmlreader.cpp b/src/xmlreader.cpp index 08bf03c7..e56f3f48 100644 --- a/src/xmlreader.cpp +++ b/src/xmlreader.cpp @@ -1050,6 +1050,10 @@ bool XMLReader::transition() bool control = (type == nullptr || (strcmp(type, "true") == 0)); xmlFree(type); + char* color_raw = getAttribute("color"); + auto color = std::string{color_raw ? color_raw : "#000000"}; + xmlFree(color_raw); + char* id = getAttribute("action"); auto actname = std::string{id ? id : "SKIP"}; xmlFree(id); @@ -1058,7 +1062,7 @@ bool XMLReader::transition() std::string from = source(); std::string to = target(); - parser->proc_edge_begin(from.c_str(), to.c_str(), control, actname.c_str()); + parser->proc_edge_begin(from.c_str(), to.c_str(), control, color.c_str(), actname.c_str()); while (label()) ; while (begin(tag_t::NAIL)) diff --git a/test/test_parser.cpp b/test/test_parser.cpp index 7193a4df..82c8c049 100644 --- a/test/test_parser.cpp +++ b/test/test_parser.cpp @@ -546,6 +546,7 @@ TEST_CASE("T-ALT properties") { auto res = parseProperty("<< red, green >> [ true U false ]", builder.get()); REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); auto expr = &builder->getProperties().front(); CHECK(expr->intermediate.get_size() == 4); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_UNTIL); @@ -555,6 +556,7 @@ TEST_CASE("T-ALT properties") { auto res = parseProperty("[[red, green]] [ true U false ]", builder.get()); REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); auto expr = &builder->getProperties().front(); CHECK(expr->intermediate.get_size() == 4); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_UNTIL); @@ -562,8 +564,9 @@ TEST_CASE("T-ALT properties") } SUBCASE("Basic EnforceF property") { - auto res = parseProperty("<> <> true", builder.get()); + auto res = parseProperty("<> <> true", builder.get()); REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); auto expr = &builder->getProperties().front(); CHECK(expr->intermediate.get_size() == 3); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_F); @@ -571,8 +574,9 @@ TEST_CASE("T-ALT properties") } SUBCASE("Basic DespiteF property") { - auto res = parseProperty("[[red, green]] <> true", builder.get()); + auto res = parseProperty("[[cyan, yellow]] <> true", builder.get()); REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); auto expr = &builder->getProperties().front(); CHECK(expr->intermediate.get_size() == 3); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_F); @@ -580,8 +584,9 @@ TEST_CASE("T-ALT properties") } SUBCASE("Basic EnforceG property") { - auto res = parseProperty("<> [] true", builder.get()); + auto res = parseProperty("<> [] true", builder.get()); REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); auto expr = &builder->getProperties().front(); CHECK(expr->intermediate.get_size() == 3); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_G); @@ -589,8 +594,9 @@ TEST_CASE("T-ALT properties") } SUBCASE("Basic DespiteG property") { - auto res = parseProperty("[[red, green]] [] true", builder.get()); + auto res = parseProperty("[[lightgray, darkgray]] [] true", builder.get()); REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); auto expr = &builder->getProperties().front(); CHECK(expr->intermediate.get_size() == 3); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_G); @@ -598,8 +604,9 @@ TEST_CASE("T-ALT properties") } SUBCASE("Basic EnforceNext property") { - auto res = parseProperty("<> X true", builder.get()); + auto res = parseProperty("<> X true", builder.get()); REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); auto expr = &builder->getProperties().front(); CHECK(expr->intermediate.get_size() == 3); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_NEXT); @@ -607,11 +614,24 @@ TEST_CASE("T-ALT properties") } SUBCASE("Basic DespiteNext property") { - auto res = parseProperty("[[red, green]] X true", builder.get()); + auto res = parseProperty("[[pink, green]] X true", builder.get()); REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); auto expr = &builder->getProperties().front(); CHECK(expr->intermediate.get_size() == 3); CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_DESPITE_NEXT); CHECK(expr->type == UTAP::quant_t::Atl); } + SUBCASE("Repeated player color error") + { + auto res = parseProperty("<> <> true", builder.get()); + REQUIRE(res == 0); + CHECK(doc->get_errors().size() == 1); + } + SUBCASE("Unknown player color error") + { + auto res = parseProperty("[[red, giraffe]] [] true", builder.get()); + REQUIRE(res == 0); + CHECK(doc->get_errors().size() == 1); + } } \ No newline at end of file From 2888f774af520cc8ccbdb0ca5bbd5fbcc0b3871d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Wed, 30 Oct 2024 14:04:06 +0100 Subject: [PATCH 06/16] Add get_player_count and printing of ATL formula --- include/utap/expression.h | 3 ++ src/expression.cpp | 91 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 94 insertions(+) diff --git a/include/utap/expression.h b/include/utap/expression.h index 2ad68386..7a62da9e 100644 --- a/include/utap/expression.h +++ b/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; diff --git a/src/expression.cpp b/src/expression.cpp index d5f59a5c..2a553f3c 100644 --- a/src/expression.cpp +++ b/src/expression.cpp @@ -505,6 +505,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); @@ -846,10 +867,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: @@ -1434,6 +1463,68 @@ std::ostream& expression_t::print(std::ostream& os, bool old) const case RATE: get(0).print(os, old) << '\''; 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(0).print(os, old); + if (i < n - 1) os << ", "; + } + os << ">> "; + 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(0).print(os, 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); From 73bc77ff431e3aa89d2354a61089a308a83b4684 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Mon, 4 Nov 2024 10:44:25 +0100 Subject: [PATCH 07/16] Replace colors with uint32_t --- include/utap/DocumentBuilder.hpp | 2 ++ include/utap/document.h | 2 +- src/DocumentBuilder.cpp | 7 ++++++- src/document.cpp | 2 +- src/typechecker.cpp | 27 +++++++++++++-------------- 5 files changed, 23 insertions(+), 17 deletions(-) diff --git a/include/utap/DocumentBuilder.hpp b/include/utap/DocumentBuilder.hpp index 6a318743..6fa3e851 100644 --- a/include/utap/DocumentBuilder.hpp +++ b/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 paths = {}); diff --git a/include/utap/document.h b/include/utap/document.h index 36a80f40..ad4c420e 100644 --- a/include/utap/document.h +++ b/include/utap/document.h @@ -107,7 +107,7 @@ struct edge_t : stringify_t { int nr; /**< Placement in input file */ bool control; /**< Controllable (true/false) */ - std::string color; + uint32_t color; std::string actname; location_t* src{nullptr}; /**< Pointer to source location */ branchpoint_t* srcb{nullptr}; /**< Pointer to source branchpoint */ diff --git a/src/DocumentBuilder.cpp b/src/DocumentBuilder.cpp index 00e84679..585d2817 100644 --- a/src/DocumentBuilder.cpp +++ b/src/DocumentBuilder.cpp @@ -243,7 +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 = ¤tTemplate->add_edge(fid, tid, control, actname); - currentEdge->color = color; + currentEdge->color = parse_hex_color(color); currentEdge->guard = make_constant(1); currentEdge->assign = make_constant(1); // default "probability" weight is 1. @@ -755,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); +} diff --git a/src/document.cpp b/src/document.cpp index a6768535..f284ed47 100644 --- a/src/document.cpp +++ b/src/document.cpp @@ -315,7 +315,7 @@ edge_t& template_t::add_edge(symbol_t src, symbol_t dst, bool control, string ac } edge.control = control; - edge.color = string{"#000000"}; + edge.color = 0x000000; edge.actname = std::move(actname); edge.nr = nr; return edge; diff --git a/src/typechecker.cpp b/src/typechecker.cpp index 91497a34..6b3d1a8d 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -2239,18 +2239,18 @@ bool TypeChecker::checkExpression(expression_t expr) case ATL_DESPITE_NEXT: { bool isUntil = expr.get_kind() == ATL_ENFORCE_UNTIL || expr.get_kind() == ATL_DESPITE_UNTIL; int numPlayer = expr.get_size() - (isUntil ? 2 : 1); - std::array, 11> color_map {{ - {"black", "#000000"}, - {"lightgray", "#c0c0c0"}, - {"darkgray", "#a9a9a9"}, - {"red", "#ff0000"}, - {"green", "#00ff00"}, - {"blue", "#0000ff"}, - {"yellow", "#ffff00"}, - {"cyan", "#00ffff"}, - {"magenta", "#ff00ff"}, - {"orange", "#ffa500"}, - {"pink", "#ffc0cb"}, + std::array, 11> color_map {{ + {"black", 0x000000}, + {"lightgray", 0xc0c0c0}, + {"darkgray", 0xa9a9a9}, + {"red", 0xff0000}, + {"green", 0x00ff00}, + {"blue", 0x0000ff}, + {"yellow", 0xffff00}, + {"cyan", 0x00ffff}, + {"magenta", 0xff00ff}, + {"orange", 0xffa500}, + {"pink", 0xffc0cb}, }}; std::array used{}; for (int i = 0; i < numPlayer; ++i) { @@ -2259,8 +2259,7 @@ bool TypeChecker::checkExpression(expression_t expr) for (int j = 0; j < color_map.size(); ++j) { auto [name, hex] = color_map[j]; if (str == name) { - auto str_id = document.add_string(hex); - expr[i] = expression_t::create_string(str_id, expr[i].get_position()); + expr[i] = expression_t::create_constant(hex, expr.get_position()); if (used[j]) { handleError(expr[i], "$Atl_player_color_used_twice"); } From fa92d0d1008827667a1313241f44e0c9dfef94c2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Wed, 6 Nov 2024 10:01:06 +0100 Subject: [PATCH 08/16] Fix ATL expr printing --- src/expression.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/expression.cpp b/src/expression.cpp index 2a553f3c..5df5855c 100644 --- a/src/expression.cpp +++ b/src/expression.cpp @@ -1470,10 +1470,10 @@ std::ostream& expression_t::print(std::ostream& os, bool old) const os << "<<"; size_t n = get_player_count(); for (int i = 0; i < n; ++i) { - get(0).print(os, old); + get(i).print(os << "#" << std::hex, old); if (i < n - 1) os << ", "; } - os << ">> "; + os << std::dec << ">> "; switch (data->kind) { case Constants::ATL_ENFORCE_UNTIL: get(n).print(os << "[", old) << " U "; From d9438174d108ecf5df7b24e6f983cb91ad18f61f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Wed, 6 Nov 2024 10:11:53 +0100 Subject: [PATCH 09/16] Fix ATL despite expr print and use 0 fill --- src/expression.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/expression.cpp b/src/expression.cpp index 5df5855c..4930587b 100644 --- a/src/expression.cpp +++ b/src/expression.cpp @@ -1470,7 +1470,7 @@ std::ostream& expression_t::print(std::ostream& os, bool old) const os << "<<"; size_t n = get_player_count(); for (int i = 0; i < n; ++i) { - get(i).print(os << "#" << std::hex, old); + get(i).print(os << "#" << std::setfill('0') << std::setw(6) << std::hex, old); if (i < n - 1) os << ", "; } os << std::dec << ">> "; @@ -1501,7 +1501,7 @@ std::ostream& expression_t::print(std::ostream& os, bool old) const os << "[["; size_t n = get_player_count(); for (int i = 0; i < n; ++i) { - get(0).print(os, old); + get(i).print(os << "#" << std::setfill('0') << std::setw(6) << std::hex, old); if (i < n - 1) os << ", "; } os << "]] "; From 67ba0023cce3e950badb78ea023e4f65c672d063 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Thu, 21 Nov 2024 12:41:43 +0100 Subject: [PATCH 10/16] Add nested ATL formula --- CMakeLists.txt | 2 +- src/parser.y | 66 ++++++++++++++++++++++++++------------------ src/typechecker.cpp | 2 ++ test/test_parser.cpp | 32 ++++++++++++++++++++- 4 files changed, 73 insertions(+), 29 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index f5695a60..71a10d23 100644 --- a/CMakeLists.txt +++ b/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}") \ No newline at end of file diff --git a/src/parser.y b/src/parser.y index b0c6e5d7..607747a3 100644 --- a/src/parser.y +++ b/src/parser.y @@ -1393,6 +1393,44 @@ DynamicExpression: } ; +AtlExpressionOrExpression: + '(' AtlExpression ')' + // FIXME: Fix ambiguity and remove ugly parenthesis + | '(' AtlExpression ')' T_BOOL_AND AtlExpressionOrExpression { + CALL(@1, @5, expr_binary(AND)); + } + // FIXME: Fix ambiguity and remove ugly parenthesis + | '(' AtlExpression ')' T_BOOL_OR AtlExpressionOrExpression { + CALL(@1, @5, expr_binary(OR)); + } + | Expression; + +AtlExpression: + T_LSHIFT PlayerColorList T_RSHIFT '[' AtlExpressionOrExpression 'U' AtlExpressionOrExpression ']' { + CALL(@1, @8, expr_atl($2, ATL_ENFORCE_UNTIL)); + } + | T_LBRBR PlayerColorList T_RBRBR '[' AtlExpressionOrExpression 'U' AtlExpressionOrExpression ']' { + CALL(@1, @8, expr_atl($2, ATL_DESPITE_UNTIL)); + } + | T_LSHIFT PlayerColorList T_RSHIFT T_DIAMOND AtlExpressionOrExpression { + CALL(@1, @5, expr_atl($2, ATL_ENFORCE_F)); + } + | T_LBRBR PlayerColorList T_RBRBR T_DIAMOND AtlExpressionOrExpression { + CALL(@1, @5, expr_atl($2, ATL_DESPITE_F)); + } + | T_LSHIFT PlayerColorList T_RSHIFT T_BOX AtlExpressionOrExpression { + CALL(@1, @5, expr_atl($2, ATL_ENFORCE_G)); + } + | T_LBRBR PlayerColorList T_RBRBR T_BOX AtlExpressionOrExpression { + CALL(@1, @5, expr_atl($2, ATL_DESPITE_G)); + } + | T_LSHIFT PlayerColorList T_RSHIFT 'X' AtlExpressionOrExpression { + CALL(@1, @5, expr_atl($2, ATL_ENFORCE_NEXT)); + } + | T_LBRBR PlayerColorList T_RBRBR 'X' AtlExpressionOrExpression { + CALL(@1, @5, expr_atl($2, ATL_DESPITE_NEXT)); + } +; Assignment: Expression AssignOp Expression { @@ -1749,34 +1787,8 @@ Query: BoolOrKWAnd: T_KW_AND | T_BOOL_AND; -SubPropertyOrExpression: - SubProperty | Expression; - SubProperty: - T_LSHIFT PlayerColorList T_RSHIFT '[' SubPropertyOrExpression 'U' SubPropertyOrExpression ']' { - CALL(@1, @8, expr_atl($2, ATL_ENFORCE_UNTIL)); - } - | T_LBRBR PlayerColorList T_RBRBR '[' SubPropertyOrExpression 'U' SubPropertyOrExpression ']' { - CALL(@1, @8, expr_atl($2, ATL_DESPITE_UNTIL)); - } - | T_LSHIFT PlayerColorList T_RSHIFT T_DIAMOND SubPropertyOrExpression { - CALL(@1, @5, expr_atl($2, ATL_ENFORCE_F)); - } - | T_LBRBR PlayerColorList T_RBRBR T_DIAMOND SubPropertyOrExpression { - CALL(@1, @5, expr_atl($2, ATL_DESPITE_F)); - } - | T_LSHIFT PlayerColorList T_RSHIFT T_BOX SubPropertyOrExpression { - CALL(@1, @5, expr_atl($2, ATL_ENFORCE_G)); - } - | T_LBRBR PlayerColorList T_RBRBR T_BOX SubPropertyOrExpression { - CALL(@1, @5, expr_atl($2, ATL_DESPITE_G)); - } - | T_LSHIFT PlayerColorList T_RSHIFT 'X' SubPropertyOrExpression { - CALL(@1, @5, expr_atl($2, ATL_ENFORCE_NEXT)); - } - | T_LBRBR PlayerColorList T_RBRBR 'X' SubPropertyOrExpression { - CALL(@1, @5, expr_atl($2, ATL_DESPITE_NEXT)); - } + AtlExpression | T_AF Expression { CALL(@1, @2, expr_unary(AF)); } diff --git a/src/typechecker.cpp b/src/typechecker.cpp index 6b3d1a8d..f3e7d01f 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -1778,6 +1778,8 @@ bool TypeChecker::checkExpression(expression_t expr) type = type_t::create_primitive(GUARD); } else if (is_constraint(expr[0]) && is_constraint(expr[1])) { type = type_t::create_primitive(CONSTRAINT); + } else if (is_formula(expr[0]) && is_formula(expr[1])) { + type = type_t::create_primitive(FORMULA); } break; diff --git a/test/test_parser.cpp b/test/test_parser.cpp index 82c8c049..9233e0c7 100644 --- a/test/test_parser.cpp +++ b/test/test_parser.cpp @@ -554,7 +554,7 @@ TEST_CASE("T-ALT properties") } SUBCASE("Basic DespiteUntil property") { - auto res = parseProperty("[[red, green]] [ true U false ]", builder.get()); + auto res = parseProperty("[[ red, green ]] [ true U false ]", builder.get()); REQUIRE(res == 0); REQUIRE(doc->get_errors().empty()); auto expr = &builder->getProperties().front(); @@ -634,4 +634,34 @@ TEST_CASE("T-ALT properties") REQUIRE(res == 0); CHECK(doc->get_errors().size() == 1); } + SUBCASE("Nested ATL until property") + { + auto res = parseProperty("<> [(<> <> true) U false]", builder.get()); + REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); + auto expr = &builder->getProperties().front(); + CHECK(expr->intermediate.get_size() == 3); + CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_UNTIL); + CHECK(expr->type == UTAP::quant_t::Atl); + } + SUBCASE("Nested ATL eventually property") + { + auto res = parseProperty("<> <> ([[blue]] <> false)", builder.get()); + REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); + auto expr = &builder->getProperties().front(); + CHECK(expr->intermediate.get_size() == 2); + CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_F); + CHECK(expr->type == UTAP::quant_t::Atl); + } + SUBCASE("Nested ATL property with logical operators") + { + auto res = parseProperty("<> <> (<> [] false && true) || ([[black]] [(<> <> true) && true U false])", builder.get()); + REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); + auto expr = &builder->getProperties().front(); + CHECK(expr->intermediate.get_size() == 2); + CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_F); + CHECK(expr->type == UTAP::quant_t::Atl); + } } \ No newline at end of file From 2752a159ee28c45ce901c5b508a981f7d71d4da8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Fri, 22 Nov 2024 14:16:56 +0100 Subject: [PATCH 11/16] Add negated ATL formula --- src/parser.y | 10 ++++++++-- src/typechecker.cpp | 2 ++ test/test_parser.cpp | 10 ++++++++++ 3 files changed, 20 insertions(+), 2 deletions(-) diff --git a/src/parser.y b/src/parser.y index 607747a3..ba94146e 100644 --- a/src/parser.y +++ b/src/parser.y @@ -1396,13 +1396,16 @@ DynamicExpression: AtlExpressionOrExpression: '(' AtlExpression ')' // FIXME: Fix ambiguity and remove ugly parenthesis - | '(' AtlExpression ')' T_BOOL_AND AtlExpressionOrExpression { + | '(' AtlExpression ')' BoolOrKWAnd AtlExpressionOrExpression { CALL(@1, @5, expr_binary(AND)); } // FIXME: Fix ambiguity and remove ugly parenthesis - | '(' AtlExpression ')' T_BOOL_OR AtlExpressionOrExpression { + | '(' AtlExpression ')' BoolOrKWOr AtlExpressionOrExpression { CALL(@1, @5, expr_binary(OR)); } + | T_KW_NOT '(' AtlExpression ')' { + CALL(@1, @4, expr_unary(NOT)); + } | Expression; AtlExpression: @@ -1787,6 +1790,9 @@ Query: BoolOrKWAnd: T_KW_AND | T_BOOL_AND; +BoolOrKWOr: + T_KW_OR | T_BOOL_OR; + SubProperty: AtlExpression | T_AF Expression { diff --git a/src/typechecker.cpp b/src/typechecker.cpp index f3e7d01f..0483c712 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -1928,6 +1928,8 @@ bool TypeChecker::checkExpression(expression_t expr) type = type_t::create_primitive(Constants::BOOL); } else if (is_constraint(expr[0])) { type = type_t::create_primitive(CONSTRAINT); + } else if (is_formula(expr[0])) { + type = type_t::create_primitive(FORMULA); } break; diff --git a/test/test_parser.cpp b/test/test_parser.cpp index 9233e0c7..9c1e695c 100644 --- a/test/test_parser.cpp +++ b/test/test_parser.cpp @@ -654,6 +654,16 @@ TEST_CASE("T-ALT properties") CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_F); CHECK(expr->type == UTAP::quant_t::Atl); } + SUBCASE("Nested ATL property with negation") + { + auto res = parseProperty("<> <> not ([[blue]] <> false)", builder.get()); + REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); + auto expr = &builder->getProperties().front(); + CHECK(expr->intermediate.get_size() == 2); + CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_F); + CHECK(expr->type == UTAP::quant_t::Atl); + } SUBCASE("Nested ATL property with logical operators") { auto res = parseProperty("<> <> (<> [] false && true) || ([[black]] [(<> <> true) && true U false])", builder.get()); From 8e18f2d08ba7f320532ba7f861014105f1968418 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Tue, 10 Dec 2024 15:04:34 +0100 Subject: [PATCH 12/16] Add freeze operator --- include/utap/common.h | 1 + src/expression.cpp | 1 + src/lexer.l | 6 +++--- src/parser.y | 6 +++++- src/property.cpp | 1 + src/typechecker.cpp | 13 +++++++++++++ test/test_parser.cpp | 15 ++++++++++++++- 7 files changed, 38 insertions(+), 5 deletions(-) diff --git a/include/utap/common.h b/include/utap/common.h index e2d1482f..45ed55f3 100644 --- a/include/utap/common.h +++ b/include/utap/common.h @@ -44,6 +44,7 @@ enum kind_t { MAX, RATE, FRACTION, + FREEZE, /******************************************************** * Relational operators diff --git a/src/expression.cpp b/src/expression.cpp index 4930587b..1402bff9 100644 --- a/src/expression.cpp +++ b/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: diff --git a/src/lexer.l b/src/lexer.l index b19c9c17..15de2e5c 100644 --- a/src/lexer.l +++ b/src/lexer.l @@ -90,6 +90,8 @@ idchr [a-zA-Z0-9_$#] "]" { return ']'; } "(" { return '('; } ")" { return ')'; } +"[[" { return T_LBRBR; } +"]]" { return T_RBRBR; } "?" { return '?'; } "'" { return '\''; } "!" { return T_EXCLAM; } @@ -129,8 +131,6 @@ idchr [a-zA-Z0-9_$#] "&&" { return T_BOOL_AND; } "/\\" { return T_MITL_AND; } "\\/" { return T_MITL_OR; } -"[[" { return T_LBRBR; } -"]]" { return T_RBRBR; } "<=" { return T_LEQ; } ">=" { return T_GEQ; } @@ -152,9 +152,9 @@ 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'; } diff --git a/src/parser.y b/src/parser.y index ba94146e..63263dee 100644 --- a/src/parser.y +++ b/src/parser.y @@ -186,6 +186,7 @@ const char* utap_msg(const char *msg) %token T_OR T_XOR T_LSHIFT T_RSHIFT %token T_BOOL_AND T_BOOL_OR %token T_KW_AND T_KW_OR T_KW_XOR T_KW_IMPLY T_KW_NOT +%token T_FREEZE /* Special */ %token T_SUP T_INF T_BOUNDS @@ -1409,7 +1410,10 @@ AtlExpressionOrExpression: | Expression; AtlExpression: - T_LSHIFT PlayerColorList T_RSHIFT '[' AtlExpressionOrExpression 'U' AtlExpressionOrExpression ']' { + NonTypeId { CALL(@1, @1, expr_identifier($1)); } T_FREEZE AtlExpressionOrExpression { + CALL(@1, @3, expr_binary(FREEZE)); + } + | T_LSHIFT PlayerColorList T_RSHIFT '[' AtlExpressionOrExpression 'U' AtlExpressionOrExpression ']' { CALL(@1, @8, expr_atl($2, ATL_ENFORCE_UNTIL)); } | T_LBRBR PlayerColorList T_RBRBR '[' AtlExpressionOrExpression 'U' AtlExpressionOrExpression ']' { diff --git a/src/property.cpp b/src/property.cpp index 7fd9a1f5..abda815f 100644 --- a/src/property.cpp +++ b/src/property.cpp @@ -490,6 +490,7 @@ void AtlPropertyBuilder::typeProperty(UTAP::expression_t expr) case ATL_DESPITE_G: case ATL_ENFORCE_NEXT: case ATL_DESPITE_NEXT: + case FREEZE: properties.back().type = quant_t::Atl; break; default: diff --git a/src/typechecker.cpp b/src/typechecker.cpp index 0483c712..a55ca576 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -1002,6 +1002,7 @@ static bool isGameProperty(expression_t expr) case ATL_DESPITE_G: case ATL_ENFORCE_NEXT: case ATL_DESPITE_NEXT: + case FREEZE: case CONTROL: case SMC_CONTROL: case EF_CONTROL: @@ -1789,6 +1790,18 @@ bool TypeChecker::checkExpression(expression_t expr) } break; + case FREEZE: + if (!is_clock(expr[0])) { + handleError(expr, "Left-hand side of freeze operator must be a clock"); + return false; + } + if (!is_formula(expr[1])) { + handleError(expr, "Right-hand side of freeze operator must be a formula"); + return false; + } + type = type_t::create_primitive(FORMULA); + break; + case SPAWN: { template_t* temp = document.find_dynamic_template(expr[0].get_symbol().get_name()); if (!temp) { diff --git a/test/test_parser.cpp b/test/test_parser.cpp index 9c1e695c..ece4df38 100644 --- a/test/test_parser.cpp +++ b/test/test_parser.cpp @@ -674,4 +674,17 @@ TEST_CASE("T-ALT properties") CHECK(expr->intermediate.get_kind() == UTAP::Constants::ATL_ENFORCE_F); CHECK(expr->type == UTAP::quant_t::Atl); } -} \ No newline at end of file +} + +TEST_CASE("Freeze operator") +{ + auto doc = document_fixture{} + .add_global_decl("clock x;") + .add_default_process() + .parse(); + + auto builder = std::make_unique(*doc); + auto res = parseProperty("x ¤ true", builder.get()); + REQUIRE(res == 0); + REQUIRE(doc->get_errors().empty()); +} From 362ce302fc0f18ed910faf54ca03c908c5af4c9a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98sterby=20Jensen?= Date: Thu, 12 Dec 2024 14:31:21 +0100 Subject: [PATCH 13/16] Fix nested array subscripting not parsing correctly --- src/lexer.l | 2 -- src/parser.y | 21 +++++++++------------ 2 files changed, 9 insertions(+), 14 deletions(-) diff --git a/src/lexer.l b/src/lexer.l index 15de2e5c..d0fcfb03 100644 --- a/src/lexer.l +++ b/src/lexer.l @@ -90,8 +90,6 @@ idchr [a-zA-Z0-9_$#] "]" { return ']'; } "(" { return '('; } ")" { return ')'; } -"[[" { return T_LBRBR; } -"]]" { return T_RBRBR; } "?" { return '?'; } "'" { return '\''; } "!" { return T_EXCLAM; } diff --git a/src/parser.y b/src/parser.y index 63263dee..1b018e92 100644 --- a/src/parser.y +++ b/src/parser.y @@ -284,9 +284,6 @@ const char* utap_msg(const char *msg) %token T_DYNAMIC T_HYBRID %token T_SPAWN T_EXIT T_NUMOF -/* ATL */ -%token T_LBRBR T_RBRBR - %type ExpQuantifier ExpPrQuantifier %type PathType %type ArgList FieldDeclList FieldDeclIdList FieldDecl @@ -321,7 +318,7 @@ const char* utap_msg(const char *msg) %left T_POWOP %right T_EXCLAM T_KW_NOT UOPERATOR %right T_INCREMENT T_DECREMENT -%left '(' ')' '[' ']' '.' '\'' T_LBRBR T_RBRBR +%left '(' ')' '[' ']' '.' '\'' %union { @@ -1416,26 +1413,26 @@ AtlExpression: | T_LSHIFT PlayerColorList T_RSHIFT '[' AtlExpressionOrExpression 'U' AtlExpressionOrExpression ']' { CALL(@1, @8, expr_atl($2, ATL_ENFORCE_UNTIL)); } - | T_LBRBR PlayerColorList T_RBRBR '[' AtlExpressionOrExpression 'U' AtlExpressionOrExpression ']' { - CALL(@1, @8, expr_atl($2, ATL_DESPITE_UNTIL)); + | '[' '[' PlayerColorList ']' ']' '[' AtlExpressionOrExpression 'U' AtlExpressionOrExpression ']' { + CALL(@1, @10, expr_atl($3, ATL_DESPITE_UNTIL)); } | T_LSHIFT PlayerColorList T_RSHIFT T_DIAMOND AtlExpressionOrExpression { CALL(@1, @5, expr_atl($2, ATL_ENFORCE_F)); } - | T_LBRBR PlayerColorList T_RBRBR T_DIAMOND AtlExpressionOrExpression { - CALL(@1, @5, expr_atl($2, ATL_DESPITE_F)); + | '[' '[' PlayerColorList ']' ']' T_DIAMOND AtlExpressionOrExpression { + CALL(@1, @7, expr_atl($3, ATL_DESPITE_F)); } | T_LSHIFT PlayerColorList T_RSHIFT T_BOX AtlExpressionOrExpression { CALL(@1, @5, expr_atl($2, ATL_ENFORCE_G)); } - | T_LBRBR PlayerColorList T_RBRBR T_BOX AtlExpressionOrExpression { - CALL(@1, @5, expr_atl($2, ATL_DESPITE_G)); + | '[' '[' PlayerColorList ']' ']' T_BOX AtlExpressionOrExpression { + CALL(@1, @7, expr_atl($3, ATL_DESPITE_G)); } | T_LSHIFT PlayerColorList T_RSHIFT 'X' AtlExpressionOrExpression { CALL(@1, @5, expr_atl($2, ATL_ENFORCE_NEXT)); } - | T_LBRBR PlayerColorList T_RBRBR 'X' AtlExpressionOrExpression { - CALL(@1, @5, expr_atl($2, ATL_DESPITE_NEXT)); + | '[' '[' PlayerColorList ']' ']' 'X' AtlExpressionOrExpression { + CALL(@1, @7, expr_atl($3, ATL_DESPITE_NEXT)); } ; From 4179ebae295e151c4dfeab0359b69c6757e3d9fd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98=20Jensen?= Date: Thu, 30 Oct 2025 15:58:46 +0100 Subject: [PATCH 14/16] Make freeze operator printable --- src/expression.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/expression.cpp b/src/expression.cpp index 1402bff9..a52dd908 100644 --- a/src/expression.cpp +++ b/src/expression.cpp @@ -1464,6 +1464,8 @@ 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: From 14f33f002b421abd935a862462feb39a1e8c90c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98=20Jensen?= Date: Wed, 5 Nov 2025 15:34:38 +0100 Subject: [PATCH 15/16] Add missing #include --- src/typechecker.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/typechecker.cpp b/src/typechecker.cpp index a55ca576..e8980608 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -26,6 +26,7 @@ #include "utap/utap.h" #include +#include using namespace UTAP; using namespace Constants; From d6b5c98133781110ed3864c6becc94a2c2ece463 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolaj=20=C3=98=20Jensen?= Date: Wed, 5 Nov 2025 15:36:44 +0100 Subject: [PATCH 16/16] Change freeze operator to @ --- src/expression.cpp | 2 +- src/lexer.l | 3 ++- test/test_parser.cpp | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/expression.cpp b/src/expression.cpp index a52dd908..897fe24b 100644 --- a/src/expression.cpp +++ b/src/expression.cpp @@ -1464,7 +1464,7 @@ 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 FREEZE: os << get(0) << " @ " << get(1); break; case ATL_ENFORCE_UNTIL: case ATL_ENFORCE_F: diff --git a/src/lexer.l b/src/lexer.l index d0fcfb03..cb5358da 100644 --- a/src/lexer.l +++ b/src/lexer.l @@ -152,7 +152,8 @@ idchr [a-zA-Z0-9_$#] "!=" { return T_NEQ; } "++" { return T_INCREMENT; } "--" { return T_DECREMENT; } -"¤" { return T_FREEZE; } + +"@" { return T_FREEZE; } "A" { return 'A'; } "U" { return 'U'; } diff --git a/test/test_parser.cpp b/test/test_parser.cpp index ece4df38..50c7254c 100644 --- a/test/test_parser.cpp +++ b/test/test_parser.cpp @@ -684,7 +684,7 @@ TEST_CASE("Freeze operator") .parse(); auto builder = std::make_unique(*doc); - auto res = parseProperty("x ¤ true", builder.get()); + auto res = parseProperty("x @ true", builder.get()); REQUIRE(res == 0); REQUIRE(doc->get_errors().empty()); }