Add state invariants?

[MattWindsor91]

It should be possible to add invariants to RoboCert (which pull in specification-level variables and maybe eventually model variables), with the Lima et al. encoding of emitting an invalid_trace event. (This is how I expected we'd want to encode failure in RoboCert, so it's nice to see that it indeed is taken up in the literature.)

We would need an example for the usefulness of this.