Should --only-trace should imply --log when using interaction?

[thoughtpolice]

Consider the DieHard example. If you run it normally, the counterexample is generated. Running it with --only-trace, it obviously succeeds, but simply exits with

specification: trace: success

Now, if you look at the options, this is obvious, since it says it only traces behaviors and turns off model checking. But when I was first using Spectacle, I actually typo'd -t and -l several times which confused me: why did this succeed? Ignoring that entirely though, -t is practically useless without -l because you literally can't see the traces without it. So I just always run with -tl most of the time until I want to check and just run it without either option (or I'm debugging.)

This is more of a UX question than anything: if we're just tracing without checks, should we always diagram the output traces? This will probably impact the Interaction API, of course...

[riz0id]

The CLI doesn't have a great way of doing implying options like GHC will with options or language extensions since the implementation is still naive. I agree its awkward however, I made some changes to the CLI in #55 which will warn users if --trace is flagged without --diagram until the CLI has been developed to the point where there is:

• A canonical method for defining options that should imply other options.
• Mirrored "negative" flags to disable options, similar to --no-* with GHC.