imported>Pascal |
imported>Mathieu |
| Line 1: |
Line 1: |
| − | The purpose of this page is to list and justify the rewriting / simplification rules applied in the event model decomposition when building the ''external'' events, and more especially their actions.
| + | ''Help copied from [http://www.mediawiki.org/wiki/Help:Contents]'' |
| | | | |
| − | == Equivalence relation == | + | ==Reading== |
| − | It is possible to define an equivalence relation on the Event-B actions, and by restrictions on the Event-B assignments (an action is a set of assignments). Two actions are considered as being equivalent if the proof obligations generated for these actions are logically equivalent.
| + | * [[Help:Navigation|Navigation]] |
| | + | * [[Help:Searching|Searching]] |
| | + | * [[Help:Tracking changes|Tracking changes]] |
| | + | * [[Help:Watchlist|Watchlist]] |
| | | | |
| − | This relation is represented with the <math>\equiv</math> symbol.
| + | ==Editing== |
| | + | * [[Help:Editing pages|Editing pages]] |
| | + | * [[Help:Starting a new page|Starting a new page]] |
| | + | * [[Help:Formatting|Formatting]] |
| | + | * [[Help:Links|Links]] |
| | + | * [[Help:User page|User pages]] |
| | + | * [[Help:Talk pages|Talk pages]] |
| | | | |
| − |
| + | ===Advanced editing=== |
| | + | * [[Help:Images|Images]] |
| | + | * [[Help:Tables|Tables]] |
| | + | * [[Help:Maths|Maths]] |
| | + | * [[Help:Categories|Categories]] |
| | + | * [[Help:Subpages|Subpages]] |
| | + | * [[Help:Managing files|Managing files]] |
| | + | * [[Help:Moving a page|Moving a page]] |
| | + | * [[Help:Redirects|Redirects]] |
| | + | * [[Help:Deleting a page|Deleting a page]] |
| | + | * [[Help:Protected pages|Protected pages]] |
| | | | |
| − | == Rewriting rules on Event-B assignments ==
| + | * [[Help:Templates|Templates]] |
| − | As detailed in [[Actions_(Modelling_Language)|the modelling language]], the Event-B assignments are formed of two parts:
| + | * [[Help:Variables|Variables]] |
| − | * a left-hand side, which is a list of free identifiers. | + | * [[Help:Namespaces|Namespaces]] |
| − | * a right-hand side. | |
| | | | |
| − | There are various kinds of assignments:
| + | * [[Help:Special pages|Special pages]] |
| − | * The <math>\bcmsuch</math> ("becomes such that") assignment is the most general (non-deterministic) assignment, where a predicate is given on the before and after values of assigned identifiers. The after values of the assigned identifiers are denoted by a primed identifier whose prefix is the assigned identifier. | + | * [[Help:External searches|External searches]] |
| − | * The <math>\bcmeq</math> ("becomes equal to") assignment is the deterministic assignment where an expression is given for each assigned identifier.
| |
| − | * The <math>\bcmin</math> ("becomes member of") assignment is the set-based (non-deterministic) assignment, where a set expression is given for the assigned identifier.
| |
| | | | |
| − | Let <math>v</math> and <math>w</math> be variables, and <math>E</math> and <math>F</math> be expressions. In the following table, the left-hand assignments are equivalent (<math>\equiv</math>) to the right-hand ones:
| + | ===Personal customization=== |
| − | {{SimpleHeader}}
| + | * [[Help:Preferences|Preferences]] |
| − | |-
| + | * [[Help:Skins|Skins]] |
| − | |<math>v \bcmeq E</math>||<math>v \bcmsuch v' = E</math>||<font id="rule_1">Rule 1</font>
| |
| − | |-
| |
| − | |<math>v(E) \bcmeq F</math>||<math>v \bcmeq v \ovl \{E \mapsto F\}</math>||<font id="rule_2">Rule 2</font>
| |
| − | |- | |
| − | |<math>v \bcmin E</math>||<math>v \bcmsuch v' \in E</math>||<font id="rule_3">Rule 3</font>
| |
| − | |} | |
| | | | |
| − | Thus, each Event-B assignment can be expressed in a "becomes such that" form, and more precisely as <math>v_1,...,v_n \bcmsuch P(v_1,...v_n,v_1',...v_n')</math>, where <math>P</math> is a before-after predicate.
| + | ==Wiki administration== |
| | | | |
| − | == Rewriting rules on Event-B actions ==
| + | * [[Help:Sysops and permissions|Sysops and permissions]] |
| − | Let <math>v</math> and <math>w</math> be variables, <math>E</math> and <math>F</math> be expressions, and <math>P</math> and <math>Q</math> be predicates. The left-hand actions are equivalent (<math>\equiv</math>) to the right-hand ones:
| |
| − | {{SimpleHeader}}
| |
| − | |-
| |
| − | |<math>v~ \bcmsuch P(v,v')</math><br><math>w \bcmsuch Q(w,w')</math>||<math>v,w \bcmsuch P(v,v') \land Q(w,w')</math>||<font id="rule_4">Rule 4</font>
| |
| − | |-
| |
| − | |<math>v,w \bcmeq E,F</math>||<math>v~ \bcmeq E</math><br><math>w \bcmeq F</math>||<font id="rule_5">Rule 5</font>
| |
| − | |}
| |
| | | | |
| − | == Simplification rules on Event-B predicates ==
| + | The following features require extra permissions that are not normally granted to all wiki users. |
| − | Let <math>x_i</math>, <math>y</math> and <math>z</math> be variables, and <math>P</math> and <math>Q</math> be predicates.
| |
| − | * <font id="rule_6">Rule 6</font>: If <math>P(x_1,...,x_n,y)~</math> is equal to <math>y = Q(x_1,...,x_n)~</math>, then the <math>\exists y.P(x1,...,x_n,y)</math> predicate is true, and it may be deleted in conjunctive predicates (<math>\land</math>) where it appears.
| |
| − | * <font id="rule_7">Rule 7</font>: The <math>(\exists z.P(x_1,...,x_n,z) \land Q(y_1,...,y_m))</math> predicate, where <math>z \notin \{y_1,...,y_n\}</math>, may be rewritten as <math>(\exists z.P(x_1,...,x_n,z)) \land Q(y_1,...,y_m)</math>.
| |
| | | | |
| − | == Simplification rules based on Event-B proof obligations ==
| + | * [[Help:Protecting and unprotecting pages|Protecting and unprotecting pages]] |
| | + | * [[Help:Sysop deleting and undeleting|Sysop deleting and undeleting]] |
| | + | * [[Help:Patrolled edits|Patrolled edits]] |
| | + | * [[Help:Blocking users|Blocking users]] |
| | + | * [[Help:Range blocks|Range IP blocks]] |
| | + | * [[Help:Assigning permissions|Assigning permissions]] |
| | | | |
| − | == Example ==
| + | [[Category:Help| ]] |
| − | Let <math>a</math>, <math>b</math> and <math>x</math> be variables, and <math>P</math> and <math>Q</math> be predicates.
| + | __NOTOC__ |
| − | {|
| |
| − | |-
| |
| − | |<math>a,b \bcmsuch \exists x.P(a,a',x) \land Q(b,b')</math>
| |
| − | |-
| |
| − | |<center><math>\equiv</math> [[#rule_7|(Rule 7)]]</center>
| |
| − | |-
| |
| − | |<math>a,b \bcmsuch (\exists x.P(a,a',x)) \land Q(b,b')</math>
| |
| − | |-
| |
| − | |<center><math>\equiv</math> [[#rule_4|(Rule 4)]]</center>
| |
| − | |-
| |
| − | |<math>a \bcmsuch \exists x.P(a,a',x)</math><br><math>b \bcmsuch Q(b,b')</math>
| |
| − | |}
| |
