TL Props

[juanrh]

Atomic propositions should correspond to assertions on the current batch of each dstream

[juanrh]

In the "to now or next" transformation of TL formulas use Either<Result, Next> as the result to type check the approach. Note this only refers to the outer constructor, as more temporal operators might be nested in Next, as all we can evaluate is what happens now, with turns into a specs2 Result. That Results for now corresponds to proposition symbols which are assertions on the current batch, and to non modal propositional operators like not, implication etc. Be as lazy as possible via short circuit

[juanrh]

Define a Scala ADT for a TLFormula abstract class with case classes as children. In particular Now is a wrapper on Result as described above. Use operator that make constructor calls to get a DSL that allows expressions like

(x === 0) until (x === 1)

via an implicit conversion from Matcher to Now, and a method until in TLFormula, obtaining Until(Now(x ===0), Now(x===1)) as a result. View bounds could be useful here https://twitter.github.io/scala_school/advanced-types.html http://docs.scala-lang.org/tutorials/tour/views.html for the arguments of methods like TLFormula.until

[juanrh]

The evaluation of the "to now or next" transformation could be improved if the result is lazy. Lazyness can be obtained in Scala with streams and lazy views for collections (maybe for the list of pending formulas), but also with a combination of a by-name parameter that is read only once through a lazy val, see an example in chapter 5 of "Functional programming in Scala" and in http://www.scala-lang.org/old/node/6045.html. Maybe lazy wrapper classes on Either<Result, Next> based on that, with a stream for the candidates, would be a good option

[juanrh]

tests passed in travis, solved ok