Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Integrating types 4: migrated tests to Snowcat #652

Merged
merged 4 commits into from
Mar 24, 2021
Merged

Integrating types 4: migrated tests to Snowcat #652

merged 4 commits into from
Mar 24, 2021

Conversation

konnov
Copy link
Collaborator

@konnov konnov commented Mar 15, 2021

This PR fixes type annotations in the integration tests. Several tests are still failing. This PR is created for the purpose of seeing a small diff.

  • 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

shonfeder
shonfeder approved these changes Mar 18, 2021
View reviewed changes
Copy link
Contributor

@shonfeder shonfeder left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, my questions notwithstanding.

test/tla/Paxos.tla
@@ -124,8 +129,13 @@ TypeOK == /\ maxBal \in [Acceptor -> Ballot \cup {-1}]
(* the array `votes' describing the votes cast by the acceptors is defined *)
(* as follows. *)
(***************************************************************************)

\* the original specification does not have this definition, we need it for types
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we need this? Is this kind of thing a short term work around, or a permanent requirement?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it is a permanent construct. It is often too cumbersome to distinguish between tuples and sequences. I was even thinking of introducing operators like in Scala: tuple0(), tuple1(x), tuple2(x, y), ...

test/tla/Paxos.tla Show resolved Hide resolved
@shonfeder
Copy link
Contributor

But, iiuc, we should hold of merging this into the feature branch until that has been reviewed first.

@konnov
Copy link
Collaborator Author

konnov commented Mar 19, 2021

But, iiuc, we should hold of merging this into the feature branch until that has been reviewed first.

Yes, we are doing matryoshka PRs now :)

Kukovec
Kukovec approved these changes Mar 22, 2021
View reviewed changes
Copy link
Collaborator

@Kukovec Kukovec left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

test/tla/Paxos.tla Show resolved Hide resolved
@konnov
Copy link
Collaborator Author

konnov commented Mar 22, 2021

I would actually be more in favor of fixing the signature of UNCHANGED to always expect tuples. There's really no reason to have sequences in UC, you never get the variable vectors from Seq(...)-type sets.

You can write UNCHANGED x. If x is a sequence, you have a sequence ;-)

@konnov
Integrating types 5: made Inliner, Unroller, and ParameterNormalizer …
5bf4f82 
…type-aware (#657)

* bugfix: translating labels

* fixing types in Unroller and Inliner

* moved and rewrote TestInlinerofUserOper, made it type-aware

* made TestUnroller type-aware

* made ParameterNormalizer type-aware

* made TestUnroller and Unroller type-aware

* running the type checker right after the parser

* a reference to the closed issue

* Integrating types 6: made Desugarer type aware (#658)

* add a watchdog listener

* close #647: Desugarer preprocesses the general case of EXCEPT

* unrelease notes

* type-aware test for Desugarer

* made Desugarer type-aware!

* fixed a type bug that was found by the type watchdog

* propagating types in AssignmentOperatorIntroduction

* made SkolemizationMarker type-aware

* made ExpansionMarker type-aware

* fixed TestSymbTransGenerator

* moved the integration tests to test/tla

* removed the Paxos tests, which is already in the integration tests

* enabled snowcat by default, as the preprocessing is type-aware

* Integrating types 7: victory over enthropy (#663)

* a temporary fix for the old type annotations

* a fix for lazy annotations of nullary operators

* fix SymbTransGenerator

* fixed plenty of integration tests

* fixed a bug in ITE, found by Jure

* made the TLC config parser type-aware

* add type annotations to the tests

* made VCGenerator type-aware

* moved TlaType1, TypedPredefs, and TypingException to lir, to break cyclic dependencies

* fixing types in TestConstAndDefRewriter

* made TlcConfigImporter type-aware

* fixed TestTlcConfigImporter

* removed the reference to lir.

* Integrating types 8: using new types in the checker core (#668)

* migrated rewriting rules to use the types inferred by snowcat

* forbid the old type annotations

* fixed FunExcept

* the error about old type annotations is qualified as a normal user error

* fixed: set constructor, map, and in

* fix the CHOOSE rule

* removed the old type annotations, as they are no longer supported

* Mad TestSymbStateRewriterBool, AndRule, and OrRule type-aware

* made TestSymbStateRewriterInt typed

* fixed all but one tests in TestSymbStateRewriterAssignment

* remove the tests that are labelled as ignore

* fix a funny bug in caching expressions

* fix arena corruption in PowSetCtorRule

* fix a bug in Builder: produced Int instead of Nat

* equality throws when incomparable types are met

* fixed an error message for infinite sets

* made tests in TestSymbStateRewriterSet type-aware

* eliminated the old TrivialTypeFinder and ModelChecker, no need to maintain them

* fix a bug in FunExceptRule

* fix TestSymbStateRewriterFun

* fix TestSymbStateRewriterStr and TestSymbStateRewriterTuple

* fix TestSymbStateRewriterRecord and a bug in EXCEPT

* fix TestCherryPick

* remove the unit test that is covered by TestKeramelizer

* fix TestSymbStateRewriterChoose

* fix TestSymbStateRewriterControl

* fix TestSymbStateRewriterExpand

* fix TestSymbStateRewriterFiniteSets

* TestSymbStateRewriterFunSet

* fix TestSymbStateRewriterRecFun

* fix TestSymbStateRewriterSequence

* fix TestSeqModelChecker

* fix TestSymbStateDecoder

* fix TestSymbStateRewriterTlc

* old annotations are expected to throw an error now

* fix TestSymbStateRewriterPowerset

* fixed cherry picking of records that have compatible but different domains

* fixed type annotations in SimpT1

* fix cherry-picking of records that was broken in Paxos

* removed --with-snowcat from CLI

* changelog

* Integrating types 9: a few bugfixes (#671)

* a better error message

* fix the structure of EXCEPT expressions + add support for sequences

* fixed the comment by Shon
@konnov
Merge branch 'igor/with-snowcat3' into igor/with-snowcat4
2f1b4c5
@konnov
fixed the accidental bug introduced in refactoring
b3e04da
@konnov konnov merged commit cbeda08 into igor/with-snowcat3 Mar 24, 2021
@konnov konnov deleted the igor/with-snowcat4 branch March 24, 2021 07:51
konnov added a commit that referenced this pull request Mar 24, 2021
@konnov
Integrating types 3: Refactored tla.lir.Builder and made several pass…
fb90414 
…es type-aware (#650)

* made Normalizer type-aware

* Refactored Builder, introduced UntypedPredefs and TypedPredefs, removed several implicits

* fix TestReplaceFixed

* fix TestChangeListener

* fix TestLetInExpander

* fix TestIncrementalRenaming

* fix TestBuilder

* fix TestSourceStore

* fix TestSanyImporter

* fix Keramelizer and TestKeramelizer

* fix TestDesugarer

* fix TestExprOptimizer

* fix TestOperAppToLetInDef

* fix TestUnroller

* fix TestAssignmentStrategyEncoder

* fix TestSmtFreeSTE

* fix TestSymbTransGenerator

* fix TestRewriterKeraSet

* fix TestExpansionMarker

* fix TestSkolemizationMarker

* fix TestSparseOracle

* fix oracles

* fix more tests

* fix AbstractTestTransitionExecutorImpl

* fox TestSymbStateRewriterSequence

* fix TestSymbStateRewriterInt

* a quick test for Normalizer and a bug fix in Normalizer

* fixed the copy-pasted test

* fix formatting

* fixed after comments by Jure

* changed two expressions to the IR form, for consistency

* addressed the comments by Shon

* Integrating types 4: migrated tests to Snowcat (#652)

* annotated all tests and fixed some

* Integrating types 5: made Inliner, Unroller, and ParameterNormalizer type-aware (#657)

* bugfix: translating labels

* fixing types in Unroller and Inliner

* moved and rewrote TestInlinerofUserOper, made it type-aware

* made TestUnroller type-aware

* made ParameterNormalizer type-aware

* made TestUnroller and Unroller type-aware

* running the type checker right after the parser

* a reference to the closed issue

* Integrating types 6: made Desugarer type aware (#658)

* add a watchdog listener

* close #647: Desugarer preprocesses the general case of EXCEPT

* unrelease notes

* type-aware test for Desugarer

* made Desugarer type-aware!

* fixed a type bug that was found by the type watchdog

* propagating types in AssignmentOperatorIntroduction

* made SkolemizationMarker type-aware

* made ExpansionMarker type-aware

* fixed TestSymbTransGenerator

* moved the integration tests to test/tla

* removed the Paxos tests, which is already in the integration tests

* enabled snowcat by default, as the preprocessing is type-aware

* Integrating types 7: victory over enthropy (#663)

* a temporary fix for the old type annotations

* a fix for lazy annotations of nullary operators

* fix SymbTransGenerator

* fixed plenty of integration tests

* fixed a bug in ITE, found by Jure

* made the TLC config parser type-aware

* add type annotations to the tests

* made VCGenerator type-aware

* moved TlaType1, TypedPredefs, and TypingException to lir, to break cyclic dependencies

* fixing types in TestConstAndDefRewriter

* made TlcConfigImporter type-aware

* fixed TestTlcConfigImporter

* removed the reference to lir.

* Integrating types 8: using new types in the checker core (#668)

* migrated rewriting rules to use the types inferred by snowcat

* forbid the old type annotations

* fixed FunExcept

* the error about old type annotations is qualified as a normal user error

* fixed: set constructor, map, and in

* fix the CHOOSE rule

* removed the old type annotations, as they are no longer supported

* Mad TestSymbStateRewriterBool, AndRule, and OrRule type-aware

* made TestSymbStateRewriterInt typed

* fixed all but one tests in TestSymbStateRewriterAssignment

* remove the tests that are labelled as ignore

* fix a funny bug in caching expressions

* fix arena corruption in PowSetCtorRule

* fix a bug in Builder: produced Int instead of Nat

* equality throws when incomparable types are met

* fixed an error message for infinite sets

* made tests in TestSymbStateRewriterSet type-aware

* eliminated the old TrivialTypeFinder and ModelChecker, no need to maintain them

* fix a bug in FunExceptRule

* fix TestSymbStateRewriterFun

* fix TestSymbStateRewriterStr and TestSymbStateRewriterTuple

* fix TestSymbStateRewriterRecord and a bug in EXCEPT

* fix TestCherryPick

* remove the unit test that is covered by TestKeramelizer

* fix TestSymbStateRewriterChoose

* fix TestSymbStateRewriterControl

* fix TestSymbStateRewriterExpand

* fix TestSymbStateRewriterFiniteSets

* TestSymbStateRewriterFunSet

* fix TestSymbStateRewriterRecFun

* fix TestSymbStateRewriterSequence

* fix TestSeqModelChecker

* fix TestSymbStateDecoder

* fix TestSymbStateRewriterTlc

* old annotations are expected to throw an error now

* fix TestSymbStateRewriterPowerset

* fixed cherry picking of records that have compatible but different domains

* fixed type annotations in SimpT1

* fix cherry-picking of records that was broken in Paxos

* removed --with-snowcat from CLI

* changelog

* Integrating types 9: a few bugfixes (#671)

* a better error message

* fix the structure of EXCEPT expressions + add support for sequences

* fixed the comment by Shon

* fixed the accidental bug introduced in refactoring
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@shonfeder shonfeder shonfeder approved these changes

@Kukovec Kukovec Kukovec approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@konnov @shonfeder @Kukovec