Merge pr #65: added bounds query generalizing inf and sup in one check

Bounds query to generalize infimum and supremum
UPPAALModelChecker · Sep 21, 2023 · bf88583 · bf88583
2 parents 1914e39 + 0bdcb06
commit bf88583
Show file tree

Hide file tree

Showing 10 changed files with 133 additions and 49 deletions.
diff --git a/include/utap/common.h b/include/utap/common.h
@@ -182,10 +182,11 @@ enum kind_t {
  LOAD_STRAT,
 
  /*******************************************************
- * Get supremum or infimum of variables/clocks
+ * Get supremum, infimum or (generalized) bounds for variable/clock values
  */
  SUP_VAR,
  INF_VAR,
+ BOUNDS_VAR,
 
  /*******************************************************
  * Verify a LSC scenario

diff --git a/include/utap/property.h b/include/utap/property.h
@@ -99,9 +99,10 @@ enum class quant_t {
  strategy_load,
  strategy_save,
 
- /* Extensions for getting supremum/infimum of variables/clocks */
+ /* Extensions for getting supremum/infimum/bounds for variable/clock values */
  supremum,
  infimum,
+ bounds,
 
  /* Prob properties */
  PMax,

diff --git a/src/expression.cpp b/src/expression.cpp
@@ -356,6 +356,7 @@ size_t expression_t::get_size() const
  case SUM:
  case SUP_VAR:
  case INF_VAR:
+ case BOUNDS_VAR:
  case FRACTION:
  case FMOD_F:
  case FMAX_F:
@@ -868,7 +869,8 @@ int expression_t::get_precedence(kind_t kind)
  case CONTROL_TOPT_DEF1:
  case CONTROL_TOPT_DEF2:
  case SUP_VAR:
- case INF_VAR: return 3;
+ case INF_VAR:
+ case BOUNDS_VAR: return 3;
 
  case SYNC: return 0;
 
@@ -1590,6 +1592,12 @@ std::ostream& expression_t::print(std::ostream& os, bool old) const
  get(1).print(os, old);
  break;
 
+ case BOUNDS_VAR:
+ os << "bounds{";
+ get(0).print(os, old) << "}: ";
+ get(1).print(os, old);
+ break;
+
  case MITL_FORMULA:
  os << "MITL: ";
  get(0).print(os, old);

diff --git a/src/keywords.cpp b/src/keywords.cpp
@@ -76,6 +76,7 @@ namespace UTAP {
  {"sat", Keyword{T_SCENARIO, syntax_t::PROPERTY}},
  {"inf", Keyword{T_INF, syntax_t::PROPERTY}},
  {"sup", Keyword{T_SUP, syntax_t::PROPERTY}},
+ {"bounds", Keyword{T_BOUNDS, syntax_t::PROPERTY}},
  {"Pmax", Keyword{T_PMAX, syntax_t::PROPERTY_PROB}},
  {"Pr", Keyword{T_PROBA, syntax_t::PROPERTY}},
  {"X", Keyword{T_MITL_NEXT, syntax_t::PROPERTY}},

diff --git a/src/parser.y b/src/parser.y
@@ -188,7 +188,7 @@ const char* utap_msg(const char *msg)
 %token T_KW_AND T_KW_OR T_KW_XOR T_KW_IMPLY T_KW_NOT
 
 /* Special */
-%token T_SUP T_INF
+%token T_SUP T_INF T_BOUNDS
 
 /* Math functions */
 %token T_ABS T_FABS T_FMOD T_FMA T_FMAX T_FMIN T_FDIM
@@ -756,6 +756,7 @@ NonTypeId:
  | 'M' { strncpy($$, "M", MAXLEN); }
  | T_SUP { strncpy($$, "sup", MAXLEN); }
  | T_INF { strncpy($$, "inf", MAXLEN); }
+ | T_BOUNDS { strncpy($$, "bounds", MAXLEN); }
  | T_SIMULATION { strncpy($$, "simulation", MAXLEN); }
  ;
 
@@ -1942,16 +1943,23 @@ SupPrefix:
  T_SUP ':' {
  CALL(@1, @2, expr_true());
  }
- | T_SUP '{' Expression '}' ':'
+ | T_SUP '{' Expression '}' ':'
  ;
 
 InfPrefix:
  T_INF ':' {
  CALL(@1, @2, expr_true());
  }
- | T_INF '{' Expression '}' ':'
+ | T_INF '{' Expression '}' ':'
  ;
-
+
+BoundsPrefix:
+ T_BOUNDS ':' {
+ CALL(@1, @2, expr_true());
+ }
+ | T_BOUNDS '{' Expression '}' ':'
+ ;
+
 
 StrategyAssignment: 
  T_STRATEGY Id T_ASSIGNMENT AssignablePropperty { 
@@ -1964,14 +1972,19 @@ Property:
  | PropertyExpr
  | SupPrefix NonEmptyExpressionList Subjection {
  CALL(@1, @2, expr_nary(LIST,$2));
-  CALL(@1, @2, expr_binary(SUP_VAR));
+  CALL(@1, @2, expr_binary(SUP_VAR));
  CALL(@1, @2, property());
  }
  | InfPrefix NonEmptyExpressionList Subjection {
  CALL(@1, @2, expr_nary(LIST,$2));
-  CALL(@1, @2, expr_binary(INF_VAR));
+  CALL(@1, @2, expr_binary(INF_VAR));
  CALL(@1, @2, property());
- };
+ }
+ | BoundsPrefix NonEmptyExpressionList Subjection {
+ CALL(@1, @2, expr_nary(LIST,$2));
+ CALL(@1, @2, expr_binary(BOUNDS_VAR));
+ CALL(@1, @2, property());
+ };
 
 %%
 

diff --git a/src/property.cpp b/src/property.cpp
@@ -170,6 +170,7 @@ static bool symbolicProperty(const expression_t& expr)
  case CONTROL_TOPT_DEF2:
  case SUP_VAR:
  case INF_VAR:
+ case BOUNDS_VAR:
  case SCENARIO:
  case SCENARIO2: return true;
  default: return false;
@@ -195,6 +196,7 @@ void PropertyBuilder::typeProperty(expression_t expr) // NOLINT
  break;
  case SUP_VAR: properties.back().type = quant_t::supremum; break;
  case INF_VAR: properties.back().type = quant_t::infimum; break;
+ case BOUNDS_VAR: properties.back().type = quant_t::bounds; break;
  case PROBA_MIN_BOX:
  properties.back().type = quant_t::probaMinBox;
  prob = true;

diff --git a/src/typechecker.cpp b/src/typechecker.cpp
@@ -1057,11 +1057,12 @@ void TypeChecker::visitProperty(expression_t expr)
  }
  }
  */
