Maude-help mailing list

[Javier Valero Enríquez de Salamanca <mrwylli AT gmail.com>]

Hi everyone,

I have a question about Maude, I think it´s not difficult to do but I have been messing with it and I am not getting it.

I have this module:

fmod ARCH{X :: TRIV} is

sort Arch{X} .
op arch : X$Elt X$Elt -> Arch{X} [ctor] .
ops source destiny : Arch{X} -> X$Elt .
vars E E2 : X$Elt .
eq source(arch(E, E2)) = E .
eq destiny(arch(E, E2)) = E2 . 

endfm

And this one:

fmod SET3{X :: TRIV} is
pr NAT .
sort Set3{X} .

 

op crear : -> Set3{X} [ctor] .
op {_} : X$Elt -> Set3{X} [ctor] .
op _U_ : Set3{X} Set3{X} -> Set3{X} [ctor assoc comm id: create] .
op add : Set3{X} X$Elt -> Set3{X} .
op erase : Set3{X} X$Elt -> Set3{X} .
op intersection : Set3{X} Set3{X} -> Set3{X} .
op difference : Set3{X} Set3{X} -> Set3{X} .
op _belongsTo_ : X$Elt Set3{X} -> Bool .
op _includedIn_ : Set3{X} Set3{X} -> Bool . 
op cardinal : Set3{X} -> Nat .

 

vars C1 C2 : Set3{X} .
vars E1 E2 : X$Elt .
***equations
eq {E1} U {E1} = {E1} . *** idempotencia de la unión

(...) 

endfm

What I want is to use a Set3 of Arches, I think it´s about creating a theory and a view but I tried with differents one and didn´t work.

I would appreciate any help.

Greetings,