Maude-help mailing list

[Francisco Durán <fdm AT uma.es>]

Hi Marco,

You are right, Maude does not allow messages to external objects in 
executions of the model checker or search commands. 

Future releases of Maude may support such uses in the case of stateless and 
deterministic invocations to external objects for verification purposes, 
however, as I said, it is not currently supported. 

The only way I can think of getting such a behavior in the current Maude is 
using hooks, but that would imply writing C++ code and compiling your own 
version of Maude. As you may know, the special attributes allow you to 
connect Maude operators with C++ functions. There have been experiences in 
the past connecting Maude to termination checkers, SMT solvers, etc., or 
simply adding new operations on strings, using hooks. Basically, one could 
define a Maude operator that is internally handled as a built-in function, 
solved by C++ code that is in charge of connecting to the external tool and 
placing back the result. 

The main problem with this path is that there is no documentation on how to 
do it other than the comments in Maude's source code. I'm sure there must be 
people that have developed hooks I'm not aware of. There was an attempt a few 
years back of joining different versions of Maude with hooks for different 
purposes, but that was discontinued. The git repo is still at 
https://urldefense.com/v3/__https://github.com/maude-team/maude__;!!DZ3fjg!61rXWdnu5I_pYte1kZrI7Qi5VdhhpCM6GF1HeeDBZ74P7uSXIiQ5umnzyXAnVMhRwk0-J7olv1_XJ09Aee2yOg$
 . There there are branches for different hook developments that were merged 
into one common source. Perhaps it can be of use in learning the basics. 

If I can do anything else to help, please, let me know. Also, I'd appreciate 
any info on your future developments and suggestions. 

Cheers, 

F. Durán



> On 25 Jul 2024, at 21:48, Feliu Gabaldon, Marco A (LARC-D320)[RSES] 
> <marco.feliu AT nasa.gov> wrote:
> 
> Hi everybody,
>  We have connected Maude to an external system that produces data 
> deterministically using external objects.
>  We had in mind using (embedding) that connection inside a bigger 
> non-deterministic rewriting system while performing model-checking, so that 
> the rewriting of the whole system is partially computed by Maude and 
> partially by our external system. After some tests we are starting to think 
> that it is impossible, since there does not seem to be any way to 
> `erewrite` inside a deterministic context such as a call to the 
> model-checker.
>  Are we wrong? Does anybody have any advice about how to achieve something 
> like this?
>  Thank you.
>  Marco A.