Primary tabs

Trace data for OFFLINE/Team4/Bench2

The property formalizes a compliance policy for a banking system that processes customer transactions.

Specification (in MFOTL)

ALWAYS FORALL c, t, a.
trans(c,t,a) AND 2000 < a IMPLIES ONCE[2,21) EXISTS e. auth(e,t)

Informal explanation
The property requires that executed transactions t of any customer cmust be reported within at most 5 days if the transferred money aexceeds a given threshold of $2,000.

The event trans(c,t,a) denotes that the client c performs thetransaction t, transferring the amount a. The report(t) event denotesthat the transaction t is reported.

Verdict
The property is not satisfied. In particular, there are twoviolations, namely :

@92 (time-point 323302): (807,17368,2495)
@92 (time-point 323303): (3196,26167,2120)
@92 (time-point 323304): (2552,4409,2151)

The first one reads as follows: At timestamp 92 the transaction 26167of the client 3196 transferring the amount $2,120 does not satisfy the requirement.

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.