maude-help AT lists.siebelschool.illinois.edu

Subject: Maude-help mailing list

List archive

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

From: "Feliu Gabaldon, Marco A (LARC-D320)[RSES]" <marco.feliu AT nasa.gov>
To: "maude-help AT lists.cs.illinois.edu" <maude-help AT lists.cs.illinois.edu>
Subject: [[maude-help] ] Maude external connection while model-checking
Date: Thu, 25 Jul 2024 19:48:32 +0000

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.

[[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