You can subscribe to this list here.
2009 
_{Jan}
(10) 
_{Feb}
(57) 
_{Mar}
(16) 
_{Apr}
(15) 
_{May}
(31) 
_{Jun}
(17) 
_{Jul}
(10) 
_{Aug}
(18) 
_{Sep}
(20) 
_{Oct}
(31) 
_{Nov}
(6) 
_{Dec}
(7) 

2010 
_{Jan}
(21) 
_{Feb}
(40) 
_{Mar}
(35) 
_{Apr}
(14) 
_{May}
(21) 
_{Jun}
(6) 
_{Jul}
(33) 
_{Aug}
(97) 
_{Sep}
(55) 
_{Oct}
(37) 
_{Nov}
(35) 
_{Dec}
(23) 
2011 
_{Jan}
(9) 
_{Feb}
(9) 
_{Mar}
(57) 
_{Apr}
(21) 
_{May}
(4) 
_{Jun}
(6) 
_{Jul}
(12) 
_{Aug}
(13) 
_{Sep}
(18) 
_{Oct}
(9) 
_{Nov}
(11) 
_{Dec}
(3) 
2012 
_{Jan}
(45) 
_{Feb}
(18) 
_{Mar}
(18) 
_{Apr}
(14) 
_{May}
(11) 
_{Jun}
(14) 
_{Jul}
(3) 
_{Aug}
(6) 
_{Sep}
(2) 
_{Oct}
(16) 
_{Nov}
(31) 
_{Dec}
(10) 
2013 
_{Jan}
(29) 
_{Feb}
(7) 
_{Mar}
(21) 
_{Apr}
(52) 
_{May}
(32) 
_{Jun}
(8) 
_{Jul}
(9) 
_{Aug}
(9) 
_{Sep}
(7) 
_{Oct}
(22) 
_{Nov}
(12) 
_{Dec}

2014 
_{Jan}
(36) 
_{Feb}
(11) 
_{Mar}
(11) 
_{Apr}
(18) 
_{May}
(8) 
_{Jun}
(19) 
_{Jul}
(15) 
_{Aug}
(22) 
_{Sep}
(11) 
_{Oct}
(8) 
_{Nov}
(4) 
_{Dec}
(7) 
S  M  T  W  T  F  S 




1
(4) 
2
(1) 
3

4

5

6

7
(10) 
8
(3) 
9

10
(7) 
11

12
(3) 
13
(6) 
14
(9) 
15

16

17
(1) 
18

19

20
(1) 
21
(2) 
22

23

24

25
(1) 
26
(2) 
27
(2) 
28

29
(2) 
30
(1) 


From: Wei, Wei <wei01.wei@sa...>  20100930 07:32:34

Using Matthias's setting of autotactic deployment, the number goes further up to 390... Original Message From: Wei, Wei [mailto:wei01.wei@...] Sent: Mittwoch, 29. September 2010 19:11 To: Jann Röder; rodinbsharpuser@... Subject: Re: [Rodinbsharpuser] Relevance filter plugin Hi Jann, Thanks for the plugin. You have done an excellent job, congratulations. I tried to prove automatically all POs for an EventB model of online retailer. The model was used as a case study whose result was published in a paper (with Jeremy Bryans) at FMICS 10. In the case study, 300 POs were automatically discharged. With your plugin, the number went up to 335. Note that this is done by simply adding "Meta prover" to the end of the queue of deployed autotactics. I will try to have Matthias's setting and see whether even more POs can be proved. Best regards, Wei Original Message From: Jann Röder [mailto:roederja@...] Sent: Montag, 27. September 2010 17:15 To: rodinbsharpuser@... Subject: [Rodinbsharpuser] Relevance filter plugin I have finally managed to package the relevance filter(s) I developed for my Master's thesis. The purpose of the relevance filter plugin is to try to automatically select relevant hypotheses for a proof as opposed to the user doing this manually. In my Master thesis I could show that relevance filtering can increase the amount of automatically discharged proofs by 20% (on average). The relevance filter can be invoked either by clicking the RF button in the proof control, or automatically as part of the auto tactic. It also comes with a preference dialog that allows you to configure the filter(s). The plugin implements several filtering methods that will be tried sequentially. The default setting is a selection of filters that have been found to work well. If you want to add the relevance filter to the auto tactic you should add the Meta Prover item. It replaces NewPP after lasoo, NewPP unrestricted, Atelier B P1 and Atelier B PP since this functionality is already included in the Meta prover. You still have to add ML at the appropriate place in the tactic as well as NewPP restricted and Atelier B P0. You can download the plugin here: http://n.ethz.ch/~roederja/download/RelevanceFilter.zip To install just copy the three .jar files from the plugin folder into your Rodin plugin folder. I also created a feature (in the feature folder) but I could not get Rodin to recognize it. Help on this is appreciated. If you want to learn more about the relevance filtering techniques I implemented you can read my thesis: http://n.ethz.ch/~roederja/download/thesis.pdf Let me know if you run into problems. I myself keep running into memory leaks in NewPP... The plugin should work with Rodin 1.3 . Jann  Start uncovering the many advantages of virtual appliances and start using them to simplify application deployment and accelerate your shift to cloud computing. http://p.sf.net/sfu/novellsfdev2dev _______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser  Start uncovering the many advantages of virtual appliances and start using them to simplify application deployment and accelerate your shift to cloud computing. http://p.sf.net/sfu/novellsfdev2dev _______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Alexei Iliasov <alexei.iliasov@nc...>  20100929 23:17:53

