Linear Temporal Logic (finite) POC

This is a proof of concept for a simple linear temporal logic (LTL) implementation in Java. The implementation is based on the finite semantics of LTL, see LTL for details.

The goal is to eventually provide something like Quickstrom in jqwik

TODOs

• atomic facts
• not
• and
• or
• implies
• always
• eventually
• next
• until
• last
• Make all formulae describe itself in toString()
• Make LTLFormula generic (by any state type)
• Property-based tests for LTL
• Provide mismatching details in case of failed match
• Allow to switch between finite and infinite semantics