From c7e2ca7fee424ab062d135c0aae51541cdc91ddf Mon Sep 17 00:00:00 2001 From: Asger Horn Brorholt Date: Tue, 18 Feb 2025 11:45:30 +0100 Subject: [PATCH 1/7] Add HYPA "enforce" query --- include/utap/AbstractBuilder.hpp | 4 +++ include/utap/ExpressionBuilder.hpp | 4 +++ include/utap/builder.h | 4 +++ include/utap/common.h | 9 +++++ include/utap/property.h | 5 ++- src/ExpressionBuilder.cpp | 32 ++++++++++++++++++ src/abstractbuilder.cpp | 4 +++ src/expression.cpp | 40 ++++++++++++++++++++++ src/keywords.cpp | 1 + src/parser.y | 43 +++++++++++++++++++++++- src/property.cpp | 1 + src/type.cpp | 3 ++ src/typechecker.cpp | 41 ++++++++++++++++++++++- test/test_prettyprint.cpp | 54 ++++++++++++++++++++++++++++++ 14 files changed, 242 insertions(+), 3 deletions(-) diff --git a/include/utap/AbstractBuilder.hpp b/include/utap/AbstractBuilder.hpp index 1b43870a..80b42001 100644 --- a/include/utap/AbstractBuilder.hpp +++ b/include/utap/AbstractBuilder.hpp @@ -284,6 +284,10 @@ class AbstractBuilder : public ParserBuilder void expr_MITL_exists_dynamic_begin(const char*, const char*) override; void expr_MITL_exists_dynamic_end(const char* name) override; + void expr_enforce() override; + void expr_discrete_interval() override; + void expr_interval(int32_t divisions) override; + /** Verification queries */ void model_option(const char* key, const char* value) override; void query_begin() override; diff --git a/include/utap/ExpressionBuilder.hpp b/include/utap/ExpressionBuilder.hpp index 88d469ec..db0deffa 100644 --- a/include/utap/ExpressionBuilder.hpp +++ b/include/utap/ExpressionBuilder.hpp @@ -206,6 +206,10 @@ class ExpressionBuilder : public AbstractBuilder void expr_MITL_diamond(int, int) override; void expr_MITL_box(int, int) override; + void expr_enforce() override; + void expr_discrete_interval() override; + void expr_interval(int32_t divisions) override; + /* Dynamic process creation */ void expr_spawn(int params) override; void expr_exit() override; diff --git a/include/utap/builder.h b/include/utap/builder.h index 32f903bf..71c9022e 100644 --- a/include/utap/builder.h +++ b/include/utap/builder.h @@ -430,6 +430,10 @@ class ParserBuilder virtual void expr_MITL_exists_dynamic_end(const char* name) = 0; virtual void expr_dynamic_process_expr(const char*) = 0; + virtual void expr_enforce() = 0; + virtual void expr_discrete_interval() = 0; + virtual void expr_interval(int32_t divisions) = 0; + /** Verification queries */ virtual void model_option(const char* key, const char* value) = 0; virtual void query_begin() = 0; diff --git a/include/utap/common.h b/include/utap/common.h index 1341e605..457294d5 100644 --- a/include/utap/common.h +++ b/include/utap/common.h @@ -278,6 +278,15 @@ enum kind_t { MITL_ATOM, MITL_EXISTS, MITL_FORALL, + + /****************************************************** + * HYPA + */ + ENFORCE, + DISCRETE_INTERVAL, + INTERVAL, + INTERVAL_LIST, + /*Dynamic */ SPAWN, EXIT, diff --git a/include/utap/property.h b/include/utap/property.h index dedaa79f..0584e1c0 100644 --- a/include/utap/property.h +++ b/include/utap/property.h @@ -108,7 +108,10 @@ enum class quant_t { PMax, /* LSC scenario property */ - scenario + scenario, + + /* HYPA: enforce : ... {} -> {} */ + enforce, }; /** property status */ diff --git a/src/ExpressionBuilder.cpp b/src/ExpressionBuilder.cpp index e07181a9..2362c721 100644 --- a/src/ExpressionBuilder.cpp +++ b/src/ExpressionBuilder.cpp @@ -917,6 +917,38 @@ void ExpressionBuilder::expr_MITL_box(int low, int high) fragments.push(form); } +void ExpressionBuilder::expr_enforce() +{ + const auto partition = fragments[0]; + assert(partition.get_kind() == INTERVAL_LIST); + const auto to_enforce = fragments[1]; + fragments.pop(2); + fragments.push(expression_t::create_binary(ENFORCE, 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_t::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_t::create_constant(divisions, position); + auto args = std::vector{identifier, lower, upper, divisions2}; + const auto interval = expression_t::create_nary(INTERVAL, std::move(args), position); + fragments.push(interval); +} + void ExpressionBuilder::expr_MITL_disj() { auto& left = fragments[1]; diff --git a/src/abstractbuilder.cpp b/src/abstractbuilder.cpp index 08621726..c1cb42f8 100644 --- a/src/abstractbuilder.cpp +++ b/src/abstractbuilder.cpp @@ -276,6 +276,10 @@ void AbstractBuilder::expr_MITL_forall_dynamic_end(const char* name) { UNSUPPORT void AbstractBuilder::expr_MITL_exists_dynamic_begin(const char*, const char*) { UNSUPPORTED; } void AbstractBuilder::expr_MITL_exists_dynamic_end(const char* name) { UNSUPPORTED; } +void AbstractBuilder::expr_enforce() { 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(const char*, const char*) { UNSUPPORTED; } diff --git a/src/expression.cpp b/src/expression.cpp index af2e7499..e13869af 100644 --- a/src/expression.cpp +++ b/src/expression.cpp @@ -440,6 +440,7 @@ size_t expression_t::get_size() const case FUN_CALL: case FUN_CALL_EXT: case LIST: + case INTERVAL_LIST: case SIMULATE: case SIMULATEREACH: case SPAWN: return std::get(data->value); @@ -492,6 +493,9 @@ size_t expression_t::get_size() const case MITL_FORALL: case FOREACH_DYNAMIC: assert(data->sub.size() == 3); return 3; case DYNAMIC_EVAL: assert(data->sub.size() == 2); return 2; + case ENFORCE: assert(data->sub.size() == 2); return 2; + case DISCRETE_INTERVAL: assert(data->sub.size() == 3); return 3; + case INTERVAL: assert(data->sub.size() == 4); return 4; default: assert(0); return 0; } } @@ -1662,6 +1666,42 @@ std::ostream& expression_t::print(std::ostream& os, bool old) const break; case TYPEDEF: os << "typedef"; break; + case ENFORCE: + os << "enforce: "; + get(0).print(os, old); + get(1).print(os, old); + break; + + case INTERVAL_LIST: + os << " { "; + for (size_t i = 0; i < get_size(); ++i) { + get(i).print(os, old); + if (i + 1 < get_size()) { + os << ", "; + } + } + os << " }"; + break; + + case INTERVAL: + get(0).print(os, old); + os << "["; + get(1).print(os, old); + os << ", "; + get(2).print(os, old); + os << "]:"; + get(3).print(os, old); + break; + + case DISCRETE_INTERVAL: + get(0).print(os, old); + os << "["; + get(1).print(os, old); + os << ", "; + get(2).print(os, old); + os << "]"; + break; + // Types - Not applicable in expression printing case RANGE: case RECORD: diff --git a/src/keywords.cpp b/src/keywords.cpp index 9c2903b8..ffbadd60 100644 --- a/src/keywords.cpp +++ b/src/keywords.cpp @@ -149,6 +149,7 @@ namespace UTAP { {"foreach", Keyword{T_FOREACH, syntax_t::PROPERTY}}, {"query", Keyword{T_QUERY, syntax_t::NEW}}, {"location", Keyword{T_LOCATION, syntax_t::NEW}}, + {"enforce", Keyword{T_ENFORCE, syntax_t::NEW_PROPERTY}}, }; // clang-format on diff --git a/src/parser.y b/src/parser.y index 265b992e..fa87fcaa 100644 --- a/src/parser.y +++ b/src/parser.y @@ -283,11 +283,15 @@ const char* utap_msg(const char *msg) %token T_DYNAMIC T_HYBRID %token T_SPAWN T_EXIT T_NUMOF +/* HYPA */ +%token T_ENFORCE + %type ExpQuantifier ExpPrQuantifier %type PathType %type ArgList FieldDeclList FieldDeclIdList FieldDecl %type ParameterList FieldInitList %type OptionalInstanceParameterList ExpressionList NonEmptyExpressionList +%type IntervalList NonEmptyIntervalList %type Type TypePrefix %type Id NonTypeId %type UnaryOp AssignOp @@ -1768,6 +1772,40 @@ Features: { } | BracketExprList T_ARROW BracketExprList; + +/* Binary tree inspired by BracketExprList */ +BracketIntervalList: + '{' IntervalList '}' { + CALL(@1, @3, expr_nary(INTERVAL_LIST, $2)); + } + ; + +/* $$ is number of intervals in the list. */ +IntervalList: + /* empty */ { $$ = 0; } + | NonEmptyIntervalList + ; + +NonEmptyIntervalList: + Interval { $$ = 1; } + | NonEmptyIntervalList ',' Interval { $$ = $1 + 1; } + ; + +Interval: + T_ID '[' Expression ',' Expression ']' { + CALL(@1, @1, expr_identifier($1)); + CALL(@1, @6, expr_discrete_interval()); + } + | T_ID '[' Expression ',' Expression ']' ':' T_NAT { + CALL(@1, @1, expr_identifier($1)); + CALL(@1, @8, expr_interval($8)); + } + ; + + +Partition: + | BracketIntervalList; + AssignablePropperty: T_CONTROL ':' SubProperty Subjection { CALL(@1, @3, expr_unary(CONTROL)); @@ -1789,6 +1827,10 @@ AssignablePropperty: CALL(@1, @4, expr_unary(EF_CONTROL)); CALL(@1, @4, property()); } + | T_ENFORCE ':' Expression Partition { + CALL(@1, @4, expr_enforce()); + CALL(@1, @4, property()); + } | BracketExprList T_CONTROL ':' SubProperty Subjection { CALL(@1, @4, expr_binary(PO_CONTROL)); CALL(@1, @4, property()); @@ -1985,7 +2027,6 @@ Property: CALL(@1, @2, expr_binary(BOUNDS_VAR)); CALL(@1, @2, property()); }; - %% #include "lexer.cc" diff --git a/src/property.cpp b/src/property.cpp index 6f174190..ef5ba53c 100644 --- a/src/property.cpp +++ b/src/property.cpp @@ -230,6 +230,7 @@ void PropertyBuilder::typeProperty(expression_t expr) // NOLINT prob = true; break; case MITL_FORMULA: properties.back().type = quant_t::Mitl; break; + case ENFORCE: properties.back().type = quant_t::enforce; break; default: throw UTAP::TypeException("$Invalid_property_type"); prob = true; } diff --git a/src/type.cpp b/src/type.cpp index def9be47..41d5d98a 100644 --- a/src/type.cpp +++ b/src/type.cpp @@ -134,6 +134,9 @@ bool type_t::is_prefix() const case Constants::TYPEDEF: case Constants::LABEL: case Constants::RATE: + case Constants::INTERVAL: + case Constants::DISCRETE_INTERVAL: + case Constants::INTERVAL_LIST: case Constants::INSTANCE_LINE: // LSC case Constants::MESSAGE: // LSC case Constants::CONDITION: // LSC diff --git a/src/typechecker.cpp b/src/typechecker.cpp index 553f3463..9ea19372 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -181,6 +181,17 @@ static bool isAssignable(type_t type) } } +static bool is_interval_list(expression_t expression) +{ + const auto n_expressions = expression.get_size(); + for (size_t i = 0; i < n_expressions; ++i) { + if (!(expression[i].get_type().is(INTERVAL) || expression[i].get_type().is(DISCRETE_INTERVAL))) + return false; + } + + return true; +} + /////////////////////////////////////////////////////////////////////////// void CompileTimeComputableValues::visitVariable(variable_t& variable) @@ -1000,7 +1011,8 @@ static bool isGameProperty(expression_t expr) case CONTROL_TOPT: case PO_CONTROL: case CONTROL_TOPT_DEF1: - case CONTROL_TOPT_DEF2: return true; + case CONTROL_TOPT_DEF2: + case ENFORCE: return true; default: return false; } } @@ -2242,6 +2254,33 @@ bool TypeChecker::checkExpression(expression_t expr) } break; + case INTERVAL_LIST: + if (is_interval_list(expr)) { + type = type_t::create_primitive(INTERVAL_LIST); + } + break; + + case INTERVAL: { + const auto e0 = expr[0].get_type(); + const auto e1 = expr[1].get_type(); + const auto e2 = expr[2].get_type(); + if ((e0.is_integer() || e0.is_double()) && (e1.is_integer() || e1.is_double()) && e2.is_integer()) { + type = type_t::create_primitive(INTERVAL); + } + } break; + + case DISCRETE_INTERVAL: + if (expr[0].get_type().is_integer() && expr[1].get_type().is_integer()) { + type = type_t::create_primitive(DISCRETE_INTERVAL); + } + break; + + case ENFORCE: + if (expr[0].get_type().is_integral() && is_interval_list(expr[1])) { + type = type_t::create_primitive(FORMULA); + } + break; + case LEADS_TO: case SCENARIO2: case A_UNTIL: diff --git a/test/test_prettyprint.cpp b/test/test_prettyprint.cpp index fb1f6c50..6501ff5f 100644 --- a/test/test_prettyprint.cpp +++ b/test/test_prettyprint.cpp @@ -321,4 +321,58 @@ TEST_CASE("Post incrementing an identifier should not require parenthesis") auto expr = expression_t::create_unary(Constants::POST_INCREMENT, id); CHECK(expr.str() == "foo++"); +} + +TEST_CASE("Enforce query") +{ + auto f = document_fixture{} + .add_default_process() + .add_system_decl("bool myBool;") + .add_system_decl("int myInt;") + .add_system_decl("int[1, 10] myConstrainedInt;") + .add_system_decl("double myDouble;") + .add_system_decl("clock myClock;") + .add_system_decl("chan MyChannel;") + .build_query_fixture(); + + const auto foo = f.get_errors(); + REQUIRE(f.get_errors().empty()); + + SUBCASE("Correct types") + { + // NB: Whitespace is significant since it must match the pretty-printer. + const std::string query_string = "enforce: myDouble < 1 " + "{ " + "myInt[2 + 2, 10], " + "myConstrainedInt[1, 2 * 5], " + "myDouble[M_PI, 21 * 100]:100 " + "}"; + + auto query1 = f.parse_query(query_string.data()).intermediate; + + REQUIRE(query1.get_kind() == UTAP::Constants::ENFORCE); + CHECK(query_string == query1.str()); + } + + SUBCASE("Invalid condition to enforce") + { + const auto query_string = "enforce: (-2.2) { }"; + REQUIRE_THROWS_WITH(f.parse_query(query_string).intermediate, "$Type_error"); + + const auto query_string2 = "enforce: myChannel { }"; + REQUIRE_THROWS_WITH(f.parse_query(query_string2).intermediate, "$Type_error"); + } + + SUBCASE("Invalid number of divisions") + { + const auto query_string = "enforce: myDouble < 1 { myDouble[M_PI, 21 * 100]:1.5 }"; + REQUIRE_THROWS_WITH(f.parse_query(query_string), "$syntax_error: $unexpected T_FLOATING, $expecting T_NAT"); + + // Don't know why it still says "T_FLOATING" here. + const auto query_string2 = "enforce: myDouble < 1 { myDouble[M_PI, 21 * 100]:myChannel }"; + REQUIRE_THROWS_WITH(f.parse_query(query_string2), "$syntax_error: $unexpected T_FLOATING, $expecting T_NAT"); + + const auto query_string3 = "enforce: myDouble < 1 { myDouble[M_PI, 21 * 100]:myClock }"; + REQUIRE_THROWS_WITH(f.parse_query(query_string3), "$syntax_error: $unexpected T_FLOATING, $expecting T_NAT"); + } } \ No newline at end of file From e27523d38189e84162362f061235bb9bc33fc827 Mon Sep 17 00:00:00 2001 From: Asger Horn Brorholt Date: Wed, 19 Feb 2025 13:23:00 +0100 Subject: [PATCH 2/7] Allow clocks --- src/typechecker.cpp | 9 +++++---- test/test_prettyprint.cpp | 16 ++++++++++++++++ 2 files changed, 21 insertions(+), 4 deletions(-) diff --git a/src/typechecker.cpp b/src/typechecker.cpp index 9ea19372..5a08d5e9 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -2261,10 +2261,11 @@ bool TypeChecker::checkExpression(expression_t expr) break; case INTERVAL: { - const auto e0 = expr[0].get_type(); - const auto e1 = expr[1].get_type(); - const auto e2 = expr[2].get_type(); - if ((e0.is_integer() || e0.is_double()) && (e1.is_integer() || e1.is_double()) && e2.is_integer()) { + const auto lower = expr[0].get_type(); + const auto upper = expr[1].get_type(); + const auto divisions = expr[2].get_type(); + if ((lower.is_integer() || lower.is_double() || lower.is_clock()) && + (upper.is_integer() || upper.is_double() || upper.is_clock()) && divisions.is_integer()) { type = type_t::create_primitive(INTERVAL); } } break; diff --git a/test/test_prettyprint.cpp b/test/test_prettyprint.cpp index 6501ff5f..14c6a05a 100644 --- a/test/test_prettyprint.cpp +++ b/test/test_prettyprint.cpp @@ -354,6 +354,22 @@ TEST_CASE("Enforce query") CHECK(query_string == query1.str()); } + SUBCASE("Mixing some clocks in there") + { + // Expressions involving clocks typecheck as invariants. + // Invariants aren't considered boolean expressions for some reason. I don't consider this my problem. + // The workaround is to add a floating-point number to the clock to appease the type checker. + const std::string query_string = "enforce: myClock + 0.0 < 10 && myClock + 0.0 > 0 { myClock[-1, 10]:100 }"; + + auto query1 = f.parse_query(query_string.data()).intermediate; + + // And then I have to respect that the prettyprinter prints `0` instead of `0.0` for doubles. + // Also not my problem. And no, adding `0` in the query does not work. + const std::string expected_string = "enforce: myClock + 0 < 10 && myClock + 0 > 0 { myClock[-1, 10]:100 }"; + REQUIRE(query1.get_kind() == UTAP::Constants::ENFORCE); + CHECK(expected_string == query1.str()); + } + SUBCASE("Invalid condition to enforce") { const auto query_string = "enforce: (-2.2) { }"; From 5dd44407956eacfc7819972f28d9ceac8975941f Mon Sep 17 00:00:00 2001 From: Asger Horn Brorholt Date: Tue, 25 Feb 2025 13:14:19 +0100 Subject: [PATCH 3/7] Remove this stupid assert --- src/ExpressionBuilder.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ExpressionBuilder.cpp b/src/ExpressionBuilder.cpp index 2362c721..329b7de3 100644 --- a/src/ExpressionBuilder.cpp +++ b/src/ExpressionBuilder.cpp @@ -750,7 +750,7 @@ void ExpressionBuilder::expr_load_strategy() void ExpressionBuilder::expr_save_strategy(const char* strategy_name) { - assert(fragments.size() == 1); + //assert(fragments.size() == 1); fragments[0] = expression_t::create_binary(SAVE_STRAT, fragments[0], make_constant(strategy_name), position); } From afc00bd6dfbf01d268e4209265d784c47db1fd11 Mon Sep 17 00:00:00 2001 From: Asger Horn Brorholt Date: Thu, 27 Feb 2025 10:50:12 +0100 Subject: [PATCH 4/7] Support of Locations in interval lists --- include/utap/AbstractBuilder.hpp | 1 + include/utap/ExpressionBuilder.hpp | 1 + include/utap/builder.h | 1 + src/ExpressionBuilder.cpp | 14 ++++++++++++++ src/abstractbuilder.cpp | 1 + src/parser.y | 3 +++ src/typechecker.cpp | 3 ++- test/test_prettyprint.cpp | 12 ++++++++++++ 8 files changed, 35 insertions(+), 1 deletion(-) diff --git a/include/utap/AbstractBuilder.hpp b/include/utap/AbstractBuilder.hpp index 80b42001..9622d0fb 100644 --- a/include/utap/AbstractBuilder.hpp +++ b/include/utap/AbstractBuilder.hpp @@ -180,6 +180,7 @@ class AbstractBuilder : public ParserBuilder void expr_false() override; void expr_double(double) override; void expr_string(const char*) override; + void expr_location(const char* name) override; void expr_location() override; void expr_identifier(const char* varName) override; void expr_nat(int32_t) override; // natural number diff --git a/include/utap/ExpressionBuilder.hpp b/include/utap/ExpressionBuilder.hpp index db0deffa..b80073c7 100644 --- a/include/utap/ExpressionBuilder.hpp +++ b/include/utap/ExpressionBuilder.hpp @@ -175,6 +175,7 @@ class ExpressionBuilder : public AbstractBuilder void expr_ternary(Constants::kind_t ternaryop, bool firstMissing) override; void expr_inline_if() override; void expr_comma() override; + void expr_location(const char* name); void expr_dot(const char*) override; void expr_deadlock() override; void expr_forall_begin(const char* name) override; diff --git a/include/utap/builder.h b/include/utap/builder.h index 71c9022e..fb78dcf8 100644 --- a/include/utap/builder.h +++ b/include/utap/builder.h @@ -319,6 +319,7 @@ class ParserBuilder virtual void expr_double(double) = 0; virtual void expr_string(const char* name) = 0; virtual void expr_identifier(const char* varName) = 0; + virtual void expr_location(const char* name) = 0; virtual void expr_location() = 0; virtual void expr_nat(int32_t) = 0; // natural number virtual void expr_call_begin() = 0; diff --git a/src/ExpressionBuilder.cpp b/src/ExpressionBuilder.cpp index 329b7de3..95e74d16 100644 --- a/src/ExpressionBuilder.cpp +++ b/src/ExpressionBuilder.cpp @@ -557,6 +557,20 @@ void ExpressionBuilder::expr_comma() fragments.push(expression_t::create_binary(COMMA, e1, e2, position, e2.get_type())); } +void ExpressionBuilder::expr_location(const char* name) +{ + + symbol_t uid; + + if (!resolve(name, uid)) { + expr_false(); + throw UnknownIdentifierError(name); + } + + fragments.push(expression_t::create_identifier(uid, position)); + expr_location(); +} + void ExpressionBuilder::expr_location() { expression_t expr = fragments[0]; diff --git a/src/abstractbuilder.cpp b/src/abstractbuilder.cpp index c1cb42f8..61a8fd56 100644 --- a/src/abstractbuilder.cpp +++ b/src/abstractbuilder.cpp @@ -199,6 +199,7 @@ void AbstractBuilder::expr_ternary(Constants::kind_t ternaryop, bool firstMissin void AbstractBuilder::expr_inline_if() { UNSUPPORTED; } void AbstractBuilder::expr_comma() { UNSUPPORTED; } void AbstractBuilder::expr_location() { UNSUPPORTED; } +void AbstractBuilder::expr_location(const char* name) { UNSUPPORTED; } void AbstractBuilder::expr_dot(const char*) { UNSUPPORTED; } void AbstractBuilder::expr_deadlock() { UNSUPPORTED; } void AbstractBuilder::expr_forall_begin(const char* name) { UNSUPPORTED; } diff --git a/src/parser.y b/src/parser.y index fa87fcaa..fee8e657 100644 --- a/src/parser.y +++ b/src/parser.y @@ -1800,6 +1800,9 @@ Interval: CALL(@1, @1, expr_identifier($1)); CALL(@1, @8, expr_interval($8)); } + | T_ID '.' T_LOCATION { + CALL(@1, @3, expr_location($1)); + } ; diff --git a/src/typechecker.cpp b/src/typechecker.cpp index 5a08d5e9..7bb12f32 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -185,7 +185,8 @@ static bool is_interval_list(expression_t expression) { const auto n_expressions = expression.get_size(); for (size_t i = 0; i < n_expressions; ++i) { - if (!(expression[i].get_type().is(INTERVAL) || expression[i].get_type().is(DISCRETE_INTERVAL))) + auto e = expression[i]; + if (!(e.get_type().is(INTERVAL) || e.get_type().is(DISCRETE_INTERVAL) || e.get_type().is(LOCATION_EXPR))) return false; } diff --git a/test/test_prettyprint.cpp b/test/test_prettyprint.cpp index 14c6a05a..d331d254 100644 --- a/test/test_prettyprint.cpp +++ b/test/test_prettyprint.cpp @@ -338,6 +338,18 @@ TEST_CASE("Enforce query") const auto foo = f.get_errors(); REQUIRE(f.get_errors().empty()); + SUBCASE("Support of locations") + { + + auto query_string = "enforce: Process.location != Process._id0 { Process.location, myClock[2, 10]:100 }"; + + auto query = f.parse_query(query_string).intermediate; + + REQUIRE(query.get_kind() == UTAP::Constants::ENFORCE); + CHECK(query_string == query.str()); + } + + SUBCASE("Correct types") { // NB: Whitespace is significant since it must match the pretty-printer. From 9efd54775b875a4ee380a2dc09863c80daea366d Mon Sep 17 00:00:00 2001 From: Asger Horn Brorholt Date: Tue, 11 Mar 2025 13:22:32 +0100 Subject: [PATCH 5/7] Change query from "enforce" to "acontrol" --- include/utap/AbstractBuilder.hpp | 2 +- include/utap/ExpressionBuilder.hpp | 2 +- include/utap/builder.h | 2 +- include/utap/common.h | 2 +- include/utap/property.h | 4 ++-- src/ExpressionBuilder.cpp | 4 ++-- src/abstractbuilder.cpp | 2 +- src/expression.cpp | 6 +++--- src/keywords.cpp | 2 +- src/parser.y | 9 +++++---- src/property.cpp | 2 +- src/typechecker.cpp | 4 ++-- test/test_prettyprint.cpp | 28 ++++++++++++++-------------- 13 files changed, 35 insertions(+), 34 deletions(-) diff --git a/include/utap/AbstractBuilder.hpp b/include/utap/AbstractBuilder.hpp index 9622d0fb..a519eb47 100644 --- a/include/utap/AbstractBuilder.hpp +++ b/include/utap/AbstractBuilder.hpp @@ -285,7 +285,7 @@ class AbstractBuilder : public ParserBuilder void expr_MITL_exists_dynamic_begin(const char*, const char*) override; void expr_MITL_exists_dynamic_end(const char* name) override; - void expr_enforce() override; + void expr_acontrol() override; void expr_discrete_interval() override; void expr_interval(int32_t divisions) override; diff --git a/include/utap/ExpressionBuilder.hpp b/include/utap/ExpressionBuilder.hpp index b80073c7..8fa99f5a 100644 --- a/include/utap/ExpressionBuilder.hpp +++ b/include/utap/ExpressionBuilder.hpp @@ -207,7 +207,7 @@ class ExpressionBuilder : public AbstractBuilder void expr_MITL_diamond(int, int) override; void expr_MITL_box(int, int) override; - void expr_enforce() override; + void expr_acontrol() override; void expr_discrete_interval() override; void expr_interval(int32_t divisions) override; diff --git a/include/utap/builder.h b/include/utap/builder.h index fb78dcf8..67a2b65d 100644 --- a/include/utap/builder.h +++ b/include/utap/builder.h @@ -431,7 +431,7 @@ class ParserBuilder virtual void expr_MITL_exists_dynamic_end(const char* name) = 0; virtual void expr_dynamic_process_expr(const char*) = 0; - virtual void expr_enforce() = 0; + virtual void expr_acontrol() = 0; virtual void expr_discrete_interval() = 0; virtual void expr_interval(int32_t divisions) = 0; diff --git a/include/utap/common.h b/include/utap/common.h index 457294d5..72fefc89 100644 --- a/include/utap/common.h +++ b/include/utap/common.h @@ -282,7 +282,7 @@ enum kind_t { /****************************************************** * HYPA */ - ENFORCE, + ACONTROL, DISCRETE_INTERVAL, INTERVAL, INTERVAL_LIST, diff --git a/include/utap/property.h b/include/utap/property.h index 0584e1c0..6ad6dda9 100644 --- a/include/utap/property.h +++ b/include/utap/property.h @@ -110,8 +110,8 @@ enum class quant_t { /* LSC scenario property */ scenario, - /* HYPA: enforce : ... {} -> {} */ - enforce, + /* HYPA: acontrol: A[] ... {} -> {} */ + acontrol, }; /** property status */ diff --git a/src/ExpressionBuilder.cpp b/src/ExpressionBuilder.cpp index 95e74d16..e3ebdcec 100644 --- a/src/ExpressionBuilder.cpp +++ b/src/ExpressionBuilder.cpp @@ -931,13 +931,13 @@ void ExpressionBuilder::expr_MITL_box(int low, int high) fragments.push(form); } -void ExpressionBuilder::expr_enforce() +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_t::create_binary(ENFORCE, to_enforce, partition, position)); + fragments.push(expression_t::create_binary(ACONTROL, to_enforce, partition, position)); } void ExpressionBuilder::expr_discrete_interval() diff --git a/src/abstractbuilder.cpp b/src/abstractbuilder.cpp index 61a8fd56..ad3631fe 100644 --- a/src/abstractbuilder.cpp +++ b/src/abstractbuilder.cpp @@ -277,7 +277,7 @@ void AbstractBuilder::expr_MITL_forall_dynamic_end(const char* name) { UNSUPPORT void AbstractBuilder::expr_MITL_exists_dynamic_begin(const char*, const char*) { UNSUPPORTED; } void AbstractBuilder::expr_MITL_exists_dynamic_end(const char* name) { UNSUPPORTED; } -void AbstractBuilder::expr_enforce() { UNSUPPORTED; } +void AbstractBuilder::expr_acontrol() { UNSUPPORTED; } void AbstractBuilder::expr_discrete_interval() { UNSUPPORTED; } void AbstractBuilder::expr_interval(int32_t divisions) { UNSUPPORTED; } diff --git a/src/expression.cpp b/src/expression.cpp index e13869af..600f86ea 100644 --- a/src/expression.cpp +++ b/src/expression.cpp @@ -493,7 +493,7 @@ size_t expression_t::get_size() const case MITL_FORALL: case FOREACH_DYNAMIC: assert(data->sub.size() == 3); return 3; case DYNAMIC_EVAL: assert(data->sub.size() == 2); return 2; - case ENFORCE: assert(data->sub.size() == 2); return 2; + case ACONTROL: assert(data->sub.size() == 2); return 2; case DISCRETE_INTERVAL: assert(data->sub.size() == 3); return 3; case INTERVAL: assert(data->sub.size() == 4); return 4; default: assert(0); return 0; @@ -1666,8 +1666,8 @@ std::ostream& expression_t::print(std::ostream& os, bool old) const break; case TYPEDEF: os << "typedef"; break; - case ENFORCE: - os << "enforce: "; + case ACONTROL: + os << "acontrol: A[] "; get(0).print(os, old); get(1).print(os, old); break; diff --git a/src/keywords.cpp b/src/keywords.cpp index ffbadd60..e41ebcea 100644 --- a/src/keywords.cpp +++ b/src/keywords.cpp @@ -149,7 +149,7 @@ namespace UTAP { {"foreach", Keyword{T_FOREACH, syntax_t::PROPERTY}}, {"query", Keyword{T_QUERY, syntax_t::NEW}}, {"location", Keyword{T_LOCATION, syntax_t::NEW}}, - {"enforce", Keyword{T_ENFORCE, syntax_t::NEW_PROPERTY}}, + {"acontrol", Keyword{T_ACRONTROL, syntax_t::NEW_PROPERTY}}, }; // clang-format on diff --git a/src/parser.y b/src/parser.y index fee8e657..3acce70c 100644 --- a/src/parser.y +++ b/src/parser.y @@ -234,6 +234,9 @@ const char* utap_msg(const char *msg) /* Control Synthesis */ %token T_CONTROL T_CONTROL_T T_SIMULATION +/* HYPA */ +%token T_ACRONTROL + /* Expectation optimization */ %token T_MINEXP T_MAXEXP T_MINPR T_MAXPR T_STRATEGY T_LOAD_STRAT T_SAVE_STRAT @@ -283,8 +286,6 @@ const char* utap_msg(const char *msg) %token T_DYNAMIC T_HYBRID %token T_SPAWN T_EXIT T_NUMOF -/* HYPA */ -%token T_ENFORCE %type ExpQuantifier ExpPrQuantifier %type PathType @@ -1830,8 +1831,8 @@ AssignablePropperty: CALL(@1, @4, expr_unary(EF_CONTROL)); CALL(@1, @4, property()); } - | T_ENFORCE ':' Expression Partition { - CALL(@1, @4, expr_enforce()); + | T_ACRONTROL ':' T_AG Expression Partition { + CALL(@1, @4, expr_acontrol()); CALL(@1, @4, property()); } | BracketExprList T_CONTROL ':' SubProperty Subjection { diff --git a/src/property.cpp b/src/property.cpp index ef5ba53c..010b342a 100644 --- a/src/property.cpp +++ b/src/property.cpp @@ -230,7 +230,7 @@ void PropertyBuilder::typeProperty(expression_t expr) // NOLINT prob = true; break; case MITL_FORMULA: properties.back().type = quant_t::Mitl; break; - case ENFORCE: properties.back().type = quant_t::enforce; break; + case ACONTROL: properties.back().type = quant_t::acontrol; break; default: throw UTAP::TypeException("$Invalid_property_type"); prob = true; } diff --git a/src/typechecker.cpp b/src/typechecker.cpp index 7bb12f32..383b5057 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -1013,7 +1013,7 @@ static bool isGameProperty(expression_t expr) case PO_CONTROL: case CONTROL_TOPT_DEF1: case CONTROL_TOPT_DEF2: - case ENFORCE: return true; + case ACONTROL: return true; default: return false; } } @@ -2277,7 +2277,7 @@ bool TypeChecker::checkExpression(expression_t expr) } break; - case ENFORCE: + case ACONTROL: if (expr[0].get_type().is_integral() && is_interval_list(expr[1])) { type = type_t::create_primitive(FORMULA); } diff --git a/test/test_prettyprint.cpp b/test/test_prettyprint.cpp index d331d254..55d7f7bd 100644 --- a/test/test_prettyprint.cpp +++ b/test/test_prettyprint.cpp @@ -323,7 +323,7 @@ TEST_CASE("Post incrementing an identifier should not require parenthesis") CHECK(expr.str() == "foo++"); } -TEST_CASE("Enforce query") +TEST_CASE("acontrol query") { auto f = document_fixture{} .add_default_process() @@ -341,11 +341,11 @@ TEST_CASE("Enforce query") SUBCASE("Support of locations") { - auto query_string = "enforce: Process.location != Process._id0 { Process.location, myClock[2, 10]:100 }"; + const std::string query_string = "acontrol: A[] Process.location != Process._id0 { Process.location, myClock[2, 10]:100 }"; - auto query = f.parse_query(query_string).intermediate; + auto query = f.parse_query(query_string.data()).intermediate; - REQUIRE(query.get_kind() == UTAP::Constants::ENFORCE); + REQUIRE(query.get_kind() == UTAP::Constants::ACONTROL); CHECK(query_string == query.str()); } @@ -353,7 +353,7 @@ TEST_CASE("Enforce query") SUBCASE("Correct types") { // NB: Whitespace is significant since it must match the pretty-printer. - const std::string query_string = "enforce: myDouble < 1 " + const std::string query_string = "acontrol: A[] myDouble < 1 " "{ " "myInt[2 + 2, 10], " "myConstrainedInt[1, 2 * 5], " @@ -362,7 +362,7 @@ TEST_CASE("Enforce query") auto query1 = f.parse_query(query_string.data()).intermediate; - REQUIRE(query1.get_kind() == UTAP::Constants::ENFORCE); + REQUIRE(query1.get_kind() == UTAP::Constants::ACONTROL); CHECK(query_string == query1.str()); } @@ -371,36 +371,36 @@ TEST_CASE("Enforce query") // Expressions involving clocks typecheck as invariants. // Invariants aren't considered boolean expressions for some reason. I don't consider this my problem. // The workaround is to add a floating-point number to the clock to appease the type checker. - const std::string query_string = "enforce: myClock + 0.0 < 10 && myClock + 0.0 > 0 { myClock[-1, 10]:100 }"; + const std::string query_string = "acontrol: A[] myClock + 0.0 < 10 && myClock + 0.0 > 0 { myClock[-1, 10]:100 }"; auto query1 = f.parse_query(query_string.data()).intermediate; // And then I have to respect that the prettyprinter prints `0` instead of `0.0` for doubles. // Also not my problem. And no, adding `0` in the query does not work. - const std::string expected_string = "enforce: myClock + 0 < 10 && myClock + 0 > 0 { myClock[-1, 10]:100 }"; - REQUIRE(query1.get_kind() == UTAP::Constants::ENFORCE); + const std::string expected_string = "acontrol: A[] myClock + 0 < 10 && myClock + 0 > 0 { myClock[-1, 10]:100 }"; + REQUIRE(query1.get_kind() == UTAP::Constants::ACONTROL); CHECK(expected_string == query1.str()); } SUBCASE("Invalid condition to enforce") { - const auto query_string = "enforce: (-2.2) { }"; + const auto query_string = "acontrol: A[] (-2.2) { }"; REQUIRE_THROWS_WITH(f.parse_query(query_string).intermediate, "$Type_error"); - const auto query_string2 = "enforce: myChannel { }"; + const auto query_string2 = "acontrol: A[] myChannel { }"; REQUIRE_THROWS_WITH(f.parse_query(query_string2).intermediate, "$Type_error"); } SUBCASE("Invalid number of divisions") { - const auto query_string = "enforce: myDouble < 1 { myDouble[M_PI, 21 * 100]:1.5 }"; + const auto query_string = "acontrol: A[] myDouble < 1 { myDouble[M_PI, 21 * 100]:1.5 }"; REQUIRE_THROWS_WITH(f.parse_query(query_string), "$syntax_error: $unexpected T_FLOATING, $expecting T_NAT"); // Don't know why it still says "T_FLOATING" here. - const auto query_string2 = "enforce: myDouble < 1 { myDouble[M_PI, 21 * 100]:myChannel }"; + const auto query_string2 = "acontrol: A[] myDouble < 1 { myDouble[M_PI, 21 * 100]:myChannel }"; REQUIRE_THROWS_WITH(f.parse_query(query_string2), "$syntax_error: $unexpected T_FLOATING, $expecting T_NAT"); - const auto query_string3 = "enforce: myDouble < 1 { myDouble[M_PI, 21 * 100]:myClock }"; + const auto query_string3 = "acontrol: A[] myDouble < 1 { myDouble[M_PI, 21 * 100]:myClock }"; REQUIRE_THROWS_WITH(f.parse_query(query_string3), "$syntax_error: $unexpected T_FLOATING, $expecting T_NAT"); } } \ No newline at end of file From a454cc227d428f52320881bb643295bff0f361f2 Mon Sep 17 00:00:00 2001 From: Asger Horn Brorholt Date: Mon, 28 Apr 2025 13:40:32 +0200 Subject: [PATCH 6/7] Fix that stupid +0.0 bug. Maybe being too permissive but idc --- src/typechecker.cpp | 2 +- test/test_prettyprint.cpp | 10 ++-------- 2 files changed, 3 insertions(+), 9 deletions(-) diff --git a/src/typechecker.cpp b/src/typechecker.cpp index 383b5057..6363c69c 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -2278,7 +2278,7 @@ bool TypeChecker::checkExpression(expression_t expr) break; case ACONTROL: - if (expr[0].get_type().is_integral() && is_interval_list(expr[1])) { + if (expr[0].get_type().is_guard() && is_interval_list(expr[1])) { type = type_t::create_primitive(FORMULA); } break; diff --git a/test/test_prettyprint.cpp b/test/test_prettyprint.cpp index 55d7f7bd..1e274106 100644 --- a/test/test_prettyprint.cpp +++ b/test/test_prettyprint.cpp @@ -368,18 +368,12 @@ TEST_CASE("acontrol query") SUBCASE("Mixing some clocks in there") { - // Expressions involving clocks typecheck as invariants. - // Invariants aren't considered boolean expressions for some reason. I don't consider this my problem. - // The workaround is to add a floating-point number to the clock to appease the type checker. - const std::string query_string = "acontrol: A[] myClock + 0.0 < 10 && myClock + 0.0 > 0 { myClock[-1, 10]:100 }"; + const std::string query_string = "acontrol: A[] myClock < 10 && myClock > 0 { myClock[-1, 10]:100 }"; auto query1 = f.parse_query(query_string.data()).intermediate; - // And then I have to respect that the prettyprinter prints `0` instead of `0.0` for doubles. - // Also not my problem. And no, adding `0` in the query does not work. - const std::string expected_string = "acontrol: A[] myClock + 0 < 10 && myClock + 0 > 0 { myClock[-1, 10]:100 }"; REQUIRE(query1.get_kind() == UTAP::Constants::ACONTROL); - CHECK(expected_string == query1.str()); + CHECK(query_string == query1.str()); } SUBCASE("Invalid condition to enforce") From 6b001c5aa55f8c182cbd2d590f3fbb8ce9178225 Mon Sep 17 00:00:00 2001 From: Asger Horn Brorholt Date: Mon, 28 Apr 2025 15:29:21 +0200 Subject: [PATCH 7/7] Fix typechecking error of intervals (this allows floating points to be used as bounds) --- src/typechecker.cpp | 10 ++++++---- test/test_prettyprint.cpp | 27 +++++++++++++-------------- 2 files changed, 19 insertions(+), 18 deletions(-) diff --git a/src/typechecker.cpp b/src/typechecker.cpp index 6363c69c..493aedf6 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -2262,10 +2262,12 @@ bool TypeChecker::checkExpression(expression_t expr) break; case INTERVAL: { - const auto lower = expr[0].get_type(); - const auto upper = expr[1].get_type(); - const auto divisions = expr[2].get_type(); - if ((lower.is_integer() || lower.is_double() || lower.is_clock()) && + const auto ident = expr[0].get_type(); + const auto lower = expr[1].get_type(); + const auto upper = expr[2].get_type(); + const auto divisions = expr[3].get_type(); + if ((ident.is_integer() || ident.is_double() || ident.is_clock()) && + (lower.is_integer() || lower.is_double() || lower.is_clock()) && (upper.is_integer() || upper.is_double() || upper.is_clock()) && divisions.is_integer()) { type = type_t::create_primitive(INTERVAL); } diff --git a/test/test_prettyprint.cpp b/test/test_prettyprint.cpp index 1e274106..75edcec5 100644 --- a/test/test_prettyprint.cpp +++ b/test/test_prettyprint.cpp @@ -338,26 +338,14 @@ TEST_CASE("acontrol query") const auto foo = f.get_errors(); REQUIRE(f.get_errors().empty()); - SUBCASE("Support of locations") - { - - const std::string query_string = "acontrol: A[] Process.location != Process._id0 { Process.location, myClock[2, 10]:100 }"; - - auto query = f.parse_query(query_string.data()).intermediate; - - REQUIRE(query.get_kind() == UTAP::Constants::ACONTROL); - CHECK(query_string == query.str()); - } - - - SUBCASE("Correct types") + SUBCASE("Basics") { // NB: Whitespace is significant since it must match the pretty-printer. const std::string query_string = "acontrol: A[] myDouble < 1 " "{ " "myInt[2 + 2, 10], " "myConstrainedInt[1, 2 * 5], " - "myDouble[M_PI, 21 * 100]:100 " + "myDouble[M_PI, 2.1 * 100]:100 " "}"; auto query1 = f.parse_query(query_string.data()).intermediate; @@ -366,6 +354,17 @@ TEST_CASE("acontrol query") CHECK(query_string == query1.str()); } + SUBCASE("Support of locations") + { + const std::string query_string = + "acontrol: A[] Process.location != Process._id0 { Process.location, myClock[2, 10]:100 }"; + + auto query = f.parse_query(query_string.data()).intermediate; + + REQUIRE(query.get_kind() == UTAP::Constants::ACONTROL); + CHECK(query_string == query.str()); + } + SUBCASE("Mixing some clocks in there") { const std::string query_string = "acontrol: A[] myClock < 10 && myClock > 0 { myClock[-1, 10]:100 }";