digraph Lattice {
    // Define nodes
    splines=false;
    node [shape=circle, style=filled, fillcolor=lightblue];
    nodesep=0.6;

    TOP [label="⊤"];
    BOT [label="⊥"];

    XCTRL [label="~Ctrl"];
    CTRL [label="Ctrl"];

    INT_TOP [label="IntTop"];
    INT_BOT [label="IntBot"];

    INT_MIN [label="-n"];
    INT_MINDOTS [label="..." shape=none style=none];
    INT_MINUS [label="-1"];
    INT_ZERO [label="0"];
    INT_PLUS [label="1"];
    INT_MAXDOTS [label="..." shape=none style=none];
    INT_MAX [label="+n"];

    TUPLE [label="TUPLE"];

    // Define edges
    edge [arrowhead=none];

    TOP         -> INT_TOP;
    INT_TOP     -> INT_MIN;
    INT_TOP     -> INT_MINDOTS;
    INT_TOP     -> INT_MINUS;
    INT_TOP     -> INT_ZERO;
    INT_TOP     -> INT_PLUS;
    INT_TOP     -> INT_MAXDOTS;
    INT_TOP     -> INT_MAX;
    INT_MIN     -> INT_BOT;
    INT_MINDOTS -> INT_BOT;
    INT_MINUS   -> INT_BOT;
    INT_ZERO    -> INT_BOT;
    INT_PLUS    -> INT_BOT;
    INT_MAXDOTS -> INT_BOT;
    INT_MAX     -> INT_BOT;
    INT_BOT     -> BOT;

    INT_MIN -> INT_MINDOTS -> INT_MINUS -> INT_ZERO -> INT_PLUS -> INT_MAXDOTS -> INT_MAX [style=invis];

    TOP          -> TUPLE;
    TUPLE        -> BOT;

    TOP -> XCTRL;
    XCTRL -> CTRL;
    CTRL -> BOT;

    // Additional customization
    {rank=same; TOP}
    {rank=same; INT_TOP; XCTRL}
    {rank=same; INT_MIN; INT_MINDOTS;
                INT_MINUS; INT_ZERO;
                INT_PLUS; INT_MAXDOTS;
                INT_MAX; TUPLE}
    {rank=same; INT_BOT; CTRL}
    {rank=same; BOT;}
}