-
-
Notifications
You must be signed in to change notification settings - Fork 40
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
shonfeder
committed
Mar 29, 2021
1 parent
ead57bb
commit b9d04a0
Showing
12 changed files
with
45 additions
and
43 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
## 0.15.0 | ||
|
||
### Features | ||
|
||
* Model checker: receiving the types from with the type checker Snowcat, see #668 and #350 | ||
* Model checker and type checker: Snowcat is the only way to compute types now | ||
* Type checker: the old Apalache type annotations are no longer supported, see #668 | ||
* Type checker: tagging all expressions with the reconstructed types, see #608 | ||
* Type checker: handling TLA+ labels like `lab("a", "b") :: e`, see #653 | ||
* Type checker: always treating `<<...>>` in `UNCHANGED <<...>>` as a tuple, see #660 | ||
* Type checker: handling the general case of EXCEPT, see #617 | ||
* Preprocessing: handling the general case of EXCEPT, see #647 | ||
|
||
### Changed | ||
|
||
* Preprocessing: massive refactoring of the passes to support types. This may have introduced unexpected bugs. | ||
* Model checker: translation rules for records and functions have been modified, in order to support new types. Bugs to | ||
be expected. | ||
* Intermediate representation: renamed BmcOper to ApalacheOper. Its operators have the prefix `Apalache!` now. | ||
|
||
### Removed | ||
|
||
* Unused rewriting rules and `FailPredT` in the model checker, see #665 | ||
* Intermediate representation: removed non-standard operators subsetProper, supset, supseteq, see #615 | ||
* Intermediate representation: removed TlaArithOper.{sum,prod}, as they are not standard, see #580 | ||
* Intermediate representation: removed TlaOper.chooseIdiom |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters