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}
(14) 
2015 
_{Jan}
(2) 
_{Feb}
(4) 
_{Mar}
(10) 
_{Apr}
(7) 
_{May}
(4) 
_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 


1

2
(2) 
3

4

5

6

7

8

9

10

11

12
(1) 
13

14

15

16

17
(5) 
18
(4) 
19

20

21
(7) 
22
(2) 
23
(4) 
24
(3) 
25
(3) 
26

27

28

29
(3) 
30
(1) 
31




From: Renato Silva <ras07r@ec...>  20100330 10:42:09

Dear Users, A service release (version 0.0.7) of the Renaming/Refactory is available on the main Rodin update site. Changes: a) fix bug when renaming event whose machine has refinements. A wiki page with more information about this plugin and installation steps is available: http://wiki.eventb.org/index.php/Refactoring_Framework If you any problem, please let me know. Kind Regards, Renato Silva email: ras07r@... Direct tel: +44 (0)23 80595052 PhD Student at Declarative Systems and Software Engineering Group School of Electronics and Computer Science, University of Southampton, Highfield, Southampton SO17 1BJ United Kingdom 
From: Colin Snook <cfs@ec...>  20100329 16:10:37

Dear All, Another bug was revealed by this mornings release so we had to make a second service release 1.0.2 This fixes a bug in the UMLB extension of the navigator, which causes an exception if a subfolder is present in the project. Colin Begin forwarded message: > From: Colin Snook <cfs@...> > Date: 29 March 2010 10:26:40 GMT+01:00 > To: rodinbsharpuser@..., rodinbsharpannounce@... > Subject: UMLB service release 1.0.1 > > Dear Users, > > A service release (Version 1.0.1) of UMLB is available on the main Rodin update site. > Changes: > a) fix bug that prevents adding a state machine to a refined state > b) fix bug that leaves context diagram unusable after using the button "remove unused class types" > c) add icon for package diagram > > Please note that the sourceforge FRS seems to be running very slowly and sometimes times out. If this happens, just repeat the install and it will continue from where it was. > > Dr Colin F. Snook > Dependable Systems and Software Engineering, > School of Electronics and Computer Science, > University of Southampton > Southampton > SO17 1BJ > > > > > Dr Colin F. Snook Dependable Systems and Software Engineering, School of Electronics and Computer Science, University of Southampton Southampton SO17 1BJ 
From: Colin Snook <cfs@ec...>  20100329 09:32:49

Dear Users, A new release (Version 0.1.3) of UMLB Statemachine Animation is available on the main Rodin update site. This release is an update to work with the latest version of UMLB. Please note that the sourceforge FRS seems to be running very slowly and sometimes times out. If this happens, just repeat the install and it will continue from where it was. Dr Colin F. Snook Dependable Systems and Software Engineering, School of Electronics and Computer Science, University of Southampton Southampton SO17 1BJ 
From: Colin Snook <cfs@ec...>  20100329 09:26:55

Dear Users, A service release (Version 1.0.1) of UMLB is available on the main Rodin update site. Changes: a) fix bug that prevents adding a state machine to a refined state b) fix bug that leaves context diagram unusable after using the button "remove unused class types" c) add icon for package diagram Please note that the sourceforge FRS seems to be running very slowly and sometimes times out. If this happens, just repeat the install and it will continue from where it was. Dr Colin F. Snook Dependable Systems and Software Engineering, School of Electronics and Computer Science, University of Southampton Southampton SO17 1BJ 
From: Ken Robinson <kenr@cs...>  20100325 14:44:51

