Add version of Voting.tla that can be analyzed by Apalache.

[nano-o]

[muenchnerkindl]

Thanks for adding this! See above for two minor remarks on comments in the TLA module. Also, the module should be added to the manifest for the CI to succeed.

[nano-o]

@muenchnerkindl Thanks for having a look. I cannot find your remarks? Where are they?

[ahelwer]

This looks good to me, interesting to learn that Apalache doesn't use a separate model file for constants but defines everything in one file.

[nano-o]

This looks good to me, interesting to learn that Apalache doesn't use a separate model file for constants but defines everything in one file.

Maybe a better way would be to be to make a few changes to Voting.tla:

• Rewrite ShowsSafeAt and SafeAt in Voting.tla to not use integer ranges (which Apalache does not support when the bounds are not constant).
• Make Ballot a constant

Then I think VotingApalache could just instantiate Voting and make the necessary substitutions.

[lemmy]

This looks good to me, interesting to learn that Apalache doesn't use a separate model file for constants but defines everything in one file.

Maybe a better way would be to be to make a few changes to Voting.tla:

• Rewrite ShowsSafeAt and SafeAt in Voting.tla to not use integer ranges (which Apalache does not support when the bounds are not constant).
• Make Ballot a constant

Then I think VotingApalache could just instantiate Voting and make the necessary substitutions.

Instead of changing Voting.tla, doesn't Apalache come with functionality that lets users redefine operators during model checking (similar to what TLC has)?

[muenchnerkindl]

@muenchnerkindl Thanks for having a look. I cannot find your remarks? Where are they?

@nano-o One comment was about a spurious "for" in the introductory comment, which I believe you removed already. The second one was about your remark about Ballot being used as the domain of a function: I don't see where you are pointing, and I suspect that the problem is rather the existential quantifier over ballots in the definition of ShowsSafeAt.

[nano-o]

I tried to make it a little cleaner by moving the definitions of constants to a different file.

Instead of changing Voting.tla, doesn't Apalache come with functionality that lets users redefine operators during model checking (similar to what TLC has)?

Module instantiation is supported, but I don't think you can redefine things like you can with a .cfg file. @konnov is that correct?

[muenchnerkindl]

About making Ballot a constant, what properties would you have to require? You clearly need a linear order, anything else?

[nano-o]

@nano-o One comment was about a spurious "for" in the introductory comment, which I believe you removed already. The second one was about your remark about Ballot being used as the domain of a function: I don't see where you are pointing, and I suspect that the problem is rather the existential quantifier over ballots in the definition of ShowsSafeAt.

You're right, this comment does not make sense.

[nano-o]

About making Ballot a constant, what properties would you have to require? You clearly need a linear order, anything else?

I don't think Apalache supports uninterpreted types of unspecified cardinality. So you would have to explicitly define the set of ballots anyway.

[muenchnerkindl]

About making Ballot a constant, what properties would you have to require? You clearly need a linear order, anything else?

I don't think Apalache supports uninterpreted types of unspecified cardinality. So you would have to explicitly define the set of ballots anyway.

I understand that the question is not very relevant for model checking, but Voting.tla is also used for theorem proving, so it should state the necessary assumptions for the correctness proof to go through.

[nano-o]

About making Ballot a constant, what properties would you have to require? You clearly need a linear order, anything else?

I don't think Apalache supports uninterpreted types of unspecified cardinality. So you would have to explicitly define the set of ballots anyway.

I understand that the question is not very relevant for model checking, but Voting.tla is also used for theorem proving, so it should state the necessary assumptions for the correctness proof to go through.

Sorry, I lost track of the context. I think that just assuming that Ballot is linearly ordered would be enough if, like in Voting2.tla, we do not use + and ranges (otherwise we would need assumptions about those too).

[konnov]

I tried to make it a little cleaner by moving the definitions of constants to a different file.

Instead of changing Voting.tla, doesn't Apalache come with functionality that lets users redefine operators during model checking (similar to what TLC has)?

Module instantiation is supported, but I don't think you can redefine things like you can with a .cfg file. @konnov is that correct?

I think you can replace constants with constant expressions in the .cfg, but it was long time since I tried that in Apalache. There is also this way to replace operators, but it is very Apalache-specific.

[lemmy]

There is also this way to replace operators, but it is very Apalache-specific.

Did you create the prefix convention before introducing type annotations? It appears to me that using some annotation to defining overrides is more preferable than a prefix convention.

[konnov]

There is also this way to replace operators, but it is very Apalache-specific.

Did you create the prefix convention before introducing type annotations? It appears to me that using some annotation to defining overrides is more preferable than a prefix convention.

That's true. This convention was introduced way before annotations in comments. It's actually quite a good idea to do overrides in annotations.

Update: see https://github.com/informalsystems/apalache/issues/2818.

[shonfeder]

Instead of changing Voting.tla, doesn't Apalache come with functionality that lets users redefine operators during model checking (similar to what TLC has)?

Unfortunately Apalache cannot currently cope with Voting.tla as is, as explained in https://github.com/informalsystems/apalache/issues/2816#issuecomment-1906402538

However, it seems like like a small refactor may be enough to make it Apalache compatible?

[lemmy]

However, it seems like like a small refactor may be enough to make it Apalache compatible?

Refactoring of Apalache or Voting.tla? In my opinion, TLA+ examples should not be customized for a specific tool unless it is limited to a model checking (MC) file. Specifications are primarily meant to be readable by humans.

[shonfeder]

For Apalache we need to add a new feature. The refactor would be of the Voting spec.

The 5 line refactor I propose in the link would not impact readability afaict. But I have no opinion here nor an agenda. Just sharing the current limitations and the known workaround.

Cheers.

[muenchnerkindl]

Refactoring of Apalache or Voting.tla? In my opinion, TLA+ examples should not be customized for a specific tool unless it is limited to a model checking (MC) file. Specifications are primarily meant to be readable by humans.

I completely agree. However, separating the proof in Consensus.tla from the specification module (and importing WellFoundedInduction.tla only in the proof) would IMHO be acceptable if this is enough to fix the problem. In fact, it would make sense to add the Paxos proofs to this repo: currently, they are found in the TLAPS distribution where they are much less visible. This would require some light refactoring so that specs and proofs are aligned.

[nano-o]

@muenchnerkindl if you want to do that, make a different PR and then I'll rebase on yours.

[ahelwer]

@muenchnerkindl @nano-o is this still blocked? I'm happy to do a bit of work to get this unblocked if so. Stephan I just need to take the proofs from the TLAPS repo for Paxos and get them set up here?

[nano-o]

@ahelwer this is blocked until we factor out the proofs that cause Apalache to fail.