model reverse{
var Id_k0,
Mg_k1,
Mg_k2,
Mg_k3,
k;

states S16,
S18,
S5,
S8,
S10,
S12,
S14,
S15,
S17,
 MemL,
S0,
S1,
S2,
S3,
S4,
S6,
S9,
S11,
S13;

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:= true;
  action:= Id_k0'=Id_k0;
};
transition t4 := {
 from:=S3;
 to:=S4;
  guard:= Mg_k1=1;
  action:= Id_k0'=Id_k0;
};
transition t5 := {
 from:=S3;
 to:=S5;
  guard:= Mg_k1>1;
  action:= Mg_k2'=Mg_k1-1,Mg_k1'=1;
};
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:= Mg_k1=1;
  action:= Id_k0'=Id_k0;
};
transition t9 := {
 from:=S5;
 to:=MemL;
  guard:= Mg_k1>1;
  action:= Id_k0'=Id_k0;
};
transition t10 := {
 from:=S6;
 to:=S9;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t11 := {
 from:=S8;
 to:=S10;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t12 := {
 from:=S9;
 to:=S11;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t13 := {
 from:=S10;
 to:=S12;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t14 := {
 from:=S11;
 to:=S13;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t15 := {
 from:=S12;
 to:=S14;
  guard:= true;
  action:= Id_k0'=Id_k0;
};
transition t16 := {
 from:=S14;
 to:=S15;
  guard:= Mg_k2=1;
  action:= Id_k0'=Id_k0;
};
transition t17 := {
 from:=S14;
 to:=S16;
  guard:= Mg_k2>1;
  action:= Mg_k3'=Mg_k2-1,Mg_k2'=1;
};
transition t18 := {
 from:=S15;
 to:=S17;
  guard:= Mg_k2=1;
  action:= Id_k0'=Id_k0;
};
transition t19 := {
 from:=S15;
 to:=MemL;
  guard:= Mg_k2>1;
  action:= Id_k0'=Id_k0;
};
transition t20 := {
 from:=S16;
 to:=S18;
  guard:= Mg_k2=1;
  action:= Id_k0'=Id_k0;
};
transition t21 := {
 from:=S16;
 to:=MemL;
  guard:= Mg_k2>1;
  action:= Id_k0'=Id_k0;
};
transition t22 := {
 from:=S17;
 to:=S9;
  guard:= true;
  action:= Mg_k1'=Mg_k2+Mg_k1,Mg_k2'=0;
};
transition t23 := {
 from:=S18;
 to:=S10;
  guard:= true;
  action:= Mg_k1'=Mg_k2+Mg_k1,Mg_k2'=Mg_k3,Mg_k3'=0;
};
}

strategy reverse{
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,t19,t20,t21,t22,t23};
Region bad:={state=MemL};
}