diff --git a/Specs/Quint/asyncModelsTest.qnt b/Specs/Quint/asyncModelsTest.qnt index a570992da..c20de39c7 100644 --- a/Specs/Quint/asyncModelsTest.qnt +++ b/Specs/Quint/asyncModelsTest.qnt @@ -190,7 +190,7 @@ import statemachineAsync( Heights = Set(0) // , 1, 2, 3) ) as N4F2 from "./statemachineAsync" -// v3 and v4 are correct. v2 is a N4N4F22aulty proposal and proposes diN4N4F22N4N4F22erently to v3 and v4 +// v3 and v4 are correct. v2 is a faulty proposal and proposes differently to v3 and v4 // this run leads to disagreement run DisagreementTest = { N4F2::init @@ -245,4 +245,4 @@ run DisagreementTest = { -} \ No newline at end of file +} diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt index 051abf9a0..a22770bfe 100644 --- a/Specs/Quint/voteBookkeeper.qnt +++ b/Specs/Quint/voteBookkeeper.qnt @@ -152,7 +152,7 @@ module voteBookkeeper { // Called by the executor when it receives a vote. The function takes the following steps: // - It first adds the vote and then computes a threshold. // - If there exist a threshold and has not emitted before, the function returns the corresponsing ExecutorEvent. - // - Othewise, the function returns a no-threshold event. + // - Otherwise, the function returns a no-threshold event. // - Note that if there is no threshold after adding the vote, the function checks if there is a skip threshold. // TO DISCUSS: // - There might be a problem if we generalize from single-shot to multi-shot: the keeper only keeps the totalWeight