Title SAS^+ parser does not fail on additional operators
Priority bug Status chatting
Superseder Nosy List florian, jendrik, malte
Assigned To Keywords
Optional summary

Created on 2022-01-19.19:02:15 by florian, last changed by florian.

File name Uploaded Type Edit Remove florian, 2022-01-19.19:17:58 application/octet-stream
msg10463 (view) Author: florian Date: 2022-01-19.19:37:43
> I'm not sure, but I expect we'd even interpret every non-integer token (e.g.
> the word "bla") as the number 0 without complaining.

Yes, I think this is the problem in this case: the second "begin_operator" is parsed as 0 and that is then interpreted as "there are no axioms". After the axiom section, there is nothing left to parse, so the parser returns and the search starts.
msg10462 (view) Author: malte Date: 2022-01-19.19:33:37
Ah, I see. Generally speaking, I think we're doing very little to check the validity of the files, which are treated mostly as internal. But of course we do document the format and occasionally encourage people to generate it themselves, so perhaps this lack of checks is something we should change.

For example, we document line breaks but I think we don't care about them at all except perhaps around magic words where we might use line-based input rather than token-based input. I don't think we range-check any of the integers except perhaps via assertions, which are a debug feature rather than an input validation feature. I'm not sure, but I expect we'd even interpret every non-integer token (e.g. the word "bla") as the number 0 without complaining. There are also more semantic things like affecting the same variable twice with non-conditional effects, which we don't allow.

That doesn't mean I'd be against introducing checks that people find useful. But then perhaps we should consider doing this consistently while we're looking at this part of the planner.

All the mentioned possible deficiencies are from memory. Perhaps we do actually check the input and I forgot. :-)
msg10461 (view) Author: florian Date: 2022-01-19.19:19:45
I had already deleted the file, but it's not too complicated. With "declared", I meant the number above the first "begin_operator" that says how many operators there will be. It is 1 in this case, but then there two blocks of "begin_operator ... end_operator" (and no axiom section).
msg10460 (view) Author: malte Date: 2022-01-19.19:07:22
I think no file was attached, can you add it? Not sure what you mean with "declared" vs. "defined", looking forward to seeing the file. :-)
msg10459 (view) Author: florian Date: 2022-01-19.19:02:14
In the attached file, one operator is declared but then two are defined. I would have expected the parser to parse the first operator and then try to parse the axiom section and fail because instead of a number of axioms, it gets "begin_operator". But instead, the parser accepts the file.
Date User Action Args
2022-01-19 19:37:43floriansetmessages: + msg10463
2022-01-19 19:33:38maltesetmessages: + msg10462
2022-01-19 19:19:45floriansetmessages: + msg10461
2022-01-19 19:17:58floriansetfiles: +
2022-01-19 19:07:22maltesetstatus: unread -> chatting
messages: + msg10460
2022-01-19 19:02:15floriancreate