search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
194 stars 40 forks source link

reqparser error: UnexpectedRequirementsParserFailureResult #422

Open Breee opened 5 years ago

Breee commented 5 years ago

Ultimate fails to parse test_req in the following example: 

CONST MAX_TIME IS 50.0

Input x IS bool
Input y IS bool

test_req: Globally, it is always the case that if "x" holds for at least "10 * MAX_TIME" time units, then "y" holds afterwards

Ultimate produces a UnexpectedRequirementsParserFailureResult, caused by a parsing error in the reqparser:

[2019-04-11 11:13:53,094 INFO  L276        PluginConnector]: ReqParser initialized
[2019-04-11 11:13:53,094 INFO  L430   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: reqparser_error.req
[2019-04-11 11:13:53,094 INFO  L94               ReqParser]: Parsing file reqparser_error.req
[2019-04-11 11:13:53,111 ERROR L320              ReqParser]: reqparser_error.req:6:77: Syntax Error
[2019-04-11 11:13:53,112 ERROR L93     ReqParserResultUtil]: The parser failed on some requirements from reqparser_error.req

The 10 * MAX_TIME are responsible for the failure.

The error log is attached. reqparser_error.req.log

danieldietsch commented 5 years ago

Fixing this issue is more involved than it appears. As it can usually be fixed manually, we will postphone it a little bit.