Parsing some modal formulae with time fails

[jgroote]

Issue migrated from trac ticket # 1434

component: Core: Parse Library | priority: minor | resolution: fixed

2017-09-29 12:57:15: @tneele created the issue

---

For some modal formulae with time, the parser fails. For instance for the formula

<true . true @ 5 > true

the parser returns the error

Line 1, column 23: syntax error after 'true'
  <true . true @ 5 > true

There is a workaround: changing the formula to <true . (true @ 5) > true resolves the issue.

[jgroote]

2017-09-29 17:57:31: @wiegerw commented

---

The formula within the angle brackets is parsed as (true . true) @ 5, where true . true is a regular formula. This fails, since for regular formulas the @ operator is undefined.

This particular case can be solved by adding RegFrm ('@' $binary_op_left 34) DataExpr to the grammar for regular formulas. I don't know if this solution has any side effects.

[jgroote]

2017-11-15 15:50:38: @tneele commented

---

It turns out there are more issues with the parsing of timed mu calculus formulae. The following properties also yield a syntax error:

<true @ 7.5 > true
<true @ (5) > true

Especially for the first property, this is annoying, since I cannot come up with a workaround for that issue.

[jgroote]

2017-11-15 16:27:13: @wiegerw commented

---

I think this is because real numbers like 7.5 are not supported by the parser. So the parser will treat this as a list element, which fails.

[jgroote]

2017-11-15 16:35:30: @tneele commented

---

Okay, agreed. Even then, I want to be able to express the property that in the initial state some action is possible at time 7.5. I've tried the following variations:

<true@15/2>true
<true@(15/2)>true
<true@val(15/2)>true

These also lead to syntax errors. Since there seems to be a structural issue in the parsing of timed formulas, can you please see if this can be fixed?

[jgroote]

2017-11-15 18:04:25: @wiegerw commented

---

The issue is that parsing of the action formula "true @ (5)" currently fails. It has to do with the precedences of the rules for parentheses. If I increase the precedence for data expressions between parentheses to 40, it works.

I find it hard to predict what the consequences of such a change will be. So we first need to figure out what the proper values for those precedences are, and then we can apply this change to the grammar.

[jgroote]

2017-11-16 15:06:22: @wiegerw changed status from new to closed

[jgroote]

2017-11-16 15:06:22: @wiegerw set resolution to fixed

[jgroote]

2017-11-16 15:06:22: @wiegerw commented

---

(In r15078) - Set the precedences of several '(' Expression ')' rules in the grammar to 50, i.e. the highest value. This enables parsing action formulas like 'a @ (2 / 3)'.

N.B. This change doesn't break any of the tests. But the meaning of precedences in dparser isn't completely understood. So if it later turns out that this change has unwanted side effects, it may be necessary to revert it.

Fixes #1434.

[jgroote]

2017-11-16 16:27:35: @tneele commented

---

I'm thinking this issue may need to be reopened, because not all issues have been resolved. Parsing of the formula <true . true@5 > true still results in a syntax error. Of course, this is not as prohibitive as the second problem.

After having a look at the grammar, I don't think we should change the rule for regular formulas. Rather, I think the @ operator for action formulas should have a higher precedence such that it binds stronger than the operators for regular formulas. Formulas of the shape (true.true)@5 make no sense, since consecutive actions can never happen at the same absolute time.

[tneele]

I am reopening this ticket, because the problem I mentioned in the above comment still persists. Parsing formulas of the shape <true . true@5 > true results in a syntax error.