Dear Laurent, Thank you for your patient and as always helpful answer. My previous email was very long. Sorry for that and I intend to keep this short. For that reason I'm putting my answer up front rather than distribute. You probably thought my earlier email was a complaint. It wasn't meant to be that. The concern is as follows. I think I can claim to be a keen advocate of EventB. I am concerned with scalability, which is the thing that can kill EventB. When you develop a significant model you expect to get some difficult POs. You are going to be put off by simple POs that don't discharge easily. The latter will not impress. Just as a trivial example of that. The first assignment I set was a simple familiarisation exercise. One of the POs the students got was FIS NAT1 /= {}, which was not discharged by the autoprover. It was as you expect discharged by ml and by the auto prover once the auto tactics were set up. But you might concede that is doesn't impress., and it screams "this thing won't scale". That was essentially my main concern. I certainly want to develop a better understanding so I can give better advice. I do recognise that there is no universal tactic. And I haven't looked at the rule based prover. I certainly intend to. Thanks again. Cheers, Ken On 25/03/2010, at 23:03 PM, Laurent Voisin wrote: > Dear Ken, > > Le 25 mars 10 à 06:31, Ken Robinson a écrit : > >> Dear JR and fellow Rodin/EventB devotees, >> >> On 25/03/2010, at 06:02 AM, JeanRaymond Abrial wrote: >> >>>> I very much appreciate all the help one gets in this group. >> >>> Yes, at the moment this group is very active. People are very interested >>> and enthusiastic. I am just hoping that this will continue in the future. >> >> I would like to echo these thoughts. >> >> I've been taught two very interesting lessons in the last two weeks via this forum. >> >> Most recently was the advice from Kimmo Varpaaniemi advising a strategy involving contradicting the goal and then showing that the hypotheses are false. >> >> Logically this must work, but I would never have used it, although now I believe I can think of cases where it would have simplified the proof. >> >> What interests me is that I wouldn't have used it because I wouldn't have thought there would be any point of using it. >> >> The point of interest is that it reveals something interesting about the provers, not proof itself. >> >> The second was the help I got on my own problem from Christophe and Matthias. >> >> The goal was >> >> X → Y≠∅ >> >> where X and Y are finite sets. >> >> Christophe's directions: >> >> you can build the proof in the following way : >> >> from Y/={} you can derive x:Y >> >> then >> you rewrite not ( X>Y) = {} >> >> You obtain #x . x : X>Y >> >> Then propose the following witness X*{x} >> >> Looked fine, but I hadn't the foggiest idea of how to execute them. >> >> Matthias eventually overcame my ignorance and all was fine. >> >> Except the strategy was bizarre. >> >> There were hypotheses that once proved were regarded as true and eliminated from the hypotheses. I'd seen that happen before and never understood what was happening. I'd never thought of backtracking to uncover an earlier proved hypothesis. > > This happens when the hypothesis is considered as useless in the general case. The point in doing this is to reduce clutter in the hypothesis stack. > > For instance, a hypothesis of form > > x : Y > > where Y is a type is considered useless as it is a property of the typing of variable "x", and is not providing any additional information. I nevertheless understand that, here, this property is exactly what you intended to create and that the prover appears deceptive. Design decisions are always debatable and one size doesn't fit all. > > However, there is another way out that the one you described. The prover is highly configurable. In this case, if you look at the proof tree, you see that your hypothesis has been removed by a reasoner labelled "type rewrites" which has been fired automatically (that is by the post tactic). By clicking on the small downpointing triangle which appears in the top right of the "Proof Control" window title bar, a menu pops up. Select "Preferences..." in this menu. This is a rapid shortcut to the configuration of the posttactic. > > Then, in the righthand pane, you will see an automated tactic called "Type Rewriter (Simplify)" (as an aside, we're currently working at making these labels more consistent with each other). Click on this tactic and click on the "<<" button to remove it from the posttactic, then click "OK". From now on, the posttactic will not perform this kind of simplification anymore. > >> And there were other things that were a long way from intuitive. >> >> Apologies for this long ramble, but there is a point. >> >> And the point is that both of these lessons revealed a lot about the prover rather than proof as such. >> >> You have to remember that both of the above goals were trivially obvious, and there was nothing clever about the final proof. It was all about how to drive the prover. >> >> And this happens often. > > For this particular case, my understanding is that such lemmas shall be discharged automatically and you should not have to spend time with such trivial properties. However, whatever the effort we put in improving the automated provers, there still will be cases where one needs to resort to interactive proof, so your point is very relevant. > >> Is there any documentation anywhere that helps you to understand how to drive the prover. > > There is part of it on the wiki, but it is spread in various places and far from sufficient. We're currently working on better documenting the various tactics, with the stress put on describing their purpose and use cases where they are useful. However, this is not yet available. > > Currently, the best available documentation remains the tutorial: > > http://wiki.eventb.org/index.php/Mathematical_proofs_%28Rodin_Tutorial%29 > >> Otherwise, I am worried. I spend a lot of time discharging POs that are obvious, but they take more time to prove than I would have thought reasonable. > > We would be very happy to get feedback in this area. If you often encounter lemmas that look trivial to you, please report them on this mailing list, or even better, enter a Feature Request on the SourceForge web site. This will make us aware of your typical problems and allow us to tackle them. > > Another option would be to use the rulebased prover (available as a separate plugin from the Rodin update site). With this prover, you can enter your own proof rules in a friendly manner in socalled theories (only rewrite rules in the current version, but inference rule will appear this year). This is quite similar to the approach used by the B toolkit or Atelier B. However, there is one difference, you need to prove your rule correct (or at least review it) before using it. > > But, even if you take this route, please let us know the rules you felt interesting to add. This is very interesting feedback for us to improve the general prover used by everybody. > >> If I am correct then this is bad news for Rodin, and indirectly EventB. That's not intended to be a criticism; it's a heartfelt concern. >> >> It is necessary to understand the underlying tactics of the provers. You see it all the time. There are all these red operators and it's not clear what to do with them. Some times selecting them works miracles (genuinely) and other times it seems to send you off on a wild goose chase. > > Most of the time, when a tactic is not applied automatically, it is because of this risk of leading you to a dead end. So, in general, "red operators" are a doubleedge sword and need human expertise to decide whether and when to click on them. I completely understand that taking this decision when you have no idea of what clicking on the operator would do is a very frustrating experience. Hence, the work we've already started on documenting them is really needed. > >> I don't think that is very good, and it means that this wonderful community is sometimes spending a lot of time on things that should be trivial. >> >> I hope someone is going to tell me that I've missed something and my concerns are wasted. :) >> >> Hoping. > > As usual your concerns are very helpful to us and to the point. I'm however happy to see that, this time, we started addressing them before you expressed them strongly. From the bright side, your constructive criticism is reinforcing the impression we are on the right track (albeit a bit late, this tactic documentation should have started earlier). > > Cheers, > Laurent. > 
From: Laurent Voisin <lpvoisin@gm...>  20100325 12:03:59

Dear Ken, Le 25 mars 10 à 06:31, Ken Robinson a écrit : > Dear JR and fellow Rodin/EventB devotees, > > On 25/03/2010, at 06:02 AM, JeanRaymond Abrial wrote: > >>> I very much appreciate all the help one gets in this group. > >> Yes, at the moment this group is very active. People are very >> interested >> and enthusiastic. I am just hoping that this will continue in the >> future. > > I would like to echo these thoughts. > > I've been taught two very interesting lessons in the last two weeks > via this forum. > > Most recently was the advice from Kimmo Varpaaniemi advising a > strategy involving contradicting the goal and then showing that the > hypotheses are false. > > Logically this must work, but I would never have used it, although > now I believe I can think of cases where it would have simplified > the proof. > > What interests me is that I wouldn't have used it because I wouldn't > have thought there would be any point of using it. > > The point of interest is that it reveals something interesting about > the provers, not proof itself. > > The second was the help I got on my own problem from Christophe and > Matthias. > > The goal was > > X → Y≠∅ > > where X and Y are finite sets. > > Christophe's directions: > > you can build the proof in the following way : > > from Y/={} you can derive x:Y > > then > you rewrite not ( X>Y) = {} > > You obtain #x . x : X>Y > > Then propose the following witness X*{x} > > Looked fine, but I hadn't the foggiest idea of how to execute them. > > Matthias eventually overcame my ignorance and all was fine. > > Except the strategy was bizarre. > > There were hypotheses that once proved were regarded as true and > eliminated from the hypotheses. I'd seen that happen before and > never understood what was happening. I'd never thought of > backtracking to uncover an earlier proved hypothesis. This happens when the hypothesis is considered as useless in the general case. The point in doing this is to reduce clutter in the hypothesis stack. For instance, a hypothesis of form x : Y where Y is a type is considered useless as it is a property of the typing of variable "x", and is not providing any additional information. I nevertheless understand that, here, this property is exactly what you intended to create and that the prover appears deceptive. Design decisions are always debatable and one size doesn't fit all. However, there is another way out that the one you described. The prover is highly configurable. In this case, if you look at the proof tree, you see that your hypothesis has been removed by a reasoner labelled "type rewrites" which has been fired automatically (that is by the post tactic). By clicking on the small downpointing triangle which appears in the top right of the "Proof Control" window title bar, a menu pops up. Select "Preferences..." in this menu. This is a rapid shortcut to the configuration of the posttactic. Then, in the righthand pane, you will see an automated tactic called "Type Rewriter (Simplify)" (as an aside, we're currently working at making these labels more consistent with each other). Click on this tactic and click on the "<<" button to remove it from the posttactic, then click "OK". From now on, the posttactic will not perform this kind of simplification anymore. > And there were other things that were a long way from intuitive. > > Apologies for this long ramble, but there is a point. > > And the point is that both of these lessons revealed a lot about the > prover rather than proof as such. > > You have to remember that both of the above goals were trivially > obvious, and there was nothing clever about the final proof. It was > all about how to drive the prover. > > And this happens often. For this particular case, my understanding is that such lemmas shall be discharged automatically and you should not have to spend time with such trivial properties. However, whatever the effort we put in improving the automated provers, there still will be cases where one needs to resort to interactive proof, so your point is very relevant. > Is there any documentation anywhere that helps you to understand how > to drive the prover. There is part of it on the wiki, but it is spread in various places and far from sufficient. We're currently working on better documenting the various tactics, with the stress put on describing their purpose and use cases where they are useful. However, this is not yet available. Currently, the best available documentation remains the tutorial: http://wiki.eventb.org/index.php/Mathematical_proofs_%28Rodin_Tutorial%29 > Otherwise, I am worried. I spend a lot of time discharging POs that > are obvious, but they take more time to prove than I would have > thought reasonable. We would be very happy to get feedback in this area. If you often encounter lemmas that look trivial to you, please report them on this mailing list, or even better, enter a Feature Request on the SourceForge web site. This will make us aware of your typical problems and allow us to tackle them. Another option would be to use the rulebased prover (available as a separate plugin from the Rodin update site). With this prover, you can enter your own proof rules in a friendly manner in socalled theories (only rewrite rules in the current version, but inference rule will appear this year). This is quite similar to the approach used by the B toolkit or Atelier B. However, there is one difference, you need to prove your rule correct (or at least review it) before using it. But, even if you take this route, please let us know the rules you felt interesting to add. This is very interesting feedback for us to improve the general prover used by everybody. > If I am correct then this is bad news for Rodin, and indirectly > EventB. That's not intended to be a criticism; it's a heartfelt > concern. > > It is necessary to understand the underlying tactics of the > provers. You see it all the time. There are all these red > operators and it's not clear what to do with them. Some times > selecting them works miracles (genuinely) and other times it seems > to send you off on a wild goose chase. Most of the time, when a tactic is not applied automatically, it is because of this risk of leading you to a dead end. So, in general, "red operators" are a doubleedge sword and need human expertise to decide whether and when to click on them. I completely understand that taking this decision when you have no idea of what clicking on the operator would do is a very frustrating experience. Hence, the work we've already started on documenting them is really needed. > I don't think that is very good, and it means that this wonderful > community is sometimes spending a lot of time on things that should > be trivial. > > I hope someone is going to tell me that I've missed something and my > concerns are wasted. :) > > Hoping. As usual your concerns are very helpful to us and to the point. I'm however happy to see that, this time, we started addressing them before you expressed them strongly. From the bright side, your constructive criticism is reinforcing the impression we are on the right track (albeit a bit late, this tactic documentation should have started earlier). Cheers, Laurent. 
From: Ken Robinson <kenr@cs...>  20100325 06:32:37

