gerasimou / EvoChecker

EvoChecker
GNU General Public License v2.0
4 stars 3 forks source link

Problems when parsing guards in reward structures #6

Open ytzemih opened 3 years ago

ytzemih commented 3 years ago

Hi, I found some issues with the parser, please, see below:

mdp
// evolve int p [1..10];
module m
a: [0..5] init 0;
b: bool init true;
c: [0..1] init 0;
[] a>0 & (b & a!=3) -> (a'=a);
[] c!=1 -> (c'=1);
endmodule

rewards "test"
// works
[] a>1 & b : 10; 
[] a>1 & (c=1) : 10; 
[] a>1 & (c!=1) : 10; 
// doesn't work
[] a>1 & !b : 10; 
[] a>1 & b=false : 10; 
endrewards

Nice work otherwise. Thanks.