Maude-help mailing list

[Francisco Duran <duran AT lcc.uma.es>]

Martin,

Thanks for your email, and my apologies for answering so late.

There seems to be a bug in Full Maude, I'll fix it ASAP. I'll come back to you 
once it's fixed.

Paco


mp463634 AT mail.inf.tu-dresden.de
 wrote:

> Hello,
>
> I am playing around with FullMaude 2.1 and parameterized modules, thinking
> of the very simple graph theory with a module for finite paths over a
> graph
>
> think of the very simple example code
> **********************
> (fth graph is
>         sorts N E .
>         ops s t : E -> N .
> endfth)
>
> (fmod path(G :: graph) is
>         sort P(G) .
>         subsort 
> G@E
>  < P(G) .
>         op _;_ : P(G) P(G) ~> P(G) [assoc] .
>
>         ops s t : P(G) -> 
> G@N
>  .
>         cmb g:P`(G`) ; h:P`(G`) : P(G) if t(g:P`(G`)) = s(h:P`(G`)) .
>
>         var g h : P(G) .
>
>         ceq s(g ; h) = s(g) if t(g) = s(h) .
>         ceq t(g ; h) = t(h) if t(g) = s(h) .
> endfm)
> **************************
>
> it can directly be executed
>
> while
>         cmb g:P`(G`) ; h:P`(G`) : P(G) if t(g:P`(G`)) = s(h:P`(G`)) .
> may be cumbersome, it can be done, however
>         ceq s(g ; h) = s(g) if t(g) = s(h) .
> cannot stand, it should and in some cases has to be replaced by
>         ceq s(g ; h) = s(g) if (g ; h) : P(G) .
> or anything like this, however i seem unable to get a correct syntax for
> this... usually the error goes like: could not find sort "P`(G`)"
> but instantiating P(G) to P`(G`) gives parse errors
>
> matching equations like
>         ceq s(f) = s(g) if g ; h := f .
> work but are not always applicable
>
> looking for help, martin
>
>
> *****************************************
> for testing:
>
> (fmod nc is
>         including graph .
>
>         ops A B : -> N .
>         ops z y : -> E .
>
>         eq s(z) = A .
>         eq t(z) = B .
>         eq s(y) = B .
>         eq t(y) = B .
> endfm)
>
> (view gnc from graph to nc is
>          sort N to N .
>          sort E to E .
> endv)
>
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help