SPECIFICATION TPSpec
INVARIANT TPInvariant
PROPERTY BarAltSpec