Maude-help mailing list

[Ozan Kahramanogullari <ozan.kah AT gmail.com>]

Thank you, Steven and Santiago! This works. I am trying to make it work smoothly also with the Python binders. Including the "set" statement there in the Maude file achieves this but, a programmatic solution would be nicer. Looking at the documentation, this does not seem to be the case at the moment.

Best regards,

Ozan

=======================

 Ozan Kahramanoğulları, PhD

              ozan-k.com       

=======================

On Mon, 27 Feb 2023 at 23:42, Santiago Escobar <sescobar AT upv.es> wrote:

Dear Ozan, 

just type “set trace on .” before executing the search command.

Also there are some graphical tools for animating Maude programs that show all kinds of internal information. 

For example <http://safe-tools.dsic.upv.es/anima/>

Best,

—Santiago 

On 27 Feb 2023, at 20:11, Ozan Kahramanogullari <ozan.kah AT gmail.com> wrote:

Hi,

I am experimenting with some of my system modules and I could not find a simple solution to the following problem. I was wondering if someone could help.

Consider the following module.

mod S is
  sorts Atom Structure .
  subsort Atom < Structure .
  ops a b : -> Atom .

  op -_ : Atom -> Atom [ prec 50 ].
  op [_,_] : Structure Structure -> Structure [assoc comm ] .
  op {_,_} : Structure Structure -> Structure [assoc comm ] .

 var R T U : Structure . var A : Atom .

  rl [rls] : [ { R , T } , U ] => { [ R , U ] , T } .
endm

I do a one-step search as follows, which behaves as expected.

search in S : [[{a,b},{a,b}],{[- a,- b],[- a,- b]}] =>1 X .

Solution 1 (state 1)

states: 2  rewrites: 1 in 0ms cpu (0ms real) (11764 rewrites/second)

X --> {[- a,- b],[- a,[- b,[{a,b},{a,b}]]]}

Solution 2 (state 2)

states: 3  rewrites: 2 in 0ms cpu (0ms real) (17391 rewrites/second)

X --> [{a,b},{[- a,- b],[- a,[- b,{a,b}]]}]

Solution 3 (state 3)

states: 4  rewrites: 3 in 0ms cpu (0ms real) (20689 rewrites/second)

X --> {b,[a,[{[- a,- b],[- a,- b]},{a,b}]]}

Solution 4 (state 4)

states: 5  rewrites: 4 in 0ms cpu (0ms real) (23529 rewrites/second)

X --> [{[- a,- b],[- a,- b]},{b,[a,{a,b}]}]

Solution 5 (state 5)

states: 6  rewrites: 5 in 0ms cpu (0ms real) (25510 rewrites/second)

X --> [{a,b},{b,[a,{[- a,- b],[- a,- b]}]}]

Solution 6 (state 6)

states: 7  rewrites: 6 in 0ms cpu (0ms real) (27027 rewrites/second)

X --> {a,[b,[{[- a,- b],[- a,- b]},{a,b}]]}

Solution 7 (state 7)

states: 8  rewrites: 7 in 0ms cpu (0ms real) (28340 rewrites/second)

X --> [{[- a,- b],[- a,- b]},{a,[b,{a,b}]}]

Solution 8 (state 8)

states: 9  rewrites: 8 in 0ms cpu (0ms real) (29520 rewrites/second)

X --> [{a,b},{a,[b,{[- a,- b],[- a,- b]}]}]

No more solutions.

states: 9  rewrites: 8 in 0ms cpu (0ms real) (26755 rewrites/second)

The question is how can I get the information on the substitution in each solution? What I am looking for is not the X's substitution, but the subterms with which R, T, and U of the rule are matched. How can I get this information?

Thanks in advance!

Ozan

=======================

 Ozan Kahramanoğulları, PhD

              ozan-k.com       

=======================