The goal of this milestone is two-fold. On the one hand, we need to lay the ground work for invariant learning. This includes, among other things, at least

1. check whether a given trap abstraction does already imply some property, and, if not,
2. compute a counter-example trap for a given property; an incorporation of, e.g., clingo would be ideal. However, an adhoc solution should be acceptable for this first step.
3. Check for some language whether it satisfies the initially marked and trap property for a given regular transition system. Otherwise, we should get an example which invalidates that all languages are initially marked traps.