% @(#) $Id: Arc_Pre_Trait.lsl,v 1.1 1997/07/31 17:25:48 leavens Exp $

% This trait would be automatically constructed by Larch/C++
% as part of the model of the members in the Arc struct
% found in DirectedGraph.pri.

Arc_Pre_Trait(Arc, Loc, Val): trait

  assumes TypedObj(Loc, Node),
          contained_objects(Loc[Node])

  includes NoContainedObjects(Val), contained_objects(Arc)

  Arc tuple of source: Loc[Node], target: Loc[Node]
  Val tuple of source: Node, target: Node

  introduces
    eval: Arc, State -> Val
    allocated, assigned: Arc, State -> Bool

  asserts
    \forall a: Arc, on,on2: Loc[Node], st: State
       contained_objects([on,on2], st)
         == {asTypeTaggedObject(on)} \U {asTypeTaggedObject(on2)};
       eval(a,st) == [eval(a.source,st), eval(a.target,st)];
       allocated(a,st)
         == allocated(a.source, st) /\ allocated(a.target, st);
       assigned(a,st)
         == assigned(a.source, st) /\ assigned(a.target, st);

  implies
    converts
      contained_objects: Arc, State -> Set[TypeTaggedObject],
      eval: Arc, State -> Val,
      allocated: Arc, State -> Bool, assigned: Arc, State -> Bool

[Index]

HTML generated using lcpp2html.