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}
(8) 
S  M  T  W  T  F  S 





1
(5) 
2
(2) 
3

4

5

6
(4) 
7

8
(1) 
9
(6) 
10

11

12
(2) 
13
(4) 
14

15

16
(4) 
17
(1) 
18

19

20
(2) 
21

22

23

24

25

26

27

28

29

30

31

From: Colin Snook <cfs@ec...>  20091020 13:45:53

Dear All, A new version of UMLB is now available. UMLB 0.6.0 works in Rodin 1.1.x. You can install it from the Rodin Update site as usual New in this version: You can now double click on diagram objects to open associated diagrams. Designate Invariants and axioms as theorems. New properties tables in Machine and Context for classes and classtypes (resp) (this allows you to control the order of translation) Fixed a bug in the translation of state machine nested final transitions. Regards Colin 
From: Carine Pascal <carine.pascal@sy...>  20091020 12:50:21

Dear All, The Rodin team is proud to announce the availability of the release 1.1 of the Rodin platform. More information about what has changed since Rodin 1.0 is available at http://sourceforge.net/projects/rodinbsharp/files/Core_%20Rodin%20Platform/1.1/relnotes.txt/download and http://wiki.eventb.org/index.php/Rodin_Platform_1.1_Release_Notes  WARNING This release is not backward compatible with releases 0.9.x or less. Your workspace files will be automatically upgraded to the new file version, so please BACKUP your workspace(s) before using this new release.  Important Notes:  You also need to have a Java JRE (5.0 or later) installed on your computer. The Rodin product will not work with a previous version.  To enhance your proving experience, you're strongly advised to install the Atelier B provers, as explained in the Welcome page of the tool.  If you plan to reuse projects created with a release 0.9.x of the platform or earlier, you have to clean up these projects first. For that, just click "Project > Clean..." in the menubar and select the projects to clean in the window that pops up. Best regards, Carine.   Carine PASCAL Tél. : (+33)(0)4 42 90 41 24 SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Benoît Fraikin <benoit.fraikin@us...>  20091017 02:33:18

Dear Son, I did it a wrong. I have mixed up the two columns and thought that the left column was the selected items. Thank again > I am a bit confused here. There are two different set of tactics: >  Auto Tactics: for the autoprover. >  Post Tactics: to run after every interactive step. > In the preferences, the list on the right contains the selected > tactics. > I assumed here what you do is to put Atelier B ML in the set of post > tactics. > This is not done by default as the posttactics run in the > interactive mode should be fast. > Is that what you did here? > Cheers, > Son Benoît Fraikin, Ph.D., Chargé de cours à forfait, http://pages.usherbrooke.ca/gril/fraikin 
From: Thai Son Hoang <htson@in...>  20091016 21:58:45

Hi Benoit Fraikin, On 16102009, at 23:06, Benoît Fraikin wrote: > Thank you for your help. > > I have just seen that I put Atelier B ML in the available autotactic. > When I've removed it from the list, the prover accepted to prove my > sequent (x <= r1  x <= r) > Do you know why it tackles the autoprover to do its job when I put it > on the list ? > I am a bit confused here. There are two different set of tactics:  Auto Tactics: for the autoprover.  Post Tactics: to run after every interactive step. In the preferences, the list on the right contains the selected tactics. I assumed here what you do is to put Atelier B ML in the set of post tactics. This is not done by default as the posttactics run in the interactive mode should be fast. Is that what you did here? Cheers, Son  Thai Son Hoang htson@... IFW C48.2 ETH Zentrum Tel: +41 44 632 85 94 Fax: +41 44 632 11 72 
From: Benoît Fraikin <benoit.fraikin@us...>  20091016 21:06:50

Thank you for your help. I have just seen that I put Atelier B ML in the available autotactic. When I've removed it from the list, the prover accepted to prove my sequent (x <= r1  x <= r) Do you know why it tackles the autoprover to do its job when I put it on the list ? Again thank you for your answer Benoît Fraikin, Ph.D., Chargé de cours à forfait, http://pages.usherbrooke.ca/gril/fraikin 
From: Thai Son Hoang <htson@in...>  20091016 20:17:20

