From b88b257e24847e930286e04299576823056d67b5 Mon Sep 17 00:00:00 2001 From: Ikko Eltociear Ashimine Date: Thu, 31 Oct 2024 14:26:21 +0900 Subject: [PATCH 1/2] copilot-theorem: update README.md occurences -> occurrences --- copilot-theorem/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-theorem/README.md b/copilot-theorem/README.md index e16d7f1e..21c57b80 100644 --- a/copilot-theorem/README.md +++ b/copilot-theorem/README.md @@ -391,7 +391,7 @@ the model-checking techniques we are using. The reification process used to build the `Core.Spec` object looses many informations about the structure of the original Copilot program. In fact, a stream is kept in the reified program only if it is recursively defined. -Otherwise, all its occurences will be inlined. Moreover, let's look at the +Otherwise, all its occurrences will be inlined. Moreover, let's look at the `intCounter` function defined in the example `Grey.hs`: ```haskell From 973ae14f8d602b85b47a90d644628af0e84b0f74 Mon Sep 17 00:00:00 2001 From: Ikko Eltociear Ashimine Date: Fri, 20 Dec 2024 17:23:51 +0900 Subject: [PATCH 2/2] `copilot-theorem:` Fix typo in README. fixed typo. --- copilot-theorem/README.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/copilot-theorem/README.md b/copilot-theorem/README.md index 21c57b80..98108bca 100644 --- a/copilot-theorem/README.md +++ b/copilot-theorem/README.md @@ -44,7 +44,7 @@ Intuitively, a safety property is a property which express the idea that disproved by a finite execution trace of the program called a **counterexample**. Safety properties are often opposed to **liveness** properties, which express the idea that *something good will eventually -happen*. The latters are out of the scope of *copilot-theorem*. +happen*. The latter are out of the scope of *copilot-theorem*. Safety properties are simply expressed with standard boolean streams. In addition to triggers and observers declarations, it is possible to bind a @@ -139,7 +139,7 @@ available: into a *state transition system* [1]. Moreover, in order to keep some structure in this representation, the variables of this system are grouped by *nodes*, each node exporting and importing variables. The *Kind2 prover* uses - this format, which can be easily translated into the native format. + this format, which can be easily translated into the native format. For each of these formats, there is a folder in `src/Copilot/Theorem` which contains at least @@ -388,7 +388,7 @@ the model-checking techniques we are using. #### Limitations related to Copilot implementation -The reification process used to build the `Core.Spec` object looses many +The reification process used to build the `Core.Spec` object loses many informations about the structure of the original Copilot program. In fact, a stream is kept in the reified program only if it is recursively defined. Otherwise, all its occurrences will be inlined. Moreover, let's look at the @@ -487,7 +487,7 @@ forAllCst l f = conj $ map (f . constant) l ``` However, this solution isn't completely satisfying because the size of the -property generated is proportionnal to the cardinal of `allowed`. +property generated is proportional to the cardinal of `allowed`. #### Some scalability issues