The Analysis Component Sample Clauses

The Analysis Component. The analysis component currently consists of a logical analyser that is capable of checking properties against traces. To this end, the tool takes a dynamic property in TTL format and one or more traces as input, and checks whether the dynamic property holds for the traces. Traces are represented by sets of Prolog facts of the form holds(state(m1, t(2)), a, true) where m1 is the trace name, t(2) time point 2, and a is a state property as introduced in Section 2.1. The above example indicates that state formula a is true in trace m1 at time point 2. The Analysis Component basically uses Prolog rules for the predicate sat that reduce the satisfaction of the temporal formula finally to the satisfaction of atomic state formulae at certain time points, which can be read from the trace representation. Examples of such reduction rules are: sat(and(F,G)) :- sat(F), sat(G). sat(not(and(F,G))) :- sat(or(not(F), not(G))). sat(or(F,G)) :- sat(F). sat(or(F,G)) :- sat(G). sat(not(or(F,G))) :- sat(and(not(F), not(G))). In addition, if a dynamic property does not hold in a trace, then the software reports the places in the trace where the property failed.