User profiles

[konnov]

In the recent months, we were oscillating between turning off and on by default some of the command line parameters. Here are some of the related issues that showed up:

• PR Make example trace output optional via --save-runs #2047: disabling --save-runs (now called --output-traces) by default as it may affect performance.
• Comment in [BUG] Log message is not ideal on exhausting state space that is the image of View #1040: --no-deadlock should be disabled by default, as it may produce unclear output and may affect performance.
• Reviewing the Entry-level Model Checker Tutorial #2017 (not written there, but communicated by Hillel) : the default location of counterexamples is not friendly to the beginners.
• Reviewing the Entry-level Model Checker Tutorial #2017: the tool output is verbose.
• Don't check Inv in state 0 with --init=Inv #1825: the default behavior when checking inductive invariants is annoying
• [FEATURE] Add flags to control verbosity of output #278: do not show timestamps

It is more or less clear that we have a conflict between the beginner's settings and expert settings. As @bugarela suggested, we probably should introduce user profiles, to choose between different combinations of default parameters.

I would like to open a discussion on this. In my opinion, it would be great to have at least two profiles. Most likely, we will need an additional profile for external tools later.

Expert profile

The main goal is to do exactly what the user is asking for, and no more than that.

• Turn off by default everything that seriously affects performance of the search:
  • --output-traces is disabled
  • --no-deadlock is enabled
• If some search behavior is affected by the options, the decisions should be reflected in the detailed.log (as they are now).
• The console output is kept to the minimum, e.g., no timestamps are printed, except the final running times.
• The intermediate files go to the directory that is set up via config options (as it is now).

The tools that call Apalache probably fall into this category too.

Beginner profile

Maximize whatever can be computed by the tool in a single run. Assuming that the user is discovering how the tool can help them.

