Support configuration of expected results in the three-valued temporal logic

[juanrh]

Currently we use org.scalacheck.Prop.Undecided for the value ? of the logic. Specs2 interprets that as a failing test, and you cannot use org.specs2.matcher.ResultMatchers to mark a property as expecting undecided because the integration of specs2 with scalacheck understands Undecided as a failure, and there is no matcher in ResultMatchers for Undecided. To solve this we could do one of these:

• define a new specs2 matcher sin the line of ResultMatchers for undecided properties. This is the preferred approach as the undecided result could be expressed in the definition of is, or even several alternatives by using specs2 or
• add an argument to DStreamProp.forall to specify a set of aceptable prop status, so for example we can specify that undecided, proof and true are aceptable final results for a temporal property. This is very easy to implement

[juanrh]

Note ScalaCheck is not a problem here, because when it gets a undecided result for a test case it continues with the next test case. This can we tested by using a forall formula with a during longer than the size of the input generator

[juanrh]

currently converting Prop.Undecided into Prop.passed as we are interested in finding counterexamples, this should be the default but also should be configurable