model create{
var Id_k0,
Mg_k1,
Mg_k2;

states S11,
S13,
 MemL,
S4,
S6,
S8,
S9,
S10,
S12,
S0,
S1,
S2,
S3,
S5;

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:=S6;
 to:=S8;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t9 := {
 from:=S8;
 to:=S9;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t10 := {
 from:=S8;
 to:=S10;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t11 := {
 from:=S9;
 to:=S11;
  guard:= true;
  action:= Mg_k2'=1;
};
transition t12 := {
 from:=S10;
 to:=S12;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t13 := {
 from:=S11;
 to:=S13;
  guard:= Mg_k2=1;
  action:= Id_k0'=Id_k0;
};
transition t14 := {
 from:=S11;
 to:=MemL;
  guard:= Mg_k2>1;
  action:= Id_k0'=Id_k0;
};
transition t15 := {
 from:=S13;
 to:=S8;
  guard:= true;
  action:= Mg_k1'=Mg_k2+Mg_k1,Mg_k2'=0;
};
}

strategy create{
print("Analysis of the Counter System create ");
Region init:={state=S0};
Transitions t:={t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15};
Region NoMemLeak:={!state=MemL};
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
}