• Turn on by default everything that may help the user learn something new about their spec:
  • --output-traces is enabled. If the tool reports no error, the user may at least inspect the example trace and check their intuition about the spec. Obviously, no beginner would know that --output-traces even exists.
  • --no-deadlock is disabled. If we manage to find a deadlock, the user will learn something new. Although deadlock detection is incomplete (see [BUG] Deadlock detection may report false negatives #711), it may still be useful.
• The console output only suppresses the messages by the passes before PASS 12 and it shows only the messages by PASS 13: Bounded checker, which are important for learning where Apalache is searching and how. Importantly, timestamps are shown, so the user may learn about bottlenecks in their specs.
• The intermediate files (including counterexamples and examples) go to a simply named directory, e.g., ./results. So a beginner user does not have to struggle with weird-looking directory names.

[konnov]

@tesnimab, @bugarela, @shonfeder, @thpani, @Kukovec, @rodrigo7491, what are your thoughts on that?

[konnov]

There are two very important sentences about the goals of the users:

• Beginner's profile: Maximize whatever can be computed by the tool in a single run. Assuming that the user is discovering how the tool can help them.
• Expert's profile: The main goal is to do exactly what the user is asking for, and no more than that.

An expert, even being an expert, does not have to know in detail, how a certain option propagates to z3. We basically want to guarantee that we are not changing the tool performance for the expert profile, when we are adding new features. This happened several times. An expert is not always an Apalache developer.

[thpani]

I'm not arguing about the expert profile, it is exactly as I think things should be.

I'm not convinced by the need for a beginner profile; I think it just points to bad default behavior of the tool.

Beginner's profile: Maximize whatever can be computed by the tool in a single run. Assuming that the user is discovering how the tool can help them.

This can be computationally costly, and could drive beginners away thinking that Apalache is not performant. I think also Hillel pointed out in his review of the tutorial that there is already too much information handed to the novice user, not too little.

[konnov]

Beginner's profile: Maximize whatever can be computed by the tool in a single run. Assuming that the user is discovering how the tool can help them.

This can be computationally costly, and could drive beginners away thinking that Apalache is not performant. I think also Hillel pointed out in his review of the tutorial that there is already too much information handed to the novice user, not too little.

The difference is that beginners are playing with tiny examples as they learn, so for them it would not make a difference. It is too much information, because most of it is not useful information any longer. (It was useful when the tool was crashing in arbitrary passes.)

[thpani]

I don't think people can really learn about a tool if you just hand them a sledgehammer.
How do people graduate from beginners to experts in this model? Seems there is a high cliff when they want to switch from beginner to expert profiles.

[thpani]

Maybe our first priority should be

• clean up the output + make sure it's useful,
• make sure we have sensible defaults on existing flags,
• weed out flags that are unnecessary (or limit them to text config files).

On these issues we have a much stronger signal from users.

I'd be surprised if we still need user profiles after this. If we do, I'm happy to revisit.

[thpani]

Not a big fan of user profiles, I think we can do without.
If there's only two that we can think of, the beginner profile should be Apalache without any flags.

More detailed thoughts on individual points:

• Reviewing the Entry-level Model Checker Tutorial #2017 (not written there, but communicated by Hillel) : the default location of counterexamples is not friendly to the beginners.

• Reviewing the Entry-level Model Checker Tutorial #2017: the tool output is verbose.

These two are general feedback on the output we generate.
I think they should be addressed by improving the quality of output, not by adding user profiles.

• Don't check Inv in state 0 with --init=Inv #1825: the default behavior when checking inductive invariants is annoying

I don't see how we would address this with user profiles?
It just needs some additional logic for when --init equals --inv.

• If some search behavior is affected by the options, the decisions should be reflected in the detailed.log (as they are now).

I think we should do this either way?

• The console output is kept to the minimum, e.g., no timestamps are printed, except the final running times.

Why? Especially experts will want to understand bottlenecks in checking their spec.

The tools that call Apalache probably fall into this category too.

The preferred way to do this would be via the server mode and chai?

• --output-traces is enabled. If the tool reports no error, the user may at least inspect the example trace and check their intuition about the spec. Obviously, no beginner would know that --output-traces even exists.

We already have simulate that covers this behavior.
Also, I still need to see a user who actually wants this feature 😄

• --no-deadlock is disabled. If we manage to find a deadlock, the user will learn something new. Although deadlock detection is incomplete (see [BUG] Deadlock detection may report false negatives #711), it may still be useful.

Not sure if this is well-motivated. If an invariant is violated, the user also learns something, yet we don't check invariants by default.

• The console output only suppresses the messages by the passes before PASS 12 and it shows only the messages by PASS 13: Bounded checker, which are important for learning where Apalache is searching and how. Importantly, timestamps are shown, so the user may learn about bottlenecks in their specs.

I think the passes before BMC are stable enough to do this in any case (modulo type-checking for user feedback).

• The intermediate files (including counterexamples and examples) go to a simply named directory, e.g., ./results. So a beginner user does not have to struggle with weird-looking directory names.

I don't think beginner users care much about these files. The relevant output should be on the console. If beginners have to go searching for files, there's something wrong with what we're printing to stdout.

[konnov]

Not sure if this is well-motivated. If an invariant is violated, the user also learns something, yet we don't check invariants by default.

We do not check invariants by default, because there are no default invariants. If there were some, we could check them.

[thpani]

We do not check invariants by default, because there are no default invariants. If there were some, we could check them.

I mean, we default --init to Init and --next to Next; why not default --inv to Inv?

[konnov]

I don't think beginner users care much about these files. The relevant output should be on the console. If beginners have to go searching for files, there's something wrong with what we're printing to stdout.

This is also an option for the beginner's default behavior. I would not like to stare at long counterexamples in the console output. So I would prefer to have files in the expert mode ;-)

[konnov]

I mean, we default --init to Init and --next to Next; why not default --inv to Inv?

Init and Next are more or less stable idioms in TLA+, whereas Inv is not.

[konnov]

The beginners will read the counterexamples in the output, as you are suggesting. I don't want this behavior as an expert.

[Kukovec]

I'm more or less with Thomas on this, the need for a "beginner" profile just signals sensible defaults, whereas "experts" know how to configure individual flags.

We already have "profiles" as user-customizable sets of flags (not as something we predefine): .cfgs. If I always happen to need, for example, --output-traces disabled and --no-deadlock enabled, I can write a "profile" (config) for myself that has that.

[Kukovec]

Though I suppose it can't hurt to pre-write a few sensible standard configs and ship them with Apalache.