Skip to content
  • Alexandre Duret-Lutz's avatar
    Add a new length_boolone() function to fix an assert in randpsl. · ed0dd0b4
    Alexandre Duret-Lutz authored
    * src/ltlvisit/length.hh (length_boolone): New function.
    * src/ltlvisit/length.cc (length_boolone): Implement it using...
    (length_boolone_visitor): ... this new visitor.
    * src/ltltest/randltl.cc: Use length_boolone() to check the result
    of the random generator, and ignore any formula larger (in
    length()) than opt_f.  This fix a bug where the random formula
    generator would sometime produce formula larger than requested,
    because of the trivial rewriting of {f}[]->e as e|!f.
    * src/ltltest/length.cc: Add option -b to call length_boolone().
    * src/ltltest/length.test: Test length_boolone().
    ed0dd0b4