Dear JR and fellow Rodin/EventB devotees, On 25/03/2010, at 06:02 AM, JeanRaymond Abrial wrote: >> I very much appreciate all the help one gets in this group. > Yes, at the moment this group is very active. People are very interested > and enthusiastic. I am just hoping that this will continue in the future. I would like to echo these thoughts. I've been taught two very interesting lessons in the last two weeks via this forum. Most recently was the advice from Kimmo Varpaaniemi advising a strategy involving contradicting the goal and then showing that the hypotheses are false. Logically this must work, but I would never have used it, although now I believe I can think of cases where it would have simplified the proof. What interests me is that I wouldn't have used it because I wouldn't have thought there would be any point of using it. The point of interest is that it reveals something interesting about the provers, not proof itself. The second was the help I got on my own problem from Christophe and Matthias. The goal was X → Y≠∅ where X and Y are finite sets. Christophe's directions: you can build the proof in the following way : from Y/={} you can derive x:Y then you rewrite not ( X>Y) = {} You obtain #x . x : X>Y Then propose the following witness X*{x} Looked fine, but I hadn't the foggiest idea of how to execute them. Matthias eventually overcame my ignorance and all was fine. Except the strategy was bizarre. There were hypotheses that once proved were regarded as true and eliminated from the hypotheses. I'd seen that happen before and never understood what was happening. I'd never thought of backtracking to uncover an earlier proved hypothesis. And there were other things that were a long way from intuitive. Apologies for this long ramble, but there is a point. And the point is that both of these lessons revealed a lot about the prover rather than proof as such. You have to remember that both of the above goals were trivially obvious, and there was nothing clever about the final proof. It was all about how to drive the prover. And this happens often. Is there any documentation anywhere that helps you to understand how to drive the prover. Otherwise, I am worried. I spend a lot of time discharging POs that are obvious, but they take more time to prove than I would have thought reasonable. If I am correct then this is bad news for Rodin, and indirectly EventB. That's not intended to be a criticism; it's a heartfelt concern. It is necessary to understand the underlying tactics of the provers. You see it all the time. There are all these red operators and it's not clear what to do with them. Some times selecting them works miracles (genuinely) and other times it seems to send you off on a wild goose chase. I don't think that is very good, and it means that this wonderful community is sometimes spending a lot of time on things that should be trivial. I hope someone is going to tell me that I've missed something and my concerns are wasted. :) Hoping. Cheers, Ken > > Yours, > > JeanRaymond >> Regards >> >> Jonathan >> >> Original Message >> From: Laurent Voisin [mailto:lpvoisin@...] >> Sent: Wednesday, March 24, 2010 11:09 AM >> To: Jonathan S. Ostroff >> Cc: 'User Rodin Bsharp User' >> Subject: Re: [Rodinbsharpuser] Total functions and the empty set >> >> Dear Jonathan, >> >> Le 23 mars 10 à 02:34, Jonathan S. Ostroff a écrit : >> >> >>> (*) Given n>0 I would like to prove that: ¬ (0‥n → {0} ⊆ ∅) >>> >>> [More generally I would like to prove that (**) ¬ (0‥n → {0} = >>> ∅), but the above theorem is the critical one. This is the PO for >>> initializing all values in an array to zero.] >>> >> >> If I inferred correctly from your explanation, you have an >> INITIALISATION action of form: >> >> x :: 0..n > {0} >> >> to say that variable "x" is initialised so that it is a total >> function. Then, lemma (*) comes from the feasibility proof obligation >> you get from this action. >> >> However, as your set is actually a singleton: >> >> 0..n > {0} = { 0..n ** {0} } >> >> you could use a deterministic action in your INITIALISATION >> >> x := 0..n ** {0} >> >> And then, you don't have any proof obligation for feasibility. Also, >> the prover as good support for proving lemmas similar to: >> >> 0..n ** {0} : 0..n +> INT >> >> >>> I would have thought that (*) and (**) would be discharged >>> automatically as part of the background theory. This does not happen >>> and I can see no way of guiding the proof, other than by induction >>> on n). >>> >>> I have not done an inductive proof before: >>> >>> http://wiki.eventb.org/index.php/Induction_proof >>> >>> Am I doing this correctly? One introduces the "proof key" ∀s• >>> s⊆ℕ1 ∧1∈s∧(∀n•n∈s⇒n+1∈s)⇒ℕ1⊆s as an axiom >>> in a context (this generates a warning because n is already used), >>> and then instantiate the proof key appropriately. I tried this and >>> after a long proof tree everything eventually discharges (I can >>> forward my proof if needed). >>> >>> This seems like quite a bit of work to prove (*). >>> >>> Your advice would be much appreciated, as usual. >>> >> >> From my experience, it is very rare that one needs to make an >> inductive proof. For most cases, there is good support from the >> provers (you need to install Atelier B provers, though) and one very >> seldom needs to go back to the root (which use of induction is, here) >> to carry proofs. >> >> Most of the time, the need to prove some intricate lemma that doesn't >> work well with the current provers is more a symptom of a problem in a >> model (unnecessarily complicated) rather than in the prover. But don't >> forget to take this rule with a grain of salt, as there are >> exceptions... >> >> Hope this helps, >> Laurent. >> >> >>  >> Download Intel® Parallel Studio Eval >> Try the new software tools for yourself. Speed compiling, find bugs >> proactively, and finetune applications for parallel performance. >> See why Intel Parallel Studio got high marks during beta. >> http://p.sf.net/sfu/intelswdev >> _______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser >> > > >  > Download Intel® Parallel Studio Eval > Try the new software tools for yourself. Speed compiling, find bugs > proactively, and finetune applications for parallel performance. > See why Intel Parallel Studio got high marks during beta. > http://p.sf.net/sfu/intelswdev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: JeanRaymond Abrial <jabrial@in...>  20100324 19:02:57

