safeWordLength can now only be compute for the subset of formulas corresponding to the old formulas. For example we can have a formula that uses a Now that builds an eventually with a timeout defined on the value of the current word, which is completely dynamic and cannot be bounded at the time the formula is defined. Hence safeWordLength should now be def safeWordLength : Option[Timeout] and use the Option monad to propagate None up in a formula as required
safeWordLength
can now only be compute for the subset of formulas corresponding to the old formulas. For example we can have a formula that uses a Now that builds an eventually with a timeout defined on the value of the current word, which is completely dynamic and cannot be bounded at the time the formula is defined. HencesafeWordLength
should now bedef safeWordLength : Option[Timeout]
and use the Option monad to propagateNone
up in a formula as required