Template:L witness

From Event-B
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Usage

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

Example

MACHINE

AntiCollide

REFINES

Safety

SEES

Network

Acyclic

VARIABLES

v1

v2

control ≙
// not extended and no convergence

WITH

a :
a = c

END

END

Template

{{{1}}} :

{{{2}}}