Dear Benoit Fraikin, On 16102009, at 21:30, Benoît Fraikin wrote: > Greeting, > > I have a little problem. I want to prove this simple result > > x <= r1  x<=r > [picture 1] > <Picture 1.png> > > > Why is Rodin not able to prove that ? > At this level... what can I do ? > ML should be able to finish the job. You can just launch ML from the Proof Control. > > This prove comes from the need to prove this sequent > x > x0 : 1..(r1) < (cle;clair)  x > x0 : 1..r < > (cle;clair) > [picture 2] > <Picture 2.png> > > > And this is needed from > (1..(r1) < (cle;clair)) \/ {r> clair(cle(r))} = 1..r < > (cle;clair) > [picture 3] > <Picture 3.png> > > Is this a bug in the prover ? > If you are asking that why Rodin cannot prove the above (the last one), then Rodin probably cannot. The interactive proof steps that you did is to simplify the obligation so that one of the legacy prover, e.g. ML, PP or newPP can finish the proving for you. Cheers, Son  Thai Son Hoang htson@... IFW C48.2 ETH Zentrum Tel: +41 44 632 85 94 Fax: +41 44 632 11 72 
From: Benoît Fraikin <Benoit.Fraikin@USherbrooke.ca>  20091016 19:30:48

Greeting, I have a little problem. I want to prove this simple result x <= r1  x<=r [picture 1] 
From: Nicolas Beauger <nicolas.beauger@sy...>  20091013 16:18:09

Ken, > so maybe that will be fixed in the full release of 1.1? > I'm working on it !   Nicolas BEAUGER Tél. : (+33)(0)4 42 90 41 24 SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Ken Robinson <kenr@cs...>  20091013 15:31:32

Hi Nicolas, On 14/10/2009, at 02:15 AM, Nicolas Beauger wrote: > I think this is related to bug #2648926 : PostTactic is invoked > after saving > Does it still happen if posttactics are disabled when pressing the > save button ? Thanks. That fixes it. so maybe that will be fixed in the full release of 1.1? Cheers, Ken > Ken Robinson a écrit : >> >> I am getting strange behaviour with Rodin 1.1RC1. >> >> When I discharge some POs the Save icon is raised as expected. >> >> But when I click that icon and save the proofs the icon is still >> highlighted when the save has apparently completed. >> >> Indeed clicking on the save icon (or using command S) displays the >> same list of proofs that should have been saved. >> >> If I reload Rodin I am prompted to save those proofs and that seems >> to >> force the save. >> >> Any idea what might be causing this? >> >> The .log file does not show any problems, or anything else for that >> matter. >> >> Cheers, >> >> Ken >> >>  >> Come build with us! The BlackBerry(R) Developer Conference in SF, CA >> is the only developer event you need to attend this year. Jumpstart >> your >> developing skills, take BlackBerry mobile applications to market >> and stay >> ahead of the curve. Join us from November 9  12, 2009. Register now! >> http://p.sf.net/sfu/devconference >> _______________________________________________ >> 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. >> >> >> >> > >  >  > Nicolas BEAUGER Tél. : (+33)(0)4 42 90 41 24 > > SYSTEREL >  > Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr >  
From: Nicolas Beauger <nicolas.beauger@sy...>  20091013 15:19:41

Hi Ken, I think this is related to bug #2648926 <https://sourceforge.net/tracker/?func=detail&aid=2648926&group_id=108850&atid=651669>; : PostTactic is invoked after saving Does it still happen if posttactics are disabled when pressing the save button ? Cheers, Nicolas Ken Robinson a écrit : > I am getting strange behaviour with Rodin 1.1RC1. > > When I discharge some POs the Save icon is raised as expected. > > But when I click that icon and save the proofs the icon is still > highlighted when the save has apparently completed. > > Indeed clicking on the save icon (or using command S) displays the > same list of proofs that should have been saved. > > If I reload Rodin I am prompted to save those proofs and that seems to > force the save. > > Any idea what might be causing this? > > The .log file does not show any problems, or anything else for that > matter. > > Cheers, > > Ken > >  > Come build with us! The BlackBerry(R) Developer Conference in SF, CA > is the only developer event you need to attend this year. Jumpstart your > developing skills, take BlackBerry mobile applications to market and stay > ahead of the curve. Join us from November 9  12, 2009. Register now! > http://p.sf.net/sfu/devconference > _______________________________________________ > 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. > > > >   Nicolas BEAUGER Tél. : (+33)(0)4 42 90 41 24 SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Ken Robinson <kenr@cs...>  20091013 14:44:16

