support transition-based properties

[adl]

We'd like to test formulas involving transition-based properties, such as events. The kripke interface is not suitable for this, but we could use the twa interface in that case.