search

doganulus / reelay

A header-only C++ library for system-level verification and declarative testing of real-time systems with Python bindings.
https://doganulus.github.io/reelay/
Mozilla Public License 2.0
33 stars 5 forks source link

Monitor formula to compare two data values #20

Open lesire opened 3 years ago

lesire commented 3 years ago

Hi, I have a time serie that contains two data, let's say 'x' and 'y'. I want to create a monitor that compares these two data. However, it seems that data comparison is not supported. I tried the following formulas, each time raising a "syntex error" when creating the (discrete) monitor:

  1. "{x > y}"
  2. "{y: ref, x > ref}"
  3. "exists[ref]. ({y: ref, x > ref})"

also with "implies" relations, nothing works.

Any suggestion?

doganulus commented 3 years ago

You are right. Numerical comparison between two data fields or references are not supported so the parser doesn't accept these formulas. If possible, you can pre-process time-series to insert a Boolean field of "x gt y" to the series and use it as a proposition inside other formulas.

Regarding the rest, such numerical data comparison with references is quite hard due to the symbolic approach chosen in the algorithm. Consider these data references only for categorical variables (string fields only in practice).

And what do you mean exactly by also with "implies" relations, nothing works.? Do you have an example formula you have tried?

lesire commented 3 years ago

I tried to use implies to solve my comparison problem, like "exists[ref]. {y: ref} => {x > ref}". I can clearly write a function that compaires the values and returns a new bool... I just hoped it was not necessary :) Thanks