Skip to content
Snippets Groups Projects

Fork of Eclipse TRACE4CPS™ for my thesis

This is a fork of the Eclipse TRACE4CPS™ repository for the implementation of the functionality developed in Edo Mangelaars' Master thesis:

The new functionality of this fork concerns the presentation of the results of the runtime verification features of Eclipse TRACE4CPS™, in order to make them more understandable. Because the primary goal of the implementation of this functionality was to support the thesis, the code may not (yet) be of the quality required to merge them back into the main repository. Tests were added for some of the most important functionality.

This fork contains the following features:

Four-valued ETL semantics

4vv

When verifying an etl file on a trace, instead of always returning one of three possible verdicts (GOOD, BAD, NON-INFORMATIVE), where NON-INFORMATIVE means that the verdict (possibly) relies on information beyond the end of the trace, the user is asked whether to use the finite, three-valued of four-valued semantics.

The three-valued semantics corresponds to the previous behavior, but the verdicts GOOD and BAD were renamed to TRUE and FALSE. The finite semantics always returns either TRUE or FALSE, and uses a checking method that was already present but unused in the codebase. The four-valued semantics is a combination of the three-valued and finite semantics which returns STILL_TRUE if it would have been NON-INFORMATIVE but is TRUE in the finite semantics, and STILL_FALSE if it would have been NON-INFORMATIVE but is FALSE in the finite semantics.

The checking algorithm in the four-valued semantics is implemented in the following file:

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/check/RecursiveMemoizationChecker.java

STL properties are always checked in the finite semantics as before. The property explanations also the use the four-valued semantics for intermediate values.

Files changed to implement this:
  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/check/RecursiveMemoizationChecker.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/check/CompactExplanationTableImpl.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/check/TabularExplanationTable.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/VerificationSemantics.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/InformativePrefix.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/VerificationResultView.java

  • temporallogic/org.eclipse.trace4cps.tl.cmd/src/main/java/org/eclipse/trace4cps/tl/cmd/Verify.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/action/VerifyAction.java

  • temporallogic/org.eclipse.trace4cps.tl/src/org/eclipse/trace4cps/tl/VerificationHelper.java

  • temporallogic/org.eclipse.trace4cps.tl/src/org/eclipse/trace4cps/tl/VerificationResult.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/MtlChecker.java

Visualization of subformulas

verification panel new

The property explanations, which were obtained by double-clicking a property in the Verification panel and shown as events in the Trace view corresponding to named defs in the ETL formula, were extended so that arbitrary subformulas of ETL properties can be explained.

The tree view in the Verification panel was reorganized so that instead of being organized by verdict, it follows the following hierarchy:

  • trace file > specification file > property > (parameterized property) > subformulas of the property…​

The verdict is shown together with the (parameterized) property.

Double-clicking a formula generates an explanation as before, but now double-clicking a subformula adds an explanation for that (sub)formula. Support for subformula explanations for STL formulas is limited. The lanes added to the trace view are sorted in the order in which you added them.

To generate the explanations, a mapping between the MTL representation and the ETL formula is kept, so that the ETL syntax can be shown in the tree even though the MTL representation is used internally to check the property.

A new button was added to the toolbar that switches between showing explanation events with different validities in separate lanes, or keeping them in the same lane.

Files changed to implement this:
  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/VerificationResultView.java

  • temporallogic/org.eclipse.trace4cps.tl/src/org/eclipse/trace4cps/tl/FormulaTuple.java

  • temporallogic/org.eclipse.trace4cps.tl/src/org/eclipse/trace4cps/tl/VerificationResult.java

  • temporallogic/org.eclipse.trace4cps.tl/src/org/eclipse/trace4cps/tl/FormulaBuilder.java

  • temporallogic/org.eclipse.trace4cps.tl/src/org/eclipse/trace4cps/tl/FormulaHelper.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/core/impl/TraceHelper.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/ResultTree.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/CheckNode.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/FileNode.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/FormulaNode.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/IExplainableNode.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/ParameterizedCheckNode.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/SpecNode.java

  • trace/org.eclipse.trace4cps.vis/src/main/java/org/eclipse/trace4cps/vis/jfree/TracePlotManager.java

  • trace/org.eclipse.trace4cps.vis/src/main/java/org/eclipse/trace4cps/vis/jfree/impl/Cell.java

  • trace/org.eclipse.trace4cps.vis/src/main/java/org/eclipse/trace4cps/vis/jfree/impl/ClaimPartition.java

  • trace/org.eclipse.trace4cps.vis/src/main/java/org/eclipse/trace4cps/vis/jfree/impl/Partition.java

  • trace/org.eclipse.trace4cps.ui/icons/formula.png

  • trace/org.eclipse.trace4cps.ui/icons/separate_sat.png

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/EclipseSelectionWrapper.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/TraceView.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/action/SeparateSatAction.java

Interval explanations

odse new explanation interval

By right-clicking on a formula in the Verification panel and selecting “Explain intervals”, a lane is added to the trace view that shows the interval in which the temporal operators of the chosen (sub)formula were checked.

This was implemented by keeping a record of checked intervals in the checking algorithm in the following file:

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/check/RecursiveMemoizationChecker.java

