Maude-help mailing list

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

Hi All,

Ruben pointed to a different feature in the binders that achieves this functionality. I include his response below in case it might also be useful to others.

Best regards,

Ozan

Tracing can be enabled from the Python side with maude.input('set trace on .\n'), but the traces will still be printed to the terminal and you cannot access them programmatically. However, you can use the Term.apply method to obtain the matching substitution of a one-step rewrite.

for term, subs, ctx, rl in myTerm.apply(None):
	# code to deal with each rewrite

Here, term is the rewritten term, subs the substitution object, ctx the matching context, and rl the rule that has been applied. That is, the term ctx(subs.instantiate(rl.getRhs())) is term. The argument None can be replaced by a string label to apply only rules with that label.

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

 Ozan Kahramanoğulları, PhD

              ozan-k.com       

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

On Tue, 28 Feb 2023 at 19:39, Steven Eker <eker AT csl.sri.com> wrote:

You might want to suggest this feature to Rubén.

Steven

On 2/28/23 01:31, Ozan Kahramanogullari wrote:

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       

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