search

xiaohe27 / LogReader

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

Check the ltl plugin of RVM #61

Open xiaohe27 opened 9 years ago

xiaohe27 commented 9 years ago

Whether there is a way to express the happens before (not transit states easily)

xiaohe27 commented 9 years ago

for formulas like: [](publish => <*> approve) The trace (after slicing): approve publish publish publish is valid. But it requires to store all the approve events. This is unavoidable because we do not know whether there will be publish events at later stage. For huge logs, this may use up the heap memory soon.

xiaohe27 commented 9 years ago

@12 publish(7) @22 publish(7) ... In RVM: Multiple violations only result in a single record in the output if the param of the events are the same.

In Monpoly, the same kind of violation will be not repeated inside one time point, but WILL repeat if they occur at different time points.

xiaohe27 commented 9 years ago

Solution: Use __RESET; to reset the monitor states

xiaohe27 commented 9 years ago

Need to solve this: If multiple violations with the same param occur in the same time point, then only one will be reported.

xiaohe27 commented 9 years ago

Idea: provide an option of minimizing the output of violations so that it is exactly the same as Monpoly. It takes a little more time to check whether a record has occurred in the violation list, but with this option we can check the correctness of output

xiaohe27 commented 9 years ago

Use a config file to specify which fields need to present in the violation output.