Cannot convert unterminated properties

[HansvdLaan]

The file below is a valid PRISM property file. However when trying to convert it with storm we get an error saying that formula could not be parsed.

In a PRISM property file, properties aren't required to be seperated by an ';'. It seems as the converter has this as an (implicit) requirement.

Properties

// property_1
Pmin=? [ F state = 1 ]

// property_2
Pmin=? [ F state = 2 ]

Error:

hans@debian:~/storm/build/bin$ ./storm-conv --prism ../../../Documents/testcases/nested_pctl_1/prism_pctl_benchmark.nm --tojani ../../../Documents/testcases/nested_pctl_1/prism_pctl_benchmark.jani --prop ../../../Documents/testcases/nested_pctl_1/properties.props
Storm-conv 1.3.1 (dev)

Date: Tue Apr  9 09:44:05 2019
Command line arguments: --prism ../../../Documents/testcases/nested_pctl_1/prism_pctl_benchmark.nm --tojani ../../../Documents/testcases/nested_pctl_1/prism_pctl_benchmark.jani --prop ../../../Documents/testcases/nested_pctl_1/properties.props
Current working directory: /home/hans/storm/build/bin

Parsing PRISM input ... ERROR (FormulaParser.cpp:91): Could not parse formula.
ERROR (storm-conv.cpp:338): An unexpected exception occurred and caused Storm-conv to terminate. The message of this exception is: std::exception

[tquatmann]

The Prism Website states the following about this:

A PRISM properties file can contain any number of properties. It is good practice, as shown in the examples above, to terminate each property with a semicolon. Currently, this is not enforced by PRISM (to prevent incompatibility with old properties files) but this may change in the future.

In Storm we decided to enforce this as this simplifies the parsing process (which is already complicated enough). I can see that the error message could be more descriptive, though.