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}
(11) 
_{Jun}
(17) 
_{Jul}
(5) 
_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 



1

2

3

4
(8) 
5

6

7

8

9

10

11
(8) 
12
(4) 
13
(1) 
14
(3) 
15
(3) 
16
(11) 
17
(5) 
18

19

20

21
(3) 
22

23
(4) 
24

25
(7) 
26

27

28

29

30

31



From: Thiago Carvalho de Sousa <thiagocsousa@gm...>  20110325 11:52:50

Laurent and Joachim, Thanks for your help. It was a semantic confusion. Now I understood! Thiago 2011/3/25 Joachim Breitner <mail@...>: > Hi, > > Am Freitag, den 25.03.2011, 10:39 +0100 schrieb Laurent Voisin: >> It just occurs to me that naming "SETS" the clause that introduces new >> types can be confusing to a newbie. It never occurred to me before >> because I always read it as CARRIER_SETS. > > I’d understand it as TYPES or BASE_TYPES. Maybe that would be clearer? > > Greetings, > Joachim > > >  > Joachim Breitner > eMail: mail@... > Homepage: http://www.joachimbreitner.de > ICQ#: 74513189 > JabberID: nomeata@... > >  > Enable your software for Intel(R) Active Management Technology to meet the > growing manageability and security demands of your customers. Businesses > are taking advantage of Intel(R) vPro (TM) technology  will your software > be a part of the solution? Download the Intel(R) Manageability Checker > today! http://p.sf.net/sfu/inteldev2devmar > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > 
From: Mathieu Clabaut <mathieu.clabaut@sy...>  20110325 11:07:37

From: Mathieu Clabaut <mathieu.clabaut@sy...>  20110325 10:20:02

From: Joachim Breitner <mail@jo...>  20110325 10:05:23

Hi, Am Freitag, den 25.03.2011, 10:39 +0100 schrieb Laurent Voisin: > It just occurs to me that naming "SETS" the clause that introduces new > types can be confusing to a newbie. It never occurred to me before > because I always read it as CARRIER_SETS. I’d understand it as TYPES or BASE_TYPES. Maybe that would be clearer? Greetings, Joachim  Joachim Breitner eMail: mail@... Homepage: http://www.joachimbreitner.de ICQ#: 74513189 JabberID: nomeata@... 
From: Laurent Voisin <laurent.voisin@sy...>  20110325 09:39:39

Dear Thiago, Le 25 mars 2011 à 06:03, Joachim Breitner a écrit : > Am Donnerstag, den 24.03.2011, 21:18 0300 schrieb Thiago Carvalho de > Sousa: >> Maybe it's a stupid question, but I will do it >> >> I'd like to have a set exactly like the natural set but without {1}. >> So, I tried to do "NATWITHOUTONE = NAT \ {1}" and I got "Types >> NATWITHOUTONE and Z do not match" >> Am I doing anything wrong?? How can I express this set? >> >> Thanks in advance, > > did you introduce NATWITHOUTONE as a "Set"? From my understanding it > would be sufficient to introduce it as an constant, and giving the above > equation as an axiom. Joachim is right. The SETS clause introduces new carrier sets that define new types. Each of these types have a different set of values which is also different from the predefined types Z and BOOL. If you want to define just a set of integers, you have to declare a constant. It just occurs to me that naming "SETS" the clause that introduces new types can be confusing to a newbie. It never occurred to me before because I always read it as CARRIER_SETS. Cheers, Laurent. 
From: Joachim Breitner <mail@jo...>  20110325 05:03:27

Hi, Am Donnerstag, den 24.03.2011, 21:18 0300 schrieb Thiago Carvalho de Sousa: > Maybe it's a stupid question, but I will do it > > I'd like to have a set exactly like the natural set but without {1}. > So, I tried to do "NATWITHOUTONE = NAT \ {1}" and I got "Types > NATWITHOUTONE and Z do not match" > Am I doing anything wrong?? How can I express this set? > > Thanks in advance, did you introduce NATWITHOUTONE as a "Set"? From my understanding it would be sufficient to introduce it as an constant, and giving the above equation as an axiom. Greetings, Joachim  Joachim "nomeata" Breitner mail: mail@...  ICQ# 74513189  GPGKey: 4743206C JID: nomeata@...  http://www.joachimbreitner.de/ Debian Developer: nomeata@... 
From: Thiago Carvalho de Sousa <thiagocsousa@gm...>  20110325 00:18:14