I am getting strange behaviour with Rodin 1.1RC1. When I discharge some POs the Save icon is raised as expected. But when I click that icon and save the proofs the icon is still highlighted when the save has apparently completed. Indeed clicking on the save icon (or using command S) displays the same list of proofs that should have been saved. If I reload Rodin I am prompted to save those proofs and that seems to force the save. Any idea what might be causing this? The .log file does not show any problems, or anything else for that matter. Cheers, Ken 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20091012 08:20:22

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Hi Pierre, if you select the "theorem" field, you claim (and have to prove) that the predicate next to it is a theorem. A theorem is a logical consequence of the preceeding axioms and theorems. Best, Matthias Pierre Casteran schrieb: > Hello, > > I've just downloaded rodin 1.0, and notices a "theorem" field besides > axioms and invariants. > > I didn't find on the user manual how it is used. > > Pierre > > >  > Come build with us! The BlackBerry(R) Developer Conference in SF, CA > is the only developer event you need to attend this year. Jumpstart your > developing skills, take BlackBerry mobile applications to market and stay > ahead of the curve. Join us from November 9  12, 2009. Register now! > http://p.sf.net/sfu/devconference > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFK0uadczhznXSdWggRAjWoAJ9zaiEiR1JpecevaDfptzqUEdjyrACff6MV Z4MLSnkFO3asAMf8ZzAZRLo= =nbT4 END PGP SIGNATURE 
From: Pierre Casteran <pierre.casteran@la...>  20091012 08:07:39

Hello, I've just downloaded rodin 1.0, and notices a "theorem" field besides axioms and invariants. I didn't find on the user manual how it is used. Pierre 
From: Laurent Voisin <laurent.voisin@sy...>  20091009 17:45:38

