Maude-help mailing list

[Geert Janssen <geert AT watson.ibm.com>]

Dear Maude Help Team,

Can anybody please confirm that the following is a correct alternative to
the PATH module that occurs in many Maude documents?
If not, please explain what is wrong.

Geert
------------------------------------------------------------------------

fmod A-GRAPH is
 sorts Edge Node .

***( Sample graph
 +<--f------+--e--> n5
 |          |
 n1 --a--> n2 <--d--+
 |                  |
 |                  |
 +--b--> n3 --c-->  n4
)

 ops source target : Edge -> Node .
 ops n1 n2 n3 n4 n5 : -> Node [ctor] .
 ops a b c d e f : -> Edge [ctor] .

 eq source(a) = n1 .
 eq target(a) = n2 .
 eq source(b) = n1 .
 eq target(b) = n3 .
 eq source(c) = n3 .
 eq target(c) = n4 .
 eq source(d) = n4 .
 eq target(d) = n2 .
 eq source(e) = n2 .
 eq target(e) = n5 .
 eq source(f) = n2 .
 eq target(f) = n1 .
endfm

*** Non-empty path in directed graph (might contain cycles though!)
fmod PATH is
 protecting MACHINE-INT .
 protecting A-GRAPH .
 sorts Path Path? .
 subsorts Edge < Path < Path? .

 op _;_ : Path? Path? -> Path? [assoc] .
 ops source target : Path -> Node .
 op length : Path -> MachineInt .

 var E : Edge .
 var S : Path .

 cmb (E ; S) : Path if target(E) = source(S) .

 eq source(E ; S) = source(E) .
 eq target(E ; S) = target(S) .

 eq length(E) = 1 .
 eq length(E ; S) = 1 + length(S) .
endfm