My friends, Maybe it's a stupid question, but I will do it I'd like to have a set exactly like the natural set but without {1}. So, I tried to do "NATWITHOUTONE = NAT \ {1}" and I got "Types NATWITHOUTONE and Z do not match" Am I doing anything wrong?? How can I express this set? Thanks in advance, Thiago 
From: Laurent Voisin <laurent.voisin@sy...>  20110323 16:32:46

Dear All, Le 23 mars 2011 à 14:41, Joachim Breitner a écrit : > having asked a similar question before, let me try to answer yours. > > Am Donnerstag, den 24.03.2011, 00:11 +1100 schrieb Ken Robinson: >> but not the elusive >> >> card(ds \ {d}) = card(ds)  1 > > the rule that would allow you to continue here, SIMP_CARD_SETMINUS_R on > http://wiki.eventb.org/index.php/Inference_Rules, has no * in the first > column. This means that it was proposed, but not implemented yet. (I > hope this is correct.) Yes, this is correct. We plan to implement it soon. Cheers, Laurent. 
From: Ken Robinson <kenr@cs...>  20110323 14:03:49

Thank you Joachim. Ken On 24/03/2011, at 00:41 AM, Joachim Breitner wrote: > Hi, > > having asked a similar question before, let me try to answer yours. > > Am Donnerstag, den 24.03.2011, 00:11 +1100 schrieb Ken Robinson: >> but not the elusive >> >> card(ds \ {d}) = card(ds)  1 > > the rule that would allow you to continue here, SIMP_CARD_SETMINUS_R on > http://wiki.eventb.org/index.php/Inference_Rules, has no * in the first > column. This means that it was proposed, but not implemented yet. (I > hope this is correct.) > > You can continue by adding the hypothesis > card(ds) = card(ds \ {d}) +1 > (from which your goal is solvable), then add the hypothesis > ds = (ds \ {d}) ∪ {d} > to be able to rewrite it as > card((ds \ {d}) ∪ {d}) = card(ds \ {d}) +1 > Then Rodin will be able to rewrite the left hand side to > card(ds \ {d}) + card({d})  card((ds \ {d}) ∩ {d}) = card(ds \ {d}) +1 > which will be solvable. > > Greetings, > Joachim > >  > Joachim Breitner > eMail: mail@... > Homepage: http://www.joachimbreitner.de > ICQ#: 74513189 > JabberID: nomeata@... >  > Enable your software for Intel(R) Active Management Technology to meet the > growing manageability and security demands of your customers. Businesses > are taking advantage of Intel(R) vPro (TM) technology  will your software > be a part of the solution? Download the Intel(R) Manageability Checker > today! http://p.sf.net/sfu/inteldev2devmar_______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Joachim Breitner <mail@jo...>  20110323 13:41:28

Hi, having asked a similar question before, let me try to answer yours. Am Donnerstag, den 24.03.2011, 00:11 +1100 schrieb Ken Robinson: > but not the elusive > > card(ds \ {d}) = card(ds)  1 the rule that would allow you to continue here, SIMP_CARD_SETMINUS_R on http://wiki.eventb.org/index.php/Inference_Rules, has no * in the first column. This means that it was proposed, but not implemented yet. (I hope this is correct.) You can continue by adding the hypothesis card(ds) = card(ds \ {d}) +1 (from which your goal is solvable), then add the hypothesis ds = (ds \ {d}) ∪ {d} to be able to rewrite it as card((ds \ {d}) ∪ {d}) = card(ds \ {d}) +1 Then Rodin will be able to rewrite the left hand side to card(ds \ {d}) + card({d})  card((ds \ {d}) ∩ {d}) = card(ds \ {d}) +1 which will be solvable. Greetings, Joachim  Joachim Breitner eMail: mail@... Homepage: http://www.joachimbreitner.de ICQ#: 74513189 JabberID: nomeata@... 
From: Ken Robinson <kenr@cs...>  20110323 13:12:00

