## rodin-b-sharp-user — Help and discussion among users of the Rodin platform

You can subscribe to this list here.

 2009 2010 2011 2012 2013 2014 2015 Jan (10) Feb (57) Mar (16) Apr (15) May (31) Jun (17) Jul (10) Aug (18) Sep (20) Oct (31) Nov (6) Dec (7) Jan (21) Feb (40) Mar (35) Apr (14) May (21) Jun (6) Jul (33) Aug (97) Sep (55) Oct (37) Nov (35) Dec (23) Jan (9) Feb (9) Mar (57) Apr (21) May (4) Jun (6) Jul (12) Aug (13) Sep (18) Oct (9) Nov (11) Dec (3) Jan (45) Feb (18) Mar (18) Apr (14) May (11) Jun (14) Jul (3) Aug (6) Sep (2) Oct (16) Nov (31) Dec (10) Jan (29) Feb (7) Mar (21) Apr (52) May (32) Jun (8) Jul (9) Aug (9) Sep (7) Oct (22) Nov (12) Dec Jan (36) Feb (11) Mar (11) Apr (18) May (8) Jun (19) Jul (15) Aug (22) Sep (11) Oct (8) Nov (4) Dec (14) Jan (2) Feb (4) Mar (10) Apr (7) May (11) Jun (17) Jul (5) Aug (7) Sep (23) Oct Nov Dec
S M T W T F S

1

2

3
(1)
4

5

6

7

8
(10)
9

10

11

12

13

14

15
(1)
16

17
(1)
18

19

20
(1)
21

22

23

24
(1)
25
(2)
26
(1)
27

28

29

