Make the model checker able to check liveness/fairness properties

> I'm pretty sure I know why the liveness property is not rejected. It's because HasCal's property checker will accept a model if (A) the termination checker is disabled and (B) the model never violates the property for all visited states.
>
> So in this case, the model never terminates, and because it never terminates the property is vacuously satisfied

I see, so the checker would need to do some more work here...

I don't know much about checking liveness, but I think the "classic" way of checking liveness would be to construct a Buchi automaton of the system, [translate](https://en.wikipedia.org/wiki/Linear_temporal_logic_to_B%C3%BCchi_automaton) the negation of the LTL formula to a Buchi automaton, then take the intersection of of the two and check that it's empty (if it's not we get an infinite counterexample). I believe this technique was first described in [*An Automata-Theoretic Approach to Automatic Program Verification*](http://hdl.handle.net/2268/116609).

This seems quite different from what the HasCal checker currently does though, and I wonder if more "modern" approaches such as [*Liveness Checking as Safety Checking*](http://fmv.jku.at/papers/BiereArthoSchuppan-FMICS02.pdf) would perhaps be a better fit?

Also it might make sense to separate safety and liveness/fairness into two separate `Property`s? I believe that's what TLC is effectively doing by forcing the shape of the properties it checks to be of the form: `Init /\ [][Next]_vars /\ Liveness`?

_Originally posted by @stevana in https://github.com/Gabriel439/HasCal/issues/11#issuecomment-1113953097_