rodin-b-sharp-user Mailing List for RODIN

Dear All,

I am glad to announce that Rodin 3.9 is available. You can either install it from SourceForge (https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.9/) or use the update mechanism of Eclipse.
Rodin 3.9 brings several bug fixes. It also upgrades the underlying Eclipse to 2023-12 (4.30), which can be run by Java 17 Runtimes.
Rodin will work on macOS, Linux and Windows 64-bit computers. You need to have a 64-bit Java JRE (version 17 or later) installed on your computer to run Rodin.

----
macOS caveats
----
The Rodin application is not notarized. This means that when you download it from SourceForge, macOS will quarantine the application and tell you that it is broken. Just run the command "xattr -rc Rodin.app" in a Terminal to remove the quarantine tag.

----
Important information
----
Please read the Rodin Platform release notes before proceeding with an upgrade.

See https://wiki.event-b.org/index.php/Rodin_Platform_3.9_Release_Notes

----
Fixed Bugs and Implemented Features
----
bug #829: Autorewriter generates invalid proof rule
bug #828: Trace debug/rodintypes/verbose doesn't work
bug #827: Post-tactic applied after a tactic failure
bug #826: NullPointerException in hypothesis page UI
bug #824: Exception related to proof tree UI update
bug #823: Do not allow prime in extension symbol
bug #822: Error handling when loading formula extensions
bug #821: Issues with proof tree filtering
bug #819: "Prove Automatically" setting not persisted
bug #818: Hypothesis hiding by eh/he 

Feature Requests
——
FR #403: User provided names for fresh variables
FR #400: Add factory method to check if symbol is valid
FR #398: Rewrite rule for recursive exponentiation
FR #396: New reasoners on inductive types
FR #395: Manual application of compset simplification rules
FR #394: Rule for functional image
FR #393: Simplify set membership of min/max
FR #392: Simplify bool(B=TRUE) to B
FR #385: Better message for syntax errors in set comprehension
FR #383: Additional inference rule for finiteness
FR #368: Better simplification of identity

This release would not have happened without the support from the Event-B Rodin Plus project funded by the French National Research Agency (ANR).

Best Regards,
---
Idir AIT SADOUNE
Associate Professor 

CentraleSupelec - Computer Science Department
LMF - Formal Methods Laboratory  
Paris-Saclay University
www.idiraitsadoune.com <https://www.idiraitsadoune.com/>
+33/0 1 75 31 78 46 

Dear Colin,

> On 24 Apr 2024, at 17:35, Hogben, Colin H <Col...@uk...> wrote:
> 
> - When editing text in the Rodin editor, a mini light bulb icon appears just to the left; the hover text is "Content Assist Available (Ctrl + Space)" but ctrl+space does nothing.  Should it do something?

It should provide some kind of content completion. This is a known bug in that editor; it has not been fixed yet.
https://sourceforge.net/p/rodin-b-sharp/bugs/793/

> - In one project (in 4.7) in the Event-B Explorer, a machine has a mini-icon overlaying the top-left of the "M" icon - looks a bit like some sort of "file" icon.  I guess it's trying to tell me something, but what?


This icon merely indicates that the component (machine, in your case) has a non-empty comment.
It does not indicate any kind of error or warning, but can be helpful to determine at a glance which components are documented and which ones are not.

I can’t provide any help regarding your issues with Camille, sorry.

Best regards,
Guillaume Verdier

Hi,

Having spent some time using Rodin (following examples and tutorials 
etc.) there are number of things I've seen in the Rodin UI which I'd 
like help to understand.

- While editing with Camille, sometimes there is a red cross icon at the 
bottom left by the end of file.  There are no Rodin Problems, and 
hovering over it gets nothing.  Should I worry?

- Sometimes I have seen a warning triangle icon at the top left of the 
edit window; hovering over it gets e.g. "Warnings: 2".  Again no Rodin 
problems, so what are the warnings?

- When editing text in the Rodin editor, a mini light bulb icon appears 
just to the left; the hover text is "Content Assist Available (Ctrl + 
Space)" but ctrl+space does nothing.  Should it do something?

- When I add an event or invariant in Camille and then save, sometimes 
(always?) no Proof Obligations are added.  But if I perform similar 
modifications using the Rodin editor, new POs are added.  I'd expect the 
addition of POs to be a function of the underlying model rather than the 
particular editor being used.

- In one project (in 4.7) in the Event-B Explorer, a machine has a 
mini-icon overlaying the top-left of the "M" icon - looks a bit like 
some sort of "file" icon.  I guess it's trying to tell me something, but 
what?

Any guidance appreciated.
Thanks,
-- 
Colin Hogben
Software/Control Engineer
UK Atomic Energy Authority
Tel: +44 1235 464948

Dear All,

I am glad to announce that the first release candidate of Rodin 3.9 is available. You can install it from SourceForge (https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.9-RC1/). This release is based on the latest Eclipse 2023-12 (4.30) and contains numerous bug fixes.
Rodin will work on macOS (both x86_64 and aarch 64 architectures), Linux and Windows 64-bit computers. You need to have a 64-bit Java JRE (version 17 or later) installed on your computer to run Rodin.

We are interested in getting as much feedback as possible, especially about bugs or usage issues, before publishing the final release. Please do not hesitate to report anything that looks strange to you.

Caution: This is a release candidate. This means that it has not been extensively tested and may contain many bugs, some being nasty. Please do not use it for anything important.

macOS caveats
----
The Rodin application is not notarized. This means that when you download it from SourceForge, macOS will quarantine the application and tell you that it is broken. Just run the command "xattr -rc Rodin.app" in a Terminal to remove the quarantine tag.

Note: If you open an existing workspace (set of projects) with this release, this workspace will not work anymore with prior releases of Rodin. We encourage you to duplicate your workspace to avoid any issue.

Best Regards,
---
Idir AIT SADOUNE
Associate Professor 

CentraleSupelec - Computer Science Department
LMF - Formal Methods Laboratory  
Paris-Saclay University
www.idiraitsadoune.com <https://www.idiraitsadoune.com/>
+33/0 1 75 31 78 46 

