When defining a constant in a properties file, this can not be parsed. For example, when calling
storm --prism ./model.prism --prop ./props.prop
on the model
dtmc
const double p = 0.4;
const int N = 5;
module one
x: bool init true;
num_rounds : [0..N] init 0;
[a] x & (num_rounds<N) -> p : (num_rounds' = num_rounds+1)
+ (1-p) : (x' = false) & (num_rounds' = num_rounds+1);
[a] x & (num_rounds=N) -> p : true
+ (1-p) : (x' = false);
endmodule
and the properties file
const int k=3;
P=? [F num_rounds = k];
the error message "ERROR (FormulaParser.cpp:101): Could not parse formula." arises, but it works fine, when the properties file is given as
When defining a constant in a properties file, this can not be parsed. For example, when calling
storm --prism ./model.prism --prop ./props.prop
on the modeland the properties file
the error message "ERROR (FormulaParser.cpp:101): Could not parse formula." arises, but it works fine, when the properties file is given as
and the constant k is specified via command line.