Supporting more Prism language constructs

[gerasimou]

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 '!'

[maormann]

Thank you for pointing this out. Now I'll probably have to rewrite my model a bit. 😅

[gerasimou]

There have been some ongoing updates, including in the parser, (not yet in the public version), so if you have any particular constructs or commands that cause issues and could be added, please let me know.

[maormann]

Hey @gerasimou,

there is nothing new from me here. After switching from boolean variables to int [0..1], Evochecker now works. I was very happy that formulas were not affected.

formula s1_needs_probing = (s1_latest_probe = s1_latest_probe_max) | (s1_knowledge = 1);
[start_UAC] uac_s = 0 & successful_invocation = 0 & ! s1_needs_probing & s2_needs_probing ...

Many thanks and all the best. I'm looking forward to the new version when it comes out.