Difference between revisions of "Auto-Completion Design"
From Event-B
Jump to navigationJump to searchimported>Laurent m |
imported>Nicolas |
||
| Line 19: | Line 19: | ||
* Variables (all) | * Variables (all) | ||
* Parameters (of concrete event) | * Parameters (of concrete event) | ||
| + | |||
| + | ==== Event Labels ==== | ||
| + | |||
| + | * Seen events labels (of abstract machine) | ||
==== Witness Labels ==== | ==== Witness Labels ==== | ||
Revision as of 15:21, 3 June 2009
Contents
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)
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)
- Witness Label
