Add writeup of AGREE, GUMBO, FRET #101
Conversation
There was a problem hiding this comment.
mv spec_languages.md docs/SPEC_LANGUAGES.md
Looks good!
@peterohanley if you have spare cycles, can you come up with a small (almost trivial) example expressed in all three languages for comparison (AGREE, GUMBO, CN)?
Such example would serve as a great starting point for the discussion about automated spec translation / refinement across different levels of abstractions in the model.
| from their specification. Global variables are considered only as they are | ||
| manipulated by functions. | ||
|
|
||
| AGREE allows temporal logic constraints and works over "systems" with input and |
There was a problem hiding this comment.
| AGREE allows temporal logic constraints and works over "systems" with input and | |
| AGREE allows temporal logic constraints and works over *systems* with input and |
| level. | ||
|
|
||
| GUMBO works over threads that can receive and send events and access data | ||
| "ports". It assumes there is a runtime system available that will run the |
There was a problem hiding this comment.
| "ports". It assumes there is a runtime system available that will run the | |
| *ports*. It assumes there is a runtime system available that will run the |
| conveniet, but it will still work if the well-formed constraints are | ||
| transparently inlined into every spec. | ||
|
|
||
| GUMBO's entry points have various restrictions on what kinds of data each can |
There was a problem hiding this comment.
GUMBO's entry points have various restrictions on what kinds of data each can
Each entry point ?
There was a problem hiding this comment.
@peterohanley thanks for putting this together. There are a few things I'm curious about that I'm hoping you can add. For AGREE/Gumbo/FRET:
- What is the intended use, and when might one use AGREE vs. Gumbo vs. FRET? Or do they complement each other?
- What do they model, and what does the model look like (ideally with a small example, such as one might find in their docs/tutorials)?
- e.g. what is a "system" in AGREE, what is a "thread" in Gumbo", etc.
- What specs do they support, with a few examples?
- I see AGREE and FRET support temporal logic in specs, what about Gumbo?
- Presumably they're used to specify safety and liveness properties? Perhaps list an example for each?
| states of a set of variables. It does not consider implementation below this | ||
| level. | ||
|
|
||
| GUMBO works over threads that can receive and send events and access data |
There was a problem hiding this comment.
What kinds of properties can you write with GUMBO? Also temporal properties?
|
@peterohanley please timebox this and update by 12/4 |
Describe your changes
Add a document with an overview of the relationship between CN, GUMBO, AGREE, FRET, and how CN could serve as the bottom layer for these specs.
Issue ticket number and link
#91
Checklist before requesting a review