Supporting more Prism language constructs #4
Description
The following model cannot be parsed by EvoChecker parser
mdp
module m
a: [0..5] init 0;
b: bool init true;
c: [0..1] init 0;
// don't work
[] b=false -> (b'=true); // true/false not parsed
[] a>0 & (b | !a=3) -> 1:(a'=a); // problems with operators/parentheses?
[] a>0 & (b & !a=3) -> 1:(a'=a);
[] a>0 & (b & !(a=3)) -> 1:(a'=a);
// works
[] a>0 & (b & a!=3) -> (a'=a);
[] c=0 -> (c'=1); // boolean variable converted into INT
endmodule
the following errors are produced
line 9:5 no viable alternative at input 'false'
line 9:18 no viable alternative at input 'true'
line 11:14 no viable alternative at input '&(b|!'
line 11:14 no viable alternative at input '!'
line 12:14 no viable alternative at input '&(b&!'
line 12:14 no viable alternative at input '!'
line 13:14 no viable alternative at input '&(b&!'
line 13:14 no viable alternative at input '!'