Showing 18 results of 18

 Re: [Rodin-b-sharp-user] Rodin/ProB/Initialization From: Michael Leuschel - 2012-02-26 06:40:04 Attachments: Message as HTML ```Hi Jonathan, On 26 Feb 2012, at 03:39, Jonathan S. Ostroff wrote: > > I am attaching my model of a supermarket (taken from Ken Robinson's book) > but with some revisions. I see now: the issue is that you have three variables being initialized non-determinisically: > shelf :: ORDER > || > price :: PRODUCT --> NAT > || > cash :: NAT Before finding another solution for price, ProB will first enumerate all solutions to cash. So, increasing MAXINT won't help; actually to the contrary as there will be more solutions for cash. If you set MAXINT to 3 and increasing the number of initializations computed to 50 will give you more interesting solutions for price. If you also want interesting solutions to shelf, you need to set the number of initializations even higher. For example, setting the number of initializations to 500 will give you as 500th solution the values below in the screenshots below. A future version of ProB may support a more random enumeration algorithm (the difficulty is doing this efficiently and ensuring completeness for model checking). > The problem is that > in some cases it makes the proofs harder and also non-deterministic You can also create a refinement of your machine just for animation purposes: - in the refinement you can alter the INITIALISATION or give names to the products You could also add a new event: MY_INITIALISATION which gives more concrete values to price, cash and shelf. This should not alter provability of the rest of the machine (you will have to prove the event itself correct, though.) > I have not yet tried exporting to ProB. Presumably I must first install ProB > to do this? No, not for exporting ;-) Later to manipulate the .eventb file, yes. You should download the stand-alone version of ProB from http://www.stups.uni-duesseldorf.de/ProB/index.php5/Download Greetings, Michael ```
 Re: [Rodin-b-sharp-user] Rodin/ProB/Initialization From: Michael Leuschel - 2012-02-25 08:26:51 ```Hi Jonathan, On 20 Feb 2012, at 05:53, Jonathan S. Ostroff wrote: > I am trying out the latest version of ProB with Rodin, and I forget how to > change initialization from the default to ones of my choice. > > Suppose we have some variable whose type is PRODUCT --> NAT (i.e. a bag > really). The default generated by ProB is {PRODUCT1 |-> 0, PRODUCT2 |->0} as > the initial value. I would like to have, say, {PRODUCT1 |-> 5, PRODUCT2 > |->3}. There are several solutions. It would be good if you send me the model so that I can better help you. - One solution is to change the initialization and write x:= {PRODUCT1 |-> 5, PRODUCT |-> 3}. - Another solution is to export your model to ProB Classic and then use the command "Animate -> Execute Operation …". Here you can provide additional predicates/values for the various applicable operations/events. (I have just added a tutorial page for exporting to ProB Classic here http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_Rodin_Exporting). - Finally, ProB should enumerate possible solutions for the initialization. The number of initializations computed can be controlled by a preference. You need to set the value high enough to see your desired option appear. However, this may be impractical due to the high number of possible initializations and due to the way ProB currently enumerates these solutions. The tutorial page is maybe of help to you: http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_Setup_Phases. > > A right click on the initial event does provides a show dialog option, but I > cannot see how to change the value of the NAT. You cannot change the value of NAT. However, in case ProB has to find solutions for variables/constants of type NAT and in case the value cannot be inferred by other means, ProB will (usually) enumerate between 0 and MAXINT. You can set the value of MAXINT in the ProB preferences dialog. > Also, can I change PRODUCT1 > To something simpler like p1? You can do so by changing PRODUCT into an enumerated set in the context. You can then give the elements of PRODUCT whatever names you want. > > Is there more documentation for ProB under Rodin? There is a bit of information here: http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial In particular: - http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_Rodin_First_Step - http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_Rodin_Parameters However, I just realized that for some reason the pictures have disappeared from the Wiki. We will investigate. Greetings, Michael ```
 Re: [Rodin-b-sharp-user] Rodin/ProB/Initialization From: Michael Leuschel - 2012-02-25 08:26:43 Attachments: Message as HTML ```On 25 Feb 2012, at 08:36, Michael Leuschel wrote: > It would be good if you send me the model so that I can better help you. > > - One solution is to change the initialization and write x:= {PRODUCT1 |-> 5, PRODUCT |-> 3}. > - Another solution is to export your model to ProB Classic and then use the command "Animate -> Execute Operation …". I just realized (just after sending the previous email) that the above will require that you first change PRODUCT into an enumerated set: this way you can talk about individual elements. Otherwise you will need to produce more convoluted initialization statements ( x: ( x: PRODUCT -->> {3,5}) or x :: PRODUCT -->> {3,5} for example) or predicates. If you send me the model, I can send you a solution. Greetings, Michael```
 [Rodin-b-sharp-user] Rodin Tutorials - Isabelle From: Matthias Schmalz - 2012-02-24 13:02:47 ```This mail concerns the Isabelle tutorial of the Rodin workshop on Monday. Unfortunately, I do not have the email addresses of all attendees. Please forward it to people who might attend the tutorial. Sorry for the inconvenience if you don't attend. Dear all, on Monday, I plan to give two tutorials on my Isabelle plug-in: a "hands-on" tutorial and a "listen and watch" tutorial. In the hands-on tutorial, you will use my toolchain to improve the automated theorem proving capabilities of Rodin. For this tutorial, some familiarity with Isabelle would be useful; you don't have to be a hardcore professional, but you should not use Isabelle for the first time. If you plan to attend the hands-on tutorial, it is important that you install the required software beforehand. The installation is not difficult, but it takes some time and you have to download hundreds of megabytes. Instructions below. Sorry for the late notice. In the "listen and watch" tutorial, I will develop some of these theorem prover improvements by myself and you will listen and watch. I will proceed slowly and explain every step. You can also point out your favorite weakness of Rodin's automated theorem provers and I will try to fix it in an online fashion. (I may however fail to do so :-)) I am looking forward to see you on Monday! Matthias P.s.: Installation instructions for the hands-on tutorial: - Download and unzip Rodin 2.4, start it at least once. http://sourceforge.net/projects/rodin-b-sharp/ Make sure to satisfy the requirements mentioned in the release notes: http://wiki.event-b.org/index.php/Rodin_Platform_2.4_Release_Notes#Requirements_-_Compatibility - Use Rodin's installation facility to install my plug-in. Detailed instructions on: http://wiki.event-b.org/index.php/Export_to_Isabelle Note that we will use version 0.6.x during the tutorial, which I will release tomorrow. Nevertheless, it pays off to install 0.5.0, because an update to 0.6.x from 0.5.0 is much faster than a fresh installation. - Download and unpack isabelle2011-1: http://isabelle.in.tum.de/download.html *Make sure that you have all the softare that is listed in the requirements section of your system.* - Once, version 0.6.x of Isabelle for Rodin has been released, you may want to install it according to the instructions (to be announced). But we can also do that during the tutorial. ```
 [Rodin-b-sharp-user] Rodin/ProB/Initialization From: Jonathan S. Ostroff - 2012-02-20 04:54:07 ```I am trying out the latest version of ProB with Rodin, and I forget how to change initialization from the default to ones of my choice. Suppose we have some variable whose type is PRODUCT --> NAT (i.e. a bag really). The default generated by ProB is {PRODUCT1 |-> 0, PRODUCT2 |->0} as the initial value. I would like to have, say, {PRODUCT1 |-> 5, PRODUCT2 |->3}. A right click on the initial event does provides a show dialog option, but I cannot see how to change the value of the NAT. Also, can I change PRODUCT1 To something simpler like p1? Is there more documentation for ProB under Rodin? Thank you in advance, Jonathan ```
 [Rodin-b-sharp-user] [Rodin announce] SMT Solvers Plug-in v0.8.0 released From: Yoann Guyot - 2012-02-17 15:22:29 ```Dear Rodin Users, I am delighted to announce the release of the SMT Solvers Plug-in for Rodin v2.4. It can be installed from the main Rodin update site : http://rodin-b-sharp.sourceforge.net/updates. You will find all needed instructions on its dedicated page of the Event-B wiki : http://wiki.event-b.org/index.php/SMT_Plug-in. Best regards, -- ------------------------------------------------------------------------ Yoann GUYOT Tél. : (+33)(0)1 76 60 40 28 Ingénieur Modélisation et Preuves SYSTEREL ------------------------------------------------------------------------ Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr ------------------------------------------------------------------------ ```
 [Rodin-b-sharp-user] Rodin Handbook: Interest in Print Edition From: Michael Jastram - 2012-02-15 09:22:01 ```Dear all, Would you buy a print copy of the Rodin Handbook? Please tell us via [1]. You may be aware that the Rodin Handbook project [2] is soon coming to an end. Currently, is is only available digitally. If there is enough interest, we could also make the handbook available via a print-on-demand service (probably Amazon). But we would only do this if there is enough demand. We are kindly asking you to answer a short questionnaire (1 mandatory and 3 optional questions) to help us estimate demand [1]. Thank you for taking your time! Best wishes, - The Rodin Handbook Team [1] http://kwiksurveys.com?s=LJDEOJ_58d45059 [2] http://handbook.event-b.org/ -- Michael Jastram (http://www.jastram.de, +49 (162) 274 83 94) Geschäftsführer, Formal Mind GmbH (http://formalmind.com) Wissenschaftler, Heinrich Heine Universität Düsseldorf (http://www.stups.uni-duesseldorf.de) 1. Vorsitzender, rheinjug e.V. (http://www.rheinjug.de) ```
 Re: [Rodin-b-sharp-user] Ongoing problems with card From: - 2012-02-08 14:25:15 ```Hello, I've got used to handle cardinalities in interactive proofs but still thought that almost any "simple" property could be made auto-provable by means of some sequence of auto-provable theorems. To my disappointment, in the considered case I only managed to create the context that is displayed below in Camille format. All theorems except thm16 get discharged automatically. Manual discharging of thm16 is easy though requires backtracking in order to cancel an "unrequested rewriting" of a cardinality of a union. With best regards, Kimmo Varpaaniemi context C constants xs x sets X axioms @axm1 finite(X) @axm2 xs ⊆ X theorem @thm1 finite(X ∖ X) theorem @thm2 card(X ∖ X) = 0 theorem @thm3 (x ∈ xs) ⇒ (finite({x})) theorem @thm4 (x ∈ xs) ⇒ (card({x}) = 1) theorem @thm5 (x ∈ xs) ⇒ (finite(xs)) theorem @thm6 (x ∈ xs) ⇒ (finite(xs ∖ {x})) theorem @thm7 (x ∈ xs) ⇒ (finite((xs ∖ {x}) ∪ {x})) theorem @thm8 (x ∈ xs) ⇒ (finite((xs ∖ {x}) ∩ {x})) theorem @thm9 (x ∈ xs) ⇒ ((xs ∖ {x}) ∩ {x} = X ∖ X) theorem @thm10 (x ∈ xs) ⇒ (card((xs ∖ {x}) ∩ {x}) = card(X ∖ X)) theorem @thm11 (x ∈ xs) ⇒ (card((xs ∖ {x}) ∩ {x}) = 0) theorem @thm12 (x ∈ xs) ⇒ (card((xs ∖ {x}) ∪ {x}) = card(xs ∖ {x}) + card({x}) − card((xs ∖ {x}) ∩ {x})) theorem @thm13 (x ∈ xs) ⇒ (card((xs ∖ {x}) ∪ {x}) = card(xs ∖ {x}) + 1) theorem @thm14 (x ∈ xs) ⇒ (card(xs ∖ {x}) = card((xs ∖ {x}) ∪ {x}) − 1) theorem @thm15 (x ∈ xs) ⇒ ((xs ∖ {x}) ∪ {x} = xs) theorem @thm16 (x ∈ xs) ⇒ (card((xs ∖ {x}) ∪ {x}) = card(xs)) theorem @thm17 (x ∈ xs) ⇒ (card(xs ∖ {x}) = card(xs) − 1) end Ken Robinson [kenr@...] kirjoitti: > Dear Son, Pierre, Matthias and Rodin Users, > > Thank you Son and Pierre and Matthias for your solutions. (Son's corrected by Matthias) > > I want to try to make it clear here what I am driving at. > > I have previously discharged the PO that I mentioned in my initial email, however the proof was not contained in the project I was reviewing and "cleaning up". > > I spent a bit of time on producing a proof and then decided that the experience was painful and undesirable. Either than or I was an idiot. > > Both Son/Matthias and Pierre's solutions and also their experience does not incline me to change my mind. Don't get me wrong: they are nice proofs, but it is important to keep an eye on "what is being proved". > > I don't use "axiom" lightly and I am not suggesting a particular axiom or a set of axioms. > > What I am saying is that when you are trying to convince people that Event-B is an important tool for modelling designs, they are far from impressed to find ---and remember that they will probably find this very early in their use of Rodin-- that > > x : xs => card(xs \ {x}) = card(xs) - 1 > > is not auto proved, or at least easily proved to be a big put off. > > There is something "axiomatic" about that assertion. > > If that isn't easily proved then what about the other POs coming from the more complex requirements that they want to model? > > Luckily, many of the "more complex" POs are discharged more easily than the above! > > Unless they involve "card"! :-) > > I sent off the earlier email to see what sort of reaction I would get. > > I've just seen Matthias's later email on using Isabelle. > > That probably is comforting. > > Further note: one of the things that makes life difficult at the moment is that it is not always clear why something can's be discharged. > > OK, silly statement: that is always true about proof, but it is a special case when the lemma is "obviously true". > > My whole concern here is with "credibility". > > Thanks, > > Ken > > On 08/02/2012, at 22:33 PM, Hoang, Thai Son wrote: > > > Dear Ken, > > I just realised that I did not push my last reply to the mailing list. > > I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. > > !n,s.s <: X => card(s) = n <=> (#f.f : 1..n >->> s) > > I've been down this road before with cardinality. > > Cheers, > > Son > > > > On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: > > > >> Hi Ken, > >> On 8 Feb 2012, at 11:13, Ken Robinson wrote: > >> > >>> Hello everyone, > >>> > >>> I fear this email will demonstrate that I am an idiot, but here goes. > >>> > >> > >> You are certainly not. > >> > >>> My problems with card are long standing and persistent. > >>> > >> > >> It is the same feeling for me. > >> > >>> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. > >>> > >> > >> I assume that you they are undischarged with the old Rodin as well. > >> > >>> As usual I am having trouble with card. > >>> > >>> For example: > >>> > >>> SETS > >>> X > >>> finite X > >>> > >>> xs <: X > >>> > >>> Prove > >>> x : xs => card(xs \ {x}) = card(xs) - 1 > >>> > >>> So far this has resisted all my efforts to discharge it. > >>> > >>> and I've been this way before. > >>> > >>> I hope, and will be grateful, if someone can demonstrate a proof. > >>> > >>> And I'm hoping it will show that I am an idiot. > >>> > >>> If not then I think this is a worry, as to many this poses a serious credibility problem for Event-B. > >>> > >>> Without knowing the Event-B axioms, this would appear to be axiomatic to most people. > >>> > >>> I will be grateful for any resolution of my ineptitude. > >>> > >> > >> You are probably want to the following feature request which has not been implemented. > >> http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 > >> But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. > >> http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 > >> Cheers, > >> Son > > > > -- > > Thai Son Hoang > > CNB F105.2 > > ETH Zentrum, Zurich, Switzerland > > Tel: +41 44 632 85 94 > > Fax: +41 44 632 11 72 > > ------------------------------------------------------------------------------ > > Keep Your Developer Skills Current with LearnDevNow! > > The most comprehensive online learning library for Microsoft developers > > is just \$99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3, > > Metro Style Apps, more. Free future releases when you subscribe now! > > http://p.sf.net/sfu/learndevnow-d2d_______________________________________________ > > Rodin-b-sharp-user mailing list > > Rodin-b-sharp-user@... > > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > > > ------------------------------------------------------------------------------ > Keep Your Developer Skills Current with LearnDevNow! > The most comprehensive online learning library for Microsoft developers > is just \$99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3, > Metro Style Apps, more. Free future releases when you subscribe now! > http://p.sf.net/sfu/learndevnow-d2d > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > ```
 Re: [Rodin-b-sharp-user] Ongoing problems with card From: Pierre Casteran - 2012-02-08 14:00:07 ```Dear all, If the problem is to convince people of trusting a development made with Rodin, what you need is a possibility of showing explicitely which axioms were used in the proofs, just with a tool which can enumerate all non-proved statement in the proofs. It would be also very useful to have some way for the users to contribute some depository with theorems they think to be useful to other people (for instance a lot of theorems like Ken's, on cardinality). In combination with search tools (like "find all theorems that contain card and set-difference"), it would easier to finalize proofs. I use mainly the Coq proof assistant, but I think that Isabelle contains these tools too. About automation: tools like why3 are only proof obligation genaerators, which can send to a lot of automatic or interactive theorem provers. I would be very interested by such a tool for [Event-]B that would be a generator of POs according to the mathematical model of contexts and machines, but letting other tools doing the proofs or helping the user in difficult steps. Please notice that I am not a big user of Rodin, and that my wish list contains perhaps some already existing items. In this case, I'm sorry for the noise. Best, Pierre Le 08/02/2012 14:16, Ken Robinson a écrit : > Dear Son, Pierre, Matthias and Rodin Users, > > Thank you Son and Pierre and Matthias for your solutions. (Son's corrected by Matthias) > > I want to try to make it clear here what I am driving at. > > I have previously discharged the PO that I mentioned in my initial email, however the proof was not contained in the project I was reviewing and "cleaning up". > > I spent a bit of time on producing a proof and then decided that the experience was painful and undesirable. Either than or I was an idiot. > > Both Son/Matthias and Pierre's solutions and also their experience does not incline me to change my mind. Don't get me wrong: they are nice proofs, but it is important to keep an eye on "what is being proved". > > I don't use "axiom" lightly and I am not suggesting a particular axiom or a set of axioms. > > What I am saying is that when you are trying to convince people that Event-B is an important tool for modelling designs, they are far from impressed to find ---and remember that they will probably find this very early in their use of Rodin-- that > > x : xs => card(xs \ {x}) = card(xs) - 1 > > is not auto proved, or at least easily proved to be a big put off. > > There is something "axiomatic" about that assertion. > > If that isn't easily proved then what about the other POs coming from the more complex requirements that they want to model? > > Luckily, many of the "more complex" POs are discharged more easily than the above! > > Unless they involve "card"! :-) > > I sent off the earlier email to see what sort of reaction I would get. > > I've just seen Matthias's later email on using Isabelle. > > That probably is comforting. > > Further note: one of the things that makes life difficult at the moment is that it is not always clear why something can's be discharged. > > OK, silly statement: that is always true about proof, but it is a special case when the lemma is "obviously true". > > My whole concern here is with "credibility". > > Thanks, > > Ken > > On 08/02/2012, at 22:33 PM, Hoang, Thai Son wrote: > >> Dear Ken, >> I just realised that I did not push my last reply to the mailing list. >> I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. >> !n,s.s<: X => card(s) = n<=> (#f.f : 1..n>->> s) >> I've been down this road before with cardinality. >> Cheers, >> Son >> >> On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: >> >>> Hi Ken, >>> On 8 Feb 2012, at 11:13, Ken Robinson wrote: >>> >>>> Hello everyone, >>>> >>>> I fear this email will demonstrate that I am an idiot, but here goes. >>>> >>> >>> You are certainly not. >>> >>>> My problems with card are long standing and persistent. >>>> >>> >>> It is the same feeling for me. >>> >>>> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >>>> >>> >>> I assume that you they are undischarged with the old Rodin as well. >>> >>>> As usual I am having trouble with card. >>>> >>>> For example: >>>> >>>> SETS >>>> X >>>> finite X >>>> >>>> xs<: X >>>> >>>> Prove >>>> x : xs => card(xs \ {x}) = card(xs) - 1 >>>> >>>> So far this has resisted all my efforts to discharge it. >>>> >>>> and I've been this way before. >>>> >>>> I hope, and will be grateful, if someone can demonstrate a proof. >>>> >>>> And I'm hoping it will show that I am an idiot. >>>> >>>> If not then I think this is a worry, as to many this poses a serious credibility problem for Event-B. >>>> >>>> Without knowing the Event-B axioms, this would appear to be axiomatic to most people. >>>> >>>> I will be grateful for any resolution of my ineptitude. >>>> >>> >>> You are probably want to the following feature request which has not been implemented. >>> http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 >>> But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. >>> http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 >>> Cheers, >>> Son >> >> -- >> Thai Son Hoang >> CNB F105.2 >> ETH Zentrum, Zurich, Switzerland >> Tel: +41 44 632 85 94 >> Fax: +41 44 632 11 72 >> ------------------------------------------------------------------------------ >> Keep Your Developer Skills Current with LearnDevNow! >> The most comprehensive online learning library for Microsoft developers >> is just \$99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3, >> Metro Style Apps, more. Free future releases when you subscribe now! >> http://p.sf.net/sfu/learndevnow-d2d_______________________________________________ >> Rodin-b-sharp-user mailing list >> Rodin-b-sharp-user@... >> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > ```
 Re: [Rodin-b-sharp-user] Ongoing problems with card From: Ken Robinson - 2012-02-08 13:14:01 ```Dear Son, Pierre, Matthias and Rodin Users, Thank you Son and Pierre and Matthias for your solutions. (Son's corrected by Matthias) I want to try to make it clear here what I am driving at. I have previously discharged the PO that I mentioned in my initial email, however the proof was not contained in the project I was reviewing and "cleaning up". I spent a bit of time on producing a proof and then decided that the experience was painful and undesirable. Either than or I was an idiot. Both Son/Matthias and Pierre's solutions and also their experience does not incline me to change my mind. Don't get me wrong: they are nice proofs, but it is important to keep an eye on "what is being proved". I don't use "axiom" lightly and I am not suggesting a particular axiom or a set of axioms. What I am saying is that when you are trying to convince people that Event-B is an important tool for modelling designs, they are far from impressed to find ---and remember that they will probably find this very early in their use of Rodin-- that x : xs => card(xs \ {x}) = card(xs) - 1 is not auto proved, or at least easily proved to be a big put off. There is something "axiomatic" about that assertion. If that isn't easily proved then what about the other POs coming from the more complex requirements that they want to model? Luckily, many of the "more complex" POs are discharged more easily than the above! Unless they involve "card"! :-) I sent off the earlier email to see what sort of reaction I would get. I've just seen Matthias's later email on using Isabelle. That probably is comforting. Further note: one of the things that makes life difficult at the moment is that it is not always clear why something can's be discharged. OK, silly statement: that is always true about proof, but it is a special case when the lemma is "obviously true". My whole concern here is with "credibility". Thanks, Ken On 08/02/2012, at 22:33 PM, Hoang, Thai Son wrote: > Dear Ken, > I just realised that I did not push my last reply to the mailing list. > I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. > !n,s.s <: X => card(s) = n <=> (#f.f : 1..n >->> s) > I've been down this road before with cardinality. > Cheers, > Son > > On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: > >> Hi Ken, >> On 8 Feb 2012, at 11:13, Ken Robinson wrote: >> >>> Hello everyone, >>> >>> I fear this email will demonstrate that I am an idiot, but here goes. >>> >> >> You are certainly not. >> >>> My problems with card are long standing and persistent. >>> >> >> It is the same feeling for me. >> >>> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >>> >> >> I assume that you they are undischarged with the old Rodin as well. >> >>> As usual I am having trouble with card. >>> >>> For example: >>> >>> SETS >>> X >>> finite X >>> >>> xs <: X >>> >>> Prove >>> x : xs => card(xs \ {x}) = card(xs) - 1 >>> >>> So far this has resisted all my efforts to discharge it. >>> >>> and I've been this way before. >>> >>> I hope, and will be grateful, if someone can demonstrate a proof. >>> >>> And I'm hoping it will show that I am an idiot. >>> >>> If not then I think this is a worry, as to many this poses a serious credibility problem for Event-B. >>> >>> Without knowing the Event-B axioms, this would appear to be axiomatic to most people. >>> >>> I will be grateful for any resolution of my ineptitude. >>> >> >> You are probably want to the following feature request which has not been implemented. >> http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 >> But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. >> http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 >> Cheers, >> Son > > -- > Thai Son Hoang > CNB F105.2 > ETH Zentrum, Zurich, Switzerland > Tel: +41 44 632 85 94 > Fax: +41 44 632 11 72 > ------------------------------------------------------------------------------ > Keep Your Developer Skills Current with LearnDevNow! > The most comprehensive online learning library for Microsoft developers > is just \$99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3, > Metro Style Apps, more. Free future releases when you subscribe now! > http://p.sf.net/sfu/learndevnow-d2d_______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```
 Re: [Rodin-b-sharp-user] Ongoing problems with card From: Hoang, Thai Son - 2012-02-08 13:00:40 ``` Hi Pierre, You are right. It is very nice proof. The reason why I think of the axiom is that in some other example, I also need that. Cheers, Son On 8 Feb 2012, at 12:39, Pierre Casteran wrote: > Hi, Son, > > Did you need to assert a new axiom ? > In the following project, I proved Kens thm withous axioms, but a lot of effort (in changeme context) > -- Thai Son Hoang CNB F105.2 ETH Zentrum, Zurich, Switzerland Tel: +41 44 632 85 94 Fax: +41 44 632 11 72 ```
 Re: [Rodin-b-sharp-user] Ongoing problems with card From: Matthias Schmalz - 2012-02-08 12:49:34 ```Hi again, I just want to add that my Isabelle/HOL backend discharges Ken's theorem automatically. I regret that the plug-in is not yet ready for a broader audience. I hope to release something by the end of the month. -Matthias Am 08.02.2012 13:32, schrieb Matthias Schmalz: > Hi, > > just to keep that clear, the formula > > !n,s. s<: X => card(s) = n<=> (#f.f : 1..n>->> s) > > is not valid. Choose s as the empty set and n as -1. > Instead, it should be > > !n, s. s<: X& n : NAT => card(s) = n<=> (#f. f : 1..n>->> s). > > Ken, you are not an idiot. Reasoning about card is difficult, also in > other theorem provers. > > Best, > Matthias > > > Am 08.02.2012 12:33, schrieb Hoang, Thai Son: >> Dear Ken, >> I just realised that I did not push my last reply to the mailing list. >> I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. >> !n,s.s<: X => card(s) = n<=> (#f.f : 1..n>->> s) >> I've been down this road before with cardinality. >> Cheers, >> Son >> >> On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: >> >>> Hi Ken, >>> On 8 Feb 2012, at 11:13, Ken Robinson wrote: >>> >>>> Hello everyone, >>>> >>>> I fear this email will demonstrate that I am an idiot, but here goes. >>>> >>> >>> You are certainly not. >>> >>>> My problems with card are long standing and persistent. >>>> >>> >>> It is the same feeling for me. >>> >>>> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >>>> >>> >>> I assume that you they are undischarged with the old Rodin as well. >>> >>>> As usual I am having trouble with card. >>>> >>>> For example: >>>> >>>> SETS >>>> X >>>> finite X >>>> >>>> xs<: X >>>> >>>> Prove >>>> x : xs => card(xs \ {x}) = card(xs) - 1 >>>> >>>> So far this has resisted all my efforts to discharge it. >>>> >>>> and I've been this way before. >>>> >>>> I hope, and will be grateful, if someone can demonstrate a proof. >>>> >>>> And I'm hoping it will show that I am an idiot. >>>> >>>> If not then I think this is a worry, as to many this poses a serious credibility problem for Event-B. >>>> >>>> Without knowing the Event-B axioms, this would appear to be axiomatic to most people. >>>> >>>> I will be grateful for any resolution of my ineptitude. >>>> >>> >>> You are probably want to the following feature request which has not been implemented. >>> http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 >>> But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. >>> http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 >>> Cheers, >>> Son >> >> -- >> Thai Son Hoang >> CNB F105.2 >> ETH Zentrum, Zurich, Switzerland >> Tel: +41 44 632 85 94 >> Fax: +41 44 632 11 72 >> >> >> >> ------------------------------------------------------------------------------ >> Keep Your Developer Skills Current with LearnDevNow! >> The most comprehensive online learning library for Microsoft developers >> is just \$99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3, >> Metro Style Apps, more. Free future releases when you subscribe now! >> http://p.sf.net/sfu/learndevnow-d2d >> >> >> >> _______________________________________________ >> Rodin-b-sharp-user mailing list >> Rodin-b-sharp-user@... >> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > > ------------------------------------------------------------------------------ > Keep Your Developer Skills Current with LearnDevNow! > The most comprehensive online learning library for Microsoft developers > is just \$99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3, > Metro Style Apps, more. Free future releases when you subscribe now! > http://p.sf.net/sfu/learndevnow-d2d > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```
 Re: [Rodin-b-sharp-user] Ongoing problems with card From: Matthias Schmalz - 2012-02-08 12:32:22 ```Hi, just to keep that clear, the formula !n,s. s<: X => card(s) = n <=> (#f.f : 1..n>->> s) is not valid. Choose s as the empty set and n as -1. Instead, it should be !n, s. s <: X & n : NAT => card(s) = n <=> (#f. f : 1..n >->> s). Ken, you are not an idiot. Reasoning about card is difficult, also in other theorem provers. Best, Matthias Am 08.02.2012 12:33, schrieb Hoang, Thai Son: > Dear Ken, > I just realised that I did not push my last reply to the mailing list. > I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. > !n,s.s<: X => card(s) = n<=> (#f.f : 1..n>->> s) > I've been down this road before with cardinality. > Cheers, > Son > > On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: > >> Hi Ken, >> On 8 Feb 2012, at 11:13, Ken Robinson wrote: >> >>> Hello everyone, >>> >>> I fear this email will demonstrate that I am an idiot, but here goes. >>> >> >> You are certainly not. >> >>> My problems with card are long standing and persistent. >>> >> >> It is the same feeling for me. >> >>> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >>> >> >> I assume that you they are undischarged with the old Rodin as well. >> >>> As usual I am having trouble with card. >>> >>> For example: >>> >>> SETS >>> X >>> finite X >>> >>> xs<: X >>> >>> Prove >>> x : xs => card(xs \ {x}) = card(xs) - 1 >>> >>> So far this has resisted all my efforts to discharge it. >>> >>> and I've been this way before. >>> >>> I hope, and will be grateful, if someone can demonstrate a proof. >>> >>> And I'm hoping it will show that I am an idiot. >>> >>> If not then I think this is a worry, as to many this poses a serious credibility problem for Event-B. >>> >>> Without knowing the Event-B axioms, this would appear to be axiomatic to most people. >>> >>> I will be grateful for any resolution of my ineptitude. >>> >> >> You are probably want to the following feature request which has not been implemented. >> http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 >> But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. >> http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 >> Cheers, >> Son > > -- > Thai Son Hoang > CNB F105.2 > ETH Zentrum, Zurich, Switzerland > Tel: +41 44 632 85 94 > Fax: +41 44 632 11 72 > > > > ------------------------------------------------------------------------------ > Keep Your Developer Skills Current with LearnDevNow! > The most comprehensive online learning library for Microsoft developers > is just \$99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3, > Metro Style Apps, more. Free future releases when you subscribe now! > http://p.sf.net/sfu/learndevnow-d2d > > > > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```
 Re: [Rodin-b-sharp-user] Ongoing problems with card From: nai11 - 2012-02-08 12:21:21 ```Hi all, this is an old and embarrsing problem. Almost nothing about cardinalities is provable without helper axiom. Among the list of inference rules on the wiki there are rules that would discharge these and similar condition but they are not present in the tool. ________________________________________ From: Hoang, Thai Son [htson@...] Sent: 08 February 2012 11:33 To: User Rodin B-sharp User Subject: Re: [Rodin-b-sharp-user] Ongoing problems with card Dear Ken, I just realised that I did not push my last reply to the mailing list. I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. !n,s.s <: X => card(s) = n <=> (#f.f : 1..n >->> s) I've been down this road before with cardinality. Cheers, Son On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: > Hi Ken, > On 8 Feb 2012, at 11:13, Ken Robinson wrote: > >> Hello everyone, >> >> I fear this email will demonstrate that I am an idiot, but here goes. >> > > You are certainly not. > >> My problems with card are long standing and persistent. >> > > It is the same feeling for me. > >> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >> > > I assume that you they are undischarged with the old Rodin as well. > >> As usual I am having trouble with card. >> >> For example: >> >> SETS >> X >> finite X >> >> xs <: X >> >> Prove >> x : xs => card(xs \ {x}) = card(xs) - 1 >> >> So far this has resisted all my efforts to discharge it. >> >> and I've been this way before. >> >> I hope, and will be grateful, if someone can demonstrate a proof. >> >> And I'm hoping it will show that I am an idiot. >> >> If not then I think this is a worry, as to many this poses a serious credibility problem for Event-B. >> >> Without knowing the Event-B axioms, this would appear to be axiomatic to most people. >> >> I will be grateful for any resolution of my ineptitude. >> > > You are probably want to the following feature request which has not been implemented. > http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 > But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. > http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 > Cheers, > Son -- Thai Son Hoang CNB F105.2 ETH Zentrum, Zurich, Switzerland Tel: +41 44 632 85 94 Fax: +41 44 632 11 72 ```
 Re: [Rodin-b-sharp-user] Ongoing problems with card From: Pierre Casteran - 2012-02-08 11:40:02 Attachments: finite.zip ```Hi, Son, Did you need to assert a new axiom ? In the following project, I proved Kens thm withous axioms, but a lot of effort (in changeme context) Pierre Le 08/02/2012 12:33, Hoang, Thai Son a écrit : > Dear Ken, > I just realised that I did not push my last reply to the mailing list. > I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. > !n,s.s<: X => card(s) = n<=> (#f.f : 1..n>->> s) > I've been down this road before with cardinality. > Cheers, > Son > > On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: > >> Hi Ken, >> On 8 Feb 2012, at 11:13, Ken Robinson wrote: >> >>> Hello everyone, >>> >>> I fear this email will demonstrate that I am an idiot, but here goes. >>> >> >> You are certainly not. >> >>> My problems with card are long standing and persistent. >>> >> >> It is the same feeling for me. >> >>> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >>> >> >> I assume that you they are undischarged with the old Rodin as well. >> >>> As usual I am having trouble with card. >>> >>> For example: >>> >>> SETS >>> X >>> finite X >>> >>> xs<: X >>> >>> Prove >>> x : xs => card(xs \ {x}) = card(xs) - 1 >>> >>> So far this has resisted all my efforts to discharge it. >>> >>> and I've been this way before. >>> >>> I hope, and will be grateful, if someone can demonstrate a proof. >>> >>> And I'm hoping it will show that I am an idiot. >>> >>> If not then I think this is a worry, as to many this poses a serious credibility problem for Event-B. >>> >>> Without knowing the Event-B axioms, this would appear to be axiomatic to most people. >>> >>> I will be grateful for any resolution of my ineptitude. >>> >> >> You are probably want to the following feature request which has not been implemented. >> http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 >> But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. >> http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 >> Cheers, >> Son > > -- > Thai Son Hoang > CNB F105.2 > ETH Zentrum, Zurich, Switzerland > Tel: +41 44 632 85 94 > Fax: +41 44 632 11 72 > > > > ------------------------------------------------------------------------------ > Keep Your Developer Skills Current with LearnDevNow! > The most comprehensive online learning library for Microsoft developers > is just \$99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3, > Metro Style Apps, more. Free future releases when you subscribe now! > http://p.sf.net/sfu/learndevnow-d2d > > > > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```
 Re: [Rodin-b-sharp-user] Ongoing problems with card From: Hoang, Thai Son - 2012-02-08 11:33:16 Attachments: Cardinality-Rodin-2.4.0.zip ``` Dear Ken, I just realised that I did not push my last reply to the mailing list. I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. !n,s.s <: X => card(s) = n <=> (#f.f : 1..n >->> s) I've been down this road before with cardinality. Cheers, Son On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: > Hi Ken, > On 8 Feb 2012, at 11:13, Ken Robinson wrote: > >> Hello everyone, >> >> I fear this email will demonstrate that I am an idiot, but here goes. >> > > You are certainly not. > >> My problems with card are long standing and persistent. >> > > It is the same feeling for me. > >> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >> > > I assume that you they are undischarged with the old Rodin as well. > >> As usual I am having trouble with card. >> >> For example: >> >> SETS >> X >> finite X >> >> xs <: X >> >> Prove >> x : xs => card(xs \ {x}) = card(xs) - 1 >> >> So far this has resisted all my efforts to discharge it. >> >> and I've been this way before. >> >> I hope, and will be grateful, if someone can demonstrate a proof. >> >> And I'm hoping it will show that I am an idiot. >> >> If not then I think this is a worry, as to many this poses a serious credibility problem for Event-B. >> >> Without knowing the Event-B axioms, this would appear to be axiomatic to most people. >> >> I will be grateful for any resolution of my ineptitude. >> > > You are probably want to the following feature request which has not been implemented. > http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 > But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. > http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 > Cheers, > Son -- Thai Son Hoang CNB F105.2 ETH Zentrum, Zurich, Switzerland Tel: +41 44 632 85 94 Fax: +41 44 632 11 72 ```
 [Rodin-b-sharp-user] Ongoing problems with card From: Ken Robinson - 2012-02-08 10:26:15 ```Hello everyone, I fear this email will demonstrate that I am an idiot, but here goes. My problems with card are long standing and persistent. As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. As usual I am having trouble with card. For example: SETS X finite X xs <: X Prove x : xs => card(xs \ {x}) = card(xs) - 1 So far this has resisted all my efforts to discharge it. and I've been this way before. I hope, and will be grateful, if someone can demonstrate a proof. And I'm hoping it will show that I am an idiot. If not then I think this is a worry, as to many this poses a serious credibility problem for Event-B. Without knowing the Event-B axioms, this would appear to be axiomatic to most people. I will be grateful for any resolution of my ineptitude. Cheers, Ken Ken Robinson School of Computer Science & Engineering UNSW NSW 2052 CRICOS Provider No: 00098G This message is intended for the addressee named and may contain confidential information. If you are not the intended recipient, please delete it and notify the sender. Views expressed in this message are those of the individual sender and are not necessarily the views of UNSW. ```
 [Rodin-b-sharp-user] Rodin 2.4 From: Nicolas Beauger - 2012-02-03 14:01:55 ```Dear Rodin users, Rodin 2.4 is now available, with new features described at: http://wiki.event-b.org/index.php/Rodin_Platform_2.4_Release_Notes Here is the download area on SourceForge: http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.4/ For this new release and subsequent ones, we also provide 64 bit binaries for Linux and Windows: we hope it will simplify the usage of Rodin for the many of you running 64 bit OSes. Happy modelling ! The Rodin Team ```

Showing 18 results of 18