model main{
var Id_k0,
Mg_k1,
Mg_k2,
Mg_k3,
Mg_k4;

states Undef,
S42,
S44,
S32,
S34,
S36,
S38,
S40,
S41,
S43,
S14,
S16,
S21,
S24,
S26,
S28,
S30,
S31,
S33,
S35,
S37,
S39,
 MemL,
S4,
S6,
S9,
S12,
S13,
S15,
S17,
S18,
S19,
S20,
S22,
S25,
S27,
S29,
S0,
S1,
S2,
S3,
S5,
S8;

transition t1 := {
 from:=S0;
 to:=S1;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t2 := {
 from:=S1;
 to:=S2;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t3 := {
 from:=S1;
 to:=S3;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t4 := {
 from:=S2;
 to:=S4;
  guard:= true;
  action:= Mg_k1'=1;
};
transition t5 := {
 from:=S3;
 to:=S5;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t6 := {
 from:=S4;
 to:=S6;
  guard:= Mg_k1=1;
  action:= Id_k0'=Id_k0;
};
transition t7 := {
 from:=S4;
 to:=MemL;
  guard:= Mg_k1>1;
  action:= Id_k0'=Id_k0;
};
transition t8 := {
 from:=S5;
 to:=S8;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t9 := {
 from:=S6;
 to:=S9;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t10 := {
 from:=S8;
 to:=Undef;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t11 := {
 from:=S8;
 to:=Undef;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t12 := {
 from:=S9;
 to:=S12;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t13 := {
 from:=S9;
 to:=S13;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t14 := {
 from:=S12;
 to:=S14;
  guard:= true;
  action:= Mg_k2'=1;
};
transition t15 := {
 from:=S13;
 to:=S15;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t16 := {
 from:=S14;
 to:=S16;
  guard:= Mg_k2=1;
  action:= Id_k0'=Id_k0;
};
transition t17 := {
 from:=S14;
 to:=MemL;
  guard:= Mg_k2>1;
  action:= Id_k0'=Id_k0;
};
transition t18 := {
 from:=S15;
 to:=S17;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t19 := {
 from:=S16;
 to:=S9;
  guard:= true;
  action:= Mg_k1'=Mg_k2+Mg_k1,Mg_k2'=0;
};
transition t20 := {
 from:=S17;
 to:=S18;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t21 := {
 from:=S18;
 to:=S19;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t22 := {
 from:=S19;
 to:=S20;
  guard:= Mg_k1=1;
  action:= Id_k0'=Id_k0;
};
transition t23 := {
 from:=S19;
 to:=S21;
  guard:= Mg_k1>1;
  action:= Mg_k2'=Mg_k1-1,Mg_k1'=1;
};
transition t24 := {
 from:=S20;
 to:=S22;
  guard:= Mg_k1=1;
  action:= Id_k0'=Id_k0;
};
transition t25 := {
 from:=S20;
 to:=MemL;
  guard:= Mg_k1>1;
  action:= Id_k0'=Id_k0;
};
transition t26 := {
 from:=S21;
 to:=S24;
  guard:= Mg_k1=1;
  action:= Id_k0'=Id_k0;
};
transition t27 := {
 from:=S21;
 to:=MemL;
  guard:= Mg_k1>1;
  action:= Id_k0'=Id_k0;
};
transition t28 := {
 from:=S22;
 to:=S25;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t29 := {
 from:=S24;
 to:=S26;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t30 := {
 from:=S25;
 to:=S27;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t31 := {
 from:=S26;
 to:=S28;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t32 := {
 from:=S27;
 to:=S29;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t33 := {
 from:=S28;
 to:=S30;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t34 := {
 from:=S30;
 to:=S31;
  guard:= Mg_k2=1;
  action:= Id_k0'=Id_k0;
};
transition t35 := {
 from:=S30;
 to:=S32;
  guard:= Mg_k2>1;
  action:= Mg_k3'=Mg_k2-1,Mg_k2'=1;
};
transition t36 := {
 from:=S31;
 to:=S33;
  guard:= Mg_k2=1;
  action:= Id_k0'=Id_k0;
};
transition t37 := {
 from:=S31;
 to:=MemL;
  guard:= Mg_k2>1;
  action:= Id_k0'=Id_k0;
};
transition t38 := {
 from:=S32;
 to:=S34;
  guard:= Mg_k2=1;
  action:= Id_k0'=Id_k0;
};
transition t39 := {
 from:=S32;
 to:=MemL;
  guard:= Mg_k2>1;
  action:= Id_k0'=Id_k0;
};
transition t40 := {
 from:=S33;
 to:=S35;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t41 := {
 from:=S34;
 to:=S36;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t42 := {
 from:=S35;
 to:=S37;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t43 := {
 from:=S36;
 to:=S38;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t44 := {
 from:=S37;
 to:=S39;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t45 := {
 from:=S38;
 to:=S40;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t46 := {
 from:=S40;
 to:=S41;
  guard:= Mg_k3=1;
  action:= Id_k0'=Id_k0;
};
transition t47 := {
 from:=S40;
 to:=S42;
  guard:= Mg_k3>1;
  action:= Mg_k4'=Mg_k3-1,Mg_k3'=1;
};
transition t48 := {
 from:=S41;
 to:=S43;
  guard:= Mg_k3=1;
  action:= Id_k0'=Id_k0;
};
transition t49 := {
 from:=S41;
 to:=MemL;
  guard:= Mg_k3>1;
  action:= Id_k0'=Id_k0;
};
transition t50 := {
 from:=S42;
 to:=S44;
  guard:= Mg_k3=1;
  action:= Id_k0'=Id_k0;
};
transition t51 := {
 from:=S42;
 to:=MemL;
  guard:= Mg_k3>1;
  action:= Id_k0'=Id_k0;
};
transition t52 := {
 from:=S43;
 to:=S35;
  guard:= true;
  action:= Mg_k2'=Mg_k3+Mg_k2,Mg_k3'=0;
};
transition t53 := {
 from:=S44;
 to:=S36;
  guard:= true;
  action:= Mg_k2'=Mg_k3+Mg_k2,Mg_k3'=Mg_k4,Mg_k4'=0;
};
}

strategy main{
print("Analysis of the Counter System main ");
Region init:={state=S0};
Transitions t:={t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15,t16,t17,t18,t19,t20,t21,t22,t23,t24,t25,t26,t27,t28,t29,t30,t31,t32,t33,t34,t35,t36,t37,t38,t39,t40,t41,t42,t43,t44,t45,t46,t47,t48,t49,t50,t51,t52,t53};
Region NoMemLeak:={!state=MemL};
Region NoUndef:={!state=Undef};
Region Reach:=post*(init,t,4);
print("Looking for a Memory Leak ...");
if(subSet(Reach,NoMemLeak))
then print("There is no Memory Leak.");
else print("There is a Memory Leak.");
endif
print("Looking for an Undef error...");
if(subSet(Reach,NoUndef))
then print("There is no Undef error.");
else print("There is an Undef error.");
endif
}