diff --git a/docs/codetour/.tours/coin.tour b/docs/codetour/.tours/coin.tour index a630f2317..0f567c1d4 100644 --- a/docs/codetour/.tours/coin.tour +++ b/docs/codetour/.tours/coin.tour @@ -22,7 +22,7 @@ }, { "title": "Declare pure functions", - "description": "\n\nIt often happens that a protocol requires auxilliary definitions that do not\ndepend on the protocol state, but only on the values of their parameters.\nSuch computations are often called \"pure\". In the above code, we define two\npure definitions:\n \n - The pure value `MAX_UINT`.\n\n - The pure definition `isUInt` that computes if a given integer `i` is within\n the range from 0 to MAX_UINT (inclusive).\n\nThe main property of pure values is that they always return the same value.\nPure definitions always return the same value, if they are supplied with the\nsame arguments.\n\nTo see that no state is needed, evaluate these definitions in REPL\n(read-evaluate-print-loop):\n\n \n>> echo \"MAX_UINT\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(22)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(-1)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(MAX_UINT + 1)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n\nThe functional layer is actually quite powerful; a lot of protocol behavior can\nbe defined here without referring to protocol state.\n\nAs you can see, we have omitted the type of `MAX_UINT` but specified the type of\n`isUInt`. Most of the time, the type checker can infer the types of values and\noperator definitions, and giving additional type annotations is up to you. In\nrare cases, the type checker may get confused, and then explicit type\nannotations will help you in figuring out the issue.\n ", + "description": "\n\nIt often happens that a protocol requires auxiliary definitions that do not\ndepend on the protocol state, but only on the values of their parameters.\nSuch computations are often called \"pure\". In the above code, we define two\npure definitions:\n \n - The pure value `MAX_UINT`.\n\n - The pure definition `isUInt` that computes if a given integer `i` is within\n the range from 0 to MAX_UINT (inclusive).\n\nThe main property of pure values is that they always return the same value.\nPure definitions always return the same value, if they are supplied with the\nsame arguments.\n\nTo see that no state is needed, evaluate these definitions in REPL\n(read-evaluate-print-loop):\n\n \n>> echo \"MAX_UINT\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(22)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(-1)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(MAX_UINT + 1)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n\nThe functional layer is actually quite powerful; a lot of protocol behavior can\nbe defined here without referring to protocol state.\n\nAs you can see, we have omitted the type of `MAX_UINT` but specified the type of\n`isUInt`. Most of the time, the type checker can infer the types of values and\noperator definitions, and giving additional type annotations is up to you. In\nrare cases, the type checker may get confused, and then explicit type\nannotations will help you in figuring out the issue.\n ", "line": 38, "file": "lesson3-anatomy/coin.qnt" }, diff --git a/docs/codetour/.tours/hello.tour b/docs/codetour/.tours/hello.tour index f713ec19d..c77e8c319 100644 --- a/docs/codetour/.tours/hello.tour +++ b/docs/codetour/.tours/hello.tour @@ -34,7 +34,7 @@ }, { "title": "Introduce an action by the computer", - "description": "\n\nNow it's time to print the \"Hello, world!\" message. Similar to `init`, we\nintroduce the action `write`. In contrast to `init`, this action cannot be\nunconditionally executed in any state of our state machine. Similar to how the\nvariable `consoleOutput` is updated in the action `init`, you should be able to\nsee how the action `write` schedules an update of `consoleOutput` in the next\nstate. This only happens though, if the action `write` returns `true`.\n\nThe first statement of `write` may be confusing to you though:\n\n```scala\n consoleOutput == \"\"\n```\n\nIf you are familiar with C, Java, JavaScript and similar languages, this\nstatement looks useless, as in those languages such an expression would be\nevaluated and its result would be simply dropped. Moreover, in a static\nlanguage such a statement could be simply removed by the compiler as\nfruitless at the optimization stage.\n\nIn Quint, things are a bit different. Recall the discussion about the\naction `init` at the previous step. Assignments return `true` and\n`all { ... }` returns true only if all of its arguments return `true`.\nThe same principle applies to the expression `consoleOutput == \"\"`.\nIf `consoleOutput == \"\"` evaluates to `true` in the current state\nof the state machine, then the enclosing expression `all { ... }`\nevaluates to `true`, and only then the action `write` evaluates to `true`\nand it may produce the next state.\n\nFinally, the third statement may look useless to you too:\n\n```scala\n readByUser' = readByUser,\n```\n\nWhy shall we say that `readByUser` keeps its value in the next state?\nMost likely, we will be able to automatically infer this in the future.\nIn the current version of Quint, if an action is used to execute transitions,\nit has to explicitely assign values to all of the state variables.\n ", + "description": "\n\nNow it's time to print the \"Hello, world!\" message. Similar to `init`, we\nintroduce the action `write`. In contrast to `init`, this action cannot be\nunconditionally executed in any state of our state machine. Similar to how the\nvariable `consoleOutput` is updated in the action `init`, you should be able to\nsee how the action `write` schedules an update of `consoleOutput` in the next\nstate. This only happens though, if the action `write` returns `true`.\n\nThe first statement of `write` may be confusing to you though:\n\n```scala\n consoleOutput == \"\"\n```\n\nIf you are familiar with C, Java, JavaScript and similar languages, this\nstatement looks useless, as in those languages such an expression would be\nevaluated and its result would be simply dropped. Moreover, in a static\nlanguage such a statement could be simply removed by the compiler as\nfruitless at the optimization stage.\n\nIn Quint, things are a bit different. Recall the discussion about the\naction `init` at the previous step. Assignments return `true` and\n`all { ... }` returns true only if all of its arguments return `true`.\nThe same principle applies to the expression `consoleOutput == \"\"`.\nIf `consoleOutput == \"\"` evaluates to `true` in the current state\nof the state machine, then the enclosing expression `all { ... }`\nevaluates to `true`, and only then the action `write` evaluates to `true`\nand it may produce the next state.\n\nFinally, the third statement may look useless to you too:\n\n```scala\n readByUser' = readByUser,\n```\n\nWhy shall we say that `readByUser` keeps its value in the next state?\nMost likely, we will be able to automatically infer this in the future.\nIn the current version of Quint, if an action is used to execute transitions,\nit has to explicitly assign values to all of the state variables.\n ", "line": 25, "file": "lesson0-helloworld/hello.qnt" }, diff --git a/docs/codetour/lesson0-helloworld/hello.template.qnt b/docs/codetour/lesson0-helloworld/hello.template.qnt index d204a7bfe..dcd3182a6 100644 --- a/docs/codetour/lesson0-helloworld/hello.template.qnt +++ b/docs/codetour/lesson0-helloworld/hello.template.qnt @@ -181,7 +181,7 @@ Finally, the third statement may look useless to you too: Why shall we say that `readByUser` keeps its value in the next state? Most likely, we will be able to automatically infer this in the future. In the current version of Quint, if an action is used to execute transitions, -it has to explicitely assign values to all of the state variables. +it has to explicitly assign values to all of the state variables. !*/ diff --git a/docs/codetour/lesson0-helloworld/hello.xml b/docs/codetour/lesson0-helloworld/hello.xml index 991e96d05..8fdec224a 100644 --- a/docs/codetour/lesson0-helloworld/hello.xml +++ b/docs/codetour/lesson0-helloworld/hello.xml @@ -145,7 +145,7 @@ Finally, the third statement may look useless to you too: Why shall we say that `readByUser` keeps its value in the next state? Most likely, we will be able to automatically infer this in the future. In the current version of Quint, if an action is used to execute transitions, -it has to explicitely assign values to all of the state variables. +it has to explicitly assign values to all of the state variables. diff --git a/docs/codetour/lesson3-anatomy/coin.template.qnt b/docs/codetour/lesson3-anatomy/coin.template.qnt index 5fa122909..b75afe6a7 100644 --- a/docs/codetour/lesson3-anatomy/coin.template.qnt +++ b/docs/codetour/lesson3-anatomy/coin.template.qnt @@ -143,7 +143,7 @@ different kinds of "integers", when they are referred to via different type alia Declare pure functions -It often happens that a protocol requires auxilliary definitions that do not +It often happens that a protocol requires auxiliary definitions that do not depend on the protocol state, but only on the values of their parameters. Such computations are often called "pure". In the above code, we define two pure definitions: diff --git a/docs/codetour/lesson3-anatomy/coin.xml b/docs/codetour/lesson3-anatomy/coin.xml index 9c713f2c3..3c8832a11 100644 --- a/docs/codetour/lesson3-anatomy/coin.xml +++ b/docs/codetour/lesson3-anatomy/coin.xml @@ -98,7 +98,7 @@ different kinds of "integers", when they are referred to via different type alia Declare pure functions -It often happens that a protocol requires auxilliary definitions that do not +It often happens that a protocol requires auxiliary definitions that do not depend on the protocol state, but only on the values of their parameters. Such computations are often called "pure". In the above code, we define two pure definitions: diff --git a/docs/pages/docs/architecture-decision-records/adr008-managing-apalache.md b/docs/pages/docs/architecture-decision-records/adr008-managing-apalache.md index c3a4146a8..c0c85c098 100644 --- a/docs/pages/docs/architecture-decision-records/adr008-managing-apalache.md +++ b/docs/pages/docs/architecture-decision-records/adr008-managing-apalache.md @@ -138,7 +138,7 @@ Pros: Cons: - Requires differing per-platform docs/instructions. -- Requires maintaining per-platfrom packages; unclear who could provide and maintain these. +- Requires maintaining per-platform packages; unclear who could provide and maintain these. - Quint is already available from npm. #### 3.2.2 Using an ecosystem package manager (npm, coursier, ...) @@ -227,7 +227,7 @@ Cons: - Assumes that the JRE is installed on the local system. *Note: We did a prototype implementation querying the GitHub REST API in [#1115](https://github.com/informalsystems/quint/issues/1115). -However, we observed CI issues due to the Github API's rate limiting as described in [#1124](https://github.com/informalsystems/quint/issues/1124). In pratice, the same issues can affect users (e.g., behind a shared IP) and may segnificantly impact UX of the `verify` command. As a countermeasure, we reverted to a hardcoded Apalache version in [`4ceb7d8`](https://github.com/informalsystems/quint/commit/4ceb7d8be824ddc0a2c2a14e105baff446f71e72).* +However, we observed CI issues due to the Github API's rate limiting as described in [#1124](https://github.com/informalsystems/quint/issues/1124). In practice, the same issues can affect users (e.g., behind a shared IP) and may segnificantly impact UX of the `verify` command. As a countermeasure, we reverted to a hardcoded Apalache version in [`4ceb7d8`](https://github.com/informalsystems/quint/commit/4ceb7d8be824ddc0a2c2a14e105baff446f71e72).* #### 3.2.5 Apalache as cloud-hosted SaaS @@ -237,7 +237,7 @@ is necessary. Pros: - No installation or server management issues. -- Versioning and backwards-compatiblity could be exposed via separate endpoints. +- Versioning and backwards-compatibility could be exposed via separate endpoints. Cons: @@ -248,7 +248,7 @@ Cons: ### 3.3 Version dependencies between Quint and Apalache -We want to maintain compatiblity between Quint and Apalache, therefore we need +We want to maintain compatibility between Quint and Apalache, therefore we need some mode of linking compatible versions of both tools. Both tools follow [semantic versioning][]. diff --git a/docs/pages/docs/getting-started.mdx b/docs/pages/docs/getting-started.mdx index 712da90c9..40c8ba5ad 100644 --- a/docs/pages/docs/getting-started.mdx +++ b/docs/pages/docs/getting-started.mdx @@ -16,7 +16,7 @@ npm i @informalsystems/quint -g ### Setup your code editor -For the best experience writting Quint, you should set up your code editor with the Quint tools. The VSCode setup is, by far, the easiest, so you might want to use it if you want a quick start. +For the best experience writing Quint, you should set up your code editor with the Quint tools. The VSCode setup is, by far, the easiest, so you might want to use it if you want a quick start. diff --git a/docs/pages/docs/lessons/coin.md b/docs/pages/docs/lessons/coin.md index 1390b225b..d4f38b4f4 100644 --- a/docs/pages/docs/lessons/coin.md +++ b/docs/pages/docs/lessons/coin.md @@ -130,7 +130,7 @@ different kinds of "integers", when they are referred to via different type alia -It often happens that a protocol requires auxilliary definitions that do not +It often happens that a protocol requires auxiliary definitions that do not depend on the protocol state, but only on the values of their parameters. Such computations are often called "pure". In the above code, we define two pure definitions: diff --git a/docs/pages/docs/lessons/hello.md b/docs/pages/docs/lessons/hello.md index b1b6ec190..3aac84a88 100644 --- a/docs/pages/docs/lessons/hello.md +++ b/docs/pages/docs/lessons/hello.md @@ -182,7 +182,7 @@ Finally, the third statement may look useless to you too: Why shall we say that `readByUser` keeps its value in the next state? Most likely, we will be able to automatically infer this in the future. In the current version of Quint, if an action is used to execute transitions, -it has to explicitely assign values to all of the state variables. +it has to explicitly assign values to all of the state variables. ## 7. Introduce an action by the user diff --git a/docs/theme.config.jsx b/docs/theme.config.jsx index 2a3975074..be2bc4924 100644 --- a/docs/theme.config.jsx +++ b/docs/theme.config.jsx @@ -39,11 +39,11 @@ export default {