On 12/04/2024 11:07, I wrote:

> The good news is that I've now installed Rodin in a debian VM and have 
> managed to install the Atelier B provers.

An email from Son sent me in the direction of uml-b.org from which I 
found the versions at https://github.com/eventB-Soton/Rodin-Bundles and 
have been using those in preference (both Windows and Linux) and have 
tracked down the Rodin manual and worked through the traffic-light 
example.  Though I did have to change methode-b.com to atelierb.eu to 
get the provers.

I also note in passing that handbook.event-b.org seems broken (returns 
404 to everything AFAICT).

-- 
Colin Hogben
Software/Control Engineer
UK Atomic Energy Authority
Tel: +44 1235 464948

On 11/04/2024 17:11, Tsutomu Kobayashi wrote:

> I used to have the same issue; my Java VM could not communicate over
> SSL. In my case, I needed to import an SSL certificate file provided by
> my workplace into the Java trust store and specify it with a command
> line option when launching Rodin.

Thanks to Son / Tsutomo / Manuel for your various suggestions.  I think 
it may well be to do with our site firewall which I believe does devious 
MITM stuff, requiring trusting its CA.  I was trying to run the Windows 
version, since the site-provided Linux platform was too old (Scientific 
Linux 7 + java 1.8).

I also tried on my ubuntu 22.04 machine at home last night and had a 
similar but different error "PKIX path building failed: 
sun.security.provider.certpath.SunCertPathBuilderException: unable to 
find valid certification path to requested target" for both http and 
https URLs which I conjecture may be due to openjdk-11 not having an up 
to date list of CA certs.

The good news is that I've now installed Rodin in a debian VM and have 
managed to install the Atelier B provers.

-- 
Colin Hogben
Software/Control Engineer
UK Atomic Energy Authority
Tel: +44 1235 464948

Dear Colin,

I used to have the same issue; my Java VM could not communicate over 
SSL. In my case, I needed to import an SSL certificate file provided by 
my workplace into the Java trust store and specify it with a command 
line option when launching Rodin.

Please try the following:
1. Import the certificate with keytool:
    https://docs.oracle.com/cd/E19906-01/820-4916/geygn/index.html
2. Launch Rodin as follows:
    $ rodin -Djavax.net.ssl.trustStore=/path/to/trust-store-file

Hope this helps.


Best regards,
Tsutomu

-- 
Tsutomu Kobayashi, Ph.D.
Japan Aerospace Exploration Agency (JAXA)
https://researchmap.jp/tsutomu.kobayashi?lang=en

