The property is rooted in the domain of fraud detection.

**Specification (in MFOTL)**

ALWAYS FORALL s, u.

(s <- SUM a;u ONCE[0,28] withdraw(u,a) AND tp(i)) IMPLIES s <= 10000

**Informal explanation**

The property requires that the sum of withdrawals of each user in thelast 28 days does not exceed the limit of $10,000.

The event withdraw(u,a) denotes the withdrawal of the amount a by theuser u. The event tp(i) denotes that the current time point is i. Thisevent is used in the formalization to distinguish different events withdraw(u,a) with the same values for u and a in the relevant time window.

**Verdict**

The property is not satisfied. In particular, there are the following violations:

@29 (time-point 28): (10013,u324)

@32 (time-point 31): (10023,u324)

@39 (time-point 38): (10015,u761)

@40 (time-point 39): (10125,u761) (10215,u744)

@41 (time-point 40): (10334,u761) (10405,u744)

@42 (time-point 41): (10311,u744) (10357,u761) (10363,u977)

@43 (time-point 42): (10034,u761) (10372,u977)

@44 (time-point 43): (10375,u761) (10642,u977)

@45 (time-point 44): (10340,u761) (10961,u977)

@46 (time-point 45): (10304,u761) (10999,u977)

@47 (time-point 46): (10020,u503) (10187,u761) (11160,u977)

@48 (time-point 47): (10585,u977)

@49 (time-point 48): (10209,u977)

@51 (time-point 50): (10057,u977)

@52 (time-point 51): (10095,u977)

@53 (time-point 52): (10022,u977) (10193,u744)

@57 (time-point 56): (10114,u181)

@58 (time-point 57): (10203,u181)

The first one reads as follows: At timestamp 29, the user u324 hadwithdrawn a total amount of $10,013 in the last 28 days, and thusviolates 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.