Dear All, just to close this discussion, as I said in a private chat with Ken, the "new" features alluded below where indeed available in Rodin 1.0. So there is no issue here with the provers, when a more recent version of Rodin is installed. Laurent. Le 6 oct. 09 à 12:41, Ken Robinson a écrit : > > Dear Carine and Laurent. > > Thank you both for the explanation of what looked like a mystery for > me. > > Now there is a second mystery, as you refer to Rodin 1.1. > > But I believe I am running under 1.0 having given 1.1. away for the > moment as I experienced some other problems. > > Certainly the "about Rodin" says 1.0. > > What could be the explanation of this? > > Seems like I'm somehow running the newer release of the provers? > > Cheers, > > Ken > > On 06/10/2009, at 19:33 PM, Laurent Voisin wrote: > >> Hi Ken, >> >> here is a little expansion of Carine's answer. >> >> Le 6 oct. 09 à 05:32, Ken Robinson a écrit : >> >>> Here's the problematic case: >>> >> <pastedGraphic.png> >>> >>> >>> I enter min(liftschedule(lift)) into the yellow box and click the >>> red existential button. >>> >>> Instead of the normal behaviour, of simply running the >>> instantiation, it gives me a menu >>> >> <pastedGraphic.png> >>> >>> >>> >>> A bit strange, but I choose instantiation. >> >> This is a new feature of Rodin 1.1: when you have to prove the >> existence of a lower (resp. upper) bound, the prover now proposes >> to use an argument of finiteness (which is the purpose of the >> second tactic displayed). In practice, this means that when you >> have a goal of form: >> >> ∃b·∀x·x∈E⇒b≤x >> >> if you select the second tactic, you will get the new goal >> >> finite(E) >> >> which is a sufficient condition for the existence of the lower >> bound. Given the supposed intent of your model, this might be very >> helpful (unless you don't have any ground floor ;). You would >> need to add the invariant >> >> !lift. lift : dom(liftschedule) => finite(liftschedule(lift)) >> >>> The provers whirl for a moment and then "Tactic applied >>> successfully, but ... >>> >>> the existential goal remains (uninstantiated of course) >> >> This is because, when you introduce an expression to the prover, >> you have to show that it is welldefined before the prover accepts >> to use it (this might have not been fully implemented in previous >> version of the platform). >> >> But, here, suggesting min(liftschedule(lift)) produces a WD sub >> goal which is exactly the same subgoal. You tried to use a >> circular argument to discharge this WD subgoal and the prover just >> reflects that. >> >> Laurent. >> > >  > 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. > > 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20091009 14:35:33

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Nicolas, thanks for the answer. I was mixing up "deselect" and "hide" when I was inventing my example. Now it is clear to me. I am looking forward to the improved versions. Matthias Nicolas Beauger schrieb: > Hi Matthias, > >> 1. >> Sometimes, the proof skeleton view does not display the current proof. >> Steps to reproduce the problem (in Rodin 1.0): >> 1. Open some proof. (e.g. the proof in the attached archive) >> 2. Open the proof skeleton view as a fast view. >> 3. The proof skeleton view just contains "no proof to display". >> >> Maybe I misunderstand which proof should be displayed in the proof >> skeleton view. >> > The proof skeleton view gets updated when single clicking a PO in the > explorer. So the first time the proof skeleton view is displayed, you > have to select again the PO in the explorer to make it appear on the > view. Afterwards it's the same, except that if the skeleton view is a > fast view, you have to first click on the PO in the explorer then click > on the view to make it reappear with the new PO. I agree this behavior > is not very convenient and I'll try to improve it in the next few days. >> 2. >> The attached archive contains a proof of a trivial statment (c=c). In >> the proof I select and deselect some hypotheses several times. In the >> end, I run New PP (restricted). >> I expected this to be a perfect candidate for proof simplification, but >> "simplify proof(s)" seems not to change my proof. >> >> Is this the intended behaviour? >> > The proof simplifier handles a certain number of cases: it removes fwd, > select, hide actions when they are detected to be unused. You can try > with the small attached example. It does not work in the case you > provided because the tool does not handle deselect actions. That's an > improvement to be implemented. > > Thanks for pointing out these improvements. > > Nicolas > BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFKz0oXczhznXSdWggRAtZhAJ48aRVZ2Bu4pyl6T54BmNlJglyD1gCfTBk0 LTaNrw3gg3WtKAOS9fGEoto= =505w END PGP SIGNATURE 
From: Nicolas Beauger <nicolas.beauger@sy...>  20091009 14:29:32