Dear Rodin users, Version 1.4 of the modularisation plugin has been released and is available for installation/update. This version is for the platform version 1.3. For general plugin information and installation instruction please see the wiki page: http://wiki.eventb.org/index.php/Modularisation_Plugin Best regards, Alexei Iliasov 
From: Wei, Wei <wei01.wei@sa...>  20100929 17:11:34

Hi Jann, Thanks for the plugin. You have done an excellent job, congratulations. I tried to prove automatically all POs for an EventB model of online retailer. The model was used as a case study whose result was published in a paper (with Jeremy Bryans) at FMICS 10. In the case study, 300 POs were automatically discharged. With your plugin, the number went up to 335. Note that this is done by simply adding "Meta prover" to the end of the queue of deployed autotactics. I will try to have Matthias's setting and see whether even more POs can be proved. Best regards, Wei Original Message From: Jann Röder [mailto:roederja@...] Sent: Montag, 27. September 2010 17:15 To: rodinbsharpuser@... Subject: [Rodinbsharpuser] Relevance filter plugin I have finally managed to package the relevance filter(s) I developed for my Master's thesis. The purpose of the relevance filter plugin is to try to automatically select relevant hypotheses for a proof as opposed to the user doing this manually. In my Master thesis I could show that relevance filtering can increase the amount of automatically discharged proofs by 20% (on average). The relevance filter can be invoked either by clicking the RF button in the proof control, or automatically as part of the auto tactic. It also comes with a preference dialog that allows you to configure the filter(s). The plugin implements several filtering methods that will be tried sequentially. The default setting is a selection of filters that have been found to work well. If you want to add the relevance filter to the auto tactic you should add the Meta Prover item. It replaces NewPP after lasoo, NewPP unrestricted, Atelier B P1 and Atelier B PP since this functionality is already included in the Meta prover. You still have to add ML at the appropriate place in the tactic as well as NewPP restricted and Atelier B P0. You can download the plugin here: http://n.ethz.ch/~roederja/download/RelevanceFilter.zip To install just copy the three .jar files from the plugin folder into your Rodin plugin folder. I also created a feature (in the feature folder) but I could not get Rodin to recognize it. Help on this is appreciated. If you want to learn more about the relevance filtering techniques I implemented you can read my thesis: http://n.ethz.ch/~roederja/download/thesis.pdf Let me know if you run into problems. I myself keep running into memory leaks in NewPP... The plugin should work with Rodin 1.3 . Jann  Start uncovering the many advantages of virtual appliances and start using them to simplify application deployment and accelerate your shift to cloud computing. http://p.sf.net/sfu/novellsfdev2dev _______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Jann Röder <roederja@et...>  20100927 15:15:08

I have finally managed to package the relevance filter(s) I developed for my Master's thesis. The purpose of the relevance filter plugin is to try to automatically select relevant hypotheses for a proof as opposed to the user doing this manually. In my Master thesis I could show that relevance filtering can increase the amount of automatically discharged proofs by 20% (on average). The relevance filter can be invoked either by clicking the RF button in the proof control, or automatically as part of the auto tactic. It also comes with a preference dialog that allows you to configure the filter(s). The plugin implements several filtering methods that will be tried sequentially. The default setting is a selection of filters that have been found to work well. If you want to add the relevance filter to the auto tactic you should add the Meta Prover item. It replaces NewPP after lasoo, NewPP unrestricted, Atelier B P1 and Atelier B PP since this functionality is already included in the Meta prover. You still have to add ML at the appropriate place in the tactic as well as NewPP restricted and Atelier B P0. You can download the plugin here: http://n.ethz.ch/~roederja/download/RelevanceFilter.zip To install just copy the three .jar files from the plugin folder into your Rodin plugin folder. I also created a feature (in the feature folder) but I could not get Rodin to recognize it. Help on this is appreciated. If you want to learn more about the relevance filtering techniques I implemented you can read my thesis: http://n.ethz.ch/~roederja/download/thesis.pdf Let me know if you run into problems. I myself keep running into memory leaks in NewPP... The plugin should work with Rodin 1.3 . Jann 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20100927 13:50:15

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear Laurent, finally I have inspected the rules. They all seem to be sound. I have not carried out any formal proofs, though. Cheers, Matthias Laurent Voisin schrieb: > Dear fellow Rodin users, > > I've just changed some inference rules in the Rodin wiki, where the > notion of "toplevel" occurrence has been replaced with: > >  either a WD strictness condition, see [1], > >  or a freeness condition, > >  or nothing when the condition was useless. > > This removes from the documentation this notion of "toplevel" which > was not formally defined and difficult to grasp. > > The rules that have changed are: > > FUN_IMAGE_GOAL > SUBSET_INTER > IN_INTER > NOTIN_INTER > OV_SETENUM_L > OV_SETENUM_R > OV_L > OV_R > DIS_BINTER_R > DIS_BINTER_L > DIS_SETMINUS_R > DIS_SETMINUS_L > SIM_REL_IMAGE_R > SIM_REL_IMAGE_L > SIM_FCOMP_R > SIM_FCOMP_L > CARD_INTERV > CARD_EMPTY_INTERV > SIMP_CARD_SETMINUS_L > SIMP_CARD_SETMINUS_R > SIMP_CARD_CPROD_L > SIMP_CARD_CPROD_R > > Could you please review these changes and report any error? > > Cheers, > Laurent. > > 1: http://wiki.eventb.org/index.php/Welldefinedness_in_EventB#Strictness > > > >  > Start uncovering the many advantages of virtual appliances > and start using them to simplify application deployment and > accelerate your shift to cloud computing. > http://p.sf.net/sfu/novellsfdev2dev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFMoKEEczhznXSdWggRArE8AJoCTpyGpstFr+tcAJ9e2a7yGqR8yACdECGm hs1TVvDGmy2tSeC5T6XfqRI= =z+KT END PGP SIGNATURE 
From: Daniel Schweizer <daschwei@st...>  20100926 11:50:47

