% @(#)$Id: DirectedGraphTrait.lsl,v 1.4 1997/07/25 05:32:41 leavens Exp $

DirectedGraphTrait(N,E): trait

  includes GraphTrait(N,E)

  introduces
    includesArc: Set[E], E -> Bool

  asserts
    \forall dg: DG, a: A, sa: Set[A], sn: Set[N],
            n1,n2: N, st: State
      includesArc(dg,a) == a \in dg.arcs;

  implies
    converts includesArc

[Index]

HTML generated using lcpp2html.