moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
133 stars 74 forks source link

Error when parsing very large integer constants #60

Closed KevinBatz closed 4 years ago

KevinBatz commented 4 years ago

Hi everyone,

parsing the following prism program with storm

`dtmc const N = 10000000000; module chain

c : [0..N] init 0;
f : bool init false;

[] (c < N) -> (0.000000001): (f'=true) + (0.99999999) : (c'=c+1);

endmodule label "goal" = f=true;`

causes the error

expecting \< integer expression >, here: const N = 10000000000; ^

For N=10^9, however, everything works fine.

Best regards, Kevin

sjunges commented 4 years ago

Interesting bug.

As a workaround, I propose to use:

const int M1 = 1000; const int M2 = 10000000; const int N = M1 * M2.

Parsing passes with the current version of storm. Whether model building is successful is unclear due to the size of the model.

tquatmann commented 4 years ago

Should be fixed now. Please don't try 10^19 ;)