While loop not supported inside DEFINITIONS

[leuschel]

For the following B machine we get the error:

! An error occurred (source: parse_error) !
!   expecting: 'INVARIANT'
! Line: 4 Column: 35 until Line: 4 Column: 35 in file: /Users/leuschel/Desktop/TestWhileDEF.mch

MACHINE TestWhileDEF
DEFINITIONS
  AA==1;
  MyWhile == WHILE x > 0 DO x:=x-1 INVARIANT x:NATURAL VARIANT x END
  BB == "WHILE x > 0 DO x:=x-1 INVARIANT x:NATURAL VARIANT x END"
SETS
 ID={aa,bb}

VARIABLES xx
INVARIANT
 xx:ID
INITIALISATION xx:=aa
OPERATIONS
  res <-- Test = VAR x IN BEGIN
            x:=10;
            WHILE x > 0 DO x:=x-1 INVARIANT x:NATURAL VARIANT x END;
           res := x
         END
    END
END

[dgelessus]

The PreParser lexing is wrong here - it interprets the INVARIANT keyword as the end of the DEFINITIONS block and not as part of the right-hand side of MyWhile. Fixed in hhu-stups/probparsers@66b6e4d84530374f68272d75f82477c2cfefdba3.

(There is also a missing semicolon after the MyWhile definition, but that's not the cause of the error.)