Add smt-encoding option to CLI check command #1054

rodrigo7491 · 2021-10-21T14:20:06Z

~~Tests added for any new code~~
Ran make fmt-fix (or had formatting run automatically on all files edited)
Documentation added for any new functionality
Entry added to UNRELEASED.md for any new functionality

See title. Closes #1053.

shonfeder

Looks good, tho I have a few suggestions.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala

mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala

shonfeder · 2021-10-21T15:23:54Z

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala

@@ -85,6 +88,7 @@ class BoundedCheckerPassImpl @Inject() (val options: PassOptions, hintsStore: Fo
    params.discardDisabled = options.getOrElse("checker", "discardDisabled", true)
    params.checkForDeadlocks = !options.getOrElse("checker", "noDeadlocks", false)
    params.nMaxErrors = options.getOrElse("checker", "maxError", 1)
+    params.smtEncoding = options.getOrElse("checker", "smt-encoding", "oopsla19")


As discussed elsewhere, what about also adding a fallback to an SMT_ENCODING environment variable, that could let users set this for all runs in a given shell environment? (This also makes it easy to run all the integration tests with one flag or the other). I think that could be achieved just by getting the appropriate env var in the case that this is None?

I saw your comment on #1044 about this, I was just not sure to go about it. Do we need to wait for #1036?

Ah that is a good question. I could see an argument either way.

If #1036 ends up including a more general configuration system, I think we'll need to rework this to accommodate either way. My gut feeling is that it would be worth adding the envvar fallback here just for testing purposes, and then that can be reworked for the configuration system later if needed. I think the envvar fallback can be accommodated here with:

params.smtEncoding = options.get("checker", "smt-encoding").orElse(sys.env.get("SMT_ENCODING")).getOrElse("oopsla19")

And in the documentation (perhaps also in the inline CLI docs?) we might note that the envvar is a fall back, but that the CLI flag takes precedence?

What do you think. Seem simple enough do integrate regardless of #1306, or do you think it'd better to wait?

You can do both, but you have to define a sensible priority, which I assume would be (in order of lowest to highest):

Apalache default

ENV

CONFIG

CLI parameter

Changing OutputManager might be a bit annoying, because this is a non-bool flag. I'd wait for #1048 (to add config file support, env can be done now), when config flags all go through PassOptions and the manager doesn't track flags anymore.

Also,

Suggested change

params.smtEncoding = options.getOrElse("checker", "smt-encoding", "oopsla19")

params.smtEncoding = options.getOrElse("checker", "smt-encoding", oopsla19Encoding)

@shonfeder I think we can add this now, but I have two questions:

In my Linux distro the SMT_ENCODING env var is not being used. I assume this is the same for other OSs. Is there a way to be sure?

Your suggestion to update params.smtEncoding does not seem to work because the default for smtEncoding in CheckCmd cannot be None. The code below works with "" as default, but is not very nice.

var smtEncodingCLI: Option[String] = options.get("checker", "smt-encoding") smtEncodingCLI = if (smtEncodingCLI.get.equals("")) None else smtEncodingCLI params.smtEncoding = smtEncodingCLI.orElse(sys.env.get("SMT_ENCODING")).getOrElse("oopsla19")

I tried using Option.filter to inline this, but it didn't work. Any suggestions?

@Kukovec I think the priority order makes sense. Will leave CONFIG out for now, as suggested.

I can have a look at the code later to see where you're getting hung up. I guess the getOrElse method on options must not have the signature I expected (given the signature from Option for the method of the same name)? You solution there seems ok, tho could probably be streamlines with some mapping?

By mapping you mean key-value pairs or something else? Not sure how the former can help here.

Sorry, mapping was probably not a helpful word there. But I mean using map on an option type. Not terribly relevant tho.

Your suggestion to update params.smtEncoding does not seem to work because the default for smtEncoding in CheckCmd cannot be None.

I don't follow actually. iiuc, the code snippet I gave should not return None as a default. It should default to the given string if all previous values in the chain are None. Trying to compile it now seems to work OK. I'll make a PR into your branch by way of illustrating.

shonfeder · 2021-10-21T16:51:35Z

One other thought: now that we have a CLI arg, would it make sense to add one or more integration tests here that exercise it?

rodrigo7491 · 2021-10-22T10:17:15Z

One other thought: now that we have a CLI arg, would it make sense to add one or more integration tests here that exercise it?

There is nothing to test yet, so I'm not sure. I assume that after enabling the env var, no refactoring will be needed in the integration tests, unlike it was done in #1051 for the unit tests.

My idea is to use the same tests for both encodings,since they should produce the same results. I plan to gradually enable parts of the test suite for the new encoding as development progresses.

Co-authored-by: Shon Feder <shon@informal.systems>

shonfeder · 2021-10-22T12:52:20Z

One other thought: now that we have a CLI arg, would it make sense to add one or more integration tests here that exercise it?

There is nothing to test yet, so I'm not sure. I assume that after enabling the env var, no refactoring will be needed in the integration tests, unlike it was done in #1051 for the unit tests.

My idea is to use the same tests for both encodings,since they should produce the same results. I plan to gradually enable parts of the test suite for the new encoding as development progresses.

Ok! That makes sense to me :)

