TraceAbstraction Settings Cleanup

[maul-esel]

As proposed by @Heizmann, this PR is meant to clean up the various settings for TraceAbstraction by

1. grouping related settings into containers (for readability in the developer UI),
2. removing settings that are not (or no longer) relevant to a user,
3. potentially renaming or otherwise modifying settings (:warning: affects existing settings files)

The idea is that everyone looks at the settings for which they feel responsible, and ideally we discuss the changes in person at some point. Feel free to commit proposed changes to this branch.

[maul-esel]

I've started by grouping the concurrency-related settings into containers, and adding some labels.

[maul-esel]

I have not yet removed any obsolete settings. I'm pretty much happy with the concurrency settings as they are. I think @Heizmann had some settings on his list, related to trace checks IIRC. I suggest we discuss them next week and integrate those changes with this PR before we merge.

rendering of the container headings

Just for clarification: The UltimatePreferenceItemContainers are reflected in the list on the left. I suspect you mean the labels acting as dividers between blocks of settings in one page? Then I'd agree; perhaps we should to introduce another grouping mechanism (UltimatePreferenceItemGroup or similar).

[bahnwaerter]

I suspect you mean the labels acting as dividers between blocks of settings in one page?

Yes, I mean the labels of the dividers between setting blocks. Your suggestion sounds great.

[maul-esel]

@bahnwaerter

[danieldietsch]

@maul-esel

1. Is there a reason why you don't use the already existing PreferenceType.Label to separate groups? Did you not know or did you think them too ugly? But I agree, the newest iteration looks nice :)
2. Did you think about how to represent these things in the commandline? E.g., when using-tc "trunk/examples/toolchains/AutomizerC.xml" --help --experimental? Right now, neither the containers nor the new groupings are represented there.
3. We should definitely ask everyone wrt to obsolete settings.
4. We already have some support for experimental options. The CLI has this --experimental flag that shows options that are experimental. Right now, all options without a description are experimental. In the GUI, descriptions translate to tool tips, and labels are directly translated to CLI options. I realize that some of you either don't use the commandline enough, or don't know about the mechanisms behind our help system there. Option names like --traceabstraction.independence.relation.used.for.por.in.concurrent.analysis.#2 <arg> are not nice (I need to remove the character # as well). Anyways, having some kind of "Advanced user" toggle in the GUI as well as descriptions for all options and an additional "advanced" flag for all options might help users. But on the other hand, this might just be way too much work for to little benefit. I would recommend against that. After all, this is a scientific tool.

[danieldietsch]

Ah and, as long as this PR does not remove any settings, I approve 👍

[maul-esel]

• I was using PreferenceType.Label before
• The grouping should not affect the command line options. Or are you referring to giving nicer output in the settings list on the command line?
• @Heizmann @bahnwaerter and I discussed the existing support for experimental options. But I think we agreed that a boolean flag might be better -- if I want a setting to only show up with --experimental, that currently means I am not allowed to document it. That's a bad incentive structure, no? Even if we don't immediately give a description to all options (a lot of effort, I agree), it might be good to separate these two things.

[danieldietsch]

• 1. So, did you want the new grouping because it looks better or for something else? What is a documentation that tells people when to use what? Should we remove "label" to be more consistent?
• 2. Yes, I mean we also should group things on the command line. I would expect most people to use the command line.
• 4. Yes, that's what I meant. We should introduce a flag and transition to that. Note that I think most options should not be experimental, and that I would distinguish (at least internally) between "experimental" and "advanced". The former is just relatively new and might be removed soon (hence the current automatic with "no description"), the latter is just very situational and caters to the desire of some developers to hide settings. Also note how many of our settings do not have a description. I do not think that missing documentation relates to the current "experimental"-automatic, but correct me if you added settings and did not add a description to hide the setting through "experimental". I would say we add a flag and combine it with "no description", i.e., options are experimental if they are flagged as such or if they do not have a description.

[maul-esel]

• (1) UltimatePreferenceItemGroup gives more semantic information than these divider labels. So, in addition to the nicer display in the UI, we have more possibilities in the future (just speculating: maybe --help independence.relation to only show options in a group?)
• (2) :+1: to grouping on the command line.
• (4) :+1:

[bahnwaerter]

One more thing for future development: The settings and groups could be delivered dynamically via the Web-API, so that only a small whitelist configuration for the webserver is necessary. An explicit conversion of *.epf files in a config.json is then no longer necessary. The Web frontend can then decide which permitted settings it presents to the user.

[danieldietsch]

@bahnwaerter : I don't understand how this should work. The settings are already delivered dynamically from the website to the backend. And the backend can run arbitrary toolchains, so we need to consider all settings for the whitelist. It would be desirable to extend the whitelist mechanism with option values or validators instead of just allowing the option.

[danieldietsch]

@maul-esel I could add grouping to the CLI. Perhaps also introduce the experimental-flag and change PreferenceItems to a fluid API.

[maul-esel]

Last chance for comments; otherwise I'll merge tomorrow morning