I've had a bit of discussion before on proofs involving card. Matthias seemed to support the experience that reasoning about card was frustrating. I'd like to understand why. A simple example is proving d : ds => card(ds \ {s}) = card(ds) 1 where finite(ds) The provers easily establish card(ds \ {d}) < card(ds) card(ds \ {d}) <= card(ds)  1 but not the elusive card(ds \ {d}) = card(ds)  1 Why? Thanks for any enlightenment. Ken 
From: Thomas Muller <thomas.muller@sy...>  20110321 17:28:53

Dear Patrik, would it be possible to send us your exported models? Or, at least send us a scenario that would allow us to reproduce the bug you encounter? So that we have a starting point for investigations. Best regards, Thomas PS: Did you try Project > Clean... of the imported project? Le 21/03/2011 08:34, psihelsk@... a écrit : > Good day, > I had my rodin on computer which got stolen and now have a new > computer (win7) and I installed newest rodin 2.1.1 with Ateler B > provers as I done before. But when I import my old project (which was > exported as backup) I can only see files and cant edit them (open them > only as UML). I cant even start a new project in atelier B. Also when > I look at properties of my project I see there that there is "missing > builder (org.rodin.core.rodinbuilder)". > So I wanted to ask if you can help me with this so I can properly > access my files. > Thank You for hepl. > > Sincerely > > Patrik Sihelsky > > > >  > Colocation vs. Managed Hosting > A question and answer guide to determining the best fit > for your organization  today and in the future. > http://p.sf.net/sfu/internapsfd2d > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser   Thomas MULLER Tél. : (+33)(0)4 42 90 65 66 Engineer in Formal Methods SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Michael Jastram <michael@ja...>  20110321 08:29:41

Dear all, As many of you know, we've been planning for a while to improve the quality of the Rodin documentation. We set up a Wikipage to describe our plans and to collect suggestions and wishes for the documentation: http://wiki.eventb.org/index.php/User_Documentation_Overhaul We are particularly interested in requests from the industrial partners, but of course we will consider everybody's input. You can add your suggestions and wishes directly to the Wiki. If you don't have write access to the Wiki, you can just email me. Thanks,  Michael  Michael Jastram (http://www.jastram.de, +49 (162) 274 83 94) Wissenschaftler, Heinrich Heine Universität Düsseldorf (http://www.stups.uniduesseldorf.de) 1. Vorsitzender, rheinjug e.V. (http://www.rheinjug.de) 
From: <psihelsk@ab...>  20110321 08:10:24

Good day, I had my rodin on computer which got stolen and now have a new computer (win7) and I installed newest rodin 2.1.1 with Ateler B provers as I done before. But when I import my old project (which was exported as backup) I can only see files and cant edit them (open them only as UML). I cant even start a new project in atelier B. Also when I look at properties of my project I see there that there is "missing builder (org.rodin.core.rodinbuilder)". So I wanted to ask if you can help me with this so I can properly access my files. Thank You for hepl. Sincerely Patrik Sihelsky 
From: Laurent Voisin <laurent.voisin@sy...>  20110317 15:39:53

Dear Alexei, Le 16 mars 2011 à 22:02, Alexei Iliasov a écrit : > Regarding cardinality, may I suggest adding the following interactive rule: > > ∀ a, b · a ∈ ℙ(ℕ) ∧ b ⊆ a ∧ finite(a) ⇒ card(a ∖ b) = card(a) − card(b) > > This is a statement via which few other useful cardinalityrelated > properties may be discharged. Thank you very much for this suggestion. I've just added a slightly more general version of this rule in the wiki as SIMP_CARD_SETMINUS (see http://wiki.eventb.org/index.php/Arithmetic_Rewrite_Rules). Matthias, can you please review this new rule of the wiki at your convenience? Cheers, Laurent. 
From: Laurent Voisin <laurent.voisin@sy...>  20110317 15:10:16

Dear Joachim, just a followup to Matthias answer, Le 16 mars 2011 à 21:38, Matthias Schmalz a écrit : >> I found a way to work around the limitation by doing the convergence >> proof not in one step with one invariant that suits all events, but >> rather four separate refinements with four different variants, such that >> only selected events are proven to be convergent, while the others stay >> anticipated. This way, I did not have to simulate a lexicographic >> ordering using multiplication. > > Good. You discovered the trick by yourself. Another trick is to use > finite set variants instead of natural number variants. That allows you > to avoid the detour with card. From a more general point of view, refinement helps to decompose an intricate proof in smaller steps, so that they are more amenable to automation. As concerns variant, as a rule of thumb, either your convergence is based on a counter and then you resort to an integer variant, or it is more general and you rather use inclusion in finite sets as a wellfounded order. It is, in general, a bad idea to emulate such inclusion with cards. Unfortunately, I have no clue about your model contents, so can't give you more detailed advice on this topic. Cheers, Laurent. 
From: Nicolas Beauger <nicolas.beauger@sy...>  20110317 14:19:13

