Interfacing SageMath with an external tool

[meryem afendi]

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

[Sven Köppel]

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

--
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+...@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.

[Nils Bruin]

It sounds like you basically want an IDE-like environment to talk to SageMath. There is already an example of that: the Jupyter Notebook protocol. It is a message-based communication protocol (with normally text-based communication). It is a well-documented protocol that has been implemented in many languages. The "server" side is normally the jupyter notebook (or its more modern successor, jupyterlab), while the "kernel" has been implemented for all sorts of systems and languages: python (and therefore sage), R, julia, etc. In your case, you'd probably want to implement a server-type communication module in Java for easy integration in the IDE of your choice.

Text-based message passing protocols may be too limited for your purposes. The Jupyter message passing protocol can pass binary data too: they communicate image data on a regular basis. It may be that this is enough for your purposes. However, keep in mind that the hard work for computer algebra is generally the *serializing* of the data, not converting it to a text representation.

In the end, sagemath is a python library, so any java/python integration technique should be applicable to sagemath as well.

If you know it's really just desolve that you're interested in, I think your interface question is much more restricted than interfacing with sagemath.The symbolic solvers used by desolve presently are either from Maxima of Fricas, which are both computer algebra systems that run on lisp. So there's already a serialization layer between them to go from lisp to python. You could interface directly. If you're interested in numerical desolvers, then there are a whole bunch of libraries available; some of them used by sagemath, but then also, it is probably better to interface with those libraries from java directly.