Dear Jonathan > I very much appreciate all the help one gets in this group. > Yes, at the moment this group is very active. People are very interested and enthusiastic. I am just hoping that this will continue in the future. Yours, JeanRaymond > Regards > > Jonathan > > Original Message > From: Laurent Voisin [mailto:lpvoisin@...] > Sent: Wednesday, March 24, 2010 11:09 AM > To: Jonathan S. Ostroff > Cc: 'User Rodin Bsharp User' > Subject: Re: [Rodinbsharpuser] Total functions and the empty set > > Dear Jonathan, > > Le 23 mars 10 à 02:34, Jonathan S. Ostroff a écrit : > > >> (*) Given n>0 I would like to prove that: ¬ (0‥n → {0} ⊆ ∅) >> >> [More generally I would like to prove that (**) ¬ (0‥n → {0} = >> ∅), but the above theorem is the critical one. This is the PO for >> initializing all values in an array to zero.] >> > > If I inferred correctly from your explanation, you have an > INITIALISATION action of form: > > x :: 0..n > {0} > > to say that variable "x" is initialised so that it is a total > function. Then, lemma (*) comes from the feasibility proof obligation > you get from this action. > > However, as your set is actually a singleton: > > 0..n > {0} = { 0..n ** {0} } > > you could use a deterministic action in your INITIALISATION > > x := 0..n ** {0} > > And then, you don't have any proof obligation for feasibility. Also, > the prover as good support for proving lemmas similar to: > > 0..n ** {0} : 0..n +> INT > > >> I would have thought that (*) and (**) would be discharged >> automatically as part of the background theory. This does not happen >> and I can see no way of guiding the proof, other than by induction >> on n). >> >> I have not done an inductive proof before: >> >> http://wiki.eventb.org/index.php/Induction_proof >> >> Am I doing this correctly? One introduces the "proof key" ∀s• >> s⊆ℕ1 ∧1∈s∧(∀n•n∈s⇒n+1∈s)⇒ℕ1⊆s as an axiom >> in a context (this generates a warning because n is already used), >> and then instantiate the proof key appropriately. I tried this and >> after a long proof tree everything eventually discharges (I can >> forward my proof if needed). >> >> This seems like quite a bit of work to prove (*). >> >> Your advice would be much appreciated, as usual. >> > > From my experience, it is very rare that one needs to make an > inductive proof. For most cases, there is good support from the > provers (you need to install Atelier B provers, though) and one very > seldom needs to go back to the root (which use of induction is, here) > to carry proofs. > > Most of the time, the need to prove some intricate lemma that doesn't > work well with the current provers is more a symptom of a problem in a > model (unnecessarily complicated) rather than in the prover. But don't > forget to take this rule with a grain of salt, as there are > exceptions... > > Hope this helps, > Laurent. > > >  > Download Intel® Parallel Studio Eval > Try the new software tools for yourself. Speed compiling, find bugs > proactively, and finetune applications for parallel performance. > See why Intel Parallel Studio got high marks during beta. > http://p.sf.net/sfu/intelswdev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 
From: Jonathan S. Ostroff <jonathan@yo...>  20100324 16:11:24

Dear Laurent: Thank you for this useful information, and yes, now I see that this is the way to do it. I very much appreciate all the help one gets in this group. Regards Jonathan Original Message From: Laurent Voisin [mailto:lpvoisin@...] Sent: Wednesday, March 24, 2010 11:09 AM To: Jonathan S. Ostroff Cc: 'User Rodin Bsharp User' Subject: Re: [Rodinbsharpuser] Total functions and the empty set Dear Jonathan, Le 23 mars 10 à 02:34, Jonathan S. Ostroff a écrit : > (*) Given n>0 I would like to prove that: ¬ (0‥n → {0} ⊆ ∅) > > [More generally I would like to prove that (**) ¬ (0‥n → {0} = > ∅), but the above theorem is the critical one. This is the PO for > initializing all values in an array to zero.] If I inferred correctly from your explanation, you have an INITIALISATION action of form: x :: 0..n > {0} to say that variable "x" is initialised so that it is a total function. Then, lemma (*) comes from the feasibility proof obligation you get from this action. However, as your set is actually a singleton: 0..n > {0} = { 0..n ** {0} } you could use a deterministic action in your INITIALISATION x := 0..n ** {0} And then, you don't have any proof obligation for feasibility. Also, the prover as good support for proving lemmas similar to: 0..n ** {0} : 0..n +> INT > I would have thought that (*) and (**) would be discharged > automatically as part of the background theory. This does not happen > and I can see no way of guiding the proof, other than by induction > on n). > > I have not done an inductive proof before: > > http://wiki.eventb.org/index.php/Induction_proof > > Am I doing this correctly? One introduces the "proof key" ∀s• > s⊆ℕ1 ∧1∈s∧(∀n•n∈s⇒n+1∈s)⇒ℕ1⊆s as an axiom > in a context (this generates a warning because n is already used), > and then instantiate the proof key appropriately. I tried this and > after a long proof tree everything eventually discharges (I can > forward my proof if needed). > > This seems like quite a bit of work to prove (*). > > Your advice would be much appreciated, as usual. From my experience, it is very rare that one needs to make an inductive proof. For most cases, there is good support from the provers (you need to install Atelier B provers, though) and one very seldom needs to go back to the root (which use of induction is, here) to carry proofs. Most of the time, the need to prove some intricate lemma that doesn't work well with the current provers is more a symptom of a problem in a model (unnecessarily complicated) rather than in the prover. But don't forget to take this rule with a grain of salt, as there are exceptions... Hope this helps, Laurent. 
From: Laurent Voisin <lpvoisin@gm...>  20100324 15:09:46

