search

nickovic / rtamt

Specification-based real-time monitoring library
BSD 3-Clause "New" or "Revised" License
50 stars 20 forks source link

what is sat() in PredicateOperation? #125

Closed TomyYamy closed 2 years ago

TomyYamy commented 2 years ago

I did not understand sat() in PredicateOperation even though I know where you use it. https://github.com/nickovic/rtamt/blob/c495f36ecf32366e6f3b6ced1942e0ce5db20f56/rtamt/operation/stl/dense_time/offline/predicate_operation.py#L39-L66

nickovic commented 2 years ago

sat is the qualitative evaluation of the predicate - true or false. It cannot be inferred directly from the quantitative semantics in border cases. For instance rho(5<5) = 0 and sat(5 < 5) = false rho(5 <=5) = 0 and sat(5 <= 5) = true

TomyYamy commented 2 years ago

I see sat() makes it boolean. Still I feel we may may merge it with evaluation in some way. Let me think.