Hi Matthias, > 1. > Sometimes, the proof skeleton view does not display the current proof. > Steps to reproduce the problem (in Rodin 1.0): > 1. Open some proof. (e.g. the proof in the attached archive) > 2. Open the proof skeleton view as a fast view. > 3. The proof skeleton view just contains "no proof to display". > > Maybe I misunderstand which proof should be displayed in the proof > skeleton view. > The proof skeleton view gets updated when single clicking a PO in the explorer. So the first time the proof skeleton view is displayed, you have to select again the PO in the explorer to make it appear on the view. Afterwards it's the same, except that if the skeleton view is a fast view, you have to first click on the PO in the explorer then click on the view to make it reappear with the new PO. I agree this behavior is not very convenient and I'll try to improve it in the next few days. > 2. > The attached archive contains a proof of a trivial statment (c=c). In > the proof I select and deselect some hypotheses several times. In the > end, I run New PP (restricted). > I expected this to be a perfect candidate for proof simplification, but > "simplify proof(s)" seems not to change my proof. > > Is this the intended behaviour? > The proof simplifier handles a certain number of cases: it removes fwd, select, hide actions when they are detected to be unused. You can try with the small attached example. It does not work in the case you provided because the tool does not handle deselect actions. That's an improvement to be implemented. Thanks for pointing out these improvements. Nicolas   Nicolas BEAUGER Tél. : (+33)(0)4 42 90 41 24 SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20091009 13:52:47

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Hi Ken, thanks for the hint. Yes, it is a bit confusing that the proof displayed in the proof tree view may be different from the proof displayed in the proof skeleton view. On the other hand, I do not have to open a proof editor to see a proof. Now that I know, it is okay for me. Cheers, Matthias Ken Robinson schrieb: > ˙Hi Matthias, > > On 09/10/2009, at 19:45 PM, Matthias Schmalz wrote: > >> BEGIN PGP SIGNED MESSAGE >> Hash: SHA1 >> >> Hi, >> >> first of, I appreciate the proof skeleton view and the simplify proofs >> function. >> >> Now my questions: >> 1. >> Sometimes, the proof skeleton view does not display the current proof. >> Steps to reproduce the problem (in Rodin 1.0): >> 1. Open some proof. (e.g. the proof in the attached archive) >> 2. Open the proof skeleton view as a fast view. >> 3. The proof skeleton view just contains "no proof to display". >> >> Maybe I misunderstand which proof should be displayed in the proof >> skeleton view. > > Yes, it's a bit confusing isn't it? :) > > What you need to do is to highlight the proof obligation in the EventB > explorer and then select the proof skeleton and you should see the proof. > > Cheers, > > Ken BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFKz0AmczhznXSdWggRAsh8AJ926D3LYR+Ow0zbokxt0u4mcVdUVACdFMq0 cB7EMgobG4cKFpJCo6DAU2o= =+HWZ END PGP SIGNATURE 
From: Ken Robinson <kenr@cs...>  20091009 13:46:11

˙Hi Matthias, On 09/10/2009, at 19:45 PM, Matthias Schmalz wrote: > BEGIN PGP SIGNED MESSAGE > Hash: SHA1 > > Hi, > > first of, I appreciate the proof skeleton view and the simplify proofs > function. > > Now my questions: > 1. > Sometimes, the proof skeleton view does not display the current proof. > Steps to reproduce the problem (in Rodin 1.0): > 1. Open some proof. (e.g. the proof in the attached archive) > 2. Open the proof skeleton view as a fast view. > 3. The proof skeleton view just contains "no proof to display". > > Maybe I misunderstand which proof should be displayed in the proof > skeleton view. Yes, it's a bit confusing isn't it? :) What you need to do is to highlight the proof obligation in the Event B explorer and then select the proof skeleton and you should see the proof. Cheers, Ken 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20091009 08:45:29

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Hi, first of, I appreciate the proof skeleton view and the simplify proofs function. Now my questions: 1. Sometimes, the proof skeleton view does not display the current proof. Steps to reproduce the problem (in Rodin 1.0): 1. Open some proof. (e.g. the proof in the attached archive) 2. Open the proof skeleton view as a fast view. 3. The proof skeleton view just contains "no proof to display". Maybe I misunderstand which proof should be displayed in the proof skeleton view. 2. The attached archive contains a proof of a trivial statment (c=c). In the proof I select and deselect some hypotheses several times. In the end, I run New PP (restricted). I expected this to be a perfect candidate for proof simplification, but "simplify proof(s)" seems not to change my proof. Is this the intended behaviour? Thanks in advance, Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFKzvgZczhznXSdWggRAmivAJ45eZEnTGIlzCA52bEsR0gl+FGWtACfeJEH EFQD9S1rquWZYRkukqUdcSY= =6BK/ END PGP SIGNATURE 
From: Carine Pascal <carine.pascal@sy...>  20091008 17:21:12

