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

copilot-theorem: Fix multiple typos in README. Refs #560. #558

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

copilot-theorem: Fix multiple typos in README. Refs #560. #558

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b88b257
copilot-theorem: update README.md
eltociear Oct 31, 2024
973ae14
`copilot-theorem:` Fix typo in README.
eltociear Dec 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions copilot-theorem/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -388,10 +388,10 @@ 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 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
Expand Down Expand Up @@ -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

Expand Down