Improve feedback of TRACE4CPS's run-time verification functionality
The usability of TRACE4CPS's run-time verification needs to be improved, in particular the feedback to the user.
The first improvement involves the propositions which can be GOOD, BAD or NON_INFORMATIVE. GOOD and BAD could be renamed to TRUE/SATISFIED and FALSE/VIOLATED. NON_INFORMATIVE does not provide all information available. NON_INFORMATIVE is used because the underlying semantics assumes infinite traces. For finite traces (as used in TRACE4CPS), NON_INFORMATIVE means NOT SATISFIED YET for reachability properties and NOT VIOLATED YET for safety properties. I propose to replace NON_INFORMATIVE with NOT SATISFIED YET/NOT VIOLATED YET or something equivalent.
The second improvement involves the explanation of the run-time verification functionality. TRACE4CPS adds events and claims to explain why a property is satisfied/violated/non-informative. This information is not clear, especially with respect to the added events, because many events are added. See below for an example. In this picture, there are too many processing_starts[2], GOOD events and the processing_starts[2], BAD events do not provide useful information. This second change probably requires some study.