fmod PATH is
    protecting MACHINE-INT .

    sorts Edge Path Path? Node .
    subsorts Edge < Path < Path? .

    ops n1 n2 n3 n4 n5 : -> Node .
    ops a b c d e f : -> Edge .
    op _;_ : Path? Path? -> Path? [assoc] .
    ops source target : Path -> Node .
    op length : Path -> MachineInt .

    var E : Edge .
    var P : Path .

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

    ceq source(E ; P) = source(E) if E ; P : Path .
    ceq target(P ; E) = target(E) if P ; E : Path .
    eq length(E) = 1 .
    ceq length(E ; P) = 1 + length(P) if E ; P : Path .

    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

  red (b ; c ; d) .
  *** result Path: (b ; c ; d)

  red length(b ; c ; d) .
  *** result NzMachineInt: 3

  red (a ; b ; c) .
  *** result Path?: (a ; b ; c)

  red source(a ; b ; c) .
  *** result Error(Node): source(a ; b ; c)

  red target(a ; b ; c) .
  *** result Error(Node): target(a ; b ; c)

  red length(a ; b ; c) .
  *** result Error(MachineInt): length(a ; b ; c)