LTL24™ is a software tool for querying and verification of event-level football data collected and marketed by Opta in the form of "F24 feeds". The tool uses a formal specification of queries and requirements inspired by Linear Temporal Logic. This modal logic design enables the user to make context-sensitive queries which are impossible or (at best) cumbersome with SQL, and consequently ensure F24 data integrity at the cross-event level. An additional application of this system is querying of the data, based on the idea that searching for a feature is dual to proving the negation of that feature.
Consider the following requirement:
A shot on target (Event type 15) must be immediately followed by a save (Event type 10).
This requirement cannot be checked against given F24 match data if that data resides in an unannotated SQL database because the Event objects carry no information about what precedes or follows them. Moreover, even if the database is annotated with temporal ordering of Events, the appropriate SQL query is still relatively cumbersome and inefficient. By contrast, LTL24 expresses it in an entirely natural fashion as:
always(type_id=15 implies (next type_id=10))
using LTL's temporal modalities always and next,
and the propositional connective implies.
To use LTL24, you first
need to install the Glasgow Haskell Compiler and
the xml,
parsec and
datetime packages from
hackage.haskell.org. Then compile the sources with
$ ghc Main.hs.
At the moment, LTL24 is an interactive console system. Bundled with this
project is a file specs.txt with two sample requirements:
halves: exists (type_id=32 and period_id=1 and next (exists (type_id=32 and period_id=2)));
saves: always (type_id=15 implies (next type_id=10));
The halves requirement means simply that first and second half start events
exist and the start of the second must follow the start of the first.
Also in the project is the f24sample.xml file, which is
an anonymized -- names, dates and IDs altered, otherwise untouched -- F24 coding of
a recent football game (unfortunately I was denied
permission from Opta to include the original file). The following sample session
lets us determine if the file satisfies the two requirements:
marek@jules:/home/marek/Projects/ltl24 (master)$ ./Main
Welcome to LTL24 v0.1.0.
LTL24$ help
Available commands: quit, help, about, load, status, verify, drop.
LTL24$ help load
load -- add games or specs to the active environment.
USAGE: load [game | spec] <filename>
load spec inline <name>:<formula>
LTL24$ load spec specs.txt
0 game(s).
2 spec(s): halves, saves.
LTL24$ load game f24sample.xml
1 game(s): 476843.
2 spec(s): halves, saves.
LTL24$ verify
Verifying game 476843.
halves: passed
saves: failed
LTL24$ quit
Really quit [y/n]? y
Bye.
As we see, the halves requirement is satisfied by this data file, but saves
is not. There must be a shot on target in the Event stream that is not
immediately followed by a save. In the future versions (if any) of the software,
the actual instance of the Event violating the requirement (known as "counterexample")
should be produced, enabling the user to search for patterns of interest by attempting to prove their negation.