storm does not handle absolute property paths properly

[LeuLinda]

When calling storm with something like

storm --prism /Users/linda/some_model --prop /Users/linda/some_props it fails with ERROR (FormulaParser.cpp:101): Could not parse formula. ERROR (storm.cpp:14): An exception caused Storm to terminate. The message of the exception is: Could not parse formula

However, everything works fine when using a relative path for the properties file

storm --prism /Users/linda/some_model --prop ./some_props or when naming the properties file with some arbitrary suffix storm --prism /Users/linda/some_model --prop /Users/linda/some_props.abcd For the models file, every format seems to be OK.

I guess this comes from storm interpreting '/Users/linda/some_props' as a property, not a path to a properties file?

[cdehnert]

Yes, our current "heuristic" for determining whether it is a file or not is whether it includes a dot and whether it exists as a file... Your relative path has a dot, but not for the reason we are looking for it, so it works by coincidence. It's a bit crude, I agree, but we wanted to avoid having several different switches for the properties and there may be properties (for example just consisting of a boolean variable) that have the same name as a file, so there is no chance to uniquely say which one is meant.

[kleinj]

I guess it would make sense to just drop the check that requires a dot? I think it's much more likely to encounter a properties file without dot than having a file lying around where the filename is accidentially a syntactically and semantically valid property.

Or have something like --prop:file and --prop:property (in addition to --prop) to override the auto-detection? This might be good to have to ensure correct interpretation if called from scripting, etc.

[LeuLinda]

I agree with @kleinj. Most ambiguity that is caused by prefering paths to formulas could be avoided by not allowing paths to be a single name (without a dot or a slash). Then, only for existing paths like P=1/2 [F true] it is not clear, whether the path or the formula is meant, but I think that's ok... Nevertheless, I'd say interpreting things like '--prop true' as 'read from some (existing) file named true' would not cause to much confusion, since the computed property is printed to the log.