feat: Stepwise Execution

[MartinKoelbl]

Description

Currently, the encoding describes facts and the analyses are searching for inconsistencies in these facts.
For a real execution, a stepwise execution is needed that uses states and respects time.

Solution

Implement or use some simple form of (predicate abstraction) model checking instead of only a sat solver.
Another solution is to introduce a variable for the current date and choose actions from activated possibilities.