maude-help AT lists.siebelschool.illinois.edu

Subject: Maude-help mailing list

List archive

Re: [[maude-help] ] Maude external connection while model-checking

From: Rubén Rafael Rubio Cuéllar <rubenrub AT ucm.es>
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: Re: [[maude-help] ] Maude external connection while model-checking
Date: Fri, 26 Jul 2024 13:30:17 +0200

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.

[[maude-help] ] Maude external connection while model-checking, Feliu Gabaldon, Marco A (LARC-D320)[RSES], 07/25/2024
- Re: [[maude-help] ] Maude external connection while model-checking, Francisco Durán, 07/26/2024
  - Re: [[maude-help] ] Maude external connection while model-checking, Rubén Rafael Rubio Cuéllar, 07/26/2024
    - Re: [[maude-help] ] [EXTERNAL] Re: Maude external connection while model-checking, Feliu Gabaldon, Marco A (LARC-D320)[RSES], 07/29/2024