The property represents an approval policy for publishing business reports within a company.
Specification (in MFOTL)
ALWAYS FORALL a, f.
(NOT acc_F(a) SINCE[0,*) acc_S(a))
ONCE[0,10] EXISTS m.
(NOT mgr_F(m,a) SINCE[0,*) mgr_S(m,a)) AND approve(m,f)
The property requires that any report must be approved prior to itspublication. Furthermore, the property asks that the person whopublishes the report must be an accountant and the person who approvesthe publication must be the accountant’s manager. Finally, theapproval must happen within at most 10 days before the publication.
The event publish(a,f) denotes the publication of the report f by theaccountant a. The event approve(m,f) denotes the publishing approvalof the report f by the manager m. The event mgr_S (m,a) marks the timewhen m starts being a’s manager and the event mgr_F (m,a) marks thecorresponding finishing time. Analogously, acc_S(a) and acc_F(a) markthe starting and finishing times when a is an accountant.
The property is not satisfied. In particular, there are twoviolations, namely :
@91 (time-point 57347): (93,25218)
@91 (time-point 57348): (51,7848)
@91 (time-point 57350): (35,19053)
@91 (time-point 57351): (88,17294)
The first one reads as follows: At timestamp 91, the accountant 93published the report 25218 without satisfying the approval policy.
All properties are specified in metric first-order temporal logic (MFOTL), or in its extension to aggregation operators and function symbols.
Thus, any line in a CSV formatted trace file from these benchmarks has the form
where p is the event name, i is its time point, t is the timestamp of its occurrence, and v1,...,vn are the values of its parameters.
Events that have the same time point are assumed to be unordered. However, events with different time points are assumed to be ordered, even if they have the same timestamps.