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)
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.
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
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.