Dear Rodin users, As you probably already heard about on this mailing list, a new version of the platform is out: Rodin 2.1.1. This maintenance release contains bug fixes; it is fully compatible with Rodin 2.1. Here is the release page: http://wiki.eventb.org/index.php/Rodin_Platform_2.1.1_Release_Notes For this new version, we provide an upgrade archive, in order to ease upgrading from Rodin 2.1: rodin2.1.1repo.zip <http://sourceforge.net/projects/rodinbsharp/files/Core_%20Rodin%20Platform/2.1.1/rodin2.1.1repo.zip/download>; Explanations about how to upgrade are given on the release page. We hope you will enjoy this new version: your feedback is welcome. Best regards, Nicolas   Nicolas BEAUGER Tél. : (+33)(0)4 42 90 65 66 Ingénieur Logiciel SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20110317 09:01:04

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Ken, theorems without a proof or "reviewed" instead of a proof would also be fine. But since I have to check their axioms anyway, there is no big difference.  Matthias Ken Robinson schrieb: > Matthias, > > On 17/03/2011, at 07:50 AM, Matthias Schmalz wrote: > >> BEGIN PGP SIGNED MESSAGE >> my personal impression is that support for card (question 1, 2, and 4) >> and for nonlinear arithmetic (question 3) is poor. Therefore I tend to >> avoid them. But this is just my impression, and maybe somebody on the >> list can help you better than me. >> >> If you have to use card or nonlinear arithmetic, you can search the >> wiki for available rules: >> >> http://wiki.eventb.org/index.php/All_Rewrite_Rules >> http://wiki.eventb.org/index.php/Inference_Rules >> >> The AtelierB provers can also prove some facts about them, but it is >> hard to predict which ones. >> >> If my students are frustrated because of such issues, I allow them to >> introduce axioms. (I insist on reviewing their axioms.) Or course, as >> already pointed out on some other mailing list: axioms are evil. > > Why wouldn't you suggest that they present theorems, rather than axioms? At the very least this would reveal those that are reviewed. > > And they cannot be axioms, can they? > > Cheers, > > Ken BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFNgc3CczhznXSdWggRAjxhAJ9fn1NpSBXz5uBbJ/CoyvQ266YOzACeJdZ5 Z3UnKozKV87qaZ6CueT4iQo= =WOV8 END PGP SIGNATURE 
From: Michael Leuschel <leuschel@cs...>  20110317 06:48:41

