search

xiaohe27 / LogReader

The log reader which can read log files
0 stars 0 forks source link

Liveness property #64

Open xiaohe27 opened 9 years ago

xiaohe27 commented 9 years ago

We cannot decide whether a liveness property (<> p) is violated until the end of the log has been reached. Idea: report it as non-monitorable at the beginning.

xiaohe27 commented 9 years ago

Monpoly uses the syntax to restrict the formulas so that the valid formulas can only express some property is held within a fixed range in the future.

xiaohe27 commented 9 years ago

If the formula contains infinite future expression, then the formula is not monitored by Monpoly: It will report it as The formula contains an unbounded future temporal operator. It is hence not monitorable.