Auto-Completion Design: Difference between revisions
From Event-B
				
				
				Jump to navigationJump to search
				
				
imported>Laurent  | 
				imported>Nicolas m →In Machine Models:  took extended events into account  | 
				||
| (4 intermediate revisions by 2 users not shown) | |||
| Line 18: | Line 18: | ||
* Constants (all)  | * Constants (all)  | ||
* Variables (all)  | * Variables (all)  | ||
* Parameters (of   | * 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 ====  | ||
| Line 25: | Line 30: | ||
==== 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