Dear Ken, A section related to filtering has been added to the Wiki page dedicated to the Proof Obligation Explorer: http://wiki.eventb.org/index.php/The_Proof_Obligation_Explorer_%28Rodin_User_Manual%29 Regards, Carine. > Dear Ken, > > Le 23 sept. 09 à 15:16, Ken Robinson a écrit : > >> Sorry to ask what are probably trivial questions, but there are a >> couple of things that I have wondered about for some time: >> >> 2) the little window at the top of the EventB explorer. What's that >> for? > > It is used for filtering the POs that are displayed in the tree. If > you type some string in this window, only PO's whose name contain this > string will be displayed in the explorer tree. > > This is a feature that was already present in the old Proof Explorer > and has been ported to the new eventB explorer. > >> If there is documentation somewhere just point me to it. > > You're question shows that this not the case. We will update the User > Manual (especially page > http://wiki.eventb.org/index.php/The_Proof_Obligation_Explorer_%28Rodin_User_Manual%29) in > the wiki. > > Cheers, > Laurent.   Carine PASCAL Tél. : (+33)(0)4 42 90 41 24 SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Ken Robinson <kenr@cs...>  20091006 10:41:48

Dear Carine and Laurent. Thank you both for the explanation of what looked like a mystery for me. Now there is a second mystery, as you refer to Rodin 1.1. But I believe I am running under 1.0 having given 1.1. away for the moment as I experienced some other problems. Certainly the "about Rodin" says 1.0. What could be the explanation of this? Seems like I'm somehow running the newer release of the provers? Cheers, Ken On 06/10/2009, at 19:33 PM, Laurent Voisin wrote: > Hi Ken, > > here is a little expansion of Carine's answer. > > Le 6 oct. 09 à 05:32, Ken Robinson a écrit : > >> Here's the problematic case: >> > <pastedGraphic.png> >> >> >> I enter min(liftschedule(lift)) into the yellow box and click the >> red existential button. >> >> Instead of the normal behaviour, of simply running the >> instantiation, it gives me a menu >> > <pastedGraphic.png> >> >> >> >> A bit strange, but I choose instantiation. > > This is a new feature of Rodin 1.1: when you have to prove the > existence of a lower (resp. upper) bound, the prover now proposes > to use an argument of finiteness (which is the purpose of the second > tactic displayed). In practice, this means that when you have a > goal of form: > > ∃b·∀x·x∈E⇒b≤x > > if you select the second tactic, you will get the new goal > > finite(E) > > which is a sufficient condition for the existence of the lower > bound. Given the supposed intent of your model, this might be very > helpful (unless you don't have any ground floor ;). You would need > to add the invariant > > !lift. lift : dom(liftschedule) => finite(liftschedule(lift)) > >> The provers whirl for a moment and then "Tactic applied >> successfully, but ... >> >> the existential goal remains (uninstantiated of course) > > This is because, when you introduce an expression to the prover, you > have to show that it is welldefined before the prover accepts to > use it (this might have not been fully implemented in previous > version of the platform). > > But, here, suggesting min(liftschedule(lift)) produces a WD subgoal > which is exactly the same subgoal. You tried to use a circular > argument to discharge this WD subgoal and the prover just reflects > that. > > Laurent. > 
From: Laurent Voisin <laurent.voisin@sy...>  20091006 09:59:42

Hi Ken, here is a little expansion of Carine's answer. Le 6 oct. 09 à 05:32, Ken Robinson a écrit : > Here's the problematic case: > 
From: Carine Pascal <carine.pascal@sy...>  20091006 07:35:55