Fine, that works! Thank you, Jens. Regards, Daniel Jens Bendisposto schrieb: > Hi Daniel, > > the binary in the release does not work for Leopard. In the next > release this issue will be fixed, however in the meantime you can use > the following workaround: > > Replace the folder > <YourRodinDir>/plugins/de.prob.cli_1.7.0/prob/macos by the folder you > can download > from https://cobra.cs.uniduesseldorf.de/prob/trunk/core/de.prob.cli/prob/macos > > Regards, > Jens > > > On Sep 25, 2010, at 7:49 PM, Daniel Schweizer wrote: > >> Hello everyone! >> >> I am completely new to Rodin, having problems with ProB. >> I installed the two required ProB plugins and restarted Rodin. When I >> try to open the ProB Perspective, I get the following error message: >> "An error occured. Reason: Could not determine port of ProB server" >> I'm using Rodin 1.3.1 on Mac OS 10.5.8. Can anyone give me some help? >> >> kind regards >> Daniel >> >> >> >> >> >> >> >>  >> Start uncovering the many advantages of virtual appliances >> and start using them to simplify application deployment and >> accelerate your shift to cloud computing. >> http://p.sf.net/sfu/novellsfdev2dev >> _______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 
From: Jens Bendisposto <bendisposto@cs...>  20100926 09:22:49

Hi Daniel, the binary in the release does not work for Leopard. In the next release this issue will be fixed, however in the meantime you can use the following workaround: Replace the folder <YourRodinDir>/plugins/de.prob.cli_1.7.0/prob/macos by the folder you can download from https://cobra.cs.uniduesseldorf.de/prob/trunk/core/de.prob.cli/prob/macos Regards, Jens On Sep 25, 2010, at 7:49 PM, Daniel Schweizer wrote: > Hello everyone! > > I am completely new to Rodin, having problems with ProB. > I installed the two required ProB plugins and restarted Rodin. When I > try to open the ProB Perspective, I get the following error message: > "An error occured. Reason: Could not determine port of ProB server" > I'm using Rodin 1.3.1 on Mac OS 10.5.8. Can anyone give me some help? > > kind regards > Daniel > > > > > > > >  > Start uncovering the many advantages of virtual appliances > and start using them to simplify application deployment and > accelerate your shift to cloud computing. > http://p.sf.net/sfu/novellsfdev2dev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Daniel Schweizer <daschwei@st...>  20100925 17:49:32

Hello everyone! I am completely new to Rodin, having problems with ProB. I installed the two required ProB plugins and restarted Rodin. When I try to open the ProB Perspective, I get the following error message: "An error occured. Reason: Could not determine port of ProB server" I'm using Rodin 1.3.1 on Mac OS 10.5.8. Can anyone give me some help? kind regards Daniel 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20100921 08:17:58

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear Laurent, >> In SUBSET_INTER you require the sidecondition: >> "where \mathbf{T} and \mathbf{U} are not bound by \mathbf{G}" >> >> I have always assumed that >> P(u) represents a term of the form P[x := u]. >> In that case your sidecondition is superfluous. >> >> Do you agree? If not, what is your interpretation of P(u)? > > It is also the way I understand it, and the way it is implemented, > thanks to the de Bruijn notation used in Java classes. Good. > However, people with a classical B background think differently (because > the Atelier B implementation requires that one explicitly checks for > freeness in such cases). > > This is why I've added this sidecondition, to be sure to be on the safe > side, whatever the reader.  From my point of view you are not "on the safe side, whatever the reader". Maybe readers with B background understand, but I was truly confused by that sidecondition. > An option would be to better explain the notation, so that such > sideconditions would become superfluous. Yes, explain the notation.  Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFMmGooczhznXSdWggRAiVzAJ9PA0xPtr+J6DIO9CF7BXDtyKy+KgCggR1k HlABtvyHfy8u9qBoHAb9ZdE= =Q3V0 END PGP SIGNATURE 
From: Laurent Voisin <laurent.voisin@sy...>  20100921 06:19:40

