Difference between pages "Modularisation Plug-in Tutorial" and "Negation Normal Form"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Alexili
m
 
imported>Laurent
 
Line 1: Line 1:
−
==Modularisation Plug-in Tutorial==
+
This page describe the Negation Normal Form used in Rodin and show how it has been implemented.
−
Go to the [[Modularisation Plug-in|plug-in description page]].
 
  
−
The tutorial illustrates the use of the modularisation plug-in in an Event-B development. The example used is rather small scale but it still demonstrates some basic principles of introducing modules during the development process.
+
= Definition =
  
−
===Sluice Control Example===
+
A predicate is in Negation Normal Form when negation occurs only on atomic expression. To compute such a normal form, the following rewrite rules (which are already implemented in Rodin) are reused :
  
−
The example is a sluice with two doors connecting areas with dramatically different pressures. The pressure difference makes it unsafe to open a door unless the pressure is leveled between the areas connected by the door. The purpose of the system is to adjust the pressure in the sluice area and control the door locks to allow a user to get safely inside to outside. Such system can be deployed, for example, on a submarine to allow divers to get out while submerged.
+
SIMP_NOT_NOT : <math> \lnot\, \lnot\, P \;\;\defi\;\; P </math>
  
−
The system parts are two doors that can be operated independently of each other and a pressure controller that allows the change of pressure in the sluice area. The following is a schematic depiction of the system.
+
DISTRI_NOT_AND : <math>  \lnot\,(P \land  Q) \;\;\defi\;\;  \lnot\, P \lor  \lnot\, Q </math>
  
−
[[Image:SluiceController.png|300px]]
+
DISTRI_NOT_OR : <math>  \lnot\,(P \lor  Q) \;\;\defi\;\;  \lnot\, P \land  \lnot\, Q </math>
  
−
The system is summarised with the following set of requirements:
+
DERIV_NOT_IMP : <math>  \lnot\,(P \limp  Q) \;\;\defi\;\; P \land  \lnot\, Q </math>
−
# the system allows a user to get inside or outside by leveling pressure between room and a destination
 
−
# the system has three locations - ''outside'', ''sluice'' and ''inside''
 
−
# the system has two doors - ''door1'', connecting ''outside'' and ''sluice'', and ''door2'', connecting ''sluice'' and ''inside'';
 
−
# there is a device to change pressure in ''sluice'';
 
−
# a door may be opened only if the pressures in the locations it connects is equalised;
 
−
# at most one door is open at any moment;
 
−
# the pressure can only be switched on when the doors are closed.
 
  
−
Requirements 1-4 characterise the system by stating its goal and its major parts. The last three characterise the system behaviour. More precisely, they are the safety properties of the system.
+
DERIV_NOT_FORALL : <math>  \lnot\, \forall x \qdot  P \;\;\defi\;\;  \exists x \qdot  \lnot\, P </math>
  
−
The following diagram shows the stages of the system operation that let a user to get outside starting in the inside area.
+
DERIV_NOT_EXISTS : <math>  \lnot\, \exists x \qdot  P \;\;\defi\;\;  \forall x \qdot  \lnot\, P </math>
  
−
[[Image:SluiceControllerSolution.png|500px]]
+
However, no rule has been defined for the case where the inner predicate is an equivalence, such as <math> \lnot (P \leqv Q) </math>. The latter is equivalent to both <math> \lnot  P \leqv Q</math> and <math>P \leqv\lnot Q</math>. In this latter case, the way the tactic will work is yet to be defined. Since the "<math>\leqv</math>" is to be kept, the choice on which predicate the not will be applied to is ambiguous. Here is an example showing that difficulty :  
  
−
The shaded rectagles denote a pressure level, high pressure area corresponds to a higher rectangle. The "u" label marks the current position of a system user. Initially, a user is inside and the sluice pressure is levelled with the outside pressure. Before the door connecting to the sluice is opened, the pressure is decreased to level it with the inside pressure. Once the door is open, the user moves in, the door is sealed again. Finally, the sluice pressure is set to match the outside pressure and the door leading may be safely opened.
+
 
 +
<math>\lnot(A \leqv \lnot (B \lor C))</math> (1) which is equivalent to <math>\lnot(A \leqv (\lnot B \land \lnot C))</math> (2)
 +
 
 +
 
 +