On 2024/04/11 22:25, Son Hoang via Rodin-b-sharp-user wrote:
> Dear Colin,
> 
> I just checked and the address 
> http://www.atelierb.eu/update_site/atelierb_provers 
> <http://www.atelierb.eu/update_site/atelierb_provers> works for me. I am 
> wondering if any firewalls prevent you from accessing that update site.
> 
> Best regards,
> 
> Son
> 
> -- 
> 
> Dr Son Hoang
> 
> ECS, University of Southampton
> 
> SO17 1BJ, Southampton
> 
> UK
> 
> *From: *rod...@li... 
> <rod...@li...>
> *Date: *Thursday, 11 April 2024 at 14:14
> *To: *rod...@li... 
> <rod...@li...>
> *Subject: *Rodin-b-sharp-user Digest, Vol 158, Issue 1
> 
> [You don't often get email from 
> rod...@li.... Learn why this is 
> important at https://aka.ms/LearnAboutSenderIdentification 
> <https://aka.ms/LearnAboutSenderIdentification> ]
> 
> CAUTION: This e-mail originated outside the University of Southampton.
> 
> Send Rodin-b-sharp-user mailing list submissions to
>          rod...@li...
> 
> To subscribe or unsubscribe via the World Wide Web, visit
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user <https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user>
> or, via email, send a message with subject or body 'help' to
>          rod...@li...
> 
> You can reach the person managing the list at
>          rod...@li...
> 
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Rodin-b-sharp-user digest..."
> 
> 
> Today's Topics:
> 
>     1. New user unable to find Atelier B provers (Hogben, Colin H)
> 
> 
> ----------------------------------------------------------------------
> 
> Message: 1
> Date: Thu, 11 Apr 2024 11:39:27 +0100
> From: "Hogben, Colin H" <Col...@uk...>
> To: rod...@li...
> Subject: [Rodin-b-sharp-user] New user unable to find Atelier B
>          provers
> Message-ID: <fd8...@uk...>
> Content-Type: text/plain; charset=UTF-8; format=flowed
> 
> Hi,
> 
> I'm trying to evaluate rodin as a potential tool to use in a project,
> but have hit a bump at an early stage.
> 
> Having downloaded and started rodin-3.8.0, I've been unable to install
> the Atelier B provers.  The provided URL
> http://www.atelierb.eu/update_site/atelierb_provers <http://www.atelierb.eu/update_site/atelierb_provers> resulted in an
> Eclipse "ProvisionException"; checking with curl showed that this URL
> redirects to the https: version but then to a 404 page.
> 
> The wiki page 
> https://wiki.event-b.org/index.php/Rodin_Platform_Releases <https://wiki.event-b.org/index.php/Rodin_Platform_Releases>
> mentions 
> http://methode-b.com/update_site/atelierb_provers <http://methode-b.com/update_site/atelierb_provers> but
> methode-b.com just redirects to atelierb.eu (as does bmethod.com)
> 
> Can somebody point me to a working location for this plugin?
> 
> Thanks,
> --
> Colin Hogben
> Software/Control Engineer
> UK Atomic Energy Authority
> Tel: +44 1235 464948
> 
> 
> 
> ------------------------------
> 
> 
> 
> ------------------------------
> 
> Subject: Digest Footer
> 
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user <https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user>
> 
> 
> ------------------------------
> 
> End of Rodin-b-sharp-user Digest, Vol 158, Issue 1
> **************************************************
> 
> 
> 
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user

Sometimes the web access libraries are configured not to establish
connections to http addresses because the communication is not
encrypted.  Try editing the URL to be https .  That happened to a
student of mine earlier this semester.

Best / Saludos,

Manuel



On Thu, 11 Apr 2024 14:34:58 +0000, rod...@li... wrote:

> Send Rodin-b-sharp-user mailing list submissions to
> 	rod...@li...
> 
> To subscribe or unsubscribe via the World Wide Web, visit
> 	https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user
> or, via email, send a message with subject or body 'help' to
> 	rod...@li...
> 
> You can reach the person managing the list at
> 	rod...@li...
> 
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Rodin-b-sharp-user digest..."
> 
> 
> Today's Topics:
> 
>    1. Re: Rodin-b-sharp-user Digest, Vol 158, Issue 1 (Son Hoang)
> 
> 
> ----------------------------------------------------------------------
> 
> Message: 1
> Date: Thu, 11 Apr 2024 13:25:32 +0000
> From: Son Hoang <T.S...@so...>
> To: "rod...@li..."
> 	<rod...@li...>
> Subject: Re: [Rodin-b-sharp-user] Rodin-b-sharp-user Digest, Vol 158,
> 	Issue 1
> Message-ID:
> 	<LO2P265MB30533D3F3E9DAB23F4D2CBDDE7052@LO2P265MB3053.GBRP265.PROD.OUTLOOK.COM>
> 	
> Content-Type: text/plain; charset="cp1258"
> 
> Dear Colin,
> I just checked and the address http://www.atelierb.eu/update_site/atelierb_provers works for me. I am wondering if any firewalls prevent you from accessing that update site.
> Best regards,
> Son
> 
> --
> Dr Son Hoang
> ECS, University of Southampton
> SO17 1BJ, Southampton
> UK
> 
> From: rod...@li... <rod...@li...>
> Date: Thursday, 11 April 2024 at 14:14
> To: rod...@li... <rod...@li...>
> Subject: Rodin-b-sharp-user Digest, Vol 158, Issue 1
> [You don't often get email from rod...@li.... Learn why this is important at https://aka.ms/LearnAboutSenderIdentification ]
> 
> CAUTION: This e-mail originated outside the University of Southampton.
> 
> Send Rodin-b-sharp-user mailing list submissions to
>         rod...@li...
> 
> To subscribe or unsubscribe via the World Wide Web, visit
>         https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.sourceforge.net%2Flists%2Flistinfo%2Frodin-b-sharp-user&data=05%7C02%7Ct.s.hoang%40soton.ac.uk%7C988cfa766fc544e3c93c08dc5a294673%7C4a5378f929f44d3ebe89669d03ada9d8%7C0%7C0%7C638484380548446854%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=XOZTPPAWdme5mS6TqACY25%2B1wqMGkRSYZLwMguSUY%2Fk%3D&reserved=0<https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user>
> or, via email, send a message with subject or body 'help' to
>         rod...@li...
> 
> You can reach the person managing the list at
>         rod...@li...
> 
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Rodin-b-sharp-user digest..."
> 
> 
> Today's Topics:
> 
>    1. New user unable to find Atelier B provers (Hogben, Colin H)
> 
> 
> ----------------------------------------------------------------------
> 
> Message: 1
> Date: Thu, 11 Apr 2024 11:39:27 +0100
> From: "Hogben, Colin H" <Col...@uk...>
> To: rod...@li...
> Subject: [Rodin-b-sharp-user] New user unable to find Atelier B
>         provers
> Message-ID: <fd8...@uk...>
> Content-Type: text/plain; charset=UTF-8; format=flowed
> 
> Hi,
> 
> I'm trying to evaluate rodin as a potential tool to use in a project,
> but have hit a bump at an early stage.
> 
> Having downloaded and started rodin-3.8.0, I've been unable to install
> the Atelier B provers.  The provided URL
> https://eur03.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.atelierb.eu%2Fupdate_site%2Fatelierb_provers&data=05%7C02%7Ct.s.hoang%40soton.ac.uk%7C988cfa766fc544e3c93c08dc5a294673%7C4a5378f929f44d3ebe89669d03ada9d8%7C0%7C0%7C638484380548459586%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=%2FjFV2vLYNFgj1eDg2pjg08kTOgO4eU0PM4wEoe24YAg%3D&reserved=0<http://www.atelierb.eu/update_site/atelierb_provers> resulted in an
> Eclipse "ProvisionException"; checking with curl showed that this URL
> redirects to the https: version but then to a 404 page.
> 
> The wiki page https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwiki.event-b.org%2Findex.php%2FRodin_Platform_Releases&data=05%7C02%7Ct.s.hoang%40soton.ac.uk%7C988cfa766fc544e3c93c08dc5a294673%7C4a5378f929f44d3ebe89669d03ada9d8%7C0%7C0%7C638484380548467912%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=TppegR%2FQ6KEaxQFu%2Bu%2FpB79rtL3TtLltd%2BDsRvfL9jg%3D&reserved=0<https://wiki.event-b.org/index.php/Rodin_Platform_Releases>
> mentions https://eur03.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmethode-b.com%2Fupdate_site%2Fatelierb_provers&data=05%7C02%7Ct.s.hoang%40soton.ac.uk%7C988cfa766fc544e3c93c08dc5a294673%7C4a5378f929f44d3ebe89669d03ada9d8%7C0%7C0%7C638484380548476743%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=g6JIpqC0ceGrkoy3pj2VIEI1apn688Pj4szJ7J0g3tg%3D&reserved=0<http://methode-b.com/update_site/atelierb_provers> but
> methode-b.com just redirects to atelierb.eu (as does bmethod.com)
> 
> Can somebody point me to a working location for this plugin?
> 
> Thanks,
> --
> Colin Hogben
> Software/Control Engineer
> UK Atomic Energy Authority
> Tel: +44 1235 464948
> 
> 
> 
> ------------------------------
> 
> 
> 
> ------------------------------
> 
> Subject: Digest Footer
> 
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.sourceforge.net%2Flists%2Flistinfo%2Frodin-b-sharp-user&data=05%7C02%7Ct.s.hoang%40soton.ac.uk%7C988cfa766fc544e3c93c08dc5a294673%7C4a5378f929f44d3ebe89669d03ada9d8%7C0%7C0%7C638484380548484858%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=QlTQseh9LwIOyLqirMiLJUs8Ync5pzvnkcktNnJ7EMM%3D&reserved=0<https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user>
> 
> 
> ------------------------------
> 
> End of Rodin-b-sharp-user Digest, Vol 158, Issue 1
> **************************************************
> -------------- next part --------------
> An HTML attachment was scrubbed...
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: A?nh ma?n hi?nh 2024-04-11 lu?c 14.16.33.jpg
> Type: image/jpeg
> Size: 93682 bytes
> Desc: A?nh ma?n hi?nh 2024-04-11 lu?c 14.16.33.jpg
> 
> ------------------------------
> 
> 
> 
> ------------------------------
> 
> Subject: Digest Footer
> 
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user
> 
> 
> ------------------------------
> 
> End of Rodin-b-sharp-user Digest, Vol 158, Issue 2
> **************************************************
> 
> 

-- 
 Manuel Carro                              : manuel.carro@{upm.es,imdea.org}
 Associate Professor, School of CS, UPM    : http://www.fi.upm.es       
 Director, IMDEA Software Institute        : https://software.imdea.org  
 Board of Directors, Informatics Europe    : https://www.informatics-europe.org/
 Madrid, Spain                             : +34-91-101-2202 ext. 4140  

Dear Colin,
I just checked and the address http://www.atelierb.eu/update_site/atelierb_provers works for me. I am wondering if any firewalls prevent you from accessing that update site.
Best regards,
Son

--
Dr Son Hoang
ECS, University of Southampton
SO17 1BJ, Southampton
UK

From: rod...@li... <rod...@li...>
Date: Thursday, 11 April 2024 at 14:14
To: rod...@li... <rod...@li...>
Subject: Rodin-b-sharp-user Digest, Vol 158, Issue 1
[You don't often get email from rod...@li.... Learn why this is important at https://aka.ms/LearnAboutSenderIdentification ]

CAUTION: This e-mail originated outside the University of Southampton.

Send Rodin-b-sharp-user mailing list submissions to
        rod...@li...

To subscribe or unsubscribe via the World Wide Web, visit
        https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.sourceforge.net%2Flists%2Flistinfo%2Frodin-b-sharp-user&data=05%7C02%7Ct.s.hoang%40soton.ac.uk%7C988cfa766fc544e3c93c08dc5a294673%7C4a5378f929f44d3ebe89669d03ada9d8%7C0%7C0%7C638484380548446854%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=XOZTPPAWdme5mS6TqACY25%2B1wqMGkRSYZLwMguSUY%2Fk%3D&reserved=0<https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user>
or, via email, send a message with subject or body 'help' to
        rod...@li...

You can reach the person managing the list at
        rod...@li...

When replying, please edit your Subject line so it is more specific
than "Re: Contents of Rodin-b-sharp-user digest..."


Today's Topics:

   1. New user unable to find Atelier B provers (Hogben, Colin H)


----------------------------------------------------------------------

Message: 1
Date: Thu, 11 Apr 2024 11:39:27 +0100
From: "Hogben, Colin H" <Col...@uk...>
To: rod...@li...
Subject: [Rodin-b-sharp-user] New user unable to find Atelier B
        provers
Message-ID: <fd8...@uk...>
Content-Type: text/plain; charset=UTF-8; format=flowed

Hi,

I'm trying to evaluate rodin as a potential tool to use in a project,
but have hit a bump at an early stage.

Having downloaded and started rodin-3.8.0, I've been unable to install
the Atelier B provers.  The provided URL
https://eur03.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.atelierb.eu%2Fupdate_site%2Fatelierb_provers&data=05%7C02%7Ct.s.hoang%40soton.ac.uk%7C988cfa766fc544e3c93c08dc5a294673%7C4a5378f929f44d3ebe89669d03ada9d8%7C0%7C0%7C638484380548459586%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=%2FjFV2vLYNFgj1eDg2pjg08kTOgO4eU0PM4wEoe24YAg%3D&reserved=0<http://www.atelierb.eu/update_site/atelierb_provers> resulted in an
Eclipse "ProvisionException"; checking with curl showed that this URL
redirects to the https: version but then to a 404 page.

The wiki page https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwiki.event-b.org%2Findex.php%2FRodin_Platform_Releases&data=05%7C02%7Ct.s.hoang%40soton.ac.uk%7C988cfa766fc544e3c93c08dc5a294673%7C4a5378f929f44d3ebe89669d03ada9d8%7C0%7C0%7C638484380548467912%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=TppegR%2FQ6KEaxQFu%2Bu%2FpB79rtL3TtLltd%2BDsRvfL9jg%3D&reserved=0<https://wiki.event-b.org/index.php/Rodin_Platform_Releases>
mentions https://eur03.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmethode-b.com%2Fupdate_site%2Fatelierb_provers&data=05%7C02%7Ct.s.hoang%40soton.ac.uk%7C988cfa766fc544e3c93c08dc5a294673%7C4a5378f929f44d3ebe89669d03ada9d8%7C0%7C0%7C638484380548476743%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=g6JIpqC0ceGrkoy3pj2VIEI1apn688Pj4szJ7J0g3tg%3D&reserved=0<http://methode-b.com/update_site/atelierb_provers> but
methode-b.com just redirects to atelierb.eu (as does bmethod.com)

Can somebody point me to a working location for this plugin?

Thanks,
--
Colin Hogben
Software/Control Engineer
UK Atomic Energy Authority
Tel: +44 1235 464948



------------------------------



------------------------------

Subject: Digest Footer

_______________________________________________
Rodin-b-sharp-user mailing list
Rod...@li...
https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.sourceforge.net%2Flists%2Flistinfo%2Frodin-b-sharp-user&data=05%7C02%7Ct.s.hoang%40soton.ac.uk%7C988cfa766fc544e3c93c08dc5a294673%7C4a5378f929f44d3ebe89669d03ada9d8%7C0%7C0%7C638484380548484858%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=QlTQseh9LwIOyLqirMiLJUs8Ync5pzvnkcktNnJ7EMM%3D&reserved=0<https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user>


------------------------------

End of Rodin-b-sharp-user Digest, Vol 158, Issue 1
**************************************************

Hi,

I'm trying to evaluate rodin as a potential tool to use in a project, 
but have hit a bump at an early stage.

Having downloaded and started rodin-3.8.0, I've been unable to install 
the Atelier B provers.  The provided URL 
http://www.atelierb.eu/update_site/atelierb_provers resulted in an 
Eclipse "ProvisionException"; checking with curl showed that this URL 
redirects to the https: version but then to a 404 page.

The wiki page https://wiki.event-b.org/index.php/Rodin_Platform_Releases 
mentions http://methode-b.com/update_site/atelierb_provers but 
methode-b.com just redirects to atelierb.eu (as does bmethod.com)

Can somebody point me to a working location for this plugin?

Thanks,
-- 
Colin Hogben
Software/Control Engineer
UK Atomic Energy Authority
Tel: +44 1235 464948

Hi,

We believe that this issue is caused by a bug introduced in Rodin 3.8
related to the handling of rewritten equalities, which are incorrectly
being hidden. Therefore, provers like ML do not have access to these
equalities and may fail to prove goals that were proved in previous
versions. It will be fixed in version 3.9, for which a release candidate
will be published soon.

Best regards,
Guillaume Verdier

On Thursday, March 14, 2024 09:36 CET, Manuel Carro <man...@im...> wrote:

> 
> Hi!  I was wondering whether there has been any change in the
> post/auto-tactics in Rodin 3.8?  There were some (simple) proofs that
> were discharged automatically in Rodin 3.7 that are not discharged in
> 3.8.  It is not a big deal, because they can be discharged with a simple
> interaction with the Atelier B provers, but since I am using Rodin as a
> teaching tool, its behavior is now out of sync with my class notes, so I
> have to do some extra explanation to my students.
> 
> Some more details: It seems that in Rodin 3.7 there was a time early in
> the automatically-generated proof tree where ML was invoked and the
> proof was discharged.  In Rodin 3.8 this invocation does not take place;
> instead, a key formula is removed from the hypotheses and the proof
> cannot continue.
> 
> Thanks!
> -- 
>  Manuel Carro                              : manuel.carro@{upm.es,imdea.org}
>  Associate Professor, School of CS, UPM    : http://www.fi.upm.es       
>  Director, IMDEA Software Institute        : https://software.imdea.org  
>  Board of Directors, Informatics Europe    : https://www.informatics-europe.org/
>  Madrid, Spain                             : +34-91-101-2202 ext. 4140

Thanks a lot, Guillaume.  That makes sense!


Best / Saludos,

Manuel


On Thu, 14 Mar 2024 15:12:58 +0100, "Guillaume VERDIER" <Gui...@ir...> wrote:

> Hi,
> 
> We believe that this issue is caused by a bug introduced in Rodin 3.8
> related to the handling of rewritten equalities, which are incorrectly
> being hidden. Therefore, provers like ML do not have access to these
> equalities and may fail to prove goals that were proved in previous
> versions. It will be fixed in version 3.9, for which a release candidate
> will be published soon.
> 
> Best regards,
> Guillaume Verdier
> 
> On Thursday, March 14, 2024 09:36 CET, Manuel Carro
> <man...@im...> wrote:
> 
> > 
> > Hi!  I was wondering whether there has been any change in the
> > post/auto-tactics in Rodin 3.8?  There were some (simple) proofs that
> > were discharged automatically in Rodin 3.7 that are not discharged in
> > 3.8.  It is not a big deal, because they can be discharged with a simple
> > interaction with the Atelier B provers, but since I am using Rodin as a
> > teaching tool, its behavior is now out of sync with my class notes, so I
> > have to do some extra explanation to my students.
> > 
> > Some more details: It seems that in Rodin 3.7 there was a time early in
> > the automatically-generated proof tree where ML was invoked and the
> > proof was discharged.  In Rodin 3.8 this invocation does not take place;
> > instead, a key formula is removed from the hypotheses and the proof
> > cannot continue.
> > 
> > Thanks!
> > -- 
> >  Manuel Carro                              : manuel.carro@{upm.es,imdea.org}
> >  Associate Professor, School of CS, UPM    : http://www.fi.upm.es       
> >  Director, IMDEA Software Institute        : https://software.imdea.org  
> >  Board of Directors, Informatics Europe :
> > https://www.informatics-europe.org/
> >  Madrid, Spain                             : +34-91-101-2202 ext. 4140
> 
> 

-- 
 Manuel Carro                              : manuel.carro@{upm.es,imdea.org}
 Associate Professor, School of CS, UPM    : http://www.fi.upm.es       
 Director, IMDEA Software Institute        : https://software.imdea.org  
 Board of Directors, Informatics Europe    : https://www.informatics-europe.org/
 Madrid, Spain                             : +34-91-101-2202 ext. 4140  

Hi!  I was wondering whether there has been any change in the
post/auto-tactics in Rodin 3.8?  There were some (simple) proofs that
were discharged automatically in Rodin 3.7 that are not discharged in
3.8.  It is not a big deal, because they can be discharged with a simple
interaction with the Atelier B provers, but since I am using Rodin as a
teaching tool, its behavior is now out of sync with my class notes, so I
have to do some extra explanation to my students.

Some more details: It seems that in Rodin 3.7 there was a time early in
the automatically-generated proof tree where ML was invoked and the
proof was discharged.  In Rodin 3.8 this invocation does not take place;
instead, a key formula is removed from the hypotheses and the proof
cannot continue.

Thanks!
-- 
 Manuel Carro                              : manuel.carro@{upm.es,imdea.org}
 Associate Professor, School of CS, UPM    : http://www.fi.upm.es       
 Director, IMDEA Software Institute        : https://software.imdea.org  
 Board of Directors, Informatics Europe    : https://www.informatics-europe.org/
 Madrid, Spain                             : +34-91-101-2202 ext. 4140  

=======================================
            ProB 1.13.0
=======================================

We are happy to announce version 1.13.0 of the animator and model checker ProB.

The command-line version and the standalone Tcl/Tk version of ProB
are available for download at the ProB website:
	https://www3.hhu.de/stups/prob/index.php/Download#Latest_Release

If you have already installed the ProB plug-in within Rodin you
can simply use the update mechanism of Eclipse to get the new version of the plug-in.
Otherwise, to install ProB for Rodin, 
 first download Rodin 3.8, 
 choose Help -> Install New Software and 
 simply choose the pre-configured ProB update site
 (http://www.stups.hhu.de/prob_updates_rodin3).
More detailed installation instructions and a brief tutorial can be found here:
	http://www.stups.hhu.de/ProB/index.php5/Tutorial_Rodin_First_Step
	
We are also preparing a new release of the ProB2-UI user-interface based on JavaFX.
A snapshot version of this UI is available at:
    https://prob.hhu.de/w/index.php?title=Download#ProB2-UI
This new user interface of ProB can directly load Rodin models from Rodin workspaces.

You can also create Jupyter Notebooks in B using the ProB Jupyter Kernel:
    https://www3.hhu.de/stups/prob/index.php/Download#ProB_Jupyter_Kernel
    
In addition to Atom and VIM there is now support for the VSCode editor:
    https://prob.hhu.de/w/index.php?title=Editors_for_ProB#VSCode

A new release of the ProB Java API (also known as ProB2) has also been published:
  https://central.sonatype.com/artifact/de.hhu.stups/de.prob2.kernel/4.13.0
The Maven information is:
<dependency>
    <groupId>de.hhu.stups</groupId>
    <artifactId>de.prob2.kernel</artifactId>
    <version>4.13.0</version>
</dependency>

A lot of work went in these releases; here are a few recent
improvements made to ProB:

 - Rodin theory support improvements: 
    - support recursive inductive datatypes including recursive operators,
    - allow to use theory operators in REPL (console), VisB, trace replay files, etc.,
    - improved feedback for operators in state view,
    - improved event error feedback,
    - allow real literals and B formulas (between $) in ptm files,
    - check WD of operators (if TRY_FIND_ABORT is true within ProB2-UI only at the moment),
 - Unicode improvements:
    - support Unicode oftype operator (0x2982)
    - superset and contains_element Unicode symbols can be used within B expressions
 - Template strings surrounded by triple backquotes, expressions in template marked by ${.} or $«.»
   ```1+1=${1+1}``` is equivalent to "1+1="^TO_STRING(1+1) and evaluates to "1+1=2"
   (currently curly braces are disallowed inside template expression)
 - operations/events can be annotated with a description pragma at the end (/*@ desc "..." */),
   descriptions are visible in hovers/context menus of the state view and in VisB HTML trace exports;
   for Event-B models these descriptions can be placed in the Rodin comment field of an event
 - new variable refinement hierarchy diagram for Event-B models (e.g., probcli -dot variable_hierarchy FILE)
 - new external functions SIGN and LCM (least common multiple) in LibraryMath.def,
   and improved constraint solving for ABS, GCD and SIGN
 - VisB: support groups and the "use" element, VISB_SVG_OBJECTS can now also
   have fields with dynamic values (i.e., no separate VISB_SVG_UPDATES definition is required)
   and event and predicate fields (i.e., no separate VISB_SVG_EVENT definition is required)
 - new external function READ_JSON in LibraryXML.def to readin JSON files in same format as READ_XML
 - Tcl/Tk editor performs Latex (\cup,....) to Unicode conversions upon space or control-space
   and code completion (also for Latex commands above) upon tab,
   ProB2-UI editor does completion upon control-space
 - Monte Carlo Tree Search (MCTS) available for specifications which define GAME_OVER, GAME_PLAYER,
   GAME_VALUE definitions. MCTS tree can be visualised graphically.
   MCTS commands are available by right-clicking in Tk operations view.
   MCTS_AUTO_PLAY and RANDOM_ANIMATE are available as special event names for VisB.

The full release history can be found here: https://prob.hhu.de/w/index.php?title=ProB_Release_History


Best regards,
The ProB team
https://prob.hhu.de/w/index.php?title=Team

Dear Mathieu,

This is indeed the appropriate place for asking  question about the Rodin platform and plugins.

Welcome !

If you encounter any bug or would like some new feature to be implemented, you can also create a ticket in SourceForge.

Cheers,
Laurent.

> Le 2 oct. 2023 à 09:16, Marchand Mathieu via Rodin-b-sharp-user <rod...@li...> a écrit :
> 
> Hello,
>  
> I’m probably going to start a project with Rodin in the context of my master thesis, and I was wondering before starting if there are any active community channels to seek for help in case of problems or any contact emails.
> I saw on the wiki there used to be, but none of them exists anymore except this mailing list.
>  
> Thank you in advance for your answers,
>  
> Bests,
>  
> Mathieu
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li... <mailto:Rod...@li...>
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user

Hello,

I'm probably going to start a project with Rodin in the context of my master thesis, and I was wondering before starting if there are any active community channels to seek for help in case of problems or any contact emails.
I saw on the wiki there used to be, but none of them exists anymore except this mailing list.

Thank you in advance for your answers,

Bests,

Mathieu

Dear Sanjay,

The .mch file type is used by Atelier B. This is a plain text file format.

There used to be a Rodin plugin for converting from .mch files to .bum files.

However, I am not aware of any plugin doing the reverse conversion.

Cheers,
Laurent.

> Le 8 juin 2023 à 15:54, ANANDA Sanjay <San...@st...> a écrit :
> 
> Hello,
> 
> I am Sanjay Ananda and currently pursuing masters in Aerospace Engineering in ISAE Supaero, France. We are working on a project which requires the use of .mch files of a model. When we export model from rodin platform, we are getting file formats other than .mch like .bum etc.,. Requesting to please let me know if there is a method to export rodin files as .mch files or a tool which can convert rodin files to .mch files
> 
> Thanks and Regards,
> Sanjay Ananda​​​​​​ _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user

Hello,

I am Sanjay Ananda and currently pursuing masters in Aerospace Engineering in ISAE Supaero, France. We are working on a project which requires the use of .mch files of a model. When we export model from rodin platform, we are getting file formats other than .mch like .bum etc.,. Requesting to please let me know if there is a method to export rodin files as .mch files or a tool which can convert rodin files to .mch files

Thanks and Regards,
Sanjay Ananda​​​​​​

(appologies for multiple copies of this message)

**The 17th International Symposium on Theoretical Aspects of Software Engineering (TASE 2023)**
- Call for participation

Date : July 4 to July 6, 
Venue : Bristol, UK
Website : https://bristolpl.github.io/tase2023/


The 17th International Symposium on Theoretical Aspects of Software Engineering (TASE 2023) will be held in Bristol, UK on July 4-6, 2023. Modern society is increasingly dependent on software systems that are becoming larger and more complex. This poses new challenges to the various aspects of software engineering, for instance, software dependability in trusted computing, interaction with physical components in cyber physical systems, quality assurance in AI systems, distribution in cloud computing applications, security and privacy in general. Hence, new concepts and methodologies are required to enhance the development of software engineering from theoretical aspects.

TASE 2023 aims to provide a forum for people from academia and industry to communicate their latest results on innovative advances in software engineering. TASE 2023 is the 17th in the TASE series. The past TASE symposia were successfully held in Shanghai ('07), Nanjing ('08), Tianjin ('09), Taipei ('10), Xi'an ('11), Beijing ('12), Birmingham ('13), Changsha ('14), Nanjing ('15), Shanghai ('16), Nice ('17), Guangzhou ('18), Guilin ('19), Hangzhou ('20), Shanghai ('21), Cluj ('22).


The conference is now accepting registration!

- Deadline for standard registration: 14 June 2023
- Deadline for late registration: 29 June 2023

For more details on the registration process, please visit the dedicated webpage: https://bristolpl.github.io/tase2023/registration.html


An Eye on the Program
---------------------

In addition to over 20 peer-reviewed high-quality submissions, the conference proposes 3 invited keynotes of interest:
- Stefan Kiefer (University of Oxford)
- Naijun Zhan (Chinese Academy of Sciences)
- Peter Schrammel (Diffblue)

Details for the keynotes can be found on the website here: https://bristolpl.github.io/tase2023/invited-talks.html
The list of accepted papers is available here: https://bristolpl.github.io/tase2023/accepted-papers.html


Venue
-----

The conference will take place at Clifton Hill House in the beautiful and vibrant city of Bristol, United Kingdom. Take a look at the conference's website for anything about accommodations and details regarding access to the venue and travelling to UK.

We are looking forward to welcoming you in Great Britain!


The Organizing Committee.

Dear Alfredo,

> Le 23 mai 2023 à 14:27, Alfredo Capozucca <alf...@un...> a écrit :
> 
> When navigating a project using the Event-B explorer, under the entry "Proof Obligations" it can be found the discharged proofs.
> 
> Some of these proofs have a label "A". I want to confirm some hypotheses on this label. I believe that:
> 
> 1- when the label A appears over a discharged proof, it means the proof has been automatically completed by Roding without calling any external tool (e.g. ML, Z3, CVC4).
> 
> 2- any discharged proof without holding the label A, means that it was proven either manually or relying on an external tool.
> 
> Could you please confirm if my hypotheses are correct or not?

This is not exactly that. Then the A label just means that the proof obligation was discharged without any user intervention (A for automatically).

In the preferences, you can define the Auto-tactic that should be used to discharge proof obligations automatically.

Then, depending on what is in your Auto-tactic, external provers can be part or not of the proof. By default, only the Atelier B provers are part of the Auto-tactic.

If you install the SMT solvers, then you can change the Auto-tactic to « Default Auto Tactic with SMT » to also include these SMT solvers, in addition to Atelier B.

Finally, in the contextual menu of proof obligations, you have the « Recalculate Auto-status » that attempts again at discharging proof obligations with the current Auto-tactic and add missing A labels.

I hope this makes it clearer.

Cheers,
Laurent.

=======================================
            ProB 1.12.1
=======================================

We are happy to announce version 1.12.1 of the animator and model checker ProB.

We are also happy to announce that ProB has received the first edition of the
Alain Colmerauer Prolog Heritage Prize
as part of the 50 year celebrations of Prolog.

The command-line version and the standalone Tcl/Tk version of ProB
are available for download at the ProB website:
	https://www3.hhu.de/stups/prob/index.php/Download#Latest_Release

If you have already installed the ProB plug-in within Rodin you
can simply use the update mechanism of Eclipse to get the new version of the plug-in.
Otherwise, to install ProB for Rodin, 
 first download Rodin 3.8, 
 choose Help -> Install New Software and 
 simply choose the pre-configured ProB update site
 (http://www.stups.hhu.de/prob_updates_rodin3).
More detailed installation instructions and a brief tutorial can be found here:
	http://www.stups.hhu.de/ProB/index.php5/Tutorial_Rodin_First_Step
	
We are also preparing a new release of the ProB2-UI user-interface based on JavaFX.
A snapshot version of this UI is available at:
    https://prob.hhu.de/w/index.php?title=Download#ProB2-UI
This new user interface of ProB can directly load Rodin models from Rodin workspaces.

You can also create Jupyter Notebooks in B using the ProB Jupyter Kernel:
    https://www3.hhu.de/stups/prob/index.php/Download#ProB_Jupyter_Kernel
    
In addition to Atom and VIM there is now support for the VSCode editor
which will be updated in the coming days:
    https://www3.hhu.de/stups/prob/index.php/Editors_for_ProB#VSCode

A new release of the ProB Java API (also known as ProB2) has also been published:
  https://central.sonatype.com/artifact/de.hhu.stups/de.prob2.kernel/4.12.1
The Maven information is:
<dependency>
    <groupId>de.hhu.stups</groupId>
    <artifactId>de.prob2.kernel</artifactId>
    <version>4.12.1</version>
</dependency>

A lot of work went in these releases; here are a few recent
improvements made to ProB:

 - ProB keeps track call stack information for improved
   error messages
 - performance improvements in the parser and the constraint solving kernel
 - new LTL operators: unchanged, changed, increasing, decreasing, BA
   for example "G( changed({x}) => [Event])" or "G([Event] => decreasing({x*2+y}))"
 - VisB improvements for more convenient and faster visualizations
   https://prob.hhu.de/w/index.php?title=VisB#VisB_Additional_SVG_Objects
 - Improved support for floats, min/max can be applied to sets of floats, ...
 - Improve Event-B theory support, AUTO_DETECT_THEORY_MAPPING preference so that standard Rodin
   theories work without .ptm mapping file; support for simple Sigma/Pi operators on sets of values,
   support for Real/Float theories:
   https://prob.hhu.de/w/index.php?title=Event-B_Theories
 - Improvements in the Z3 backend and a new CDCL(T) solver
 - New syntax in classical B: allow to use Event-B style set comprehensions,
   e.g., {x·x:1..10|x*x} = {1,4,9,16,25,36,49,64,81,100}
   and allow prj1/prj2 to be applied without type arguments

This version of ProB is no longer available for 32-bit systems.
For 32-bit version you have to look at https://www3.hhu.de/stups/prob/index.php/DownloadPriorVersions.

The full release history can be found here: https://www3.hhu.de/stups/prob/index.php/ProB_Release_History


Best regards,
The ProB team
https://www3.hhu.de/stups/prob/index.php/Team

Hi,

When navigating a project using the Event-B explorer, under the entry 
"Proof Obligations" it can be found the discharged proofs.

Some of these proofs have a label "A". I want to confirm some hypotheses 
on this label. I believe that:

1- when the label A appears over a discharged proof, it means the proof 
has been automatically completed by Roding without calling any external 
tool (e.g. ML, Z3, CVC4).

2- any discharged proof without holding the label A, means that it was 
proven either manually or relying on an external tool.

Could you please confirm if my hypotheses are correct or not?

Looking forward to your reply.

-Alfredo.

Hello Manuel,

Try these steps: 
1. adding the hypothesis H1=card(S)>=1, it is discharged easly.
2. adding the hypothsis card(S)=1, it gives the goal \exists x. S={0}, put x =0
3. call the prover.

It works for me.

Amel
  
----- Mail original -----
De: "Manuel Carro" <man...@im...>
À: rod...@li...
Envoyé: Dimanche 7 Mai 2023 22:37:07
Objet: [Rodin-b-sharp-user] Help with proof related to sets?

Hi.  I have a simple proof, but I am failing to make Rodin discharge it.
It appears in the realm of a larger example, but the core of the
unfinished proof is:

CONSTANT S
axm1: S ⊆ ℕ      <not theorem>
axm2: finite(S)   <not theorem>
axm3: card(S) ≤ 1 <not theorem>
axm4: 0 ∈ S      <not theorem>
axm5: S = {0}     <theorem>

I.e., deduce that S = {0} based on the previous axioms.

If axm3 is substitute for card(S) = 1, it is immediately discharged.
But card(S) = 1 should not be difficult to infer, because S has at least
one element (because of axm4) and S cannot have more than one element
(because of axm3).  Any idea of what (else) could be necessary, or what
I am not doing right?

BTW, I am using Rodin 3.7 in Linux.

Thanks in advance!
-- 
 Manuel Carro                              : manuel.carro@{upm.es,imdea.org}
 Associate Professor, School of CS, UPM    : http://www.fi.upm.es       
 Director, IMDEA Software Institute        : https://software.imdea.org  
 Informatics Europe                        : https://www.informatics-europe.org/
 EIT Digital Spain                         : https://www.eitdigital.eu/
 Madrid, Spain                             : +34-91-101-2202 ext. 4140  


_______________________________________________
Rodin-b-sharp-user mailing list
Rod...@li...
https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user

Hi.  I have a simple proof, but I am failing to make Rodin discharge it.
It appears in the realm of a larger example, but the core of the
unfinished proof is:

CONSTANT S
axm1: S ⊆ ℕ      <not theorem>
axm2: finite(S)   <not theorem>
axm3: card(S) ≤ 1 <not theorem>
axm4: 0 ∈ S      <not theorem>
axm5: S = {0}     <theorem>

I.e., deduce that S = {0} based on the previous axioms.

If axm3 is substitute for card(S) = 1, it is immediately discharged.
But card(S) = 1 should not be difficult to infer, because S has at least
one element (because of axm4) and S cannot have more than one element
(because of axm3).  Any idea of what (else) could be necessary, or what
I am not doing right?

BTW, I am using Rodin 3.7 in Linux.

Thanks in advance!
-- 
 Manuel Carro                              : manuel.carro@{upm.es,imdea.org}
 Associate Professor, School of CS, UPM    : http://www.fi.upm.es       
 Director, IMDEA Software Institute        : https://software.imdea.org  
 Informatics Europe                        : https://www.informatics-europe.org/
 EIT Digital Spain                         : https://www.eitdigital.eu/
 Madrid, Spain                             : +34-91-101-2202 ext. 4140  

The 10th Rodin User and Developer Workshop, 30th May, 2023, Nancy, France

Rodin Workshop 2023 Website<http://wiki.event-b.org/index.php/Rodin_Workshop_2023>

The 10th Rodin workshop will be collocated with the ABZ 2023 Conference<https://abz2023.loria.fr/>.

The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers.

For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort.

If you are interested in giving a presentation at the Rodin workshop or have a plug-in to demonstrate, send a short abstract (1 or 2 pages PDF) to ro...@ec...<mailto:ro...@ec...?subject=%5BRodinWorkshop2023%5D%20Contribution> by 28th April 2023 indicating whether it is a tool usage or tool development presentation.

We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B.

The proceedings of the workshop will be available as a technical report at the University of Southampton.

Organisers

Dana Dghaym, University of Southampton

Laurent Voisin, Systerel

Fabian Vu, Heinrich Heine University Düsseldorf

Neeraj Kumar Singh, INPT-ENSEEIHT / IRIT, Univeristy of Toulouse