Primary tabs

Trace data for OFFLINE/Team4/Bench3

The property represents an approval policy for publishing business reports within a company.

Specification (in MFOTL)


ALWAYS FORALL a, f.
publish(a,f) IMPLIES
(NOT acc_F(a) SINCE[0,*) acc_S(a))
AND
ONCE[0,10] EXISTS m.
(NOT mgr_F(m,a) SINCE[0,*) mgr_S(m,a)) AND approve(m,f)

Informal explanation

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.

Verdict

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

  • p,tp=i,ts=t,f1=v1,f2=v2,...,fn=vn

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.

Data Preview: Note that by default the preview only displays up to 100 records. Use the pager to flip through more records or adjust the start and end fields to display the number of records you wish to see.