Dear Jonathan, Le 23 mars 10 à 02:34, Jonathan S. Ostroff a écrit : > (*) Given n>0 I would like to prove that: ¬ (0‥n → {0} ⊆ ∅) > > [More generally I would like to prove that (**) ¬ (0‥n → {0} = > ∅), but the above theorem is the critical one. This is the PO for > initializing all values in an array to zero.] If I inferred correctly from your explanation, you have an INITIALISATION action of form: x :: 0..n > {0} to say that variable "x" is initialised so that it is a total function. Then, lemma (*) comes from the feasibility proof obligation you get from this action. However, as your set is actually a singleton: 0..n > {0} = { 0..n ** {0} } you could use a deterministic action in your INITIALISATION x := 0..n ** {0} And then, you don't have any proof obligation for feasibility. Also, the prover as good support for proving lemmas similar to: 0..n ** {0} : 0..n +> INT > I would have thought that (*) and (**) would be discharged > automatically as part of the background theory. This does not happen > and I can see no way of guiding the proof, other than by induction > on n). > > I have not done an inductive proof before: > > http://wiki.eventb.org/index.php/Induction_proof > > Am I doing this correctly? One introduces the "proof key" ∀s• > s⊆ℕ1 ∧1∈s∧(∀n•n∈s⇒n+1∈s)⇒ℕ1⊆s as an axiom > in a context (this generates a warning because n is already used), > and then instantiate the proof key appropriately. I tried this and > after a long proof tree everything eventually discharges (I can > forward my proof if needed). > > This seems like quite a bit of work to prove (*). > > Your advice would be much appreciated, as usual. From my experience, it is very rare that one needs to make an inductive proof. For most cases, there is good support from the provers (you need to install Atelier B provers, though) and one very seldom needs to go back to the root (which use of induction is, here) to carry proofs. Most of the time, the need to prove some intricate lemma that doesn't work well with the current provers is more a symptom of a problem in a model (unnecessarily complicated) rather than in the prover. But don't forget to take this rule with a grain of salt, as there are exceptions... Hope this helps, Laurent. 
From: <kimmo.varpaaniemi@ko...>  20100323 20:28:22

Hello again, As conjectured by http://wiki.eventb.org/index.php/Induction_proof, the proof key is a _provable_ theorem itself. (It is proven e.g. in the context obsw_C008 in http://deployeprints.ecs.soton.ac.uk/136/1/BepiColombo_Models_v5.0.zip.) Anyway, the proof key is apparently to be used by replacing the universally quantified variable s with a characteristic set of the property of interest. (In the abovementioned context, s is replaced with the constant MAGIC_LENGTHS.) With best regards, Kimmo Varpaaniemi "Jonathan S. Ostroff" [jonathan@...] kirjoitti: > Dear Kimmo: > > Thank you. That is very nice! > > On the issue of doing an inductive proof, does one work as outlined below I.e. assert the proof key as an Axiom and then instantiate appropriately? > > Regards > > Jonathan > > Original Message > From: kimmo.varpaaniemi@... [mailto:kimmo.varpaaniemi@...] > Sent: Tuesday, March 23, 2010 10:35 AM > To: Jonathan S. Ostroff; 'User Rodin Bsharp User' > Subject: Re: [Rodinbsharpuser] Total functions and the empty set > > Hello, > > No induction is needed. One simple interactive proof proceeds as follows: > 1) Contradict the goal. > 2) Apply "remove negation in hypothesis" until there is no negation. > 3) Apply "remove inclusion in hypothesis". > 4) Apply "instantiate universally quantified variables" using (0 .. n) × {0} as the value of the only present universally quantified variable. > > With best regards, > Kimmo Varpaaniemi > > "Jonathan S. Ostroff" [jonathan@...] kirjoitti: > > (*) Given n>0 I would like to prove that: ¬ (0%n {0} ) > > > > [More generally I would like to prove that (**) ¬ (0%n {0} = ), but the above theorem is the critical one. This is the PO for initializing all values in an array to zero.] > > > > I would have thought that (*) and (**) would be discharged automatically as part of the background theory. This does not happen and I can see no way of guiding the proof, other than by induction on n). > > > > I have not done an inductive proof before: > > > > http://wiki.eventb.org/index.php/Induction_proof > > > > Am I doing this correctly? One introduces the "proof key" �s" s 1 '1s'(�n"nsÒn+1s)Ò1 s as an axiom in a context (this generates a warning because n is already used), and then instantiate the proof key appropriately. I tried this and after a long proof tree everything eventually discharges (I can forward my proof if needed). > > > > This seems like quite a bit of work to prove (*). > > > > Your advice would be much appreciated, as usual. > > > > Thanks > > > > Jonathan > > > > > > > > > > > > > >  > > Download Intel® Parallel Studio Eval > > Try the new software tools for yourself. Speed compiling, find bugs > > proactively, and finetune applications for parallel performance. > > See why Intel Parallel Studio got high marks during beta. > > http://p.sf.net/sfu/intelswdev > > _______________________________________________ > > Rodinbsharpuser mailing list > > Rodinbsharpuser@... > > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > > > >  > Download Intel® Parallel Studio Eval > Try the new software tools for yourself. Speed compiling, find bugs > proactively, and finetune applications for parallel performance. > See why Intel Parallel Studio got high marks during beta. > http://p.sf.net/sfu/intelswdev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 
From: Jonathan S. Ostroff <jonathan@yo...>  20100323 18:05:03

