Skip to content
  • Alexandre Duret-Lutz's avatar
    The neverclaim output by spin -f '([]a && XXXX!a)' was not · df2a950e
    Alexandre Duret-Lutz authored
    understood by Spot.
    
    * src/neverparse/neverclaimparse.yy: Support "if :: false fi;"
    instructions.  Spin sometimes output these on dead states.
    Also rewrite the "transitions" rule as a left recursion.
    * src/tgbatest/neverclaimread.test: Adjust output because
    of the right->left recursion change, and add two more formula
    to submit to Spin to test its output.
    df2a950e