пятнашки с полем 3 на 3 на ISPIN(Promela)

[Ярослав9104]

подскажите, пожалуйста, нужно написать игру пятнашки 3 на 3 на этом языке, вроде написал, но не работает, выдает все нули, z1 z2 ит.д. это значение ячеек, 0 это значит пустая.

int z1 = 3,
     z2 = 7,
     z3 = 6,
     z4 = 4,
     z5 = 0,
     z6 = 8,
     z7 = 2,
     z8 = 1,
     z9 = 5;
bool all_right = false;
 
active proctype one(){
 
do :: (z1==0)  -> 
 
        atomic{
                z1=z2;
                z2=0;}
 
            ::z1==0 ->
             atomic{    z1=z4;
                z4=0;}
        
         :: (all_right == true) -> break;
od;}
 
 
active proctype one1(){
 
do :: (z2==0)  -> 
 
   atomic{      
z2=z1;
z1=0;}
 
::z2==0-> atomic{
z2=z3;
z3=0;}
 
::z2==0 -> atomic{
z2=z5;
z5=0;}
 
 :: (all_right == true) -> break;
od;}
 
 
active proctype one2(){
 
do :: (z3==0)  -> 
 
 atomic{       
z3=z2;
z2=0;}
 
::z3==0 -> atomic{
z3=z6;
z6=0;}
 
 :: (all_right == true) -> break;
od;}
 
active proctype one3(){
 
do :: (z4==0)  -> 
 atomic{
       
z4=z1;
z1=0;}
 
::z4==0-> atomic{
z4=z5;
z5=0;}
 
::z4==0-> atomic{
z4=z7;
z7=0;}
 
 :: (all_right == true) -> break;
od;}
 
active proctype one4(){
 
do :: (z5==0)  -> 
 
 atomic{       
z5=z2;
z2=0;}
 
                
::z5==0-> atomic{
z5=z4;
z4=0;}
 
::z5==0-> atomic{
z5=z6;
z6=0;}
 
::z5==0-> atomic{
z5=z8; 
z8=0;}
 
 :: (all_right == true) -> break;
od;}
 
               active proctype one5(){
 
do :: (z6==0)  -> 
 
 atomic{      
z6=z3;
z3=0;}
 
::z6==0-> atomic{
z6=z5;
z5=0;}
 
::z6==0-> atomic{
z6=z9;
z9=0;}
 
 :: (all_right == true) -> break;
od;}
 
active proctype one6(){
 
do :: (z7==0)  -> 
 
  atomic{     
z7=z4;
z4=0;}
 
 
::z7==0-> atomic{
z7=z8;
z8=0;}
 
 :: (all_right == true) -> break;
od;}
 
active proctype one7(){
 
do :: (z8==0)  -> 
 
 atomic{     
z8=z9;
z9=0;}
 
::z8==0-> atomic{
z8=z5;
z5=0;}
 
::z8==0-> atomic{
z8=z7;
z7=0;}
 
 :: (all_right == true) -> break;
od;}
 
active proctype one8(){
 
do :: (z9==0)  ->  atomic{
 
       
z9=z6;
z6=0;}
 
 
::z9==0-> atomic{
z9=z8;
z9=0;}
 
 :: (all_right == true) -> break;
od; 
}
     
active proctype one9(){
if:: ((z1==1) && (z2==2) && (z3==3) && (z4==4) && (z5==5) && (z6==6) && (z7==7) && (z8==8) && (z9==0)) -> 
all_right = true;
 
fi;}
 
 init
{
 atomic
    {
        run one();
        run one1();
        run one2();
        run one3();
        run one4();
        run one5();
        run one6();
        run one7();
        run one8();
        run one9();
    }}

[Stilet]

Я этот язык впервые вижу...