Difference between pages "Billaude's work to finish" and "Bugs and Feature Requests"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Billaude
(New section added (in order to replace the Membership Goal section))
 
imported>Pascal
 
Line 1: Line 1:
−
This page is here to describe the work that I started, but which is yet to be finished.
+
Please, use the SourceForge trackers to report a bug on existing features, or to request new features:
−
 
+
* [http://sourceforge.net/tracker/?group_id=108850&atid=651669 Bugs]
−
= MembershipGoal =
+
* [http://sourceforge.net/tracker/?group_id=108850&atid=651672 Feature Requests]
−
 
 
−
Here the rules that could be useful for the reasoner MembershipGoal.
 
−
 
 
−
{| class="wikitable" style="text-align:center; width:80%;"
 
−
|+ Inference rules for the reasoner MembershipGoal
 
−
|-
 
−
! scope=col | Inference Rule
 
−
! scope=col | Side condition
 
−
! scope=col | Implemented in the new version
 
−
! scope=col | Implemented in the first version
 
−
|-
 
−
|align="left"|<math> x\in A,\;\; A\subseteq B\vdash x\in B </math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math> A\subset B\vdash A\subseteq B </math>
 
−
|align="left"|
 
−
|<math>\checkmark</math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math> A=B\vdash A\subseteq B</math>
 
−
|align="left"|
 
−
|<math>\checkmark</math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math> A=B\vdash B\subseteq A</math>
 
−
|align="left"|
 
−
|<math>\checkmark</math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math> A\subseteq B\vdash \dom(A)\subseteq\dom(B)</math>
 
−
|align="left"|
 
−
|<math>\checkmark</math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math> A\subseteq B\vdash \ran(A)\subseteq\ran(B)</math>
 
−
|align="left"|
 
−
|<math>\checkmark</math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math> x\in\dom(A\cprod B)\vdash x\in A</math>
 
−
|align="left"|
 
−
|<math>\checkmark</math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math> y\in\ran(A\cprod B)\vdash y\in B</math>
 
−
|align="left"|
 
−
|<math>\checkmark</math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math> x\mapsto y\in f\vdash x\in\dom(f)</math>
 
−
|align="left"|
 
−
|<math>\checkmark</math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math> x\mapsto y\in f\vdash y\in\ran(f)</math>
 
−
|align="left"|
 
−
|<math>\checkmark</math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math> \left\{a,\cdots,x,\cdots, z\right\}\subseteq A\vdash x\in A</math>
 
−
|align="left"|
 
−
|<math>\checkmark</math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math> f\ovl\cdots\ovl g\ovl\cdots\ovl h\subseteq A\vdash g\ovl\cdots\ovl h\subseteq A</math>
 
−
|align="left"|
 
−
|<math>\checkmark</math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math> f\in A\;op\;B\vdash f\subseteq A\cprod B</math>
 
−
|align="left"|where <math>\mathit{op}</math> is one of <math>\rel</math>, <math>\trel</math>, <math>\srel</math>, <math>\strel</math>, <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math>
 
−
|<math>\checkmark</math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>e\subseteq f,\;\; f\setminus g\subseteq h\quad\vdash\quad e\setminus g\subseteq h</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>g\subseteq k,\;\; f\setminus g\subseteq h \quad\vdash\quad f\setminus k\subseteq h</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>e\subseteq f\setminus g,\;\; f\subseteq h\quad\vdash\quad e\subseteq h\setminus g</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>e\subseteq f\setminus g,\;\; k\subseteq g \quad\vdash\quad e\subseteq f\setminus k</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>e\subseteq f,\;\; f\ranres B\subseteq g \quad\vdash\quad e\ranres B\subseteq g</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>A\subseteq B ,\;\; f\ranres B\subseteq g \quad\vdash\quad f\ranres A\subseteq g</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>f\subseteq g\ranres A ,\;\; g\subseteq h \quad\vdash\quad f\subseteq h\ranres A</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>f\subseteq g\ranres A ,\;\; A\subseteq B \quad\vdash\quad f\subseteq g\ranres B</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>A\subseteq B ,\;\; B\domres f\subseteq g \quad\vdash\quad A\domres f\subseteq g</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>e\subseteq f ,\;\; B\domres f\subseteq g \quad\vdash\quad B\domres e\subseteq g</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>f\subseteq A\domres g ,\;\; A\subseteq B \quad\vdash\quad f\subseteq B\domres g</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>f\subseteq A\domres g ,\;\; g\subseteq h \quad\vdash\quad f\subseteq A\domres h</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>e\subseteq f ,\;\; f\ransub A\subseteq g \quad\vdash\quad e\ransub A\subseteq g</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>f\ransub A\subseteq g ,\;\; A\subseteq B \quad\vdash\quad f\ransub B\subseteq g</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>f\subseteq g\ransub A ,\;\; g\subseteq h \quad\vdash\quad f\subseteq h\ransub A</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>f\subseteq g\ransub B ,\;\; A\subseteq B \quad\vdash\quad f\subseteq g\ransub A</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>A\domsub f\subseteq g ,\;\; A\subseteq B \quad\vdash\quad B\domsub f\subseteq g</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>e\subseteq f ,\;\; A\domsub f\subseteq g \quad\vdash\quad A\domsub e\subseteq g</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>A\subseteq B ,\;\; f\subseteq B\domsub g \quad\vdash\quad f\subseteq A\domsub g</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>f\subseteq A\domsub g ,\;\; g\subseteq h \quad\vdash\quad f\subseteq A\domsub h</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>e\subseteq f ,\;\; f\ovl g\ovl\cdots\ovl h\subseteq k \quad\vdash\quad e\ovl g\ovl\cdots\ovl h\subseteq k</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>f\subseteq g\ovl h\ovl\cdots\ovl k ,\;\; e\subseteq g \quad\vdash\quad f\subseteq e\ovl h\ovl\cdots\ovl k</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>Z\subseteq B,\;\; A\bunion\cdots\bunion B\bunion\cdots\bunion C\subseteq D\quad\vdash\quad A\bunion\cdots\bunion Z\bunion\cdots\bunion C\subseteq D</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>B\subseteq Z ,\;\; D\subseteq A\bunion\cdots\bunion B\bunion\cdots\bunion C \quad\vdash\quad D\subseteq A\bunion\cdots\bunion Z\bunion\cdots\bunion C</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>Z\subseteq B,\;\; A\binter\cdots\binter B\binter\cdots\binter C\subseteq D\quad\vdash\quad A\binter\cdots\binter Z\binter\cdots\binter C\subseteq D</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>B\subseteq Z ,\;\; D\subseteq A\binter\cdots\binter B\binter\cdots\binter C \quad\vdash\quad D\subseteq A\binter\cdots\binter Z\binter\cdots\binter C</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>A\subseteq B,\;\; B\cprod D\subseteq E \quad\vdash\quad A\cprod D\subseteq E</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>C\subseteq D,\;\; B\cprod D\subseteq E \quad\vdash\quad B\cprod C\subseteq E</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>A\subseteq B\cprod D,\;\; B\subseteq C \quad\vdash\quad A\subseteq C\cprod D</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>A\subseteq B\cprod D,\;\; D\subseteq E\quad\vdash\quad A\subseteq B\cprod E</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>\dom(f\domres\prjone)\defi f</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>\dom(f\domres\prjtwo)\defi f</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>\dom(f\domres\id)\defi f</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>\ran(\prjone\ranres f)\defi f</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>\ran(\prjtwo\ranres f)\defi f</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>\ran(\id\ranres f)\defi f</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>\ran(f\domres\prjone)\defi\dom(f)</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>\ran(f\domres\prjtwo)\defi\ran(f)</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|align="left"|<math>\ran(f\domres\id)\defi f</math>
 
−
|align="left"|
 
−
|<math></math>
 
−
|<math>\checkmark</math>
 
−
|-
 
−
|}
 
−
 
 
−
This describe the rule that I implemented in the first version of MembershipGoal. Others should also be taken into account (they will be written later). Even if those rule have been checked, they may not be implemented in the reasoner since some can explode the time research.
 
−
 
 
−
= Membership Goal Exhaustive rules =
 
−
 
 
−
To be completed ...
 
−
 
 
−
= Autorewriter =
 
−
 
 
−
In the AutorewriterL3, some re-writing about <math>\usucc</math> and <math>\upred</math> are proceeded. But, more re-writing should be done. Unfortunately, I did not take too much time to analyze all the possibilities about this two functions <math>\left(\finite(\usucc) = \bfalse,\;\cdots\right)</math>.
 
−
 
 
−
Nevertheless, one trail has been explored : instead of re-writing <math>\usucc(x) = x+1</math>, we may should better re-write : <math>\left(\lambda x\qdot\btrue\mid x+1\right)</math>.
 
−
 
 
−
Moreover, since <math>\upred\defi\usucc^{-1}</math>, instead of re-writing <math>\usucc^{-1}\defi\left(\lambda x\qdot\btrue\mid x+1\right)^{-1}\defi\left\{a\qdot\btrue\mid a-1\mapsto a\right\}</math> (the last re-writing is proceeded by the auto-rewriter, and is not really easy to read), I think that we should re-write <math>\usucc^{-1}\defi\left(\lambda x\qdot\btrue\mid x-1\right)</math>.
 
−
 
 
−
= Others Feature Requests =
 
−
 
 
−
The feature request #2887264 should also be treated.
 
−
 
 
−
[[Category:Design proposal]]
 

Revision as of 14:45, 16 November 2009

Please, use the SourceForge trackers to report a bug on existing features, or to request new features:

Retrieved from ‘https://wiki.event-b.org/index.php?title=Billaude%27s_work_to_finish&oldid=969’