## 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 2016 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 (4) Nov (9) Dec (1) Jan (4) Feb (4) Mar (10) Apr (5) May (8) Jun (1) Jul (5) Aug Sep Oct Nov Dec
S M T W T F S

1

2

3

4
(1)
5

6

7

8

9

10

11

12

13

14

15

16

17

18

19
(3)
20

21

22

23

24
(1)
25

26

27

28
(2)
29
(2)
30

31

Showing 9 results of 9

 Re: [Rodin-b-sharp-user] basic question about sets From: Alexei Iliasov - 2011-10-29 15:11:48 ```Hi, Event-B context sets are mutually disjoint by definition (I suspect it is due to the typing system of Event-B). Thus, yours S1 and S2 must be subsets of some other set, say set S. context c sets S constants S1, S2, a,b,c,d,e axioms @a1 S1 <: S @a2 S2 <: S @a3 S1 = {a,b,c} @a3 S2 = {a,d,e} you might also want to say that a,b, ... are distinct elements. Regards, Alexei > Hi everyone, > > I am first sorry for a very basic question, since I am very new to > Event-B and Rodin. > > I created 2 sets S1 = {a,b,c} , S2= {a,d,e}, it informs that there are > mistakes because of the > common element a between 2 sets. > > How can i represent such 2 sets. > > Thank you all in advance. > > Anh Le > > ```
 [Rodin-b-sharp-user] basic question about sets From: Anh Le - 2011-10-29 15:03:02 Attachments: Message as HTML ```Hi everyone, I am first sorry for a very basic question, since I am very new to Event-B and Rodin. I created 2 sets S1 = {a,b,c} , S2= {a,d,e}, it informs that there are mistakes because of the common element a between 2 sets. How can i represent such 2 sets. Thank you all in advance. Anh Le ```
 Re: [Rodin-b-sharp-user] Question about lists From: Issam Maamria - 2011-10-28 14:18:03 Attachments: Message as HTML ```Hi Juan, The support for the operators you described (lists and sequences) can be added thanks to the Theory plug-in. Lists and sequences are included in the theory library which can be downloaded from SourceForge. I am currently working on the next version of both the plug-in and the library, and that should be available next week. Finally, you said the theories you defined do not work with Rodin 2.3. They should, but just in case, can you please (if possible) send zipped MathExtensions project to check for any bugs? Regards Issam On 28 October 2011 11:23, Juan Ignacio Perna wrote: > Hi there, > > Apologies for the very basic question but I am only getting started > with Event-B/Rodin and haven't managed to find an answer to it online. > > The question is regarding support for lists/sequences in Rodin. I know > this can be done, the question is whether I should encode it myself or > there is some sort or repository where the 'theory' can > downloaded/imported from. In case I have to define it myself, is the > general advise to use the 'theory' plugin? I have recently updated to > the latest release of Rodin and that made some toy theories I had > defined unusable as the plugin is not compatible with the new version > of Rodin... > > Kind Regards, > > Juan > > > ------------------------------------------------------------------------------ > The demand for IT networking professionals continues to grow, and the > demand for specialized networking skills is growing even more rapidly. > Take a complimentary Learning@... Self-Assessment and learn > about Cisco certifications, training, and career opportunities. > http://p.sf.net/sfu/cisco-dev2dev > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > ```
 [Rodin-b-sharp-user] Question about lists From: Juan Ignacio Perna - 2011-10-28 10:23:12 ```Hi there, Apologies for the very basic question but I am only getting started with Event-B/Rodin and haven't managed to find an answer to it online. The question is regarding support for lists/sequences in Rodin. I know this can be done, the question is whether I should encode it myself or there is some sort or repository where the 'theory' can downloaded/imported from. In case I have to define it myself, is the general advise to use the 'theory' plugin? I have recently updated to the latest release of Rodin and that made some toy theories I had defined unusable as the plugin is not compatible with the new version of Rodin... Kind Regards, Juan ```
 [Rodin-b-sharp-user] New version of Event-B Statemachines v1.0.0 From: vs2 - 2011-10-24 15:54:40 Attachments: Message as HTML ``` Dear Rodin users and developers, A new version of Event-B Statemachines plug-in v1.0.0 is released, now supporting both variable and enumerated set translation. Animation add-on for this version is not yet complete, but will be released very soon. Regards, Vitaly Savicks```
 Re: [Rodin-b-sharp-user] Soundness From: Matthias Schmalz - 2011-10-19 15:39:30 ```Hi Karim, Rodin's external provers do not output proofs or certificates and therefore need to be trusted. Occasionally, these provers have been unsound. See the Rodin bug tracker for more information. -Matthias Am 19.10.2011 17:12, schrieb karim kanso: > Hello, > > Im new to the RODIN platform and was wondering if anyone could point me > in the right > direction where I can find information relating to the soundness of the > integration of external > provers. What assurances does RODIN come with that the proofs are valid, > e.g. does it check > the correctness of traces produced by the external tools, are the tools > certified/verified? > > Ive searched the wiki, but have found very little mention of the > soundness of external tools. > > > Thanks, > Karim Kanso > Swansea University > > > > ------------------------------------------------------------------------------ > All the data continuously generated in your IT infrastructure contains a > definitive record of customers, application performance, security > threats, fraudulent activity and more. Splunk takes this data and makes > sense of it. Business sense. IT sense. Common sense. > http://p.sf.net/sfu/splunk-d2d-oct > > > > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```
 [Rodin-b-sharp-user] Soundness From: karim kanso - 2011-10-19 15:12:46 Attachments: Message as HTML ```Hello, Im new to the RODIN platform and was wondering if anyone could point me in the right direction where I can find information relating to the soundness of the integration of external provers. What assurances does RODIN come with that the proofs are valid, e.g. does it check the correctness of traces produced by the external tools, are the tools certified/verified? Ive searched the wiki, but have found very little mention of the soundness of external tools. Thanks, Karim Kanso Swansea University ```
 [Rodin-b-sharp-user] SMT Solvers Plug-in v0.1.0 released From: Yoann Guyot - 2011-10-19 14:54:46 ```Dear Rodin Users, I am delighted to announce the release of the SMT Solvers Plug-in for Rodin v2.3. 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 Méthodes Formelles SYSTEREL ------------------------------------------------------------------------ Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr ------------------------------------------------------------------------ ```
 [Rodin-b-sharp-user] New Rodin 2.3 Release From: Nicolas Beauger - 2011-10-04 16:47:12 ```Dear all, We are delighted to announce that Rodin 2.3 is now available. Here is the link to the release notes: http://wiki.event-b.org/index.php/Rodin_Platform_2.3_Release_Notes which tells how to upgrade or download. Please take care with this release, as it is not forward compatible with Rodin 2.2.x. It means that once you have opened a workspace or imported a project into Rodin 2.3, you might have problems opening them later on with Rodin 2.2.x or less. So we strongly advise to make backup copies of your models, or to use new workspaces. We hope you will enjoy this new release. As always, your feedback is welcome ! Best regards, The Rodin Team -- ------------------------------------------------------------------------ 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 ------------------------------------------------------------------------ ```

Showing 9 results of 9