Open xiaohe27 opened 9 years ago
For the equality checks or other things related to comparing values, if they occur on the lhs of an implication symbol, then it can be transformed to constraints which can be used to filter out unnecessary calling of event methods (false implies anything, so do not need to create event for monitoring).
if the rvm spec does not contain expected formula, then it implies that the property is a simple propositional formula and no rvm methods are needed. In this case, just gen the log reader's monitor method from the simple condition derived from the simple formula, and no RVM thing is needed.
If the expected formula has been specified, then gen the log reader as normal