shonfeder · 2021-10-22T17:46:12Z

hmmm I don't know why CI is not running for this PR>

rodrigo7491 · 2021-10-22T17:58:30Z

hmmm I don't know why CI is not running for this PR>

Conflict on UNRELEASED?

shonfeder · 2021-10-22T19:07:41Z

Could be!

…encoding-option Suggestion for CLI option processing

shonfeder · 2021-10-25T14:50:49Z

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala

+  /**
+   * The SMT encoding to be used.
+   */
+  var smtEncoding: String = ""
+


I'd like to briefly review the way this value gets used to convince myself that an empty string make sense here. Otherwise, LGTM!

Ok, I understand.

We use the ModelCheckerParams essentially as a struct of parameter values that our various checker's consult to determine their behaviors. For some reason, some of these paramters are passed in via arguments to the constructor, and some are set via mutable assignment. This does not seem ideal to me, but @rodrigo7491 is just following the existing example.

Setting this value to an empty string as a default does not seem ideal to me, however, I have followup work planned that will transform these kind of flag into an enum (see #1056), and this will naturally be cleaned up as part of that work.

Add smt-encoding option to CLI check command

9e21f78

shonfeder reviewed Oct 21, 2021

View reviewed changes

rodrigo7491 added 2 commits October 22, 2021 10:17

Add documentation of smt-encoding cli option

1a9caa0

fix statistics file path

c0db92a

refactor smtEncoding default value

0dc5b43

Co-authored-by: Shon Feder <shon@informal.systems>

rodrigo7491 and others added 2 commits October 22, 2021 17:54

Add smt-encoding env var option

05c905b

Suggestion for CLI option processing

4529abb

shonfeder closed this Oct 22, 2021

shonfeder reopened this Oct 22, 2021

Fix optional CLI parsing

33423fd

rodrigo7491 added 2 commits October 25, 2021 10:44

Merge pull request #1055 from informalsystems/shon/suggestion/ro/cli-…

47bec69

…encoding-option Suggestion for CLI option processing

Merge branch 'unstable' into ro/cli-encoding-option

a484f00

shonfeder reviewed Oct 25, 2021

View reviewed changes

shonfeder approved these changes Oct 25, 2021

View reviewed changes

rodrigo7491 merged commit 521be67 into unstable Oct 25, 2021

rodrigo7491 deleted the ro/cli-encoding-option branch October 25, 2021 15:19

shonfeder mentioned this pull request Oct 25, 2021

Add CI set up for smt-encoding work #1061

Merged

4 tasks

rodrigo7491 mentioned this pull request Oct 28, 2021

Expose output configuration via CLI arguments #1062

Merged

4 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add smt-encoding option to CLI check command #1054

Add smt-encoding option to CLI check command #1054

rodrigo7491 commented Oct 21, 2021 •

edited

Loading

shonfeder left a comment

shonfeder Oct 21, 2021

rodrigo7491 Oct 21, 2021

shonfeder Oct 21, 2021

Kukovec Oct 22, 2021

Kukovec Oct 22, 2021

rodrigo7491 Oct 22, 2021 •

edited

Loading

rodrigo7491 Oct 22, 2021

shonfeder Oct 22, 2021

rodrigo7491 Oct 22, 2021

shonfeder Oct 22, 2021

shonfeder commented Oct 21, 2021

rodrigo7491 commented Oct 22, 2021

shonfeder commented Oct 22, 2021

shonfeder commented Oct 22, 2021

rodrigo7491 commented Oct 22, 2021

shonfeder commented Oct 22, 2021

shonfeder Oct 25, 2021

shonfeder Oct 25, 2021

	params.smtEncoding = options.getOrElse("checker", "smt-encoding", "oopsla19")
	params.smtEncoding = options.getOrElse("checker", "smt-encoding", oopsla19Encoding)

Add smt-encoding option to CLI check command #1054

Add smt-encoding option to CLI check command #1054

Conversation

rodrigo7491 commented Oct 21, 2021 • edited Loading

shonfeder left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

rodrigo7491 Oct 22, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shonfeder commented Oct 21, 2021

rodrigo7491 commented Oct 22, 2021

shonfeder commented Oct 22, 2021

shonfeder commented Oct 22, 2021

rodrigo7491 commented Oct 22, 2021

shonfeder commented Oct 22, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

rodrigo7491 commented Oct 21, 2021 •

edited

Loading

rodrigo7491 Oct 22, 2021 •

edited

Loading