spn erk(int n):={
place Raf_1Star,RKIP,Raf_1Star_RKIP,ERK_PP,MEK_PP_ERK,Raf_1Star_RKIP_ERK_PP,RKIP_P_RP,MEK_PP,ERK,RKIP_P,RP;
partition(Raf_1Star:RKIP:Raf_1Star_RKIP:Raf_1Star_RKIP_ERK_PP, ERK_PP, ERK:MEK_PP:MEK_PP_ERK,
RP:RKIP_P_RP:RKIP_P);
trans r1,r2,r3,r4,r6,r7,r9,r10,r5,r8,r11;
firing(r1:expo(tk( Raf_1Star) * tk( RKIP)), r2:expo(tk( Raf_1Star_RKIP)), r3:expo(tk( Raf_1Star_RKIP) * tk( ERK_PP)), r4:expo(tk( Raf_1Star_RKIP_ERK_PP)), r6:expo(tk( MEK_PP) * tk( ERK)), r7:expo(tk( MEK_PP_ERK)), r9:expo(tk( RKIP_P) * tk( RP)), r10:expo(tk( RKIP_P_RP)), r5:expo(tk( Raf_1Star_RKIP_ERK_PP)), r8:expo(tk( MEK_PP_ERK)), r11:expo(tk( RKIP_P_RP)));
arcs(r1:Raf_1Star_RKIP:1, Raf_1Star:r1:1, RKIP:r1:1, r2:Raf_1Star:1, r2:RKIP:1, Raf_1Star_RKIP:r2:1, r3:Raf_1Star_RKIP_ERK_PP:1, Raf_1Star_RKIP:r3:1, ERK_PP:r3:1, r4:Raf_1Star_RKIP:1, r4:ERK_PP:1, Raf_1Star_RKIP_ERK_PP:r4:1, r6:MEK_PP_ERK:1, MEK_PP:r6:1, ERK:r6:1, r7:MEK_PP:1, r7:ERK:1, MEK_PP_ERK:r7:1, r9:RKIP_P_RP:1, RKIP_P:r9:1, RP:r9:1, r10:RKIP_P:1, r10:RP:1, RKIP_P_RP:r10:1, r5:Raf_1Star:1, r5:ERK:1, r5:RKIP_P:1, Raf_1Star_RKIP_ERK_PP:r5:1, r8:ERK_PP:1, r8:MEK_PP:1, MEK_PP_ERK:r8:1, r11:RKIP:1, r11:RP:1, RKIP_P_RP:r11:1);


init(Raf_1Star:n,RKIP:n,MEK_PP:n,ERK:n,RP:n);

bigint m := num_states(false);
};
# Verbose true
# Report true
# StateStorage MDD_SATURATION
# GarbageCollection LAZY
int n := read_int("n");
print("   number of states : ", erk(n).m, "\n");