Next: , Previous: Test, Up: Principles list


7.2.67 Tree principle

This principle assumes that the Graph principle (Graph) is used on dimension D.

The principle stipulates states that D must be a tree. This principle is more specific than the Dag principle (Dag).

Here is the definition of the TreeMakeNodes constraint functor:

%% Copyright 2001-2008
%% by Ralph Debusmann <rade@ps.uni-sb.de> (Saarland University) and
%%    Denys Duchier <duchier@ps.uni-sb.de> (LIFO, Orleans) and
%%    Jorge Marques Pelizzoni <jpeliz@icmc.usp.br> (ICMC, Sao Paulo) and
%%    Jochen Setz <info@jochensetz.de> (Saarland University)
%%
functor
import
%   System(show)
   
   Helpers(checkModel) at 'Helpers.ozf'
export
   Constraint
define
   proc {Constraint Nodes G Principle FD FS Select}
      DVA2DIDA = Principle.dVA2DIDA
      %%
      DIDA = {DVA2DIDA 'D'}
   in
      %% check features
      if {Helpers.checkModel 'TreeMakeNodes.oz' Nodes
	  [DIDA#mothers
	   DIDA#equp
	   DIDA#eq
	   DIDA#up
	   DIDA#eqdown
	   DIDA#down
	   DIDA#labels
	   DIDA#daughtersL]} then
	 Models = {Map Nodes fun {$ Node} Node.DIDA.model end}
      in
	 for Model in Models do
	    %% each node has at most one mother
	    {FD.lesseq {FS.card Model.mothers} 1}
	    %% equp(v) = eq(v) uplus up(v)
	    Model.equp = {FS.partition [Model.eq Model.up]}
	    %% eqdown(v) = eq(v) uplus down(v)
	    Model.eqdown = {FS.partition [Model.eq Model.down]}
	    %% eq(v) = equp(v) intersect eqdown(v)
	    Model.eq = {FS.intersect Model.equp Model.eqdown}
	    %% daughters(v) = uplus{ daughters_l(v) | l in labels }
	    Model.daughters = {FS.partition Model.daughtersL}
	    %% post additional constraints if the graph principle has
	    %% feature mothersL
	    if {HasFeature Model mothersL} then
	       %% mothers(v) = uplus{ mothers_l(v) | l in labels }
	       Model.mothers = {FS.partition Model.mothersL}
	    end
	    %% post additional constraints if the graph principle has
	    %% feature upL
	    if {HasFeature Model upL} then
	       %% up(v) = uplus{ up_l(v) | l in labels }
	       Model.up = {FS.partition Model.upL}
	    end
	    %% post additional constraints if the graph principle has
	    %% feature downL
	    if {HasFeature Model downL} then
	       %% down(v) = uplus{ down_l(v) | l in labels }
	       Model.down = {FS.partition Model.downL}
	    end
	    %% post additional constraints if the tree is ordered
	    if {HasFeature Model yieldL} andthen
	       {HasFeature Model yieldS} then
	       %% yieldS(v) = uplus{ yield_l(v) | l in labels }
	       Model.yieldS = {FS.partition Model.yieldL}
	    end
	    %%
	    if {HasFeature Model pos} andthen
	       {HasFeature Model yield} andthen
	       {HasFeature Model yieldS} then
	       %% yield(v) = pos(v) uplus yieldS(v)
	       Model.yield = {FS.partition [Model.pos Model.yieldS]}
	    end
	 end
      end
   end
end
Here is the definition of the TreeConditions constraint functor:
%% Copyright 2001-2008
%% by Ralph Debusmann <rade@ps.uni-sb.de> (Saarland University) and
%%    Denys Duchier <duchier@ps.uni-sb.de> (LIFO, Orleans) and
%%    Jorge Marques Pelizzoni <jpeliz@icmc.usp.br> (ICMC, Sao Paulo) and
%%    Jochen Setz <info@jochensetz.de> (Saarland University)
%%
functor
import
%   System(show)
   
   Helpers(checkModel) at 'Helpers.ozf'
export
   Constraint
define
   proc {Constraint Nodes G Principle FD FS Select}
      DVA2DIDA = Principle.dVA2DIDA
      %%
      DIDA = {DVA2DIDA 'D'}
   in
      %% check features
      if {Helpers.checkModel 'TreeConditions.oz' Nodes
	  [DIDA#daughters
	   DIDA#mothers
	   DIDA#eq
	   DIDA#eqdown]} then
	 %% get node set NodeSetM
	 NodeSetM = Nodes.1.nodeSet
	 %%
	 RootsM = {FS.subset $ NodeSetM}
	 %% precisely one root
	 {FD.equal {FS.card RootsM} 1}
	 %% 
	 Models = {Map Nodes fun {$ Node} Node.DIDA.model end}
	 %%
	 DaughtersMs = {Map Models
			fun {$ Model} Model.daughters end}
      in
	 {FS.partition RootsM|DaughtersMs NodeSetM}
	 %%
	 for Model in Models I in 1..{Length Models} do
	    %% |labels(v)|=|mothers(v)|
	    {FD.equal
	     {FS.card Model.labels}
	     {FS.card Model.mothers}}
	    %% a node is root iff it has no mother
	    {FD.equi
	     {FS.reified.include I RootsM}
	     {FD.reified.equal {FS.card Model.mothers} 0} 1}
	    %% a node is root iff its eqdown-set contains all nodes
	    {FD.equi
	     {FS.reified.include I RootsM}
	     {FS.reified.equal Model.eqdown NodeSetM} 1}
	 end
      end
   end
end