Re: [sage-devel] Interfacing SageMath with an external tool
Hi Meryem,
I guess what you are looking for is a sagemath API, or more precisely, a
Python API. The most straightforward approaches which are actually
independent of Java/the JVM are going over the operating system (calling a
shell or system command) or the network (using an Interface such as the
Sage Cell Server or something Jupyter-compatible).
The traditional way over the operating system is least efficient since it
starts sagemath on every call. You can either try to control sage
interactively (probably look for ExpectBuilder), or better, if you know
what you want to do in beforehand, compose a sagemath/python script as a
file and tell sagemath to execute it. This way, you can do your way with
catching stdout or having the sagemath script print its output to another
file which you read after executing the sagemath file. What I propose goes
roughly like (semi pseudocode/Java):
String yourScript = "sage code goes here";
Path input = Paths.get("./sagemath-commands.py")
Path output = Paths.get("./where-sagemath-scripts-writes-to.txt");
Files.writeString(input, yourScript);
Runtime.getRuntime().exec("sage "+scriptPath);
String output = Files.readString(output);
The slowest part here is the execution of sage. Everything else is fine and
typical business with os-level "APIs". Don't forget to check the success of
each operation, in particular the sage execution.
If you need more performance because you run sage more regularly, I suggest
you to look into the Jupyter architecture. It is a modern network
transparent cross-language API which makes it easy to communicate with a
computing system.
All the best,
Sven
Am Mo., 13. Sept. 2021 um 11:29 Uhr schrieb meryem afendi <
meryemafen...@gmail.com>:
> Hello,
> I am Meryem Afendi, a Phd Student at Paris-Est Créteil University. My Phd
> thesis is about formal verification of Cyber Physical Systems (CPSs) using
> the formal method Event-B [1] and its support tool Rodin [2,3]. Rodin is an
> Eclipse-based IDE that allows modelling and verifying systems in Event-B.
> Once an Event-B model is specified and syntactically checked in the Rodin
> Platform, a set of proof obligations is generated by the proof obligation
> generator of the Rodin platform. ThesePOs need to be proved in order to
> ensure the correctness of developments and refinements. They can be proved
> automatically or interactively using the set of provers, like predicate
> provers and SMT solvers as well as external provers.
>
> Currently I am working on interfacing the computer algebra system
> SageMath with the Rodin platform to treat continuous aspects of
> Cyber-Physical Systems in Event-B. The continuous aspects of CPSs are
> generally represented by ordinary differential equations. Our goal is to
> extract a given differential equation from Rodin, send it to SageMath and
> then recover the result in Rodin.
>
> Therefore, I would like to learn:
> -> how can we communicate with SageMath using JAVA in order to send
> the parameters of a given differential equation to the "desolve"
> function for example.
> -> To solve a differential equation using SageMath, we need to define each
> variable separately. How can we automate this without the need to define
> the same variables each time SageMath is called.
> -> Can we send a command script to SageMath.
> -> Can we save the result returned by SageMath in a text file to use it in
> Rodin.
>
> [1] Jean-Raymond Abrial. Modeling in Event-B: System and Software
> Engineering. Cambridge University Press, New York, NY, USA, 1st edition,
> 2010.
> [2] Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thái Son
> Hoàng, Farhad Mehta, and Laurent Voisin. Rodin: an open toolset for
> modelling and reasoning in Event-B. International Journal on Software Tools
> for Technology Transfer, 12(6):447–466, 2010.
> [3] Rodin. User Manual of the RODIN Platform, October 2007.
> http://deployeprints.ecs.soton.ac.uk/11/1/manual-2.3.pdf.
>
> I would like to thank you for your help. If you need more details, don’t
> hesitate to contact me.
>
>
> Best regards,
> Meryem Afendi
>
> --
> You received this message because you are subscribed to the Google Groups
> "sage-devel" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to sage-devel+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/sage-devel/62e4569c-08a7-4b12-903e-f2b4eeed8f0cn%40googlegroups.com
>
> .
>
--
You received this message because you are subscribed to the Google Groups
"sage-devel" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to sage-devel+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/sage-devel/CAExQp%2BX-kKHZf0BSa3p2ufOfg4oB7-LPgPjj-8w7et5AT1HuXg%40mail.gmail.com.
Re: [sage-devel] Re: Outdated instructions in "git the hard way"
On Mon, 13 Sep 2021, 14:35 Thierry, wrote: > Hi, > > On Mon, Sep 13, 2021 at 02:05:36PM +0100, Dima Pasechnik wrote: > > On Fri, 10 Sep 2021, 19:39 Simon King, wrote: > > > > > Hi Dima, > > > > > > On 2021-09-09, Dima Pasechnik wrote: > > > > I think that 'git trac' is mainly used by the release manager - I > > > > won't recommend it to newcomers. > > > > > > No, I'm not a release manager, but I find it very practical to be able > > > to do "git trac pull 12345" instead of doing a series of commands that > > > I simply don't manage to memorise. > > > > > > > assuming that "trac" points to our Git server (as it normally done) this > is > > just > > > > git pull trac > > > This is not "just": your suggestion hides the fact that you have to > copy/paste the name of the ticket branch from a webbrowser, which is > boring and takes time. > > The point of the "git trac" command is to link git branches with trac > tickets, so that you do not have to do it by hand. > I was mainly saying it's not a series of commands, but one command. As well, if this branch name is already in your git tree, you can use tab completion to type it quickly in. > Ciao, > Thierry > > > > > > > > > Best regards, > > > Simon > > > > > > -- > > > You received this message because you are subscribed to the Google > Groups > > > "sage-devel" group. > > > To unsubscribe from this group and stop receiving emails from it, send > an > > > email to sage-devel+unsubscr...@googlegroups.com. > > > To view this discussion on the web visit > > > > https://groups.google.com/d/msgid/sage-devel/shg8p9%2445p%241%40ciao.gmane.io > > > . > > > > > > > -- > > You received this message because you are subscribed to the Google > Groups "sage-devel" group. > > To unsubscribe from this group and stop receiving emails from it, send > an email to sage-devel+unsubscr...@googlegroups.com. > > To view this discussion on the web visit > https://groups.google.com/d/msgid/sage-devel/CAAWYfq3%3Dk9aMWaXPv%2BpGrXtq0rv3VWFESKa5YswnhVvK_3gL2g%40mail.gmail.com > . > > -- > You received this message because you are subscribed to the Google Groups > "sage-devel" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to sage-devel+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/sage-devel/20210913133536.GA17667%40metelu.net > . > -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/CAAWYfq1mZrQsub8qqmcDJWHWR0s28eVEhNH%3DJWLVwfz%2BNNFKKg%40mail.gmail.com.
Re: [sage-devel] Re: Outdated instructions in "git the hard way"
Hi, On Mon, Sep 13, 2021 at 02:05:36PM +0100, Dima Pasechnik wrote: > On Fri, 10 Sep 2021, 19:39 Simon King, wrote: > > > Hi Dima, > > > > On 2021-09-09, Dima Pasechnik wrote: > > > I think that 'git trac' is mainly used by the release manager - I > > > won't recommend it to newcomers. > > > > No, I'm not a release manager, but I find it very practical to be able > > to do "git trac pull 12345" instead of doing a series of commands that > > I simply don't manage to memorise. > > > > assuming that "trac" points to our Git server (as it normally done) this is > just > > git pull trac This is not "just": your suggestion hides the fact that you have to copy/paste the name of the ticket branch from a webbrowser, which is boring and takes time. The point of the "git trac" command is to link git branches with trac tickets, so that you do not have to do it by hand. Ciao, Thierry > > > Best regards, > > Simon > > > > -- > > You received this message because you are subscribed to the Google Groups > > "sage-devel" group. > > To unsubscribe from this group and stop receiving emails from it, send an > > email to sage-devel+unsubscr...@googlegroups.com. > > To view this discussion on the web visit > > https://groups.google.com/d/msgid/sage-devel/shg8p9%2445p%241%40ciao.gmane.io > > . > > > > -- > You received this message because you are subscribed to the Google Groups > "sage-devel" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to sage-devel+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/sage-devel/CAAWYfq3%3Dk9aMWaXPv%2BpGrXtq0rv3VWFESKa5YswnhVvK_3gL2g%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/20210913133536.GA17667%40metelu.net.
[sage-devel] Cplex 20.1
I tried the last version of cplex (20.1) with sagemath and so far it's working well. The previous version was 12.10. I had a look at the release note and I don't see any deprecation that may be problematic for us https://www.ibm.com/docs/en/icos/20.1.0?topic=2010-release-notes-cplex Best, David. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/b15bbc37-ec68-4e42-ad79-b5b273ba8849n%40googlegroups.com.
Re: [sage-devel] Re: Outdated instructions in "git the hard way"
On Fri, 10 Sep 2021, 19:39 Simon King, wrote: > Hi Dima, > > On 2021-09-09, Dima Pasechnik wrote: > > I think that 'git trac' is mainly used by the release manager - I > > won't recommend it to newcomers. > > No, I'm not a release manager, but I find it very practical to be able > to do "git trac pull 12345" instead of doing a series of commands that > I simply don't manage to memorise. > assuming that "trac" points to our Git server (as it normally done) this is just git pull trac > Best regards, > Simon > > -- > You received this message because you are subscribed to the Google Groups > "sage-devel" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to sage-devel+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/sage-devel/shg8p9%2445p%241%40ciao.gmane.io > . > -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/CAAWYfq3%3Dk9aMWaXPv%2BpGrXtq0rv3VWFESKa5YswnhVvK_3gL2g%40mail.gmail.com.
[sage-devel] Interfacing SageMath with an external tool
Hello, I am Meryem Afendi, a Phd Student at Paris-Est Créteil University. My Phd thesis is about formal verification of Cyber Physical Systems (CPSs) using the formal method Event-B [1] and its support tool Rodin [2,3]. Rodin is an Eclipse-based IDE that allows modelling and verifying systems in Event-B. Once an Event-B model is specified and syntactically checked in the Rodin Platform, a set of proof obligations is generated by the proof obligation generator of the Rodin platform. ThesePOs need to be proved in order to ensure the correctness of developments and refinements. They can be proved automatically or interactively using the set of provers, like predicate provers and SMT solvers as well as external provers. Currently I am working on interfacing the computer algebra system SageMath with the Rodin platform to treat continuous aspects of Cyber-Physical Systems in Event-B. The continuous aspects of CPSs are generally represented by ordinary differential equations. Our goal is to extract a given differential equation from Rodin, send it to SageMath and then recover the result in Rodin. Therefore, I would like to learn: -> how can we communicate with SageMath using JAVA in order to send the parameters of a given differential equation to the "desolve" function for example. -> To solve a differential equation using SageMath, we need to define each variable separately. How can we automate this without the need to define the same variables each time SageMath is called. -> Can we send a command script to SageMath. -> Can we save the result returned by SageMath in a text file to use it in Rodin. [1] Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York, NY, USA, 1st edition, 2010. [2] Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thái Son Hoàng, Farhad Mehta, and Laurent Voisin. Rodin: an open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer, 12(6):447–466, 2010. [3] Rodin. User Manual of the RODIN Platform, October 2007. http://deployeprints.ecs.soton.ac.uk/11/1/manual-2.3.pdf. I would like to thank you for your help. If you need more details, don’t hesitate to contact me. Best regards, Meryem Afendi -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/62e4569c-08a7-4b12-903e-f2b4eeed8f0cn%40googlegroups.com.