A solution would be to applied systematically on the left expression. In that case, simple simplification in the right member as in (1) would not be applied, thus complicating the left expression.
 +
 
 +
A better solution would to apply the <math>\lnot</math> on a member containing already a <math>\lnot</math>. But it can be hard to find an expression with a <math>\lnot</math> which has already been put in its Negation Normal Form as for the right member in (2)
 +
 
 +
= Implementation =
 +
 
 +
== Tactics ==
 +
 
 +
When a predicate with a negation is matched, rules are applied following a pre-order traversal of that predicate.
 +
 
 +
<math>\lnot(A \land \lnot (B \lor C))</math>
 +
 
 +
<math>\lnot A \lor \lnot\lnot (B \lor C)</math>
 +
 
 +
<math>\lnot A \lor (B \lor C)</math>             
 +
 
 +
INSTEAD OF                                 
 +
 
 +
<math>\lnot(A \land \lnot (B \lor C))</math>
 +
 
 +
<math>\lnot(A \land (\lnot B \land \lnot C))</math>
 +
 
 +
<math>\lnot A \lor \lnot(\lnot B \land \lnot C)</math>
 +
 
 +
<math>\lnot A \lor (\lnot\lnot B \lor \lnot\lnot C)</math>
 +
 
 +
<math>\lnot A \lor (B \lor \lnot\lnot C)</math>
 +
 
 +
<math>\lnot A \lor (B \lor C)</math>
 +
 
 +
This way, tree proof is not unnecessarily complicated, and so more legible. The space used on disk is also smaller.

Revision as of 16:02, 13 April 2011

This page describe the Negation Normal Form used in Rodin and show how it has been implemented.

Definition

A predicate is in Negation Normal Form when negation occurs only on atomic expression. To compute such a normal form, the following rewrite rules (which are already implemented in Rodin) are reused :

SIMP_NOT_NOT : \lnot\, \lnot\, P \;\;\defi\;\; P

DISTRI_NOT_AND : \lnot\,(P \land Q) \;\;\defi\;\; \lnot\, P \lor \lnot\, Q

DISTRI_NOT_OR : \lnot\,(P \lor Q) \;\;\defi\;\; \lnot\, P \land \lnot\, Q

DERIV_NOT_IMP : \lnot\,(P \limp Q) \;\;\defi\;\; P \land \lnot\, Q

DERIV_NOT_FORALL : \lnot\, \forall x \qdot P \;\;\defi\;\; \exists x \qdot \lnot\, P

DERIV_NOT_EXISTS : \lnot\, \exists x \qdot P \;\;\defi\;\; \forall x \qdot \lnot\, P

However, no rule has been defined for the case where the inner predicate is an equivalence, such as \lnot (P \leqv Q) . The latter is equivalent to both \lnot P \leqv Q and P \leqv\lnot Q. In this latter case, the way the tactic will work is yet to be defined. Since the "\leqv" is to be kept, the choice on which predicate the not will be applied to is ambiguous. Here is an example showing that difficulty :


\lnot(A \leqv \lnot (B \lor C)) (1) which is equivalent to \lnot(A \leqv (\lnot B \land \lnot C)) (2)


A solution would be to applied systematically on the left expression. In that case, simple simplification in the right member as in (1) would not be applied, thus complicating the left expression.

A better solution would to apply the \lnot on a member containing already a \lnot. But it can be hard to find an expression with a \lnot which has already been put in its Negation Normal Form as for the right member in (2)

Implementation

Tactics

When a predicate with a negation is matched, rules are applied following a pre-order traversal of that predicate.

\lnot(A \land \lnot (B \lor C))

\lnot A \lor \lnot\lnot (B \lor C)

\lnot A \lor (B \lor C)

INSTEAD OF

\lnot(A \land \lnot (B \lor C))

\lnot(A \land (\lnot B \land \lnot C))

\lnot A \lor \lnot(\lnot B \land \lnot C)

\lnot A \lor (\lnot\lnot B \lor \lnot\lnot C)

\lnot A \lor (B \lor \lnot\lnot C)

\lnot A \lor (B \lor C)

This way, tree proof is not unnecessarily complicated, and so more legible. The space used on disk is also smaller.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Modularisation_Plug-in_Tutorial&oldid=6246’