Support existential quantifier for future expressions

[phiros]

Currently, the model checker only supports the forall quantifiers for future expressions. It would be cool if it could also support the existential quantifier (i.e. ∃).

This would enable a user to express things like:

behavior of "Philosophers"
  they should "not starve" in atLeastOneInterleaving {
    implicit tec =>
      new Philosophers(5).run will not complete
  }

[Jentsch]

Now it's possible to test for never completing futures. Tests for ∃ or could is right now a bit broken. Aside from that bug, this functionality should be right now available.

Example:

behavior of "Philosophers"
they should "not starve" in everyInterleaving {
  implicit tec =>
    new Philosophers(5).run willNot complete
}