Dear Matthias, Le 20 sept. 10 à 13:52, Matthias Schmalz a écrit : > a request for clarification: > > In SUBSET_INTER you require the sidecondition: > "where \mathbf{T} and \mathbf{U} are not bound by \mathbf{G}" > > I have always assumed that > P(u) represents a term of the form P[x := u]. > In that case your sidecondition is superfluous. > > Do you agree? If not, what is your interpretation of P(u)? It is also the way I understand it, and the way it is implemented, thanks to the de Bruijn notation used in Java classes. However, people with a classical B background think differently (because the Atelier B implementation requires that one explicitly checks for freeness in such cases). This is why I've added this sidecondition, to be sure to be on the safe side, whatever the reader. An option would be to better explain the notation, so that such side conditions would become superfluous. Laurent. > Laurent Voisin schrieb: >> Dear fellow Rodin users, >> >> I've just changed some inference rules in the Rodin wiki, where the >> notion of "toplevel" occurrence has been replaced with: >> >>  either a WD strictness condition, see [1], >> >>  or a freeness condition, >> >>  or nothing when the condition was useless. >> >> This removes from the documentation this notion of "toplevel" which >> was not formally defined and difficult to grasp. >> >> The rules that have changed are: >> >> FUN_IMAGE_GOAL >> SUBSET_INTER >> IN_INTER >> NOTIN_INTER >> OV_SETENUM_L >> OV_SETENUM_R >> OV_L >> OV_R >> DIS_BINTER_R >> DIS_BINTER_L >> DIS_SETMINUS_R >> DIS_SETMINUS_L >> SIM_REL_IMAGE_R >> SIM_REL_IMAGE_L >> SIM_FCOMP_R >> SIM_FCOMP_L >> CARD_INTERV >> CARD_EMPTY_INTERV >> SIMP_CARD_SETMINUS_L >> SIMP_CARD_SETMINUS_R >> SIMP_CARD_CPROD_L >> SIMP_CARD_CPROD_R >> >> Could you please review these changes and report any error? >> >> Cheers, >> Laurent. >> >> 1: http://wiki.eventb.org/index.php/Welldefinedness_in_EventB#Strictness >> >> >> >>  >> Start uncovering the many advantages of virtual appliances >> and start using them to simplify application deployment and >> accelerate your shift to cloud computing. >> http://p.sf.net/sfu/novellsfdev2dev >> _______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > BEGIN PGP SIGNATURE > Version: GnuPG v1.4.6 (GNU/Linux) > Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org > > iD8DBQFMl0sDczhznXSdWggRAj6iAJ9gHj+2++sxukQtNE9lgshSlgwY1gCgtfi5 > BN3nDXTAawPs/zMkmkRT5u8= > =s5Dg > END PGP SIGNATURE 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20100920 11:52:50

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear Laurent, a request for clarification: In SUBSET_INTER you require the sidecondition: "where \mathbf{T} and \mathbf{U} are not bound by \mathbf{G}" I have always assumed that P(u) represents a term of the form P[x := u]. In that case your sidecondition is superfluous. Do you agree? If not, what is your interpretation of P(u)?  Matthias Laurent Voisin schrieb: > Dear fellow Rodin users, > > I've just changed some inference rules in the Rodin wiki, where the > notion of "toplevel" occurrence has been replaced with: > >  either a WD strictness condition, see [1], > >  or a freeness condition, > >  or nothing when the condition was useless. > > This removes from the documentation this notion of "toplevel" which > was not formally defined and difficult to grasp. > > The rules that have changed are: > > FUN_IMAGE_GOAL > SUBSET_INTER > IN_INTER > NOTIN_INTER > OV_SETENUM_L > OV_SETENUM_R > OV_L > OV_R > DIS_BINTER_R > DIS_BINTER_L > DIS_SETMINUS_R > DIS_SETMINUS_L > SIM_REL_IMAGE_R > SIM_REL_IMAGE_L > SIM_FCOMP_R > SIM_FCOMP_L > CARD_INTERV > CARD_EMPTY_INTERV > SIMP_CARD_SETMINUS_L > SIMP_CARD_SETMINUS_R > SIMP_CARD_CPROD_L > SIMP_CARD_CPROD_R > > Could you please review these changes and report any error? > > Cheers, > Laurent. > > 1: http://wiki.eventb.org/index.php/Welldefinedness_in_EventB#Strictness > > > >  > Start uncovering the many advantages of virtual appliances > and start using them to simplify application deployment and > accelerate your shift to cloud computing. > http://p.sf.net/sfu/novellsfdev2dev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFMl0sDczhznXSdWggRAj6iAJ9gHj+2++sxukQtNE9lgshSlgwY1gCgtfi5 BN3nDXTAawPs/zMkmkRT5u8= =s5Dg END PGP SIGNATURE 
From: Laurent Voisin <laurent.voisin@sy...>  20100917 17:24:58

Dear fellow Rodin users, I've just changed some inference rules in the Rodin wiki, where the notion of "toplevel" occurrence has been replaced with:  either a WD strictness condition, see [1],  or a freeness condition,  or nothing when the condition was useless. This removes from the documentation this notion of "toplevel" which was not formally defined and difficult to grasp. The rules that have changed are: FUN_IMAGE_GOAL SUBSET_INTER IN_INTER NOTIN_INTER OV_SETENUM_L OV_SETENUM_R OV_L OV_R DIS_BINTER_R DIS_BINTER_L DIS_SETMINUS_R DIS_SETMINUS_L SIM_REL_IMAGE_R SIM_REL_IMAGE_L SIM_FCOMP_R SIM_FCOMP_L CARD_INTERV CARD_EMPTY_INTERV SIMP_CARD_SETMINUS_L SIMP_CARD_SETMINUS_R SIMP_CARD_CPROD_L SIMP_CARD_CPROD_R Could you please review these changes and report any error? Cheers, Laurent. 1: http://wiki.eventb.org/index.php/Welldefinedness_in_EventB#Strictness 
From: John Pinto <jp_ppi@ya...>  20100914 14:16:28