Hi Joachim, On 16 Mar 2011, at 10:46, Joachim Breitner wrote: > > And now that my model is fully convergent, I need to proof deadlock > freedom. I could not find a functionality for that within Rodin. Do I > need a plugin? You can find counter examples to the deadlock freedom proof obligation using constraint solving with ProB. First, load the machine for animation (http://www.stups.uniduesseldorf.de/ProB/index.php5/Tutorial_Rodin_First_Step). Then, in the ProB Events view click on "Checks > Deadlock Freedom Checking". Note: you can enter a predicate of interest to constrain the search of deadlocks. A recent paper describes this in more detail: http://www.stups.uniduesseldorf.de/~leuschel/publication_detail.php?id=325 As this constraintbased deadlock checking is pretty new functionality, we are particularly interested in feedback and/or models for our regression tests. You can also use model checking to search for deadlocks, by the way: select "Checks > Consistency Checking" with the "Find Deadlock" check box ticked (which it is by default). Greetings, Michael Leuschel 
From: Ken Robinson <kenr@cs...>  20110316 22:38:36

Matthias, On 17/03/2011, at 07:50 AM, Matthias Schmalz wrote: > BEGIN PGP SIGNED MESSAGE > my personal impression is that support for card (question 1, 2, and 4) > and for nonlinear arithmetic (question 3) is poor. Therefore I tend to > avoid them. But this is just my impression, and maybe somebody on the > list can help you better than me. > > If you have to use card or nonlinear arithmetic, you can search the > wiki for available rules: > > http://wiki.eventb.org/index.php/All_Rewrite_Rules > http://wiki.eventb.org/index.php/Inference_Rules > > The AtelierB provers can also prove some facts about them, but it is > hard to predict which ones. > > If my students are frustrated because of such issues, I allow them to > introduce axioms. (I insist on reviewing their axioms.) Or course, as > already pointed out on some other mailing list: axioms are evil. Why wouldn't you suggest that they present theorems, rather than axioms? At the very least this would reveal those that are reviewed. And they cannot be axioms, can they? Cheers, Ken 
From: Alexei Iliasov <alexei.iliasov@nc...>  20110316 21:02:27

Hi all, Regarding cardinality, may I suggest adding the following interactive rule: ∀ a, b · a ∈ ℙ(ℕ) ∧ b ⊆ a ∧ finite(a) ⇒ card(a ∖ b) = card(a) − card(b) This is a statement via which few other useful cardinalityrelated properties may be discharged. Regards, Alexei > BEGIN PGP SIGNED MESSAGE > Hash: SHA1 > > Hi again, > > my personal impression is that support for card (question 1, 2, and 4) > and for nonlinear arithmetic (question 3) is poor. Therefore I tend to > avoid them. But this is just my impression, and maybe somebody on the > list can help you better than me. > > If you have to use card or nonlinear arithmetic, you can search the > wiki for available rules: > > http://wiki.eventb.org/index.php/All_Rewrite_Rules > http://wiki.eventb.org/index.php/Inference_Rules > > The AtelierB provers can also prove some facts about them, but it is > hard to predict which ones. > > If my students are frustrated because of such issues, I allow them to > introduce axioms. (I insist on reviewing their axioms.) Or course, as > already pointed out on some other mailing list: axioms are evil. > >  Matthias > > Joachim Breitner schrieb: >> Hello, >> >> I have progressed sufficiently far with my Rodin project and now want to >> proof termination. My variant involves multiplication (to simulate a >> lexicographic ordering) and cardinality – both areas where Rodin does >> not seem to be very strong. For example, I am not able to proof this >> obligation (which is simple transitivity of< with<=): >> >> ￼hyps:￼ finite(ran(fan)) >> ￼￼ finite(V) >> ￼￼ card(V)≤card(V)∗(1+card(V) − card(ran(fan))) >> ￼￼ 0<card(V) >> goal: 0<card(V)∗(1+card(V) − card(ran(fan))) >> >> This is part of a workaround to hopefully be able to prove this – maybe >> it is possible to obtain it directly? >> >> ￼￼ 0≤card(V) − card(ran(fan)) >> ￼￼ 0<card(V) >> goal: 0<card(V)∗(1+card(V) − card(ran(fan))) >> >> >> I am basically looking for rules such as >> A * C< B * C<=> A< B (if C> 0) >> and >> 0< A& 0< B ==> 0< A * B >> >> >> And while I am at it, is there a way to reason about cardinality of >> images and domains of total and injective functions? Things like >> f : A > B ==> card(ran(f))<= card(dom(f)) >> and f : A>+> B ==> card(ran(f)) = card(dom(f)) >> >> I had to add an axiom to my context stating something that would follow >> from the other axioms if I could express this in Rodin. >> >> Thanks in advance, >> Joachim >> >> >> > BEGIN PGP SIGNATURE > Version: GnuPG v1.4.6 (GNU/Linux) > Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org > > iD8DBQFNgSKxczhznXSdWggRAtQuAJsF+cdehbO9s3o3WXsgD7UWaPud2gCfd7B5 > OWla/QeMc2cCwJ7vrwuWEfg= > =4qfS > END PGP SIGNATURE > >  > Colocation vs. Managed Hosting > A question and answer guide to determining the best fit > for your organization  today and in the future. > http://p.sf.net/sfu/internapsfd2d > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20110316 20:51:06

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Hi again, my personal impression is that support for card (question 1, 2, and 4) and for nonlinear arithmetic (question 3) is poor. Therefore I tend to avoid them. But this is just my impression, and maybe somebody on the list can help you better than me. If you have to use card or nonlinear arithmetic, you can search the wiki for available rules: http://wiki.eventb.org/index.php/All_Rewrite_Rules http://wiki.eventb.org/index.php/Inference_Rules The AtelierB provers can also prove some facts about them, but it is hard to predict which ones. If my students are frustrated because of such issues, I allow them to introduce axioms. (I insist on reviewing their axioms.) Or course, as already pointed out on some other mailing list: axioms are evil.  Matthias Joachim Breitner schrieb: > Hello, > > I have progressed sufficiently far with my Rodin project and now want to > proof termination. My variant involves multiplication (to simulate a > lexicographic ordering) and cardinality – both areas where Rodin does > not seem to be very strong. For example, I am not able to proof this > obligation (which is simple transitivity of < with <=): > > ￼hyps:￼ finite(ran(fan)) > ￼￼ finite(V) > ￼￼ card(V)≤card(V)∗(1+card(V) − card(ran(fan))) > ￼￼ 0<card(V) > goal: 0<card(V)∗(1+card(V) − card(ran(fan))) > > This is part of a workaround to hopefully be able to prove this – maybe > it is possible to obtain it directly? > > ￼￼ 0≤card(V) − card(ran(fan)) > ￼￼ 0<card(V) > goal: 0<card(V)∗(1+card(V) − card(ran(fan))) > > > I am basically looking for rules such as > A * C < B * C <=> A < B (if C > 0) > and > 0 < A & 0 < B ==> 0 < A * B > > > And while I am at it, is there a way to reason about cardinality of > images and domains of total and injective functions? Things like > f : A > B ==> card(ran(f)) <= card(dom(f)) > and f : A >+> B ==> card(ran(f)) = card(dom(f)) > > I had to add an axiom to my context stating something that would follow > from the other axioms if I could express this in Rodin. > > Thanks in advance, > Joachim > > > BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFNgSKxczhznXSdWggRAtQuAJsF+cdehbO9s3o3WXsgD7UWaPud2gCfd7B5 OWla/QeMc2cCwJ7vrwuWEfg= =4qfS END PGP SIGNATURE 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20110316 20:38:23

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Hi Joachim, > I found a way to work around the limitation by doing the convergence > proof not in one step with one invariant that suits all events, but > rather four separate refinements with four different variants, such that > only selected events are proven to be convergent, while the others stay > anticipated. This way, I did not have to simulate a lexicographic > ordering using multiplication. Good. You discovered the trick by yourself. Another trick is to use finite set variants instead of natural number variants. That allows you to avoid the detour with card. > I wish I had a simple indicator function for naturals, but worked around > with variants of the kind "max({stage−2,0})∗(card(V ∖ ran(fan)))" (stage > is 1,2 or 3). > > Also, rodin would happily leave > max({32,0})*... > in the goal. Is there a reason why literals are not automatically > folded? Limited ressources. It's possible to implement such simplifications, but nobody has done it. > I had to add the hypothesis "32=1", which can be proven > automatically, and then with this equality in the list of hypotheses, > replace 32 in the goal. Then rodin automatically calculates the > maximum. Is there a better way that I did not see? Probably not. > Is there a way to distinguish, in the final refinement, an ordinary > event that was never convergent from one that was convergent in an > earlier refinement? > I’d like it to be obvious that all events are > convergent but one special final event. Refinement preserves convergence. I think the default is that only newly convergent events have the status "convergent", but I usually also mark the events as convergent that I have proved to be convergent in an earlier refinement. > And now that my model is fully convergent, I need to proof deadlock > freedom. I could not find a functionality for that within Rodin. Do I > need a plugin? Is it the Flow plugin (which seems to be uninstallable > due to missing plugins)? If there is support for it, then by the flow plugin. You have to find out by yourself. Some time ago, I used the copy paste method, which is of course terrible. > And last but not least, what is the easiest way to get a reportlike > document out of rodin that includes all contexts, models, etc, and maybe > even some statistics about which proofs were automatic and which were > not. The LaTeXPlugin seems only to be able to export individual models, > with 12 models this does not seem like the way people do this. The LaTeXplugin is all we have. Good luck, Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFNgR+vczhznXSdWggRAmQSAJ95h3ZxJIZQgvHFI0YF8u+ncECpOgCfW/2U csccWQAZdSXL+VEICBJOuYw= =5few END PGP SIGNATURE 
From: Thomas Muller <thomas.muller@sy...>  20110316 18:16:58

Dear Pierre, the feature you requested has been previously registered, but has unfortunately not yet been treated and implemented. Here is the link to the registered request https://sourceforge.net/tracker/?func=detail&aid=3152965&group_id=108850&atid=651672 which might also help you to follow the progress and status of its implementation. Best regards, Thomas. Le 15/03/2011 13:45, Pierre Casteran a écrit : > Hello, > > I found it not trivial to prove the theorem: > > axm1 n : NAT1 > axm2 a : 1..n > INT > thm1 : finite(a) > > It required several clicks: an expansion of the constant "finite", > then the use of an auxiliary function (%i. i:1..n  (i > a(i))), etc. > > > > Would it be possible to add to the contextual menu a rule saying that > a function whose domain is finite is finite too? > There is an item in the menu to use the converse of a functon, but it > was useless > in this case. > > > The best, > > Pierre   Thomas MULLER Tél. : (+33)(0)4 42 90 65 66 Engineer in Formal Methods SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Nicolas Beauger <nicolas.beauger@sy...>  20110316 13:24:19

This problem is quite strange, because there was no problem installing Camille and other plugins the other day. After several other attempts, the bug occurred a few times. So at least we can say there is nothing to fix in plugins or in the platform, it's a p2 bug mentioned here and there on the net. I've added an item to the FAQ with the workaround: http://wiki.eventb.org/index.php/FAQ#Software_installation_fails Nicolas Le 15/03/2011 02:52, Ken Robinson a écrit : > Hi Ingo, > > On 15/03/2011, at 12:15 PM, Ingo Weigelt wrote: > >> this could be a p2 bug. Please try to remove the Galileo UpdateSite >> (http://download.eclipse.org/releases/galileo/), then restart Rodin and >> try to install Camille again. (You don't have to manually add the >> Galileo site again.) > OK, thanks. > > I seemed to have to delete the Gallileo Update site twice. After the first and a restart I got the error that is attached to this email. > > I went around again and this time it worked. > > I have no idea why. > > That now means that all the packages I've tried to install have now installed. > > But the ride was a bit bumpy for some reason. > > Cheers, > > Ken > > An error occurred while collecting items to be installed > session context was:(profile=profile, phase=org.eclipse.equinox.internal.p2.engine.phases.Collect, operand=, action=). > No repository found containing: osgi.bundle,org.eclipse.emf.compare,1.0.1.v200909161031 > No repository found containing: osgi.bundle,org.eclipse.emf.compare.diff,1.0.1.v200909161031 > No repository found containing: osgi.bundle,org.eclipse.emf.compare.diff.edit,1.0.1.v200909161031 > No repository found containing: osgi.bundle,org.eclipse.emf.compare.epatch,1.0.1.v200909161031 > No repository found containing: org.eclipse.update.feature,org.eclipse.emf.compare,1.0.1.v200909161031 > No repository found containing: osgi.bundle,org.eclipse.emf.compare.match,1.0.1.v200909161031 > No repository found containing: osgi.bundle,org.eclipse.emf.compare.ui,1.0.1.v200909161031 > >>> I have been unable to install: >>> Camille >>> >>> Camille: gives >>> An error occurred while collecting items to be installed >>> session context was:(profile=profile, phase=org.eclipse.equinox.internal.p2.engine.phases.Collect, operand=, action=). >>> No repository found containing: osgi.bundle,org.eclipse.emf.compare,1.0.1.v200909161031 >>> No repository found containing: osgi.bundle,org.eclipse.emf.compare.diff,1.0.1.v200909161031 >>> No repository found containing: osgi.bundle,org.eclipse.emf.compare.diff.edit,1.0.1.v200909161031 >>> No repository found containing: osgi.bundle,org.eclipse.emf.compare.epatch,1.0.1.v200909161031 >>> No repository found containing: org.eclipse.update.feature,org.eclipse.emf.compare,1.0.1.v200909161031 >>> No repository found containing: osgi.bundle,org.eclipse.emf.compare.match,1.0.1.v200909161031 >>> No repository found containing: osgi.bundle,org.eclipse.emf.compare.ui,1.0.1.v200909161031 >>> > >  > Colocation vs. Managed Hosting > A question and answer guide to determining the best fit > for your organization  today and in the future. > http://p.sf.net/sfu/internapsfd2d > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser >   Nicolas BEAUGER Tél. : (+33)(0)4 42 90 65 66 Ingénieur Logiciel SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  