spn fms(int n) := {
  place P1, P2, P3, P12, P2s, P3s, P1s, P12s,
        M1, M2, M3, P1wM1, P2wM2, P3M2, P12wM3,
        P1M1, P2M2, P12M3, P1d, P2d, P1wP2, P2wP1;
  trans tP1, tP2, tP3, tP12, tP1M1, tP2M2, tP3M2, 
        tP12M3, tP1s, tP2s, tP3s, tP12s, tM1,
        tM2, tM3, tx, tP1e, tP1j, tP2e, tP2j;
  
 
  weight(tM1:1, tM2:1, tM3:1, tx:1, tP1e:0.8, tP1j:0.2, tP2e:0.6, tP2j:0.4);
  arcs(P1:tP1, tP1:P1wM1, P1wM1:tM1, M1:tM1, tM1:P1M1, P1M1:tP1M1, tP1M1:M1,
    tP1M1:P1d, P1d:tP1e, P1d:tP1j, tP1e:P1s, tP1j:P1wP2, P1s:tP1s,
    tP1s:P1, P1wP2:tx, tx:P12, P12:tP12, tP12:P12wM3, P12wM3:tM3,
    M3:tM3, tM3:P12M3, P12M3:tP12M3, tP12M3:M3, tP12M3:P12s, P12s:tP12s,
    tP12s:P1, tP12s:P2, P2:tP2, tP2:P2wM2, P2wM2:tM2, M2:tM2,
    tM2:P2M2, P2M2:tP2M2, tP2M2:M2, tP2M2:P2d, P2d:tP2j, tP2j:P2wP1, P2wP1:tx,
    P2d:tP2e, tP2e:P2s, P2s:tP2s, tP2s:P2, P3:tP3, tP3:P3M2,
    P3M2:tP3M2, M2:tP3M2, tP3M2:P3s, tP3M2:M2, P3s:tP3s, tP3s:P3);

    partition(P1, P1wM1, P1M1:M1, P1d, P1s, P12s, P12M3:M3, P12wM3, P12, P1wP2, P2wP1, P2, P2wM2, P2M2:M2, P2d, P2s, P3, P3M2, P3s);
    
    init(P1:n, P2:n, P3:n, M1:3, M3:2, M2:1);
    bigint m := num_states(false);
};
# Verbose true
# StateStorage MDD_SATURATION
# MarkovStorage MATRIX_DIAGRAM_GENERAL

int N := read_int("N");
print(N, "\n");
print("number of states: ", fms(N).m,"\n");