colspn [disjunction]
{
constants:
all:
  int D1 = 25;
  int D2 = 33;
  int dS = 3;
  int dM = 5;
  int dL = 8;
parameters:
  double rateShort = 0.009;
  double rateShortInit = 0.003;
  double rateShortFinal = 0.0009;
  double rateMedium = rateShort/50;
  double rateMediumInit = rateShortInit/50;
  double rateMediumFinal = rateShortFinal/50;
  double rateLong = rateShort/100;
  double rateLongInit = rateShortInit/100;
  double rateLongFinal = rateShortFinal/100;
  double rateLoop = 1e-09;
  double weightBlock = 0.7;
block:
  int m_X = 0;
  int m_NX = 0;
  int m_Y = 0;
  int m_NY = 0;
  int m_Z = 0;
  int m_NZ = 0;

colorsets:
  Dot = {dot};
  CD1 = {1..D1};
  CD2 = {1..D2};
  enum Type = {INIT,FINAL,NORM,FORK,JOIN};
  enum Label= {E,T,F,X,NX,Y,NY,Z,NZ};
  Circuit = PROD(CD1,CD2,Type,Label);

variables:
  CD1 : x1;
  CD2 : y1;
  CD1 : x2;
  CD2 : y2;
  Type : z1;
  Type : z2;
  Label : w1;
  Label : w2;

colorfunctions:
bool Positions(CD1 x, CD2 y, Type z, Label w) {
    (x=1 & y=9 & z=INIT & w=E)|(x=3 & y=9 & z=FORK & w=E)|
    (x=4 & y=7 & z=NORM & w=X)|(x=5 & y=5 & z=NORM & w=X)|
    (x=6 & y=3 & z=NORM & w=X)|(x=7 & y=1 & z=NORM & w=X)|
    (x=9 & y=1 & z=NORM & w=X)|(x=11 & y=1 & z=NORM & w=X)|
    (x=13 & y=1 & z=NORM & w=X)|(x=15 & y=1 & z=NORM & w=X)|
    (x=17 & y=1 & z=NORM & w=X)|(x=19 & y=1 & z=NORM & w=X)|
    (x=20 & y=3 & z=NORM & w=X)|(x=21 & y=5 & z=JOIN & w=E)|
    (x=23 & y=5 & z=FINAL & w=T)|
    (x=4 & y=11 & z=NORM & w=NX)|(x=5 & y=13 & z=NORM & w=NX)|
    (x=6 & y=15 & z=NORM & w=NX)|(x=8 & y=15 & z=FORK & w=NX)|
    (x=10 & y=15 & z=NORM & w=Y)|(x=12 & y=15 & z=NORM & w=Y)|
    (x=13 & y=13 & z=NORM & w=Y)|(x=15 & y=13 & z=NORM & w=Y)|
    (x=17 & y=13 & z=JOIN & w=NX)|(x=18 & y=11 & z=NORM & w=NX)|
    (x=19 & y=9 & z=NORM & w=NX)|(x=20 & y=7 & z=NORM & w=NX)|
    (x=9 & y=17 & z=NORM & w=NY)|(x=10 & y=19 & z=NORM & w=NY)|
    (x=11 & y=21 & z=NORM & w=NY)|(x=12 & y=23 & z=FORK & w=NY)|
    (x=14 & y=23 & z=NORM & w=Z)|(x=16 & y=23 & z=NORM & w=Z)|
    (x=18 & y=23 & z=NORM & w=Z)|(x=20 & y=23 & z=NORM & w=Z)|
    (x=21 & y=21 & z=NORM & w=NY)|(x=20 & y=19 & z=NORM & w=NY)|
    (x=19 & y=17 & z=NORM & w=NY)|(x=18 & y=15 & z=NORM & w=NY)|
    (x=11 & y=25 & z=NORM & w=NZ)|(x=10 & y=27 & z=NORM & w=NZ)|
    (x=9 & y=29 & z=NORM & w=NZ)|(x=8 & y=31 & z=FINAL & w=F)
};

bool Blockage(Label w) {
    w!=E & w!=T & w!=F
};


// Rectilinear distance, Manhattan distance, L1 norm
CD1 RectilinearDistance(CD1 x1,CD2 y1,CD1 x2,CD2 y2) {abs(x1-x2) + abs(y1-y2)};
// Chessboard distance, Chebyshev distance, Loo norm
CD1 ChessboardDistance(CD1 x1,CD2 y1,CD1 x2,CD2 y2) {max(abs(x1-x2), abs(y1-y2))};

bool NoSelfLoop    (CD1 x1,CD2 y1,CD1 x2,CD2 y2) {(x1 != x2 | y1 != y2)};

bool ShortDistance (CD1 x1,CD2 y1,CD1 x2,CD2 y2) {RectilinearDistance(x1,y1,x2,y2) <= dS || ChessboardDistance(x1,y1,x2,y2) < dS};
bool MediumDistance(CD1 x1,CD2 y1,CD1 x2,CD2 y2) {(RectilinearDistance(x1,y1,x2,y2) > dS && ChessboardDistance(x1,y1,x2,y2) >= dS) && (RectilinearDistance(x1,y1,x2,y2) <= dM || ChessboardDistance(x1,y1,x2,y2) < dM)};
bool LongDistance  (CD1 x1,CD2 y1,CD1 x2,CD2 y2) {(RectilinearDistance(x1,y1,x2,y2) > dM && ChessboardDistance(x1,y1,x2,y2) >= dM) && (RectilinearDistance(x1,y1,x2,y2) <= dL || ChessboardDistance(x1,y1,x2,y2) < dL)};

bool  IsNeighbourShortD (CD1 x1,CD2 y1,Type z1,Label w1,CD1 x2,CD2 y2,Type z2,Label w2) {ShortDistance(x1,y1,x2,y2) && NoSelfLoop(x1,y1,x2,y2)  && Positions(x1,y1,z1,w1) && Positions(x2,y2,z2,w2)};
bool  IsNeighbourMediumD(CD1 x1,CD2 y1,Type z1,Label w1,CD1 x2,CD2 y2,Type z2,Label w2) {MediumDistance(x1,y1,x2,y2) && NoSelfLoop(x1,y1,x2,y2) && Positions(x1,y1,z1,w1) && Positions(x2,y2,z2,w2)};
bool  IsNeighbourLongD  (CD1 x1,CD2 y1,Type z1,Label w1,CD1 x2,CD2 y2,Type z2,Label w2) {LongDistance  (x1,y1,x2,y2) && NoSelfLoop(x1,y1,x2,y2) && Positions(x1,y1,z1,w1) && Positions(x2,y2,z2,w2)};


places:
discrete:
  Circuit A = [z1 = INIT]2`(x1,y1,z1,w1) ++ [z1 != INIT]1`(x1,y1,z1,w1);
  Circuit B = m[w1]`(x1,y1,z1,w1);

transitions:
  stepShort
 {[IsNeighbourShortD(x1,y1,z1,w1,x2,y2,z2,w2) && z1 != FINAL && z2 != FINAL]}
    :
    : [A - {2`(x1,y1,z1,w1)++1`(x2,y2,z2,w2)}] & [A + {2`(x2,y2,z2,w2)}]
    : [z1 = INIT]rateShortInit ++ [z1 != INIT]rateShort
    ;
  stepShortFinal
 {[IsNeighbourShortD(x1,y1,z1,w1,x2,y2,z2,w2) && z1 != FINAL && z2 = FINAL]}
    :
    : [A - {2`(x1,y1,z1,w1)++1`(x2,y2,z2,w2)}] & [A + {2`(x2,y2,z2,w2)}]
    : rateShortFinal
    ;
  stepMedium
 {[IsNeighbourMediumD(x1,y1,z1,w1,x2,y2,z2,w2) && z1 != FINAL && z2 != FINAL]}
    :
    : [A - {2`(x1,y1,z1,w1)++1`(x2,y2,z2,w2)}] & [A + {2`(x2,y2,z2,w2)}]
    : [z1 = INIT]rateMediumInit ++ [z1 != INIT]rateMedium
    ;
  stepMediumFinal
 {[IsNeighbourMediumD(x1,y1,z1,w1,x2,y2,z2,w2) && z1 != FINAL && z2 = FINAL]}
    :
    : [A - {2`(x1,y1,z1,w1)++1`(x2,y2,z2,w2)}] & [A + {2`(x2,y2,z2,w2)}]
    : rateMediumFinal
    ;
  stepLong
 {[IsNeighbourLongD(x1,y1,z1,w1,x2,y2,z2,w2) && z1 != FINAL && z2 != FINAL]}
    :
    : [A - {2`(x1,y1,z1,w1)++1`(x2,y2,z2,w2)}] & [A + {2`(x2,y2,z2,w2)}]
    : [z1 = INIT]rateLongInit ++ [z1 != INIT]rateLong
    ;
  stepLongFinal
 {[IsNeighbourLongD(x1,y1,z1,w1,x2,y2,z2,w2) && z1 != FINAL && z2 = FINAL]}
    :
    : [A - {2`(x1,y1,z1,w1)++1`(x2,y2,z2,w2)}] & [A + {2`(x2,y2,z2,w2)}]
    : rateLongFinal
    ;
  loop
 {[Positions(x1,y1,z1,w1) && z1 = FINAL]}
    :
    : [A - {2`(x1,y1,z1,w1)}] & [A + {2`(x1,y1,z1,w1)}]
    : rateLoop
    ;

immediate:
  block
  {[Blockage(w1) && Positions(x1,y1,z1,w1)]}
    :
    : [A - {(x1,y1,z1,w1)}] & [B - {(x1,y1,z1,w1)}]
    : weightBlock
    ;
  fail
  {[Blockage(w1) && Positions(x1,y1,z1,w1)]}
    :
    : [B - {(x1,y1,z1,w1)}]
    : 1-weightBlock
    ;
}