Hi JR! OK, I can understand that as being a rational but then I would suggest changing that sentence in the errata to indicate that in this case we can prove absolute DLF and not just relative DLF which is why we are dropping the guards from the hypotheses. That would make your development easier to follow. You might want to add in the errata that this is always an option when proving DLF for a refinement. (I don't recall you stating that in the book  at least not in chapter 2). Thanks! John At 02:44 AM 9/14/2010 Tuesday, JeanRaymond Abrial wrote: >Dear John, > >What I want to express by this statement: > >>"Notice that we have removed the disjunction of the abstract guards >>in the antecedent of the implication because we have already proved >>them in the initial model". > >is that the RELATIVE deadlock freeness is here and ABSOLUTE deadlock >freeness. In the abstraction, the disjunction of the guards has been >proved to be true. So that in the refinement the disjunction of the >guard should also be proved to be true independently from the >disjunction of the abstract guards. > >So, it is MORE than just removing an unnecessary hypothesis. > >Hoping to have convinced you :) > >Yours, > >JR > > >On 12 Sep 2010, at 13:16, John Pinto wrote: > >>On page 66 of the EventB book, there is a statement about the DLF >>under discussion: "Notice that we have removed the disjunction of >>the abstract guards in the antecedent of the implication because we >>have already proved them in the initial model". >> >>That doesn't seem like a reasonable statement because you could say >>that about any of the antecedents since the others are either >>invariants or axioms! (They have all been previously proved to be true!) >> >>It seems to me that the real reason they were dropped is because >>they turned out to be unnecessary to the proof given in the book. >>(You could cite the MON inference rule to do that) In fact, in the >>slides for this chapter they were not dropped from the proof and in >>fact were essential for the proof given in the slides! (In fact >>this is an excellent illustration that the same sequent can be >>proved in different ways) >> >>Am I on the right track here? If so, I think this sentence on page >>66 should be amended in the errata sheet. It should instead say >>something like: >> >>"Notice that we have removed the disjunction of the abstract guards >>in the antecedent of the implication as they are not necessary in >>the following proof (We can use MON to remove them)". >> >> >>Thanks! >>John >> >>Start uncovering the many advantages of virtual appliances >>and start using them to simplify application deployment and >>accelerate your shift to cloud computing >><http://p.sf.net/sfu/novellsfdev2dev>http://p.sf.net/sfu/novellsfdev2dev >>_______________________________________________ >>Rodinbsharpuser mailing list >><mailto:Rodinbsharpuser@...>Rodinbsharpuser@... >>https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: JeanRaymond Abrial <jrabrial@ne...>  20100914 07:46:38

Dear Matthias, Thanks. I'll add some errata entries in the file Yours, JR On 14 Sep 2010, at 09:36, Matthias Schmalz wrote: > > BEGIN PGP SIGNED MESSAGE > Hash: SHA1 > > Dear JeanRaymond, > >>> Chapter 9: >>>   >>> 1) Cartesian products >>> >>> I was unable to prove theorems of the form >>> "!x. x : S ** T => (#x1,x2. x1>x2 = x)". >>> I think a rule is missing. >> >> Yes, the following rule should be added on page 330 >> >> !x.x:S**T => x= prj1(x) > prj2(x) > > I agree. That solves the problem. > >>> 2) Integers >>> >>> The expression "x = 1/(1)" may be rewritten to >>> "#r. (r:NAT & r < 1 & 1=x*(1)+r)". That allows you to rewrite a >>> satisfiable predicate into an unsatisfiable one. That can be used to >>> prove false. >> >> The division rewriting rule on page 333 bottom: >> >> c=a/b == #r.r:NAT & r<b & a=c*b+r >> >> does not work with negative numbers. It should be first simplified as follows: >> >> a/(b) == (a/b) >> >> (a)/b == (a/b) >> >> (a)/(b) == a/b > > Something like that... > >>> Chapter 5: >>> 3) I was playing around with proof obligations and got an example where >>> the tool produces a proof obligation differing from the specification in >>> the book. Of course, it could also be the case that Rodin is wrong, but >>> Rodin's proof obligation makes more sense to me then yours. The final >>> decision is up to you. >>> >>> Here is the model: >>> machine ref_0 >>> >>> variables x >>> >>> invariants >>> @inv1 x ∈ ℤ >>> >>> events >>> event INITIALISATION >>> ... >>> >>> event evt0 >>> any a where >>> @grd0 a > 0 >>> begin >>> @act0 x ≔ x+a >>> end >>> end >>> >>> machine ref_1 refines ref_0 >>> >>> variables y >>> >>> invariants >>> @inv1 y ∈ ℤ >>> @inv2 x = y >>> >>> events >>> event INITIALISATION >>> ... >>> >>> event evt0 refines evt0 >>> with >>> @a 1=a >>> then >>> @act0 y ≔ y+1 >>> end >>> end >>> >>> According to your book the proof obligation evt0/inv2/INV should not >>> contain the witness "1=a", because it is the witness predicate for a >>> parameter and not for a variable. But the Rodin proof obligation does >>> contain the witness. >>> Rodin's proof obligation can be proved, yours cannot. >>> Rodin's proof obligation makes sense to me, because according to my >>> intuition and to your definition of refinement in Chapter 14 evt0 does >>> indeed refine evt0. >> >> On page 195 bottom, the proof obligation evt/act/SIM mentions BOTH witness predicates (for variables and for parameters) >> >> But, maybe, you are not speaking of the same proof obligation. > > I was talking of the INV proof obligation on page 191, which only > includes witness predicates for variables, but not for parameters. > > Cheers, > > Matthias > BEGIN PGP SIGNATURE > Version: GnuPG v1.4.6 (GNU/Linux) > Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org > > iD8DBQFMjyYKczhznXSdWggRAt0vAKCKPGrCFswi13L606ZCkZao2D5BuQCdEmDv > QPxoukpCPzHfSReDWCIhSWA= > =/fW1 > END PGP SIGNATURE > 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20100914 07:36:51

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear JeanRaymond, >> Chapter 9: >>   >> 1) Cartesian products >> >> I was unable to prove theorems of the form >> "!x. x : S ** T => (#x1,x2. x1>x2 = x)". >> I think a rule is missing. > > Yes, the following rule should be added on page 330 > > !x.x:S**T => x= prj1(x) > prj2(x) I agree. That solves the problem. >> 2) Integers >> >> The expression "x = 1/(1)" may be rewritten to >> "#r. (r:NAT & r < 1 & 1=x*(1)+r)". That allows you to rewrite a >> satisfiable predicate into an unsatisfiable one. That can be used to >> prove false. > > The division rewriting rule on page 333 bottom: > > c=a/b == #r.r:NAT & r<b & a=c*b+r > > does not work with negative numbers. It should be first simplified as follows: > > a/(b) == (a/b) > > (a)/b == (a/b) > > (a)/(b) == a/b Something like that... >> Chapter 5: >> 3) I was playing around with proof obligations and got an example where >> the tool produces a proof obligation differing from the specification in >> the book. Of course, it could also be the case that Rodin is wrong, but >> Rodin's proof obligation makes more sense to me then yours. The final >> decision is up to you. >> >> Here is the model: >> machine ref_0 >> >> variables x >> >> invariants >> @inv1 x ∈ ℤ >> >> events >> event INITIALISATION >> ... >> >> event evt0 >> any a where >> @grd0 a > 0 >> begin >> @act0 x ≔ x+a >> end >> end >> >> machine ref_1 refines ref_0 >> >> variables y >> >> invariants >> @inv1 y ∈ ℤ >> @inv2 x = y >> >> events >> event INITIALISATION >> ... >> >> event evt0 refines evt0 >> with >> @a 1=a >> then >> @act0 y ≔ y+1 >> end >> end >> >> According to your book the proof obligation evt0/inv2/INV should not >> contain the witness "1=a", because it is the witness predicate for a >> parameter and not for a variable. But the Rodin proof obligation does >> contain the witness. >> Rodin's proof obligation can be proved, yours cannot. >> Rodin's proof obligation makes sense to me, because according to my >> intuition and to your definition of refinement in Chapter 14 evt0 does >> indeed refine evt0. > > On page 195 bottom, the proof obligation evt/act/SIM mentions BOTH witness predicates (for variables and for parameters) > > But, maybe, you are not speaking of the same proof obligation. I was talking of the INV proof obligation on page 191, which only includes witness predicates for variables, but not for parameters. Cheers, Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFMjyYKczhznXSdWggRAt0vAKCKPGrCFswi13L606ZCkZao2D5BuQCdEmDv QPxoukpCPzHfSReDWCIhSWA= =/fW1 END PGP SIGNATURE 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20100914 07:18:27

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Hi John, John Pinto schrieb: > Hi Matthias! > > So you are confirming that the book has an errata in that proof since it > seems to be using an invalid inference rule. Not exactly. The proof must be wrong, because the proof obligation is invalid. (Only valid proof obligations should be provable.) > Maybe JR can take another look at that proof on page 8586 and fill in > the blanks of that proof in the errata page he has started. Or at least > post to this list what the missing steps in the proof are. > > I'm not sure how to do that inference rule you mentioned in Rodin, what > is it called and how is it accessed? Isn't this the rule you told me > doesn't exist in Rodin? You are right, the rule > H, not Q  P >  > H  P \/ Q is not available in Rodin. You can however simulate it with ct and de Morgan, just as I explained the other day. Cheers, Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFMjyG7czhznXSdWggRAg7KAJ9RnPzFN47rtztQfgyMIx9Cm0R65ACeOZ0r NZUMOUI9A/cCxdOx6s5oh30= =1qyS END PGP SIGNATURE 
From: JeanRaymond Abrial <jrabrial@ne...>  20100914 06:44:28

