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