Add lazy evaluation for the next form in formulas

[juanrh]

That could improve performance as we would avoid a big unravelled next formula, as it would unravelled on demand. An idea for that is adding an abstract method def nextFormula : NextFormula[T] to the trait Formula. This way each Formula object can act as a thunk () => NextFormula[T], for NextFormula defined as

sealed trait NextFormula[T]
  extends Serializable

case class NextNow[T, R <% Result](p : T => R) extends NextFormula[T]
case class NextNot[T](phiThunk : Formula[T]) extends NextFormula[T] {
  lazy val phi : NextFormula[T] = phiThunk.nextFormula
} 
//case class NextOr[T](phi1Thunk : Formula[T], phi2Thunk : Formula[T]) extends NextFormula[T] {
case class NextOr[T](phisThunk : Formula[T]*) extends NextFormula[T] {
  //lazy val phi1 : NextFormula[T] = phi1Thunk.nextFormula
  //lazy val phi2 : NextFormula[T] = phi2Thunk.nextFormula
  lazy val phis : Seq[NextFormula[T]] = phisThunk.map(_.nextFormula) 
} 
case class NextAnd[T](phi1Thunk : Formula[T], phi2Thunk : Formula[T]) extends NextFormula[T] {
  lazy val phi1 : NextFormula[T] = phi1Thunk.nextFormula
  lazy val phi2 : NextFormula[T] = phi2Thunk.nextFormula
}   
case class NextImplies[T](phi1Thunk : Formula[T], phi2Thunk : Formula[T]) extends NextFormula[T] {
  lazy val phi1 : NextFormula[T] = phi1Thunk.nextFormula
  lazy val phi2 : NextFormula[T] = phi2Thunk.nextFormula
}  
case class NextNext[T](phiThunk : Formula[T]) extends NextFormula[T] {
  lazy val phi : NextFormula[T] = phiThunk.nextFormula
} 

And we would have

case class Now[T, R <% Result](p : T => R) extends Formula[T] with NextFormula[T] {
...
  override def nextFormula = NextNow(p)
}
case class Not[T](phi : Formula[T]) extends Formula[T] {
...
  override def nextFormula = NextNot(phi)
}
case class Or[T](phi1 : Formula[T], phi2 : Formula[T]) extends Formula[T] {
...
  override def nextFormula = NextOr(phi1, phi2)
}
case class And[T](phi1 : Formula[T], phi2 : Formula[T]) extends Formula[T] {
...
  override def nextFormula = NextAnd(phi1, phi2)
}
case class Implies[T](phi1 : Formula[T], phi2 : Formula[T]) extends Formula[T] {
...  override def nextFormula = NextImplies(phi1, phi2)
}
case class Next[T](phi : Formula[T]) extends Formula[T] {
...
  override def nextFormula = NextNext(phi)
}
case class Eventually[T](phi : Formula[T], t : Timeout) extends Formula[T] {
...
 override def nextFormula = {   
    if (t.instants > 1)
      // consider which should be used to get lazy progress in the evaluation
      // I think this is already ok because NextOr and the constructors of
      // NextFormual are the progressing constructors
      NextOr(phi, Eventually(Next(phi), t-1))
      //NextOr(phi, Next(Eventually(phi, t-1)))
    else if (t.instants > 0)
      phi.nextFormula // note this is what the lazy val of NextOr does with its first argument
    else NextNow((x : T) => StandardResults.pending)  // timeout: this should not happen by invariant
  }

The only problem is that this code doesn't map so directly to the original definition as the obvious code, and that care must me taken to ensure lazy evaluation is really exploited. So this is a modest optimization that could be performed with the help of some regression tests. A ScalaCheck property using the old definition of next form could be very useful here, it requires a generator for Formula

[juanrh]

Implementation strategy:

• only make NextNext lazy
• use new nested next form definition that generates an equivalent next formula that is deeper and has NextNext as much the outer part of the formula as possible, thus postponing the creation of the next form to when we are able to evaluate it. See details in paper to come