Dear John, What I want to express by this statement: > "Notice that we have removed the disjunction of the abstract guards in the antecedent of the implication because we have already proved them in the initial model". is that the RELATIVE deadlock freeness is here and ABSOLUTE deadlock freeness. In the abstraction, the disjunction of the guards has been proved to be true. So that in the refinement the disjunction of the guard should also be proved to be true independently from the disjunction of the abstract guards. So, it is MORE than just removing an unnecessary hypothesis. Hoping to have convinced you :) Yours, JR On 12 Sep 2010, at 13:16, John Pinto wrote: > On page 66 of the EventB book, there is a statement about the DLF under discussion: "Notice that we have removed the disjunction of the abstract guards in the antecedent of the implication because we have already proved them in the initial model". > > That doesn't seem like a reasonable statement because you could say that about any of the antecedents since the others are either invariants or axioms! (They have all been previously proved to be true!) > > It seems to me that the real reason they were dropped is because they turned out to be unnecessary to the proof given in the book. (You could cite the MON inference rule to do that) In fact, in the slides for this chapter they were not dropped from the proof and in fact were essential for the proof given in the slides! (In fact this is an excellent illustration that the same sequent can be proved in different ways) > > Am I on the right track here? If so, I think this sentence on page 66 should be amended in the errata sheet. It should instead say something like: > > "Notice that we have removed the disjunction of the abstract guards in the antecedent of the implication as they are not necessary in the following proof (We can use MON to remove them)". > > > Thanks! > John >  > Start uncovering the many advantages of virtual appliances > and start using them to simplify application deployment and > accelerate your shift to cloud computing > http://p.sf.net/sfu/novellsfdev2dev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: JeanRaymond Abrial <jrabrial@ne...>  20100914 06:34:06

