model doubleFree{
var Id_k0,
Mg_k1,
Mg_k2,
k;

states S4,
S12,
 MemL,
S0,
S1,
S2,
S3,
S7,
S9,
S11,
 SegF,
S5,
S8,
S13,
S15;

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:=S2;
 to:=S3;
  guard:= Mg_k1=1;
  action:= Id_k0'=Id_k0;
};
transition t4 := {
 from:=S2;
 to:=S4;
  guard:= Mg_k1>1;
  action:= Mg_k2'=Mg_k1-1,Mg_k1'=1;
};
transition t5 := {
 from:=S3;
 to:=S5;
  guard:= Mg_k1=1;
  action:= Mg_k1'=0;
};
transition t6 := {
 from:=S3;
 to:=MemL;
  guard:= Mg_k1>1;
  action:= Id_k0'=Id_k0;
};
transition t7 := {
 from:=S4;
 to:=S7;
  guard:= Mg_k1=1;
  action:= Mg_k1'=0;
};
transition t8 := {
 from:=S4;
 to:=MemL;
  guard:= Mg_k1>1;
  action:= Id_k0'=Id_k0;
};
transition t9 := {
 from:=S5;
 to:=S8;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t10 := {
 from:=S7;
 to:=S9;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t11 := {
 from:=S8;
 to:=SegF;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t12 := {
 from:=S9;
 to:=S11;
  guard:= Mg_k2=1;
  action:= Id_k0'=Id_k0;
};
transition t13 := {
 from:=S9;
 to:=S12;
  guard:= Mg_k2>1;
  action:= Mg_k1'=Mg_k2-1,Mg_k2'=1;
};
transition t14 := {
 from:=S11;
 to:=S13;
  guard:= Mg_k2=1;
  action:= Mg_k2'=0;
};
transition t15 := {
 from:=S11;
 to:=MemL;
  guard:= Mg_k2>1;
  action:= Id_k0'=Id_k0;
};
transition t16 := {
 from:=S12;
 to:=S0;
  guard:= Mg_k2=1;
  action:= Mg_k2'=0;
};
transition t17 := {
 from:=S12;
 to:=MemL;
  guard:= Mg_k2>1;
  action:= Id_k0'=Id_k0;
};
transition t18 := {
 from:=S13;
 to:=S15;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
}

strategy doubleFree{
print("Analysis of the Counter System doubleFree ");
Region init:={state=S0 && Mg_k1=k && k>0};
Transitions t:={t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15,t16,t17,t18};
Region NoMemLeak:={!state=MemL};
Region NoSegF:={!state=SegF};
Region Reach:=post*(init,t,7);
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 a Segmentation Fault ...");
if(subSet(Reach,NoSegF))
then print("There is no Segmentation Fault.");
else print("There is a Segmentation Fault.");
endif
}