Difference between revisions of "Template:L machine"

From Event-B
Jump to navigationJump to search
imported>Mathieu
m
imported>Mathieu
m
(One intermediate revision by the same user not shown)
Line 7: Line 7:
 
{{l_refines|Safety}}
 
{{l_refines|Safety}}
 
{{l_sees|Network}}
 
{{l_sees|Network}}
 +
{{l_component|Acyclic}}
 
{{l_Variables|v1}}
 
{{l_Variables|v1}}
 
{{l_variable|v2}}
 
{{l_variable|v2}}
 
+
{{l_invariants}}
 +
{{l_invariant|inv1|v2 <math>\in</math> BOOL}}
 
{{l_end}}
 
{{l_end}}
  

Revision as of 14:51, 23 February 2009

Usage

Template use to typeset a machine name in an event-b listing.

Example

MACHINE

AntiCollide

REFINES

Safety

SEES

Network

Acyclic

VARIABLES

v1

v2

INVARIANTS

inv1 :
v2 \in BOOL

END

Template

MACHINE

{{{1}}}