Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
LeuLinda opened this issue Jul 30, 2018 · 1 comment

Comments

@LeuLinda
Copy link

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
Copy link
Contributor

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

@volkm volkm closed this as completed May 9, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants