Auto-Completion Design: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Nicolas |
imported>Nicolas m →In Machine Models: took extended events into account |
||
| (9 intermediate revisions by 2 users not shown) | |||
| Line 10: | Line 10: | ||
==== Invariants, Theorems and Variants ==== | ==== Invariants, Theorems and Variants ==== | ||
* Sets (all) | * Sets (all) | ||
* Constants (all) | * Constants (all) | ||
* Variables (all) | |||
==== Guards and Actions ==== | ==== Guards and Actions ==== | ||
* Sets (all) | * Sets (all) | ||
* Constants (all) | * Constants (all) | ||
* Variables (all) | |||
* Parameters (of concrete event) | |||
** in case the event is extended, Parameters of extended event(s) (through extension) | |||
==== Event Labels ==== | |||
* Seen events labels (of abstract machine) | |||
==== Witness Labels ==== | ==== Witness Labels ==== | ||
* | * Disappearing parameters (of abstract event) | ||
* | * Primed Disappearing Variables (of abstract machine) that are non-deterministically assigned in abstract event | ||
==== Witness Predicates ==== | ==== Witness Predicates ==== | ||
* Sets (all) | * Sets (all) | ||
* Constants (all) | * Constants (all) | ||
* Variables (all) | |||
* Primed Variables (concrete) | |||
* Parameters (of concrete event) | |||
** in case the event is extended, Parameters of extended event(s) (through extension) | |||
* Witness Label | |||
[[Category:Design]] | [[Category:Design]] | ||
[[Category:Work in progress]] | [[Category:Work in progress]] | ||
Latest revision as of 14:53, 21 January 2010
Proposed names depending on edit context
In Context Models
Axioms and Theorems
- Sets (all)
- Constants (all)
In Machine Models
Invariants, Theorems and Variants
- Sets (all)
- Constants (all)
- Variables (all)
Guards and Actions
- Sets (all)
- Constants (all)
- Variables (all)
- Parameters (of concrete event)
- in case the event is extended, Parameters of extended event(s) (through extension)
Event Labels
- Seen events labels (of abstract machine)
Witness Labels
- Disappearing parameters (of abstract event)
- Primed Disappearing Variables (of abstract machine) that are non-deterministically assigned in abstract event
Witness Predicates
- Sets (all)
- Constants (all)
- Variables (all)
- Primed Variables (concrete)
- Parameters (of concrete event)
- in case the event is extended, Parameters of extended event(s) (through extension)
- Witness Label