Dear Kimmo: Thank you. That is very nice! On the issue of doing an inductive proof, does one work as outlined below. I.e. assert the proof key as an Axiom and then instantiate appropriately? Regards Jonathan Original Message From: kimmo.varpaaniemi@... [mailto:kimmo.varpaaniemi@...] Sent: Tuesday, March 23, 2010 10:35 AM To: Jonathan S. Ostroff; 'User Rodin Bsharp User' Subject: Re: [Rodinbsharpuser] Total functions and the empty set Hello, No induction is needed. One simple interactive proof proceeds as follows: 1) Contradict the goal. 2) Apply "remove negation in hypothesis" until there is no negation. 3) Apply "remove inclusion in hypothesis". 4) Apply "instantiate universally quantified variables" using (0 .. n) × {0} as the value of the only present universally quantified variable. With best regards, Kimmo Varpaaniemi "Jonathan S. Ostroff" [jonathan@...] kirjoitti: > (*) Given n>0 I would like to prove that: ¬ (0%n ’ {0} † ) > > [More generally I would like to prove that (**) ¬ (0%n ’ {0} = ), but the above theorem is the critical one. This is the PO for initializing all values in an array to zero.] > > I would have thought that (*) and (**) would be discharged automatically as part of the background theory. This does not happen and I can see no way of guiding the proof, other than by induction on n). > > I have not done an inductive proof before: > > http://wiki.eventb.org/index.php/Induction_proof > > Am I doing this correctly? One introduces the "proof key" �s" s†1 '1s'(�n"nsÒn+1s)Ò1†s as an axiom in a context (this generates a warning because n is already used), and then instantiate the proof key appropriately. I tried this and after a long proof tree everything eventually discharges (I can forward my proof if needed). > > This seems like quite a bit of work to prove (*). > > Your advice would be much appreciated, as usual. > > Thanks > > Jonathan > > > > > > >  > Download Intel® Parallel Studio Eval > Try the new software tools for yourself. Speed compiling, find bugs > proactively, and finetune applications for parallel performance. > See why Intel Parallel Studio got high marks during beta. > http://p.sf.net/sfu/intelswdev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 
From: <kimmo.varpaaniemi@ko...>  20100323 14:50:12

Hello, No induction is needed. One simple interactive proof proceeds as follows: 1) Contradict the goal. 2) Apply "remove negation in hypothesis" until there is no negation. 3) Apply "remove inclusion in hypothesis". 4) Apply "instantiate universally quantified variables" using (0 .. n) × {0} as the value of the only present universally quantified variable. With best regards, Kimmo Varpaaniemi "Jonathan S. Ostroff" [jonathan@...] kirjoitti: > (*) Given n>0 I would like to prove that: ¬ (0%n {0} ) > > [More generally I would like to prove that (**) ¬ (0%n {0} = ), but the above theorem is the critical one. This is the PO for initializing all values in an array to zero.] > > I would have thought that (*) and (**) would be discharged automatically as part of the background theory. This does not happen and I can see no way of guiding the proof, other than by induction on n). > > I have not done an inductive proof before: > > http://wiki.eventb.org/index.php/Induction_proof > > Am I doing this correctly? One introduces the "proof key" �s" s1 '1s'(�n"nsÒn+1s)Ò1s as an axiom in a context (this generates a warning because n is already used), and then instantiate the proof key appropriately. I tried this and after a long proof tree everything eventually discharges (I can forward my proof if needed). > > This seems like quite a bit of work to prove (*). > > Your advice would be much appreciated, as usual. > > Thanks > > Jonathan > > > > > > >  > Download Intel® Parallel Studio Eval > Try the new software tools for yourself. Speed compiling, find bugs > proactively, and finetune applications for parallel performance. > See why Intel Parallel Studio got high marks during beta. > http://p.sf.net/sfu/intelswdev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 
From: Jonathan S. Ostroff <jonathan@yo...>  20100323 02:34:29

(*) Given n>0 I would like to prove that: ¬ (0‥n → {0} ⊆ ∅) [More generally I would like to prove that (**) ¬ (0‥n → {0} = ∅), but the above theorem is the critical one. This is the PO for initializing all values in an array to zero.] I would have thought that (*) and (**) would be discharged automatically as part of the background theory. This does not happen and I can see no way of guiding the proof, other than by induction on n). I have not done an inductive proof before: http://wiki.eventb.org/index.php/Induction_proof Am I doing this correctly? One introduces the "proof key" ∀s• s⊆ℕ1 ∧1∈s∧(∀n•n∈s⇒n+1∈s)⇒ℕ1⊆s as an axiom in a context (this generates a warning because n is already used), and then instantiate the proof key appropriately. I tried this and after a long proof tree everything eventually discharges (I can forward my proof if needed). This seems like quite a bit of work to prove (*). Your advice would be much appreciated, as usual. Thanks Jonathan 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20100322 08:24:42

BEGIN PGP SIGNED MESSAGE Hash: SHA1 > There is not much information available. Some explanations can be found > here: > > http://wiki.eventb.org/index.php/Rodin_Provers > > I tend to add all automated provers to the autotactic. It slows the > autotactic down, but given the short timeouts that was never a problem > for me. I must add: By "all automated provers" I mean:   Atelier B ML   Atelier B P*   PP *  Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFLpyklczhznXSdWggRAvxNAKCCDIXEBIb9ANC845LuxcGCBuSPvgCfSGVn S+K8PMf72uti0UwGsC76sv8= =M3ld END PGP SIGNATURE 
From: Jonathan S. Ostroff <jonathan@yo...>  20100322 03:05:32

Thank you for this information. Jonathan Original Message From: Matthias Schmalz [mailto:Matthias.Schmalz@...] Sent: Sunday, March 21, 2010 4:02 PM To: Jonathan S. Ostroff Cc: 'User Rodin Bsharp User' Subject: Re: [Rodinbsharpuser] Unique Existence BEGIN PGP SIGNED MESSAGE Hash: SHA1 There is not much information available. Some explanations can be found here: http://wiki.eventb.org/index.php/Rodin_Provers I tend to add all automated provers to the autotactic. It slows the autotactic down, but given the short timeouts that was never a problem for me. Matthias Jonathan S. Ostroff schrieb: > Sometimes p0 will work and pp not. Likewise with all the other provers. > > Are there any guidelines of when to use pp, new pp, ml, etc? > > Presumably this will depend on the main type of proof e.g. arithmetic, > settheoretic etc. > > Jonathan > > > Original Message > From: Matthias Schmalz [mailto:Matthias.Schmalz@...] > Sent: Sunday, March 21, 2010 3:38 PM > To: Thai Son Hoang > Cc: User Rodin Bsharp User > Subject: Re: [Rodinbsharpuser] Unique Existence > >>> By the way, is it fair >>> to conclude, that Rodin cannot prove a theorem (possible a wrong one) >>> when it fails within 10 seconds? > > Rigorously, the answer is no. There are sequents that are proved within > more than 10 seconds. > >>> Or how long does it usually require? > > It depends on what you mean by "usually". > The master student I am supervising has made some experiments (which > will become available within one month) and have found out that most > proofs can be found within 2s. This number does however depend on > several factors: >  processor speed >  amount of available memory >  prover (pp, new pp, ml) >  prover mode (restricted, after lasso, unrestricted) >  benchmark (in our case some models from the EventB wiki) > > So if you want to know the optimal timeout for your case, you will have > to make your own experiments. > > Matthias     Download Intel® Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and finetune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intelswdev _______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser    Download Intel® Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and finetune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intelswdev _______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iEYEARECAAYFAkumezMACgkQczhznXSdWgg30QCeOEXs0Plgv0MCDuqeN52tsqWn ijsAoIaksFIE34oSYnkkc3viOYV2bfn9 =hIhV END PGP SIGNATURE 
From: Thai Son Hoang <htson@in...>  20100321 22:02:01

