Difference between pages "Template:L machine" and "Template:L parameters"

Revision as of 14:16, 26 February 2009

Template use to typeset a parameter event clause in an event-b listing.

MACHINE

Safety

ANY

END

ANY

@@ Line 1: / Line 1: @@
 <noinclude>
 ==Usage==
-Template use to typeset a machine name in an event-b listing.
+Template use to typeset a parameter event clause in an event-b listing.
 ==Example==
+{{l_machine|Safety}}
+{{l_evente|control}}
+{{l_parameters}}
-{{l_machine|AntiCollide}}
-{{l_refines|Safety}}
-{{l_sees|Network}}
-{{l_component|Acyclic}}
-{{l_variables|v1}}
-{{l_variable|v2}}
-{{l_invariants}}
-{{l_invariant|inv1|v2 ∈ BOOL}}
-{{l_theorems}}
-{{l_theorem|inv1|v2 ∈ BOOL}}
-{{l_events}}
-{{l_event|control|extended|ordinary}}
-{{l_parameters}}
-{{l_param|a}}
-{{l_param|x|y|z}}
-{{l_guards}}
-{{l_guard|grd1|x ⊆ next}}
-{{l_witnesses}}
-{{l_witness|y|y=v}}
-{{l_actions}}
-{{l_action|act1|pro :∈ BOOL}}
-{{l_end_event}}
 {{l_end}}
@@ Line 31: / Line 12: @@
 ==Template==
 </noinclude><!--
--->
+--><p class="typeset-l_evt_clause">ANY</p>
-<div class="typeset-listing">
-<p class="typeset-l_clause" >MACHINE</p>
-<p class="typeset-l_component" >{{{1}}}</p>