Maude-help mailing list

[Santiago Escobar <sescobar AT upv.es>]

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       

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

Attachment: smime.p7s
Description: S/MIME cryptographic signature