Dear Johan, On 21032010, at 22:53, Johan Brinch wrote: > > I don't have the Aterier plugin. Is it free to use or only for > institutions? (I'm on easter holiday, not near the institution). > Instructions for installing AtelierB can also be found in the "Help > Welcome" page (which you probably seen (and quickly close that) when you run Rodin the first time). Best, Son  Thai Son Hoang htson@... CNB F105.2 ETH Zentrum Tel: +41 44 632 85 94 Fax: +41 44 632 11 72 
From: Johan Brinch <zerrez@gm...>  20100321 21:53:47

On Sun, Mar 21, 2010 at 18:48, Thai Son Hoang <htson@...> wrote: > Hi Johan, > On 21032010, at 18:42, Johan Brinch wrote: > >> On Wed, Mar 17, 2010 at 17:21, Thai Son Hoang <htson@...> >> wrote: >>> >>> Given the above property, a theorem that you want to prove is that >>> f > [S] : dom(f > S) >>> S >>> (just as you explained the idea about bijection in your mail). This >>> theorem is automatically proved by Rodin 1.2. >> >> Range restriction is very good way to describe it! Thanks! >> However, I'm having some problems proving that my bijection remains a >> bijection when I remove a mapping {x > y} from it. >> >> Right now, I have something like this: >> (F ∖ {x ↦ y}) ▷ (T \ { y })∈ dom((F ∖ {x ↦ y}) ▷ (T \ >> { y })) ⤖ (T \ { y }) >> >> where F is the function, S is dom(F), T is dom(F~) and R is a subset >> of T. >> > > I tried and the above theorem can be proved by AterierB P0 prover, > interactively. By default, P0 is not included in the set of auto > tactics. You can change this via Preferences/EventB/Sequent Prover/ > AutoTactic. After changing the preferences, you can rightclick on > the obligation from the Explorer and choose Retry AutoProver. I don't have the Aterier plugin. Is it free to use or only for institutions? (I'm on easter holiday, not near the institution). >> But Rodin seems to have trouble proving this. By the way, is it fair >> to conclude, that Rodin cannot prove a theorem (possible a wrong one) >> when it fails within 10 seconds? Or how long does it usually require? > > > In automatic mode, depending on your Preferences. For example, for > each AterlierB provers, there is a time out of 3 seconds. > In interactive mode, I think it is set to 30 seconds. I just installed the ProB counter example plugin. Hopefully, that can spot when I'm trying to proof something that isn't true.  Johan Brinch 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20100321 20:02:20

BEGIN PGP SIGNED MESSAGE Hash: SHA1 There is not much information available. Some explanations can be found here: http://wiki.eventb.org/index.php/Rodin_Provers I tend to add all automated provers to the autotactic. It slows the autotactic down, but given the short timeouts that was never a problem for me. Matthias Jonathan S. Ostroff schrieb: > Sometimes p0 will work and pp not. Likewise with all the other provers. > > Are there any guidelines of when to use pp, new pp, ml, etc? > > Presumably this will depend on the main type of proof e.g. arithmetic, > settheoretic etc. > > Jonathan > > > Original Message > From: Matthias Schmalz [mailto:Matthias.Schmalz@...] > Sent: Sunday, March 21, 2010 3:38 PM > To: Thai Son Hoang > Cc: User Rodin Bsharp User > Subject: Re: [Rodinbsharpuser] Unique Existence > >>> By the way, is it fair >>> to conclude, that Rodin cannot prove a theorem (possible a wrong one) >>> when it fails within 10 seconds? > > Rigorously, the answer is no. There are sequents that are proved within > more than 10 seconds. > >>> Or how long does it usually require? > > It depends on what you mean by "usually". > The master student I am supervising has made some experiments (which > will become available within one month) and have found out that most > proofs can be found within 2s. This number does however depend on > several factors: >  processor speed >  amount of available memory >  prover (pp, new pp, ml) >  prover mode (restricted, after lasso, unrestricted) >  benchmark (in our case some models from the EventB wiki) > > So if you want to know the optimal timeout for your case, you will have > to make your own experiments. > > Matthias     Download Intel® Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and finetune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intelswdev _______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser   Download Intel® Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and finetune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intelswdev _______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iEYEARECAAYFAkumezMACgkQczhznXSdWgg30QCeOEXs0Plgv0MCDuqeN52tsqWn ijsAoIaksFIE34oSYnkkc3viOYV2bfn9 =hIhV END PGP SIGNATURE 
From: Jonathan S. Ostroff <jonathan@yo...>  20100321 19:55:49

Sometimes p0 will work and pp not. Likewise with all the other provers. Are there any guidelines of when to use pp, new pp, ml, etc? Presumably this will depend on the main type of proof e.g. arithmetic, settheoretic etc. Jonathan Original Message From: Matthias Schmalz [mailto:Matthias.Schmalz@...] Sent: Sunday, March 21, 2010 3:38 PM To: Thai Son Hoang Cc: User Rodin Bsharp User Subject: Re: [Rodinbsharpuser] Unique Existence BEGIN PGP SIGNED MESSAGE Hash: SHA1 >> By the way, is it fair >> to conclude, that Rodin cannot prove a theorem (possible a wrong one) >> when it fails within 10 seconds? Rigorously, the answer is no. There are sequents that are proved within more than 10 seconds. >> Or how long does it usually require? It depends on what you mean by "usually". The master student I am supervising has made some experiments (which will become available within one month) and have found out that most proofs can be found within 2s. This number does however depend on several factors:   processor speed   amount of available memory   prover (pp, new pp, ml)   prover mode (restricted, after lasso, unrestricted)   benchmark (in our case some models from the EventB wiki) So if you want to know the optimal timeout for your case, you will have to make your own experiments.  Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iEYEARECAAYFAkumdYsACgkQczhznXSdWgiSsQCgoZf4ujktbGLHosou07LeWM+m BJ4AoIaHYPM7DN+tRJ9wPfs7UcCTOfKU =Dr6D END PGP SIGNATURE   Download Intel® Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and finetune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intelswdev _______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20100321 19:38:36

BEGIN PGP SIGNED MESSAGE Hash: SHA1 >> By the way, is it fair >> to conclude, that Rodin cannot prove a theorem (possible a wrong one) >> when it fails within 10 seconds? Rigorously, the answer is no. There are sequents that are proved within more than 10 seconds. >> Or how long does it usually require? It depends on what you mean by "usually". The master student I am supervising has made some experiments (which will become available within one month) and have found out that most proofs can be found within 2s. This number does however depend on several factors:   processor speed   amount of available memory   prover (pp, new pp, ml)   prover mode (restricted, after lasso, unrestricted)   benchmark (in our case some models from the EventB wiki) So if you want to know the optimal timeout for your case, you will have to make your own experiments.  Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iEYEARECAAYFAkumdYsACgkQczhznXSdWgiSsQCgoZf4ujktbGLHosou07LeWM+m BJ4AoIaHYPM7DN+tRJ9wPfs7UcCTOfKU =Dr6D END PGP SIGNATURE 
From: Thai Son Hoang <htson@in...>  20100321 18:48:42

Hi Johan, On 21032010, at 18:42, Johan Brinch wrote: > On Wed, Mar 17, 2010 at 17:21, Thai Son Hoang <htson@...> > wrote: >> >> Given the above property, a theorem that you want to prove is that >> f > [S] : dom(f > S) >>> S >> (just as you explained the idea about bijection in your mail). This >> theorem is automatically proved by Rodin 1.2. > > Range restriction is very good way to describe it! Thanks! > However, I'm having some problems proving that my bijection remains a > bijection when I remove a mapping {x > y} from it. > > Right now, I have something like this: > (F ∖ {x ↦ y}) ▷ (T \ { y })∈ dom((F ∖ {x ↦ y}) ▷ (T \ > { y })) ⤖ (T \ { y }) > > where F is the function, S is dom(F), T is dom(F~) and R is a subset > of T. > I tried and the above theorem can be proved by AterierB P0 prover, interactively. By default, P0 is not included in the set of auto tactics. You can change this via Preferences/EventB/Sequent Prover/ AutoTactic. After changing the preferences, you can rightclick on the obligation from the Explorer and choose Retry AutoProver. > But Rodin seems to have trouble proving this. By the way, is it fair > to conclude, that Rodin cannot prove a theorem (possible a wrong one) > when it fails within 10 seconds? Or how long does it usually require? In automatic mode, depending on your Preferences. For example, for each AterlierB provers, there is a time out of 3 seconds. In interactive mode, I think it is set to 30 seconds. Best, Son  Thai Son Hoang htson@... CNB F105.2 ETH Zentrum Tel: +41 44 632 85 94 Fax: +41 44 632 11 72 
From: Johan Brinch <zerrez@gm...>  20100321 17:50:23

On Wed, Mar 17, 2010 at 17:21, Thai Son Hoang <htson@...> wrote: > > Given the above property, a theorem that you want to prove is that > f > [S] : dom(f > S) >>> S > (just as you explained the idea about bijection in your mail). This > theorem is automatically proved by Rodin 1.2. Range restriction is very good way to describe it! Thanks! However, I'm having some problems proving that my bijection remains a bijection when I remove a mapping {x > y} from it. Right now, I have something like this: (F ∖ {x ↦ y}) ▷ (T \ { y })∈ dom((F ∖ {x ↦ y}) ▷ (T \ { y })) ⤖ (T \ { y }) where F is the function, S is dom(F), T is dom(F~) and R is a subset of T. But Rodin seems to have trouble proving this. By the way, is it fair to conclude, that Rodin cannot prove a theorem (possible a wrong one) when it fails within 10 seconds? Or how long does it usually require?  Johan Brinch 
From: Jonathan S. Ostroff <jonathan@yo...>  20100318 10:36:48

Thank you. Jonathan Original Message From: Carine Pascal [mailto:carine.pascal@...] Sent: Thursday, March 18, 2010 4:31 AM To: Jonathan S. Ostroff Cc: rodinbsharpuser@... Subject: Re: [Rodinbsharpuser] Automatic tactics Dear Jonathan, Nicolas has recently implemented a new feature called "Proof replay on undischarged POs", which provides a convenient way to manually replay selected undischarged POs. See the related user documentation on the wiki: http://wiki.eventb.org/index.php/Proof_Obligation_Commands. This new command will be available in the release 1.3 of the Rodin platform. The changes have already been committed and you can use it in "development mode". Regards, Carine. Jonathan S. Ostroff a écrit : > I have noticed the following: Suppose we add an element to a model (say an > event) and all the proof obligations are automatically discharged. Then > change the event and now some of the proofs may no longer work. Reverse the > changes to what they were originally  invoke "retry auto provers" does > not work; the proof may now have to be done manually even though originally > the very same proof was done automatically. > > Is there some way to run all the tactics and provers as was done initially? > > Thanks > > Jonathan > > >   > Download Intel® Parallel Studio Eval > Try the new software tools for yourself. Speed compiling, find bugs > proactively, and finetune applications for parallel performance. > See why Intel Parallel Studio got high marks during beta. > http://p.sf.net/sfu/intelswdev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser >   > Orange vous informe que cet email a ete controle par l'antivirus mail. > Aucun virus connu a ce jour par nos services n'a ete detecte. > > >   Carine PASCAL Tél. : (+33)(0)4 42 90 41 24 Chef de Projet SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Carine Pascal <carine.pascal@sy...>  20100318 08:27:56

Dear Jonathan, Nicolas has recently implemented a new feature called "Proof replay on undischarged POs", which provides a convenient way to manually replay selected undischarged POs. See the related user documentation on the wiki: http://wiki.eventb.org/index.php/Proof_Obligation_Commands. This new command will be available in the release 1.3 of the Rodin platform. The changes have already been committed and you can use it in "development mode". Regards, Carine. Jonathan S. Ostroff a écrit : > I have noticed the following: Suppose we add an element to a model (say an > event) and all the proof obligations are automatically discharged. Then > change the event and now some of the proofs may no longer work. Reverse the > changes to what they were originally  invoke "retry auto provers" does > not work; the proof may now have to be done manually even though originally > the very same proof was done automatically. > > Is there some way to run all the tactics and provers as was done initially? > > Thanks > > Jonathan > > >  > Download Intel® Parallel Studio Eval > Try the new software tools for yourself. Speed compiling, find bugs > proactively, and finetune applications for parallel performance. > See why Intel Parallel Studio got high marks during beta. > http://p.sf.net/sfu/intelswdev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser >  > Orange vous informe que cet email a ete controle par l'antivirus mail. > Aucun virus connu a ce jour par nos services n'a ete detecte. > > >   Carine PASCAL Tél. : (+33)(0)4 42 90 41 24 Chef de Projet SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  