search

GLaDOS-Michigan / dafnyMC

Integrating protocol debugging workflows into dafny
https://dafny-lang.github.io/dafny/
Other
0 stars 0 forks source link

Implement Apalache Compiler #9

Open TonyZhangND opened 2 years ago

TonyZhangND commented 2 years ago

Implement the Dafny to Apalache compiler

TonyZhangND commented 2 years ago

Since Apalache programs are also TLA programs, implement this as a mode in the TLA Compiler class. The alternative of implementing it in a separate class leads to too much code duplication.

TonyZhangND commented 2 years ago

Support for all Apalache datatypes, except for union types, added in commit 3d6e7269.

TonyZhangND commented 2 years ago

Variants are being added (or already added?) to Apalache! See design doc section 1.3.

Looks like experimental support is added in version 0.24.0. Let's check it out.

TonyZhangND commented 2 years ago

It looks like support for variant types is not yet enabled in version 0.24.1. Track Issue 401 in Apalache for updates on this feature.

If this feature does not come in time, Section 3.3 in the paper suggests annotating "the records and their sets with a super type"

In any case, I have implemented the plumbing for Apalache variants in the Dafny compiler, in commit eca23ac.