moves-rwth / storm

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

undefined constants that are declared in a properties file are assumed to be 0 #31

Closed LeuLinda closed 5 years ago

LeuLinda commented 6 years ago

When declaring a constant in a properties file, but not defining it (neither in the file nor via command line) storm assumes the constant to be 0. 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;
P=? [F num_rounds = k];

the result 1 is returned although k is not specified.

cdehnert commented 6 years ago

This should be fixed in the current state of master. Can you verify this?