- } else if (auto k = expr.get_kind(); k != SUP_VAR && k != INF_VAR && k != SCENARIO && k != PROBA_MIN_BOX &&
- k != PROBA_MIN_DIAMOND && k != PROBA_BOX && k != PROBA_DIAMOND &&
- k != PROBA_EXP && k != PROBA_CMP && k != SIMULATE && k != SIMULATEREACH &&
- k != MITL_FORMULA && k != MIN_EXP && // ALREADY CHECKED IN PARSE
- k != MAX_EXP) // ALREADY CHECKED IN PARSE
+ } else if (auto k = expr.get_kind(); k != SUP_VAR && k != INF_VAR && k != BOUNDS_VAR && k != SCENARIO &&
+ k != PROBA_MIN_BOX && k != PROBA_MIN_DIAMOND && k != PROBA_BOX &&
+ k != PROBA_DIAMOND && k != PROBA_EXP && k != PROBA_CMP && k != SIMULATE &&
+ k != SIMULATEREACH && k != MITL_FORMULA &&
+ k != MIN_EXP && // ALREADY CHECKED IN PARSE
+ k != MAX_EXP) // ALREADY CHECKED IN PARSE
  {
  for (uint32_t i = 0; i < expr.get_size(); i++) {
  /* No nesting except for constraints */
@@ -2307,6 +2308,7 @@ bool TypeChecker::checkExpression(expression_t expr)
 
  case SUP_VAR:
  case INF_VAR:
+ case BOUNDS_VAR:
  if (!is_integral(expr[0]) && !is_constraint(expr[0])) {
  handleError(expr[0], "$Boolean_expected");
  return false;

diff --git a/test/models/simpleSystem.xml b/test/models/simpleSystem.xml
@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="utf-8"?>
-<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/researoh/group/darts/uppaal/flat-1_2.dtd'>
+<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
 <nta>
  <declaration>clock c;</declaration>
  <template>

diff --git a/test/test_expression.cpp b/test/test_expression.cpp
@@ -153,7 +153,7 @@ TEST_CASE("Expression")
  MINUS, PLUS, MULT, DIV, MOD, BIT_AND, BIT_OR, BIT_XOR, BIT_LSHIFT, BIT_RSHIFT,
  AND, OR, XOR, POW, LT, LE, EQ, NEQ, GE, GT, MIN, MAX, ARRAY, COMMA,
  ASSIGN, ASS_PLUS, ASS_MINUS, ASS_DIV, ASS_MOD, ASS_MULT, ASS_AND, ASS_OR, ASS_XOR,
- ASS_LSHIFT, ASS_RSHIFT, FORALL, EXISTS, SUM, SUP_VAR, INF_VAR, FRACTION,
+ ASS_LSHIFT, ASS_RSHIFT, FORALL, EXISTS, SUM, SUP_VAR, INF_VAR, BOUNDS_VAR, FRACTION,
  FMOD_F, FMAX_F, FMIN_F, FDIM_F, POW_F, HYPOT_F, ATAN2_F, LDEXP_F, NEXT_AFTER_F, COPY_SIGN_F,
  RANDOM_ARCSINE_F, RANDOM_BETA_F, RANDOM_GAMMA_F, RANDOM_NORMAL_F, RANDOM_WEIBULL_F,
  }; // clang-format on