Dear Ogawa Kiyoshi, Thanks, corrected on the next version of the errata file. Yours, JR On 1 Sep 2010, at 06:32, ogawa.kiyoshi wrote: > > Dear JeanRaymond > > There are 2 TYPO at page 386. > > inv4_3 > ∀n·(n∈N⇒p(n)= parity(c(n)) > should be > ∀n·n∈N⇒p(n)= parity(c(n)) > > inv4_4 > ∀n·(n∈N⇒q(n) = parity(d(n)) > should be > ∀n·n∈N⇒q(n) = parity(d(n)) > > Best Regards. > ogawa.kiyoshi@... > > >> Dear Ogawa Kiyoshi, >> >>> There is a TYPO at page 83, 4th line from the bottom. >>> >>> ml_pass and ilpass >>> should be >>> ml_pass and il_pass >> >> Yes, you are right. We shall report this typo in the errata sheet of "event > b.org". >> >> Thanks for your cooperation ! >> >> JeanRaymond >> >> > > 08051218893 > > 
From: JeanRaymond Abrial <jrabrial@ne...>  20100914 06:21:29

Dear Ogawa Kiyoshi, Thanks. Yes, it is an error. It should be corrected to: a = (next(rsrtbl(b)))~(b) I'll make an entry in the errata file Yours, JR On 18 Aug 2010, at 14:41, ogawa.kiyoshi wrote: > > Dear JeanRaymond > >> Page 535 at route_reservation 7th line >> rsrtbl≔ rsrtbl ∪ rtbl ▷ {r} >> may be >> rsrtbl≔ rsrtbl ∪ (rtbl ▷ {r}) > > Page 539 at inv1_8 3rd line > a = nxt(rsrtbl(b))∼ (b) > > make > Syntax error: Invalid Term. > > In the download file, ch917_train.zip. This line is > a = (nxt(rsrtbl(b)))∼ (b) > > Is it known bug? > >> I type almost all EventB statements in this book for my training. >> This line make >> Syntax error: invalid RelationsSet Expr >> >> I can not search the reason why . >> >> In the download file, ch917_train.zip. This line is >> rsrtbl≔ rsrtbl ∪ (rtbl ▷ {r}) >> >> I may be realized what is happened. > > Best Regards. > Ogawa Kiyoshi > >>> Dear Ogawa Kiyoshi, >>> >>>> There is a TYPO at page 83, 4th line from the bottom. >>>> >>>> ml_pass and ilpass >>>> should be >>>> ml_pass and il_pass >>> >>> Yes, you are right. We shall report this typo in the errata sheet of "even > t >> b.org". >>> >>> Thanks for your cooperation ! >>> >>> JeanRaymond >>> >>> >> >> 08051218893 >> > > 08051218893 > > 
From: JeanRaymond Abrial <jrabrial@ne...>  20100914 06:13:43

Dear Ogawa Kiyoshi, Thanks for your errata. You're right it should be: rstbl := rstbl \/ (rtbl > {r}) I'll write a new entry in the errata file. Yours JR On 18 Aug 2010, at 12:48, ogawa.kiyoshi wrote: > > Dear JeanRaymond > > Page 535 at route_reservation 7th line > rsrtbl≔ rsrtbl ∪ rtbl ▷ {r} > may be > rsrtbl≔ rsrtbl ∪ (rtbl ▷ {r}) > > I type almost all EventB statements in this book for my training. > This line make > Syntax error: invalid RelationsSet Expr > > I can not search the reason why . > > In the download file, ch917_train.zip. This line is > rsrtbl≔ rsrtbl ∪ (rtbl ▷ {r}) > > I may be realized what is happened. > > Best Regards. > >> Dear Ogawa Kiyoshi, >> >>> There is a TYPO at page 83, 4th line from the bottom. >>> >>> ml_pass and ilpass >>> should be >>> ml_pass and il_pass >> >> Yes, you are right. We shall report this typo in the errata sheet of "event > b.org". >> >> Thanks for your cooperation ! >> >> JeanRaymond >> >> > > 08051218893 > > 
From: JeanRaymond Abrial <jrabrial@ne...>  20100914 05:52:38

Dear Mathias, Sorry for the delay. AT LAST, I got some time to cover the book errata you mentioned a long time ago. Thanks for your comments. I'll enter some errata in the errata file after your additional comments Thanks again, JR ======= > Chapter 9: >   > 1) Cartesian products > > I was unable to prove theorems of the form > "!x. x : S ** T => (#x1,x2. x1>x2 = x)". > I think a rule is missing. Yes, the following rule should be added on page 330 !x.x:S**T => x= prj1(x) > prj2(x) > 2) Integers > > The expression "x = 1/(1)" may be rewritten to > "#r. (r:NAT & r < 1 & 1=x*(1)+r)". That allows you to rewrite a > satisfiable predicate into an unsatisfiable one. That can be used to > prove false. The division rewriting rule on page 333 bottom: c=a/b == #r.r:NAT & r<b & a=c*b+r does not work with negative numbers. It should be first simplified as follows: a/(b) == (a/b) (a)/b == (a/b) (a)/(b) == a/b > Chapter 5: > 3) I was playing around with proof obligations and got an example where > the tool produces a proof obligation differing from the specification in > the book. Of course, it could also be the case that Rodin is wrong, but > Rodin's proof obligation makes more sense to me then yours. The final > decision is up to you. > > Here is the model: > machine ref_0 > > variables x > > invariants > @inv1 x ∈ ℤ > > events > event INITIALISATION > ... > > event evt0 > any a where > @grd0 a > 0 > begin > @act0 x ≔ x+a > end > end > > machine ref_1 refines ref_0 > > variables y > > invariants > @inv1 y ∈ ℤ > @inv2 x = y > > events > event INITIALISATION > ... > > event evt0 refines evt0 > with > @a 1=a > then > @act0 y ≔ y+1 > end > end > > According to your book the proof obligation evt0/inv2/INV should not > contain the witness "1=a", because it is the witness predicate for a > parameter and not for a variable. But the Rodin proof obligation does > contain the witness. > Rodin's proof obligation can be proved, yours cannot. > Rodin's proof obligation makes sense to me, because according to my > intuition and to your definition of refinement in Chapter 14 evt0 does > indeed refine evt0. On page 195 bottom, the proof obligation evt/act/SIM mentions BOTH witness predicates (for variables and for parameters) But, maybe, you are not speaking of the same proof obligation. ======== 
From: John Pinto <jp_ppi@ya...>  20100913 16:50:42

Hi Matthias! So you are confirming that the book has an errata in that proof since it seems to be using an invalid inference rule. Maybe JR can take another look at that proof on page 8586 and fill in the blanks of that proof in the errata page he has started. Or at least post to this list what the missing steps in the proof are. I'm not sure how to do that inference rule you mentioned in Rodin, what is it called and how is it accessed? Isn't this the rule you told me doesn't exist in Rodin? I understand that the derivation of a=0 in that proof to be what JR informally calls inference rule ARI (arithmetic), not sure how well it is formalized in the book but when I get to that step in Rodin I rely on the provers to know how to do arithmetic. (Since there is no provision for me in Rodin to just indicate what the ARI step is supposed to do  and I wouldn't want such a provision in case I make a silly mistake in arithmetic) I hope JR can take some time to go over this proof in a bit more detail and give us a cleaned up version using the inference rules in the book (I can accept the ARI steps in the book as long as I can figure them out for myself). Thanks! John At 08:00 AM 9/13/2010 Monday, Matthias Schmalz wrote: >BEGIN PGP SIGNED MESSAGE >Hash: SHA1 > >Dear John, > >I had a quick look at the DLF proof obligation on the bottom of page 85 >and come to the conclusion that it is unprovable because of missing >hypotheses. >Suppose "yellow" belongs to "COLOR" and is different from "green" and "red". >Then take: >a=0 >c=0 >ml_tl=yellow >il_tl=yellow >Then all the hypotheses are true and the goal is not. > >You can make the PO provable (in Rodin) by adding the missing hypotheses >about COLOR. The first step consists of 4 applications of >H, not Q  P >  >H  P \/ Q > >I doubt that the corrected PO will be provable from the rules in the >book, because I do e.g. not see how to derive "a = 0" from "not a > 0" >and "a : NAT". The rules about integers summarized in Chapter 9 are >incomplete, as Abrial admits by himself. > >Cheers, > >Matthias > >P.s.: >The rule > > H,P  Q v R > >  > > H  (P^Q) v R >is unsound. Take P=false and R=false as a counterexample. >BEGIN PGP SIGNATURE >Version: GnuPG v1.4.6 (GNU/Linux) >Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org > >iD8DBQFMjhJ4czhznXSdWggRAkx4AJ0d7o9VzispzPconTJNxBr8D49YgQCfcPpy >tIolZzRWZtt9He30xLpCRuQ= >=SRud >END PGP SIGNATURE 
From: Laurent Voisin <laurent.voisin@sy...>  20100913 12:10:48

Yes, you are right, Matthias. This was a mistake in the previous mail. We indeed have WD(COND(C, E1, E2)) == WD(C) & (C => WD(E1)) & (not C => WD(E2)) Cheers, Laurent. Le 13 sept. 10 à 12:13, Matthias Schmalz a écrit : > BEGIN PGP SIGNED MESSAGE > Hash: SHA1 > > Hi Nicolas, > >> WD for >> >> COND(C, E1, E2) >> >> is >> >> (C => WD(E1)) & (not C => WD(E2)) > > I would expect > > WD(C) & (C => WD(E1)) & (not C => WD(E2)) > > Cheers, > > Matthias 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20100913 12:01:04

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear John, I had a quick look at the DLF proof obligation on the bottom of page 85 and come to the conclusion that it is unprovable because of missing hypotheses. Suppose "yellow" belongs to "COLOR" and is different from "green" and "red". Then take: a=0 c=0 ml_tl=yellow il_tl=yellow Then all the hypotheses are true and the goal is not. You can make the PO provable (in Rodin) by adding the missing hypotheses about COLOR. The first step consists of 4 applications of H, not Q  P   H  P \/ Q I doubt that the corrected PO will be provable from the rules in the book, because I do e.g. not see how to derive "a = 0" from "not a > 0" and "a : NAT". The rules about integers summarized in Chapter 9 are incomplete, as Abrial admits by himself. Cheers, Matthias P.s.: The rule > H,P  Q v R >  > H  (P^Q) v R is unsound. Take P=false and R=false as a counterexample. BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFMjhJ4czhznXSdWggRAkx4AJ0d7o9VzispzPconTJNxBr8D49YgQCfcPpy tIolZzRWZtt9He30xLpCRuQ= =SRud END PGP SIGNATURE 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20100913 10:13:49

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Hi Nicolas, > WD for > > COND(C, E1, E2) > > is > > (C => WD(E1)) & (not C => WD(E2)) I would expect WD(C) & (C => WD(E1)) & (not C => WD(E2)) Cheers, Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFMjflSczhznXSdWggRAtWAAKCL4eL5Y7lR5iQSyVCAwZ0jx+1rzQCeN6/3 1615jTXWZwMkIbEK14EZS4w= =itmu END PGP SIGNATURE 