<!DOCTYPE html PUBLIC "//W3C//DTD HTML 4.01 Transitional//EN"> <html> <head> <meta content="text/html;charset=ISO88591" httpequiv="ContentType"> </head> <body bgcolor="#ffffff" text="#000000"> Dear Ken, <br> <br> ∃b·∀x·x∈E⇒b≤x is the WellDefinedness lemma for min(E);<br> As a consequence, if you enter min(liftschedule(lift)) in your instantiation, you have to prove ∃b·∀x·x∈liftschedule(lift)⇒b≤x :) Thus, the observed behavior is the expected behavior.<br> <br> Regards,<br> <br> Carine.<br> <br> Ken Robinson a écrit : <blockquote cite="mid:7638AB7A1A604E4EA0D1DCBADBE716F8@..." type="cite">Hello everyone, <br> <br> I will be grateful for any insights into a very strange problem I am having at the moment. <br> <br> A bit of history. <br> <br> I installed 1.1RC and had some very strange problems, which may be the subject of another inquiry in the future. <br> <br> I restored my old WS and am discharging some POs that have been discharged in the past. <br> <br> Here's the problematic case: <br> <br> <br>  <br> 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. <br> <br> <br> <hr size="4" width="90%"><br> <center><img src="cid:part1.07090208.08070107@..."></center> <p><br> <br> <br> I enter min(liftschedule(lift)) into the yellow box and click the red existential button. <br> <br> Instead of the normal behaviour, of simply running the instantiation, it gives me a menu <br> <br> <br> </p> <hr size="4" width="90%"><br> <center><img src="cid:part2.07020405.03080202@..."></center> <p><br> <br> A bit strange, but I choose instantiation. <br> <br> The provers whirl for a moment and then "Tactic applied successfully, but ... <br> <br> the existential goal remains (uninstantiated of course) <br> <br> ad infinitum as you can see from the proof tree: <br> <br> <br> </p> <hr size="4" width="90%"><br> <center><img src="cid:part3.03030604.06040003@..."></center> <p><br> <br> <br> The .log doesn't show anything. <br> <br> Any ideas? <br> <br> Thanks for any help <br> <br> Cheers, <br> <br> Ken<br> </p> <pre wrap=""> <hr size="4" width="90%">  Come build with us! The BlackBerry&reg; Developer Conference in SF, CA is the only developer event you need to attend this year. Jumpstart your developing skills, take BlackBerry mobile applications to market and stay ahead of the curve. Join us from November 9&#45;12, 2009. Register now&#33; <a class="moztxtlinkfreetext" href="http://p.sf.net/sfu/devconf">http://p.sf.net/sfu/devconf</a></pre>; <pre wrap=""> <hr size="4" width="90%"> _______________________________________________ Rodinbsharpuser mailing list <a class="moztxtlinkabbreviated" href="mailto:Rodinbsharpuser@...">Rodinbsharpuser@...</a> <a class="moztxtlinkfreetext" href="https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser">https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser</a>; </pre> </blockquote> <br> <br> <pre class="mozsignature" cols="72">  Carine PASCAL Tél. : (+33)(0)4 42 90 41 24 SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : <a class="moztxtlinkabbreviated" href="http://www.systerel.fr">www.systerel.fr</a>;  </pre> </body> </html> 
From: Ken Robinson <kenr@cs...>  20091006 03:32:23

Hello everyone, I will be grateful for any insights into a very strange problem I am having at the moment. A bit of history. I installed 1.1RC and had some very strange problems, which may be the subject of another inquiry in the future. I restored my old WS and am discharging some POs that have been discharged in the past. Here's the problematic case: 
From: Thai Son Hoang <htson@in...>  20091002 06:38:36

Dear Benoit Fraikin, This is the bug that has been fixed by Laurent. https://sourceforge.net/tracker/index.php?func=detail&aid=2856893&group_id=108850&atid=651669 You need to get Rodin RC1.1 (release candidate) where the fix is included. The actual release Rodin 1.1 will be available in the next 2 weeks. Cheers, Son On 02102009, at 05:40, Benoît Fraikin wrote: > Greeting, > > I have tried to put the car controller model from JeanRaymond's book, > but I did not succeed to finish it since it is impossible to add a new > invariant above the thirtieth. I have 19 variables, 30 invariants, 1 > "refines", 4 "sees", 1 variant and 9 events. > it seems like there is a limited number of items (variable/invariant > etc.) in RODIN. > Am I right ? > > Thank you > > Benoît Fraikin, Ph.D., > Lecturer, > > >  > Come build with us! The BlackBerry® Developer Conference in SF, CA > is the only developer event you need to attend this year. Jumpstart > your > developing skills, take BlackBerry mobile applications to market and > stay > ahead of the curve. Join us from November 912, 2009. Register > now! > http://p.sf.net/sfu/devconf > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser  Thai Son Hoang htson@... IFW C48.2 ETH Zentrum If you think I am late in replying to you, this might be the reason. http://picasaweb.google.com.vn/hangson211/2009HangNga#5345759836556203762 