WindowGen
Related Docs:
class WindowGen
| package gen
a dstream generator that has n empty batches followed by bg
a dstream generator that has exactly two batches, the first one is emptyBatch, and the second one is bg
a dstream generator with exactly bg as the only batch
a generator of Batch that generates its elements from g
a generator of Batch that generates its elements from g
a generator of Batch that generates its elements from g
Generator for the weak version of LTL release operator: either bg2 happens forever, or it happens until bg1 happens, including the moment when bg1 happens
Shrink function for Batch
Shrink function for Batch
Although a Batch is a Seq, we need this simple definition of shrink as the default doesn't work properly
Note shrinking assumes no particular structure on the batches, but that is no problem as there is no temporal structure in the Batch generators: note generators like BatchGen.now() are in fact generators of PDStream
a generator of DStream that repeats batches generated by gb1 until a batch generated by bg2 is produced Note bg2 always occurs eventually, so this is not a weak until. When bg2 occurs then the generated DStream finishes This generator is exclusive in the sense that when bg2 finally happens then bg1 doesn't occur. Example: Gen.resize(10, always(BatchGen.ofN(2, 3)) + until(BatchGen.ofN(2, 0), BatchGen.ofN(2, 1)) ). sample //> res34: Option[es.ucm.fdi.sscheck.DStream[Int]] = Some(DStream(Batch(3, 3, 0 //| , 0), Batch(3, 3, 0, 0), Batch(3, 3, 1, 1), Batch(3, 3), Batch(3, 3), Batch //| (3, 3), Batch(3, 3), Batch(3, 3), Batch(3, 3), Batch(3, 3)))
Generators for Batch, a class for representing batches of elements in a discrete data stream. This is a local representation, but you can use
import es.ucm.fdi.sscheck.gen.RDDGen._to get an automatic conversion fromGen[Batch[A]]toGen[RDD[A]]All the temporal generators defined in this object are sized generators, but the size parameters only affects the number of batches in the output DStream, not the size of the batches. The size of the batches can be changed by using Gen.resize in the definition of the batch generator that is passed to these HO generators
On the other hand for generators of arbitrary DStreams like Gen.resize(5, arbitrary[DStream[Int]]) Gen.resize has effect, both in the number of batches and in the size of the batches, as those arbitrary instances are based on arbitrary for lists
TODO That should be tested // by using Gen.resize(5, TLGen.always(Batch(List(0, 1)))) (constant batch size) // and then in Gen.resize(3, TLGen.always(BatchGen.ofNtoM(1, 5, Gen.choose(0, 3)))) // the point is that we always have 3 batches, but Gen.resize doesn't affect the batch // size but only the number of batches //