Files changed to implement this:
  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/check/RecursiveMemoizationChecker.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/check/CompactExplanationTableImpl.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/check/TabularExplanationTable.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/VerificationResultView.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/check/RegionImpl.java

Cause explanations

odse order cause

In addition to the previous property explanations, which visualize the intermediate values of the MTL checking process, a new type of explanation was added which indicates only those events that caused a violation of the formula, which can be invoked by right-clicking a formula in the Verification panel and choosing “Explain LTL/MTL cause of violation”. It is based on the paper “Explaining counterexamples using causality” by Beer, I., Ben-David, S., Chockler, H. et al.

It is implemented in two separate ways:

For LTL formulas (which are MTL formulas in which all temporal operators are unconstrained), the algorithm from the previously mentioned paper is translated and implemented in the following file:

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/LtlCausalityChecker.xtend

The algorithm relies on formulas being in negation normal form (NNF). An NNF transformation and a data structure representing formulas in NNF are implemented in the following file:

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/LtlNnf.xtend

For general MTL formulas (including those containing during, within and by ETL constructs) it is implemented in a copy of the RecursiveMemoizationChecker class in the following file:

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/RecursiveMemoizationCausalityChecker.xtend

The NNF transformation for these formulas is implemented in the following file:

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/MtlNnf.xtend

It is implemented using the regular MTL data structures, but with an added Release operator implemented in the MTLrelease class.

Causes are expressed as pairs of an event and an atomic proposition (attribute filter in ETL). Attribute filters can optionally be split into single attributes, depending on which is clearer for a given formula. Claims corresponding to causal events can optionally be highlighted in blue.

What is not yet implemented is a visualization of which part of the formula (in the tree in the Verification panel) is responsible for the violation. Implementing this is not trivial because the NNF transformation can change the structure of the formula, but should not be too difficult.

Files changed to implement this:
  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/LtlCausalityChecker.xtend

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/LtlNnf.xtend

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/Cause.xtend

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/RecursiveMemoizationCausalityChecker.xtend

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/MtlNnf.xtend

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/MTLrelease.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/MTLweaknext.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/VerificationResultView.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/MtlUtil.java

Other changes

Next and True formulas

The next and true constructs (from LTL) were added to the ETL language definition and the MTL data structure in order to implement the LTL cause explanations and to test the MTL cause explanations.

Files changed to implement this:
  • temporallogic/org.eclipse.trace4cps.tl/src/org/eclipse/trace4cps/tl/Etl.xtext

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/check/RecursiveMemoizationChecker.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/impl/MTLnext.java

  • temporallogic/org.eclipse.trace4cps.tl/src/org/eclipse/trace4cps/tl/FormulaBuilder.java

  • temporallogic/org.eclipse.trace4cps.tl/src/org/eclipse/trace4cps/tl/FormulaHelper.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/MtlBuilder.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/MtlUtil.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/MTLweaknext.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/LtlCausalityChecker.xtend

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/RecursiveMemoizationCausalityChecker.xtend

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/LtlNnf.xtend

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/causality/MtlNnf.xtend

Attribute visualization

A final type of “explanation” is to visualize the values of all attributes on all events, which can be invoked by right-clicking a formula and choosing “Explain attributes”. This is implemented by splitting the atomic propositions into single attributes and checking each of them on the entire trace.

Files changed to implement this:
  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/AttributeAtom.java

  • temporallogic/org.eclipse.trace4cps.tl/src/org/eclipse/trace4cps/tl/VerificationResult.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/check/RecursiveMemoizationChecker.java

  • trace/org.eclipse.trace4cps.core/src/org/eclipse/trace4cps/analysis/mtl/check/SingleFormulaChecker.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/VerificationResultView.java

  • trace/org.eclipse.trace4cps.ui/src/org/eclipse/trace4cps/ui/view/verify/VerifyUtil.java

Separate repositories

Property-based tests

A separate repository was created to implement tests for four-valued semantics and cause explanations using property-based testing:

This was done in a separate repository in order to more easily add a Maven dependency on the junit-quickcheck library by Paul Holser.

Here, MTL formulas and traces are randomly generated so that some important properties for the correctness of the functionality can be checked on as large (or representative) a part of the total space of ETL properties and traces as possible. These tests take quite some time to run (depending on the number of generated inputs), but give great confidence in the correctness of the implementation and its underlying assumptions.

Example traces and properties

Finally, the traces and properties which were used to test and validate the new functionality can be found here:


The original README text follows:

Eclipse TRACE4CPS™

Welcome to the Eclipse TRACE4CPS™ repository!

Eclipse TRACE4CPS™ is a customizable, domain-independent and source-independent Gantt chart viewer with mathematically-founded analysis support. Eclipse TRACE4CPS™ supports the visualization of activities on resources as a function of time (Gantt charts), as well as the visualization of continuous signals. Eclipse TRACE4CPS™ also supports several analysis techniques to identify bottlenecks, check formally-specified (performance) properties, and analyze resource usage. A key feature of Eclipse TRACE4CPS™ is the ability to configure the identification, selection and visualization of such information to match any specific application domain.

Handy links: