Maude-help mailing list

["Feliu Gabaldon, Marco A (LARC-D320)[RSES]" <marco.feliu AT nasa.gov>]

Thank you, Francisco and Ruben, for your quick answers!

 

We are going to give it a try through the Python bindings, and we will let you know how it goes.

 

I will try to keep our communication with the rest of the community flowing , Francisco.

 

Thank you very much!

 

Marco A.

 

 

From: Rubén Rafael Rubio Cuéllar <rubenrub AT ucm.es>
Date: Friday, July 26, 2024 at 7:30 AM
To: Feliu Gabaldon, Marco A (LARC-D320)[RSES] <marco.feliu AT nasa.gov>
Cc: Francisco Durán <fdm AT uma.es>, maude-help AT lists.cs.illinois.edu <maude-help AT lists.cs.illinois.edu>
Subject: [EXTERNAL] Re: [[maude-help] ] Maude external connection while model-checking

CAUTION: This email originated from outside of NASA.  Please take care when clicking links or opening attachments.  Use the "Report Message" button to report suspicious messages to the NASA SOC.

Hi Marco,

Just to complement the previous answer, another option for defining hooks in Maude is using the Maude Python bindings. In the documentation, there is a section that explains how hooks can be defined so that the reduction (or rewriting) of a Maude symbol triggers the evaluation of a Python function, whose results are then passed back to Maude. There is also an example in the repository.

However, these hooks only work when Maude commands are started from Python. You can reduce the modelCheck(...) term has shown in the first example of the documentation, or better, using the built-in model checker API (there is an example here).

Best regards, Rubén.