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

states S4,
 MemL,
S0,
S1,
S2,
S3,
S5,
S7;

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:=S0;
  guard:= Mg_k1=1;
  action:= Mg_k1'=Mg_k2,Mg_k2'=0;
};
transition t8 := {
 from:=S4;
 to:=MemL;
  guard:= Mg_k1>1;
  action:= Id_k0'=Id_k0;
};
transition t9 := {
 from:=S5;
 to:=S7;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
}

strategy deleteAll{
Region init:={state=S0 && Mg_k1=k && k>0};
Transitions t:={t1,t2,t3,t4,t5,t6,t7,t8,t9};
Region bad:={state=MemL};
}