/********************************************************
Abstract model of a virtual file system (originally EXT2)
Author: Radu Siminiceanu (NIA)
Last update: August 2, 2008
********************************************************/

/* constants */

//int ND := 4;	/* maximum number of dentries */
//int NI := 4;	/* maximum number of inodes */
//int NP := 1;	/* maximum number of processes */

/* reserved file indices */
int ROOT       := 1;
int LOST_FOUND := 2;

/* i_node states */
int DELETING   := 1;

/* hash function */
/* does nothing for now */
/* could be used IF implementing the dcache */
int hashvalue(int x) := x;

/*==========================================*/
/* SMART options for state space generation */
/*==========================================*/
# Verbose true
# Report true			/* reports MDD stats */
# IgnoreWeightClasses true	/* deals with immediate events priorities */
# Generations 5000		/* For variable reordering, if needed  */
# GarbageSize 3299000
# GarbageCollection GLOBAL

/* Recommended options for the state-space construction algorithm */
/* - Kronecker consistent: */
/*    MDD_SATURATION    -- standard on-the-fly: full MDD nodes   */
/*    MDD_SPARSE        -- on-the-fly: sparse MDD nodes          */
# StateStorage MDD_SPARSE

/*==========================================*/

spn EXT2(int nd, int ni, int np) := {

  /* Superblock */
  
  place 
    superblock_root,		/* not used */
    superblock_umount_lock,	/* not used */
    superblock_lock,		/* not used */

    dcache_lock,		/* global lock on dcache */
    inode_lock;			/* global lock on inodes */

    /* Convention used in this petri net:
       Locks and mutexes have the following values:
          if available,  >0
          not avalibale, =0
       I.e.: getting a lock/mutex removes a token
             releasing a lock/mutex adds the token back
    */         

    init(dcache_lock:1, inode_lock:1);

    partition(3*nd-2+ni+8*np+1:dcache_lock:inode_lock);

  /* D_Entries */

  for (int i in {1..nd}) {
    place 
      d_allocated[i],   /* is allocated? flag */
      d_parent[i],	/* id of parent: 0=n/a, or 1..ND */
      d_count[i],	/* reference count */
      d_lock[i],	/* lock */
      d_inode[i],	/* id of corresponding inode: 0=n/a, or 1..NI */
      d_subdirs[i];	/* number of subdirectories */

    /* put all places of dentry #i in partition #i */
    /* will result in large local subspace	*/
    partition(	
      cond(i>1,3*i-4,1):d_allocated[i]:d_subdirs[i]:d_count[i]:d_lock[i],
      cond(i>1,3*i-3,1):d_parent[i],
      cond(i>1,3*i-2,1):d_inode[i]
    );

    init(d_lock[i]:1);

  }

  /* Inodes section */

  for (int i in {1..ni}) {
    place 
      i_allocated[i],	/* is allocated ? */
      i_count[i],	/* don't know what this is */
      i_lock[i],	/* lock */
      i_state[i],	/* deleting or not */
      i_mutex[i];	/* used in create() */

    partition(3*nd-2+i:
      i_allocated[i]:
      i_count[i]:
      i_lock[i]:
      i_state[i]:
      i_mutex[i]
    );
 
    init(i_mutex[i]:1);	/* initially mutex available */
    init(i_lock[i]:1);	/* initially lock available */
  }

  //===========================================
  /* Processes */
  //===========================================
  //----------------------------------------
  //       Concurrent processes
  //----------------------------------------

  for (int p in {1..np}) {

    place
      /* "program counters" */
      p_begin[p],
      p_start_create[p],
      p_start_unlink[p],
      p_start_mkdir[p],
      p_start_rmdir[p],
      p_file[p],
      p_parent[p],
      p_inode[p];

    init(p_begin[p]:1);

    partition(
      3*nd-2+ni+8*p:p_begin[p]:p_start_create[p]:p_start_unlink[p]:p_start_mkdir[p]:p_start_rmdir[p],
      3*nd-2+ni+8*p-1:p_parent[p],
      3*nd-2+ni+8*p-2:p_file[p],
      3*nd-2+ni+8*p-3:p_inode[p]
    );

    trans
      t_start_create[p],
      t_start_unlink[p],
      t_start_mkdir[p],
      t_start_rmdir[p];
    arcs(
      p_begin[p]:t_start_create[p],
        t_start_create[p]:p_start_create[p],
        /* clear old arguments */
        p_file[p]:t_start_create[p]:tk(p_file[p]),
        p_parent[p]:t_start_create[p]:tk(p_parent[p]),
        p_inode[p]:t_start_create[p]:tk(p_inode[p]),
      p_begin[p]:t_start_unlink[p],
        t_start_unlink[p]:p_start_unlink[p],
        /* clear old arguments */
        p_file[p]:t_start_unlink[p]:tk(p_file[p]),
        p_parent[p]:t_start_unlink[p]:tk(p_parent[p]),
        p_inode[p]:t_start_unlink[p]:tk(p_inode[p]),
      p_begin[p]:t_start_mkdir[p],
        t_start_mkdir[p]:p_start_mkdir[p],
        /* clear old arguments */
        p_file[p]:t_start_mkdir[p]:tk(p_file[p]),
        p_parent[p]:t_start_mkdir[p]:tk(p_parent[p]),
        p_inode[p]:t_start_mkdir[p]:tk(p_inode[p]),
      p_begin[p]:t_start_rmdir[p],
        t_start_rmdir[p]:p_start_rmdir[p],
        /* clear old arguments */
        p_file[p]:t_start_rmdir[p]:tk(p_file[p]),
        p_parent[p]:t_start_rmdir[p]:tk(p_parent[p]),
        p_inode[p]:t_start_rmdir[p]:tk(p_inode[p])
    );


    /* ----------------------------------- */
    /* PN "program counters"  for create() */
    /* ----------------------------------- */
    place
      p_create_lookup[p],       // path_lookup(parent,file)
      p_create_line1[p],        // if (!parent.is_allocated)
      p_create_line2[p],        //  return ERROR
      p_create_line3[p],        // down(parent.d_inode->i_mutex)
      p_create_line4[p],        // if (file.is_allocated && !is_directory(file))
      p_create_line5[p],        //  up(parent.d_inode->i_mutex)
      p_create_line6[p],        //  path_release(file)
      p_create_line7[p],        //  return SUCCESS
      p_create_line8[p],        // if (file.is_alocated && is_directory(file))
      p_create_line9[p],        //  up(parent.d_inode->i_mutex)
      p_create_line10[p],       //  path_release(file)
      p_create_line11[p],       //  return ERROR
      p_create_line12[p],       // spin_lock(dcache_lock)
      p_create_line13[p],       // file = allocate_dentry()
      p_create_line14[p],       // if (!file.is_allocated)
      p_create_line15[p],       //  spin_unlock(dcache_loc)
      p_create_line16[p],       //  up(parent.d_inode->i_mutex)
      p_create_line17[p],       //  dput(parent)
      p_create_line18[p],       //  return ERROR
      p_create_line19[p],       // dget(file)
      p_create_line20[p],       // spin_lock(inode_lock)
      p_create_line21[p],       // itmp = allocate_inode(file)
      p_create_line22[p],       // file.d_inode = &itmp
      p_create_line23[p],       // spin_unlock(inode_lock)
      p_create_line24[p],       // if (!file.d_inode->is_allocated)
      p_create_line25[p],       //  atomic_write(d_count)
      p_create_line26[p],       //  dput(parent)
      p_create_line27[p],       //  spin_unlock(dcache_lock)
      p_create_line28[p],       //  up(parent.d_inode->i_mutex)
      p_create_line29[p],       //  return ERROR
      p_create_line30[p],       // update(parent)
      p_create_line31[p],       // path_release(file)
      p_create_line32[p],       // spin_unlock(dcache_lock)
      p_create_line33[p],       // up(parent.d_inode->i_mutex)
      p_create_line34[p];       // return SUCCESS
    partition(
      3*nd-2+ni+8*p-4:
       p_create_line1[p]:p_create_line2[p]:p_create_line3[p]:
       p_create_line4[p]:p_create_line5[p]:p_create_line6[p]:
       p_create_line7[p]:p_create_line8[p]:p_create_line9[p]:
       p_create_line10[p]:p_create_line11[p]:p_create_line12[p]:
       p_create_line13[p]:p_create_line14[p]:p_create_line15[p]:
       p_create_line16[p]:p_create_line17[p]:p_create_line18[p]:
       p_create_line19[p]:p_create_line20[p]:p_create_line21[p]:
       p_create_line22[p]:p_create_line23[p]:p_create_line24[p]:
       p_create_line25[p]:p_create_line26[p]:p_create_line27[p]:
       p_create_line28[p]:p_create_line29[p]:p_create_line30[p]:
       p_create_line31[p]:p_create_line32[p]:p_create_line33[p]:
       p_create_line34[p]:p_create_lookup[p]
    );

    /* ----- Create transitions ----- */

    /* ---------- Create step 0 ---------- */
    // --- initiate call: store new params
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_create_step0[p][i][j];
        arcs(
          p_start_create[p]:t_create_step0[p][i][j],
            t_create_step0[p][i][j]:p_create_lookup[p],
            /* store new values */
            p_file[p]:t_create_step0[p][i][j]:tk(p_file[p]),
            p_parent[p]:t_create_step0[p][i][j]:tk(p_parent[p]),
            t_create_step0[p][i][j]:p_file[p]:i,
            t_create_step0[p][i][j]:p_parent[p]:j
        );
        inhibit(p_create_lookup[p]:t_create_step0[p][i][j]);
      }
    }
    /* ---------- Create: lookup ---------- */
    // --- path_lookup(parent,file)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_create_lookup[p][i][j];
        arcs(
          p_create_lookup[p]:t_create_lookup[p][i][j],
            t_create_lookup[p][i][j]:p_create_line1[p],
            t_create_lookup[p][i][j]:d_count[i]:cond(tk(d_allocated[i])>0, 1, 0)
        );
        cond(i!=j, arcs(
            t_create_lookup[p][i][j]:d_count[j]:cond(tk(d_allocated[j])>0, 1, 0)), null);
        guard(
          t_create_lookup[p][i][j]:tk(dcache_lock)>0 & tk(p_file[p])==i & tk(p_parent[p])==j
        );
        inhibit(d_count[i]:t_create_lookup[p][i][j]:np+1);
        cond(i!=j, inhibit(d_count[j]:t_create_lookup[p][i][j]:np+1), null);
      }
    }
    /* ---------- Create step 1 ---------- */
    // --- if (!parent.is_allocated)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_create_step1_err[p][i][j],
          t_create_step1_then[p][i][j],
          t_create_step1_else[p][i][j];
        arcs(
          p_create_line1[p]:t_create_step1_err[p][i][j],
            t_create_step1_err[p][i][j]:p_create_line2[p],
            d_count[i]:t_create_step1_err[p][i][j]:cond(tk(d_allocated[i])>0, 1, 0),
          p_create_line1[p]:t_create_step1_then[p][i][j],
            t_create_step1_then[p][i][j]:p_create_line2[p],
            d_count[i]:t_create_step1_then[p][i][j]:cond(tk(d_allocated[i])>0, 1, 0),
          p_create_line1[p]:t_create_step1_else[p][i][j],
            t_create_step1_else[p][i][j]:p_create_line3[p]
        );
        cond(i!=j, arcs(d_count[j]:t_create_step1_err[p][i][j]), null);
        guard(
          t_create_step1_err[p][i][j]: tk(p_file[p])==i & tk(p_parent[p])==j & tk(d_allocated[j])>0 & tk(d_subdirs[j])==0,
          t_create_step1_then[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j & tk(d_allocated[j])==0,
          t_create_step1_else[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j & tk(d_allocated[j])>0 & tk(d_subdirs[j])>0
        );
      }
    }
    /* ---------- Create step 2 ---------- */
    // --- return ERROR
        trans
          t_create_step2[p];
        arcs(
          p_create_line2[p]:t_create_step2[p],
            t_create_step2[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_create_step2[p]);
    /* ---------- Create step 3 ---------- */
    // --- down(parent.d_inode->i_mutex)
    for (int j in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_create_step3[p][j][k];
        arcs(
          p_create_line3[p]:t_create_step3[p][j][k],
            t_create_step3[p][j][k]:p_create_line4[p],
            i_mutex[k]:t_create_step3[p][j][k]
        );
        guard(
          t_create_step3[p][j][k]:tk(p_parent[p])==j & tk(d_inode[j])==k
        );
      }
    }
    /* ---------- Create step 4 ---------- */
    // --- if (file.is_allocated && !is_directory(file))
    for (int i in {1..nd}) {
        trans
          t_create_step4_then[p][i],
          t_create_step4_else[p][i];
        arcs(
          p_create_line4[p]:t_create_step4_then[p][i],
            t_create_step4_then[p][i]:p_create_line5[p],
          p_create_line4[p]:t_create_step4_else[p][i],
            t_create_step4_else[p][i]:p_create_line8[p]
        );
        guard(
          t_create_step4_then[p][i]:tk(p_file[p])==i &   tk(d_allocated[i])>0 & tk(d_subdirs[i])==0,
          t_create_step4_else[p][i]:tk(p_file[p])==i & !(tk(d_allocated[i])>0 & tk(d_subdirs[i])==0)
        );
    }
    /* ---------- Create step 5 ---------- */
    // --- up(parent.d_inode->i_mutex)
    for (int j in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_create_step5[p][j][k];
        arcs(
          p_create_line5[p]:t_create_step5[p][j][k],
            t_create_step5[p][j][k]:p_create_line6[p],
            t_create_step5[p][j][k]:i_mutex[k]
        );
        guard(
          t_create_step5[p][j][k]:tk(p_parent[p])==j & tk(d_inode[j])==k
        );
        inhibit(i_mutex[k]:t_create_step5[p][j][k]:np);
      }
    }
    /* ---------- Create step 6 ---------- */
    // --- path_release(file)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_create_step6[p][i][j];
        arcs(
          p_create_line6[p]:t_create_step6[p][i][j],
            t_create_step6[p][i][j]:p_create_line7[p],
            d_count[i]:t_create_step6[p][i][j]:cond(tk(d_count[i])>1, 1, 0)
        );
        cond(i!=j, arcs(
            d_count[j]:t_create_step6[p][i][j]:cond(tk(d_count[j])>1, 1, 0)), null);
        guard(
          t_create_step6[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j
        );
      }
    }
    /* ---------- Create step 7 ---------- */
    // --- return SUCCESS
        trans
          t_create_step7[p];
        arcs(
          p_create_line7[p]:t_create_step7[p],
            t_create_step7[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_create_step7[p]);
    /* ---------- Create step 8 ---------- */
    // --- if (file.is_allocated && is_directory(file))
    for (int i in {1..nd}) {
        trans
          t_create_step8_then[p][i],
          t_create_step8_else[p][i];
        arcs(
          p_create_line8[p]:t_create_step8_then[p][i],
            t_create_step8_then[p][i]:p_create_line9[p],
          p_create_line8[p]:t_create_step8_else[p][i],
            t_create_step8_else[p][i]:p_create_line12[p]
        );
        guard(
          t_create_step8_then[p][i]:tk(p_file[p])==i &   tk(d_allocated[i])>0 & tk(d_subdirs[i])>0,
          t_create_step8_else[p][i]:tk(p_file[p])==i & !(tk(d_allocated[i])>0 & tk(d_subdirs[i])>0)
        );
    }
    /* ---------- Create step 9 ---------- */
    // --- up(parent.d_inode->i_mutex)
    for (int j in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_create_step9[p][j][k];
        arcs(
          p_create_line9[p]:t_create_step9[p][j][k],
            t_create_step9[p][j][k]:p_create_line10[p],
            t_create_step9[p][j][k]:i_mutex[k]
        );
        guard(
          t_create_step9[p][j][k]:tk(p_parent[p])==j & tk(d_inode[j])==k
        );
        inhibit(i_mutex[k]:t_create_step9[p][j][k]:np);
      }
    }
    /* ---------- Create step 10 ---------- */
    // --- path_release(file)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_create_step10[p][i][j];
        arcs(
          p_create_line10[p]:t_create_step10[p][i][j],
            t_create_step10[p][i][j]:p_create_line11[p],
            d_count[i]:t_create_step10[p][i][j]:cond(tk(d_count[i])>1, 1, 0)
        );
        cond(i!=j, arcs(
            d_count[j]:t_create_step10[p][i][j]:cond(tk(d_count[j])>1, 1, 0)), null);
        guard(
          t_create_step10[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j
        );
      }
    }
    /* ---------- Create step 11 ---------- */
    // --- return SUCCESS
        trans
          t_create_step11[p];
        arcs(
          p_create_line11[p]:t_create_step11[p],
            t_create_step11[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_create_step11[p]);
    /* ---------- Create step 12 ---------- */
    // --- spin_lock(dcache_lock)
        trans
          t_create_step12[p];
        arcs(
          p_create_line12[p]:t_create_step12[p],
            t_create_step12[p]:p_create_line13[p],
            dcache_lock:t_create_step12[p]
        );
    /* ---------- Create step 13 ---------- */
    // --- allocate_dentry
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_create_step13[p][i][j];
        arcs(
          p_create_line13[p]:t_create_step13[p][i][j],
            t_create_step13[p][i][j]:p_create_line14[p],
            d_allocated[i]:t_create_step13[p][i][j]:tk(d_allocated[i]),
            t_create_step13[p][i][j]:d_allocated[i],
            d_count[i]:t_create_step13[p][i][j]:tk(d_count[i]),
            t_create_step13[p][i][j]:d_count[i],
            d_lock[i]:t_create_step13[p][i][j]:tk(d_lock[i]),
            t_create_step13[p][i][j]:d_lock[i],
            d_parent[i]:t_create_step13[p][i][j]:tk(d_parent[i]),
            t_create_step13[p][i][j]:d_parent[i]:j
        );
        guard(
          t_create_step13[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j & tk(d_allocated[i])==0
        );
      }
    }

    for (int i in {1..nd}) {
        trans
          t_create_step13x[p][i];
        arcs(
          p_create_line13[p]:t_create_step13x[p][i],
            t_create_step13x[p][i]:p_create_line15[p]
        );
        guard(
          t_create_step13x[p][i]:tk(p_file[p])==i & tk(d_allocated[i])>0
        );
    }

    /* ---------- Create step 14 ---------- */
    // --- if (!file.is_allocated)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_create_step14_then[p][i][j],
          t_create_step14_else[p][i][j];
        arcs(
          p_create_line14[p]:t_create_step14_then[p][i][j],
            t_create_step14_then[p][i][j]:p_create_line15[p],
          p_create_line14[p]:t_create_step14_else[p][i][j],
            t_create_step14_else[p][i][j]:p_create_line19[p]
        );
        guard(
          t_create_step14_then[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j & tk(d_subdirs[j])==0,
          t_create_step14_else[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j & tk(d_subdirs[j])>0
        );
      }
    }
    /* ---------- Create step 15 ---------- */
    // --- spin_unlock(dcache_lock)
        trans
          t_create_step15[p];
        arcs(
          p_create_line15[p]:t_create_step15[p],
            t_create_step15[p]:p_create_line16[p],
            t_create_step15[p]:dcache_lock
        );
        inhibit(dcache_lock:t_create_step15[p]:2);
    /* ---------- Create step 16 ---------- */
    // --- up(parent.d_inode->i_mutex)
    for (int j in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_create_step16[p][j][k];
        arcs(
          p_create_line16[p]:t_create_step16[p][j][k],
            t_create_step16[p][j][k]:p_create_line17[p],
            t_create_step16[p][j][k]:i_mutex[k]
        );
        guard(
          t_create_step16[p][j][k]:tk(p_parent[p])==j & tk(d_inode[j])==k
        );
        inhibit(i_mutex[k]:t_create_step16[p][j][k]:np);
      }
    }
    /* ---------- Create step 17 ---------- */
    // --- dput(parent)
    for (int j in {1..nd}) {
        trans
          t_create_step17[p][j];
        arcs(
          p_create_line17[p]:t_create_step17[p][j],
            t_create_step17[p][j]:p_create_line18[p],
            d_count[j]:t_create_step17[p][j]:cond(tk(d_count[j])>1, 1, 0)
        );
        guard(
          t_create_step17[p][j]:tk(p_parent[p])==j & tk(d_lock[j])>0
        );
    }
    /* ---------- Create step 18 ---------- */
    // --- return ERROR
        trans
          t_create_step18[p];
        arcs(
          p_create_line18[p]:t_create_step18[p],
            t_create_step18[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_create_step18[p]);
    /* ---------- Create step 19 ---------- */
    // --- dget(file)
    for (int i in {1..nd}) {
        trans
          t_create_step19[p][i];
        arcs(
          p_create_line19[p]:t_create_step19[p][i],
            t_create_step19[p][i]:p_create_line20[p],
            t_create_step19[p][i]:d_count[i]:cond(tk(d_count[i])>0,1,0)
        );
        guard(
          t_create_step19[p][i]:tk(p_file[p])==i & tk(d_lock[i])>0
        );
        inhibit(d_count[i]:t_create_step19[p][i]:np+1);
    }
    /* ---------- Create step 20 ---------- */
    // --- spin_lock(inode_lock)
        trans
          t_create_step20[p];
        arcs(
          p_create_line20[p]:t_create_step20[p],
            t_create_step20[p]:p_create_line21[p],
            inode_lock:t_create_step20[p]
        );
    /* ---------- Create step 21 ---------- */
    // --- allocate_inode(file)
    for (int k in {2..ni}) {
        trans
          t_create_step21[p][k];
        arcs(
          p_create_line21[p]:t_create_step21[p][k],
            t_create_step21[p][k]:p_create_line22[p],
            t_create_step21[p][k]:i_allocated[k],
            i_count[k]:t_create_step21[p][k]:tk(i_count[k]),
            t_create_step21[p][k]:i_count[k],
            i_mutex[k]:t_create_step21[p][k]:tk(i_mutex[k]),
            t_create_step21[p][k]:i_mutex[k],
            i_lock[k]:t_create_step21[p][k]:tk(i_lock[k]),
            t_create_step21[p][k]:i_lock[k],
            p_inode[p]:t_create_step21[p][k]:tk(p_inode[p]),
            t_create_step21[p][k]:p_inode[p]:k
        );
        guard(
          t_create_step21[p][k]:tk(i_allocated[k])==0
        );
        inhibit(i_allocated[k]:t_create_step21[p][k]);
        /* allocate first inode available */
        /* i.e. if allocating inode k, then all inodes before k are already allocated */
        for (int h in {1..k-1}) {
          arcs(
            i_allocated[h]:t_create_step21[p][k],
            t_create_step21[p][k]:i_allocated[h]
          );
        }
    }
        /* no inodes available */
        trans
          t_create_step21x[p];
        arcs(
          p_create_line21[p]:t_create_step21x[p],
            t_create_step21x[p]:p_create_line22[p],
            p_inode[p]:t_create_step21x[p]:tk(p_inode[p]),
            t_create_step21x[p]:p_inode[p]:ni+1
        );
        for (int h in {1..ni}) {
          arcs(
            i_allocated[h]:t_create_step21x[p],
            t_create_step21x[p]:i_allocated[h]
          );
        }
    /* ---------- Create step 22 ---------- */
    // --- file.d_inode = &itmp
    for (int i in {1..nd}) {
      for (int k in {2..ni+1}) {
        trans
          t_create_step22[p][i][k];
        arcs(
          p_create_line22[p]:t_create_step22[p][i][k],
            t_create_step22[p][i][k]:p_create_line23[p],
            d_inode[i]:t_create_step22[p][i][k]:tk(d_inode[i]),
            t_create_step22[p][i][k]:d_inode[i]:k
        );
        guard(
          t_create_step22[p][i][k]:tk(p_file[p])==i & tk(p_inode[p])==k
        );
      }
    }
    /* ---------- Create step 23 ---------- */
    // --- spin_unlock(inode_lock)
        trans
          t_create_step23[p];
        arcs(
          p_create_line23[p]:t_create_step23[p],
            t_create_step23[p]:p_create_line24[p],
            t_create_step23[p]:inode_lock
        );
        inhibit(inode_lock:t_create_step23[p]);
    /* ---------- Create step 24 ---------- */
    // --- if (!file.d_inode->is_allocated)
    for (int k in {1..ni}) {
        trans
          t_create_step24_then[p][k],
          t_create_step24_else[p][k];
        arcs(
          p_create_line24[p]:t_create_step24_then[p][k],
            t_create_step24_then[p][k]:p_create_line25[p],
          p_create_line24[p]:t_create_step24_else[p][k],
            t_create_step24_else[p][k]:p_create_line30[p]
        );
        guard(
          t_create_step24_then[p][k]:tk(p_inode[p])==k & tk(i_allocated[k])==0,
          t_create_step24_else[p][k]:tk(p_inode[p])==k & tk(i_allocated[k])>0
        );
    }
        /* none available */
        trans
          t_create_step24_thenx[p];
        arcs(
          p_create_line24[p]:t_create_step24_thenx[p],
            t_create_step24_thenx[p]:p_create_line25[p]
        );
        guard(
          t_create_step24_thenx[p]:tk(p_inode[p])==ni+1
        );
    /* ---------- Create step 25 ---------- */
    // --- atomic_write(file.d_count, 0)
    for (int i in {1..nd}) {
        trans
          t_create_step25[p][i];
        arcs(
          p_create_line25[p]:t_create_step25[p][i],
            t_create_step25[p][i]:p_create_line26[p],
            d_count[i]:t_create_step25[p][i]:tk(d_count[i]),
            d_allocated[i]:t_create_step25[p][i]:tk(d_allocated[i]),
            d_parent[i]:t_create_step25[p][i]:tk(d_parent[i])
        );
        guard(
          t_create_step25[p][i]:tk(p_file[p])==i
        );
    }
    /* ---------- Create step 26 ---------- */
    // --- dput(parent)
    for (int j in {1..nd}) {
        trans
          t_create_step26[p][j];
        arcs(
          p_create_line26[p]:t_create_step26[p][j],
            t_create_step26[p][j]:p_create_line27[p],
            d_count[j]:t_create_step26[p][j]:cond(tk(d_count[j])>1, 1, 0)
        );
        guard(
          t_create_step26[p][j]:tk(p_parent[p])==j & tk(d_lock[j])>0
        );
    }
    /* ---------- Create step 27 ---------- */
    // --- spin_unlock(dcache_lock)
        trans
          t_create_step27[p];
        arcs(
          p_create_line27[p]:t_create_step27[p],
            t_create_step27[p]:p_create_line28[p],
            t_create_step27[p]:dcache_lock
        );
        inhibit(dcache_lock:t_create_step27[p]);
    /* ---------- Create step 28 ---------- */
    // --- up(parent.d_inode->i_mutex)
    for (int j in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_create_step28[p][j][k];
        arcs(
          p_create_line28[p]:t_create_step28[p][j][k],
            t_create_step28[p][j][k]:p_create_line29[p],
            t_create_step28[p][j][k]:i_mutex[k]
        );
        guard(
          t_create_step28[p][j][k]:tk(p_parent[p])==j & tk(d_inode[j])==k
        );
        inhibit(i_mutex[k]:t_create_step28[p][j][k]);
      }
    }
    /* ---------- Create step 29 ---------- */
    // --- return ERROR
        trans
          t_create_step29[p];
        arcs(
          p_create_line29[p]:t_create_step29[p],
            t_create_step29[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_create_step29[p]);
    /* ---------- Create step 30 ---------- */
    // --- update_parent()
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_create_step30[p][i][j];
        arcs(
          p_create_line30[p]:t_create_step30[p][i][j],
            t_create_step30[p][i][j]:p_create_line31[p],
            t_create_step30[p][i][j]:d_subdirs[j]
        );
        guard(
          t_create_step30[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j
        );
        inhibit(d_subdirs[j]:t_create_step30[p][i][j]:nd);
      }
    }
    /* ---------- Create step 31 ---------- */
    // --- path_release(file)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_create_step31[p][i][j];
        arcs(
          p_create_line31[p]:t_create_step31[p][i][j],
            t_create_step31[p][i][j]:p_create_line32[p],
            d_count[i]:t_create_step31[p][i][j]:cond(tk(d_count[i])>1, 1, 0)
        );
        cond(i!=j, arcs(
            d_count[j]:t_create_step31[p][i][j]:cond(tk(d_count[j])>1, 1, 0)), null);
        guard(
          t_create_step31[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j
        );
      }
    }
    /* ---------- Create step 32 ---------- */
    // --- spin_unlock(dcache_lock)
        trans
          t_create_step32[p];
        arcs(
          p_create_line32[p]:t_create_step32[p],
            t_create_step32[p]:p_create_line33[p],
            t_create_step32[p]:dcache_lock
        );
        inhibit(dcache_lock:t_create_step32[p]);
    /* ---------- Create step 33 ---------- */
    // --- up(parent.d_inode->i_mutex)
    for (int j in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_create_step33[p][j][k];
        arcs(
          p_create_line33[p]:t_create_step33[p][j][k],
            t_create_step33[p][j][k]:p_create_line34[p],
            t_create_step33[p][j][k]:i_mutex[k]
        );
        guard(
          t_create_step33[p][j][k]:tk(p_parent[p])==j & tk(d_inode[j])==k
        );
        inhibit(i_mutex[k]:t_create_step33[p][j][k]);
      }
    }
    /* ---------- Create step 34 ---------- */
    // --- return SUCCESS
        trans
          t_create_step34[p];
        arcs(
          p_create_line34[p]:t_create_step34[p],
            t_create_step34[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_create_step34[p]);


    /* ----------------------------------- */
    /* Unlink "program counters" */
    /* ----------------------------------- */
    place
      p_unlink_lookup[p],       // path_lookup(parent, file)
      p_unlink_line1[p],        // if (!file.is_allocated)
      p_unlink_line2[p],        //  return ERROR
      p_unlink_line3[p],        // if(is_directory(file))
      p_unlink_line4[p],        //  path_release(file)
      p_unlink_line5[p],        //  return ERROR
      p_unlink_line6[p],        // down(file.d_inode->i_mutex)
      p_unlink_line7[p],        // spin_lock(dcache_lock)
      p_unlink_line8[p],        // while (atomic_read(file.d_count) != 0)
      p_unlink_line9[p],        //  spin_lock(file.d_lock)
      p_unlink_line10[p],       //  if (atomic_read(file.d_count) == 2)
      p_unlink_line11[p],       //   atomic_write(file.d_count, 0)
      p_unlink_line12[p],       // spin_unlock(file.d_lock)
      p_unlink_line13[p],       // spin_lock(inode_lock)
      p_unlink_line14[p],       // while (atomic_read(file.d_inode->i_lock) !=0 )
      p_unlink_line15[p],       //  spin_lock(file.d_inode->i_lock)
      p_unlink_line16[p],       //  if (atomic_read(file.d_inode->i_count) == 1)
      p_unlink_line17[p],       //   atomic_write(file.d_inode->i_count, 0)
      p_unlink_line18[p],       //  spin_unlock(file.d_inode->i_lock)
      p_unlink_line19[p],       // spin_unlock(inode_lock)
      p_unlink_line20[p],       // update_parent()
      p_unlink_line21[p],       // dput(parent)
      p_unlink_line22[p],       // spin_unlock(dcache_lock)
      p_unlink_line23[p];       // return SUCCESS
    partition(
      3*nd-2+ni+8*p-5:
       p_unlink_line1[p]:p_unlink_line2[p]:p_unlink_line3[p]:
       p_unlink_line4[p]:p_unlink_line5[p]:p_unlink_line6[p]:
       p_unlink_line7[p]:p_unlink_line8[p]:p_unlink_line9[p]:
       p_unlink_line10[p]:p_unlink_line11[p]:p_unlink_line12[p]:
       p_unlink_line13[p]:p_unlink_line14[p]:p_unlink_line15[p]:
       p_unlink_line16[p]:p_unlink_line17[p]:p_unlink_line18[p]:
       p_unlink_line19[p]:p_unlink_line20[p]:p_unlink_line21[p]:
       p_unlink_line22[p]:p_unlink_line23[p]:p_unlink_lookup[p]
    );

    /* ----- Unlink transitions ----- */

    /* ---------- Unlink step 0 ---------- */
    // --- initiate call: store new params
    for (int i in {1..nd}) {
        trans
          t_unlink_step0[p][i];
        arcs(
          p_start_unlink[p]:t_unlink_step0[p][i],
            t_unlink_step0[p][i]:p_unlink_line1[p],
            p_file[p]:t_unlink_step0[p][i]:tk(p_file[p]),
            p_parent[p]:t_unlink_step0[p][i]:tk(p_parent[p]),
            /* store new values */
            t_unlink_step0[p][i]:p_file[p]:i
        );
        inhibit(p_unlink_line1[p]:t_unlink_step0[p][i]);
    }
    /* ---------- Unlink step 1 ---------- */
    // --- if (!file.is_allocated)
    for (int i in {1..nd}) {
        trans
          t_unlink_step1_then[p][i],
          t_unlink_step1_else[p][i];
        arcs(
          p_unlink_line1[p]:t_unlink_step1_then[p][i],
            t_unlink_step1_then[p][i]:p_unlink_line2[p],
          p_unlink_line1[p]:t_unlink_step1_else[p][i],
            t_unlink_step1_else[p][i]:p_unlink_lookup[p]
        );
        guard(
          t_unlink_step1_then[p][i]:tk(p_file[p])==i & tk(d_allocated[i])==0,
          t_unlink_step1_else[p][i]:tk(p_file[p])==i & tk(d_allocated[i])>0
        );
    }
    /* ---------- Unlink step 2 ---------- */
    // --- return ERROR
        trans
          t_unlink_step2[p];
        arcs(
          p_unlink_line2[p]:t_unlink_step2[p],
            t_unlink_step2[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_unlink_step2[p]);
    /* ---------- Unlink: lookup ---------- */
    // --- path_lookup(parent,file)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_unlink_lookup[p][i][j];
        arcs(
          p_unlink_lookup[p]:t_unlink_lookup[p][i][j],
            t_unlink_lookup[p][i][j]:p_unlink_line3[p],
            t_unlink_lookup[p][i][j]:d_count[i]:cond(tk(d_allocated[i])>0, 1, 0),
            p_parent[p]:t_unlink_lookup[p][i][j]:tk(p_parent[p]),
            t_unlink_lookup[p][i][j]:p_parent[p]:j
        );
        cond(i!=j, arcs(
            t_unlink_lookup[p][i][j]:d_count[j]:cond(tk(d_allocated[j])>0, 1, 0)), null);
        guard(
          t_unlink_lookup[p][i][j]:tk(dcache_lock)>0 & tk(p_file[p])==i & tk(d_parent[i])==j
        );
        inhibit(d_count[i]:t_unlink_lookup[p][i][j]:np+1);
        cond(i!=j, inhibit(d_count[j]:t_unlink_lookup[p][i][j]:np+1), null);
      }
    }
    /* ---------- Unlink step 3 ---------- */
    // --- if (is_directory(file))
    for (int i in {1..nd}) {
        trans
          t_unlink_step3_then[p][i],
          t_unlink_step3_else[p][i];
        arcs(
          p_unlink_line3[p]:t_unlink_step3_then[p][i],
            t_unlink_step3_then[p][i]:p_unlink_line4[p],
          p_unlink_line3[p]:t_unlink_step3_else[p][i],
            t_unlink_step3_else[p][i]:p_unlink_line6[p]
        );
        guard(
          t_unlink_step3_then[p][i]:tk(p_file[p])==i & tk(d_subdirs[i])>0,
          t_unlink_step3_else[p][i]:tk(p_file[p])==i & tk(d_subdirs[i])==0
        );
    }
    /* ---------- Unlink step 4 ---------- */
    // --- path_release(file)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_unlink_step4[p][i][j];
        arcs(
          p_unlink_line4[p]:t_unlink_step4[p][i][j],
            t_unlink_step4[p][i][j]:p_unlink_line5[p],
            d_count[i]:t_unlink_step4[p][i][j]:
              cond(tk(d_allocated[i])>0 & tk(d_count[i])>1, 1, 0)
        );
        cond(i!=j, arcs(
            d_count[j]:t_unlink_step4[p][i][j]:
              cond(tk(d_allocated[j])>0 & tk(d_count[j])>1, 1, 0)), null);
        guard(
          t_unlink_step4[p][i][j]:tk(p_file[p])==i & tk(d_parent[i])==j
        );
      }
    }
    /* ---------- Unlink step 5 ---------- */
    // --- return ERROR
        trans
          t_unlink_step5[p];
        arcs(
          p_unlink_line5[p]:t_unlink_step5[p],
            t_unlink_step5[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_unlink_step5[p]);
    /* ---------- Unlink step 6 ---------- */
    // --- down(file.d_inode->i_mutex)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_unlink_step6[p][i][k];
        arcs(
          p_unlink_line6[p]:t_unlink_step6[p][i][k],
            t_unlink_step6[p][i][k]:p_unlink_line7[p],
            i_mutex[k]:t_unlink_step6[p][i][k]
        );
        guard(
          t_unlink_step6[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
      }
    }
    /* ---------- Unlink step 7 ---------- */
    // --- spin_lock(dcache_lock)
        trans
          t_unlink_step7[p];
        arcs(
          p_unlink_line7[p]:t_unlink_step7[p],
            t_unlink_step7[p]:p_unlink_line8[p],
            dcache_lock:t_unlink_step7[p]
        );
    /* ---------- Unlink step 8 ---------- */
    // --- while (atomic_read(file.d_count) != 0)
    for (int i in {1..nd}) {
        trans
          t_unlink_step8_while[p][i],
          t_unlink_step8_else[p][i];
        arcs(
          p_unlink_line8[p]:t_unlink_step8_while[p][i],
            t_unlink_step8_while[p][i]:p_unlink_line9[p],
          p_unlink_line8[p]:t_unlink_step8_else[p][i],
            t_unlink_step8_else[p][i]:p_unlink_line13[p]
        );
        guard(
          t_unlink_step8_while[p][i]:tk(p_file[p])==i & tk(d_count[i])!=0,
          t_unlink_step8_else[p][i]: tk(p_file[p])==i & tk(d_count[i])==0
        );
    }
    /* ---------- Unlink step 9 ---------- */
    // --- spin_lock(file.d_lock)
    for (int i in {1..nd}) {
        trans
          t_unlink_step9[p][i];
        arcs(
          p_unlink_line9[p]:t_unlink_step9[p][i],
            t_unlink_step9[p][i]:p_unlink_line10[p],
            d_lock[i]:t_unlink_step9[p][i]
        );
        guard(
          t_unlink_step9[p][i]:tk(p_file[p])==i
        );
    }
    /* ---------- Unlink step 10 ---------- */
    // --- if (atomic_read(file.d_count) == 2)
    for (int i in {1..nd}) {
        trans
          t_unlink_step10_then[p][i],
          t_unlink_step10_else[p][i];
        arcs(
          p_unlink_line10[p]:t_unlink_step10_then[p][i],
            t_unlink_step10_then[p][i]:p_unlink_line11[p],
          p_unlink_line10[p]:t_unlink_step10_else[p][i],
            t_unlink_step10_else[p][i]:p_unlink_line12[p]
        );
        guard(
          t_unlink_step10_then[p][i]:tk(p_file[p])==i & tk(d_count[i])==2,
          t_unlink_step10_else[p][i]:tk(p_file[p])==i & tk(d_count[i])!=2
        );
    }
    /* ---------- Unlink step 11 ---------- */
    // --- deallocate(file)
    for (int i in {1..nd}) {
        trans
          t_unlink_step11[p][i];
        arcs(
          p_unlink_line11[p]:t_unlink_step11[p][i],
            t_unlink_step11[p][i]:p_unlink_line12[p],
            d_count[i]:t_unlink_step11[p][i]:tk(d_count[i]),
            d_allocated[i]:t_unlink_step11[p][i]:tk(d_allocated[i])
        );
        guard(
          t_unlink_step11[p][i]:tk(p_file[p])==i
        );
    }
    /* ---------- Unlink step 12 ---------- */
    // --- spin_unlock(file.d_lock)
    for (int i in {1..nd}) {
        trans
          t_unlink_step12[p][i];
        arcs(
          p_unlink_line12[p]:t_unlink_step12[p][i],
            t_unlink_step12[p][i]:p_unlink_line8[p],
            t_unlink_step12[p][i]:d_lock[i]
        );
        guard(
          t_unlink_step12[p][i]:tk(p_file[p])==i
        );
        inhibit(d_lock[i]:t_unlink_step12[p][i]);
    }
    /* ---------- Unlink step 13 ---------- */
    // --- spin_lock(inode_lock)
        trans
          t_unlink_step13[p];
        arcs(
          p_unlink_line13[p]:t_unlink_step13[p],
            t_unlink_step13[p]:p_unlink_line14[p],
            inode_lock:t_unlink_step13[p]
        );
    /* ---------- Unlink step 14 ---------- */
    // --- while (atomic_read(file.d_inode->i_count) != 0)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_unlink_step14_while[p][i][k],
          t_unlink_step14_else[p][i][k];
        arcs(
          p_unlink_line14[p]:t_unlink_step14_while[p][i][k],
            t_unlink_step14_while[p][i][k]:p_unlink_line15[p],
          p_unlink_line14[p]:t_unlink_step14_else[p][i][k],
            t_unlink_step14_else[p][i][k]:p_unlink_line19[p]
        );
        guard(
          t_unlink_step14_while[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k & tk(i_count[k])!=0,
          t_unlink_step14_else[p][i][k]: tk(p_file[p])==i & tk(d_inode[i])==k & tk(i_count[k])==0
        );
      }
    }
    /* ---------- Unlink step 15 ---------- */
    // --- spin_lock(file.d_inode->i_lock)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_unlink_step15[p][i][k];
        arcs(
          p_unlink_line15[p]:t_unlink_step15[p][i][k],
            t_unlink_step15[p][i][k]:p_unlink_line16[p],
            i_lock[k]:t_unlink_step15[p][i][k]
        );
        guard(
          t_unlink_step15[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
      }
    }
    /* ---------- Unlink step 16 ---------- */
    // --- if (atomic_read(file.d_inode->i_count) == 1)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_unlink_step16_then[p][i][k],
          t_unlink_step16_else[p][i][k];
        arcs(
          p_unlink_line16[p]:t_unlink_step16_then[p][i][k],
            t_unlink_step16_then[p][i][k]:p_unlink_line17[p],
          p_unlink_line16[p]:t_unlink_step16_else[p][i][k],
            t_unlink_step16_else[p][i][k]:p_unlink_line18[p]
        );
        guard(
          t_unlink_step16_then[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k & tk(i_count[k])==1,
          t_unlink_step16_else[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k & tk(i_count[k])!=1
        );
      }
    }
    /* ---------- Unlink step 17 ---------- */
    // --- atomic_write(file.d_inode->i_count, 0)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_unlink_step17[p][i][k];
        arcs(
          p_unlink_line17[p]:t_unlink_step17[p][i][k],
            t_unlink_step17[p][i][k]:p_unlink_line18[p],
            i_count[k]:t_unlink_step17[p][i][k]:tk(i_count[k]),
            i_allocated[k]:t_unlink_step17[p][i][k]:tk(i_allocated[k])
        );
        guard(
          t_unlink_step17[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
      }
    }
    /* ---------- Unlink step 18 ---------- */
    // --- spin_unlock(file.d_inode->i_lock)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_unlink_step18[p][i][k];
        arcs(
          p_unlink_line18[p]:t_unlink_step18[p][i][k],
            t_unlink_step18[p][i][k]:p_unlink_line14[p],
            t_unlink_step18[p][i][k]:i_lock[k]
        );
        guard(
          t_unlink_step18[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
        inhibit(i_lock[k]:t_unlink_step18[p][i][k]);
      }
    }
    /* ---------- Unlink step 19 ---------- */
    // --- spin_unlock(inode_lock)
        trans
          t_unlink_step19[p];
        arcs(
          p_unlink_line19[p]:t_unlink_step19[p],
            t_unlink_step19[p]:p_unlink_line20[p],
            t_unlink_step19[p]:inode_lock
        );
        inhibit(inode_lock:t_unlink_step19[p]);
    /* ---------- Unlink step 20 ---------- */
    // --- update_parent()
      for (int j in {1..nd}) {
        trans
          t_unlink_step20[p][j];
        arcs(
          p_unlink_line20[p]:t_unlink_step20[p][j],
            t_unlink_step20[p][j]:p_unlink_line21[p],
            d_subdirs[j]:t_unlink_step20[p][j]
        );
        guard(
          t_unlink_step20[p][j]:tk(p_parent[p])==j
        );
      }
    /* ---------- Unlink step 21 ---------- */
    // --- dput(parent)
      for (int j in {1..nd}) {
        trans
          t_unlink_step21[p][j];
        arcs(
          p_unlink_line21[p]:t_unlink_step21[p][j],
            t_unlink_step21[p][j]:p_unlink_line22[p],
            d_count[j]:t_unlink_step21[p][j]:cond(tk(d_count[j])>1, 1, 0)
        );
        guard(
          t_unlink_step21[p][j]:tk(p_parent[p])==j & tk(d_lock[j])>0
        );
      }
    /* ---------- Unlink step 22 ---------- */
    // --- spin_unlock(dcache_lock)
        trans
          t_unlink_step22[p];
        arcs(
          p_unlink_line22[p]:t_unlink_step22[p],
            t_unlink_step22[p]:p_unlink_line23[p],
            t_unlink_step22[p]:dcache_lock
        );
        inhibit(dcache_lock:t_unlink_step22[p]);
    /* ---------- Unlink step 23 ---------- */
    // --- return SUCCESS
        trans
          t_unlink_step23[p];
        arcs(
          p_unlink_line23[p]:t_unlink_step23[p],
            t_unlink_step23[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_unlink_step23[p]);


    /* ----------------------------------- */
    /* PN "program counters"  for mkdir()  */
    /* ----------------------------------- */
    place
      p_mkdir_lookup[p],        // path_lookup(parent,dir)
      p_mkdir_line1[p],         // if (dir.is_allocated)
      p_mkdir_line2[p],         //  path_release(dir)
      p_mkdir_line3[p],         //  return ERROR
      p_mkdir_line4[p],         // if (!parent.is_allocated)
      p_mkdir_line5[p],         //  path_release(dir)
      p_mkdir_line6[p],         //  return ERROR
      p_mkdir_line7[p],         // spin_lock(dcache_lock)
      p_mkdir_line8[p],         // dir = allocate_dentry()
      p_mkdir_line9[p],         // if (!dir.is_allocated)
      p_mkdir_line10[p],        //  spin_unlock(dcache_loc)
      p_mkdir_line11[p],        //  dput(parent)
      p_mkdir_line12[p],        //  return ERROR
      p_mkdir_line13[p],        // dget(dir)
      p_mkdir_line14[p],        // spin_lock(inode_lock)
      p_mkdir_line15[p],        // itmp = allocate_inode(dir)
      p_mkdir_line16[p],        // dir.d_inode = &itmp
      p_mkdir_line17[p],        // if (dir.d_inode->is_allocated)
      p_mkdir_line18[p],        //  down(dir.d_inode->imutex)
      p_mkdir_line19[p],        // spin_unlock(inode_lock)
      p_mkdir_line20[p],        // if (!dir.d_inode->is_allocated)
      p_mkdir_line21[p],        //  atomic_write(d_count)
      p_mkdir_line22[p],        //  dput(parent)
      p_mkdir_line23[p],        //  spin_unlock(dcache_lock)
      p_mkdir_line24[p],        //  return ERROR
      p_mkdir_line25[p],        // dir.subdirs = 1;
      p_mkdir_line26[p],        // update(parent)
      p_mkdir_line27[p],        // path_release(file)
      p_mkdir_line28[p],        // spin_unlock(dcache_lock)
      p_mkdir_line29[p],        // up(dir.d_inode->i_mutex)
      p_mkdir_line30[p];        // return SUCCESS
    partition(
      3*nd-2+ni+8*p-6:
       p_mkdir_line1[p]:p_mkdir_line2[p]:p_mkdir_line3[p]:
       p_mkdir_line4[p]:p_mkdir_line5[p]:p_mkdir_line6[p]:
       p_mkdir_line7[p]:p_mkdir_line8[p]:p_mkdir_line9[p]:
       p_mkdir_line10[p]:p_mkdir_line11[p]:p_mkdir_line12[p]:
       p_mkdir_line13[p]:p_mkdir_line14[p]:p_mkdir_line15[p]:
       p_mkdir_line16[p]:p_mkdir_line17[p]:p_mkdir_line18[p]:
       p_mkdir_line19[p]:p_mkdir_line20[p]:p_mkdir_line21[p]:
       p_mkdir_line22[p]:p_mkdir_line23[p]:p_mkdir_line24[p]:
       p_mkdir_line25[p]:p_mkdir_line26[p]:p_mkdir_line27[p]:
       p_mkdir_line28[p]:p_mkdir_line29[p]:p_mkdir_line30[p]:
       p_mkdir_lookup[p]
    );

    /* ----- mkdir transitions ----- */

    /* ---------- Mkdir step 0 ---------- */
    // --- initiate call: store new params
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_mkdir_step0[p][i][j];
        arcs(
          p_start_mkdir[p]:t_mkdir_step0[p][i][j],
            t_mkdir_step0[p][i][j]:p_mkdir_lookup[p],
            p_file[p]:t_mkdir_step0[p][i][j]:tk(p_file[p]),
            p_parent[p]:t_mkdir_step0[p][i][j]:tk(p_parent[p]),
            p_inode[p]:t_mkdir_step0[p][i][j]:tk(p_inode[p]),
            /* store new values */
            t_mkdir_step0[p][i][j]:p_file[p]:i,
            t_mkdir_step0[p][i][j]:p_parent[p]:j
        );
      }
    }
    /* ---------- mkdir: lookup ---------- */
    // --- path_lookup(parent,file)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_mkdir_lookup[p][i][j];
        arcs(
          p_mkdir_lookup[p]:t_mkdir_lookup[p][i][j],
            t_mkdir_lookup[p][i][j]:p_mkdir_line1[p],
            t_mkdir_lookup[p][i][j]:d_count[i]:cond(tk(d_allocated[i])>0, 1, 0)
        );
        cond(i!=j, arcs(
            t_mkdir_lookup[p][i][j]:d_count[j]:cond(tk(d_allocated[j])>0, 1, 0)), null);
        guard(
          t_mkdir_lookup[p][i][j]:tk(dcache_lock)>0 & tk(p_file[p])==i & tk(p_parent[p])==j
        );
        inhibit(d_count[i]:t_mkdir_lookup[p][i][j]:np+1);
        cond(i!=j, inhibit(d_count[j]:t_mkdir_lookup[p][i][j]:np+1), null);
      }
    }
    /* ---------- Mkdir step 1 ---------- */
    // --- if (dir.is_allocated)
    for (int i in {1..nd}) {
        trans
          t_mkdir_step1_then[p][i],
          t_mkdir_step1_else[p][i];
        arcs(
          p_mkdir_line1[p]:t_mkdir_step1_then[p][i],
            t_mkdir_step1_then[p][i]:p_mkdir_line2[p],
          p_mkdir_line1[p]:t_mkdir_step1_else[p][i],
            t_mkdir_step1_else[p][i]:p_mkdir_line4[p]
        );
        guard(
          t_mkdir_step1_then[p][i]:tk(p_file[p])==i & tk(d_allocated[i])>0,
          t_mkdir_step1_else[p][i]:tk(p_file[p])==i & tk(d_allocated[i])==0
        );
    }
    /* ---------- Mkdir step 2 ---------- */
    // --- path_release(dir)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_mkdir_step2[p][i][j];
        arcs(
          p_mkdir_line2[p]:t_mkdir_step2[p][i][j],
            t_mkdir_step2[p][i][j]:p_mkdir_line3[p],
            d_count[i]:t_mkdir_step2[p][i][j]:cond(tk(d_count[i])>1, 1, 0)
        );
        cond(i!=j, arcs(
            d_count[j]:t_mkdir_step2[p][i][j]:cond(tk(d_count[j])>1, 1, 0)), null);
        guard(
          t_mkdir_step2[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j
        );
      }
    }
    /* ---------- Mkdir step 3 ---------- */
    // --- return ERROR
        trans
          t_mkdir_step3[p];
        arcs(
          p_mkdir_line3[p]:t_mkdir_step3[p],
            t_mkdir_step3[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_mkdir_step3[p]);
    /* ---------- Mkdir step 4 ---------- */
    // --- if (!parent.is_allocated)
    for (int j in {1..nd}) {
        trans
          t_mkdir_step4_err[p][j],
          t_mkdir_step4_then[p][j],
          t_mkdir_step4_else[p][j];
        arcs(
          p_mkdir_line4[p]:t_mkdir_step4_err[p][j],
            t_mkdir_step4_err[p][j]:p_mkdir_line5[p],
          p_mkdir_line4[p]:t_mkdir_step4_then[p][j],
            t_mkdir_step4_then[p][j]:p_mkdir_line5[p],
          p_mkdir_line4[p]:t_mkdir_step4_else[p][j],
            t_mkdir_step4_else[p][j]:p_mkdir_line7[p]
        );
        guard(
          t_mkdir_step4_err[p][j]: tk(p_parent[p])==j & tk(d_allocated[j])>0 & tk(d_subdirs[j])==0,
          t_mkdir_step4_then[p][j]:tk(p_parent[p])==j & tk(d_allocated[j])==0,
          t_mkdir_step4_else[p][j]:tk(p_parent[p])==j & tk(d_allocated[j])>0 & tk(d_subdirs[j])>0
        );
    }
    /* ---------- Mkdir step 5 ---------- */
    // --- path_release(dir)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_mkdir_step5[p][i][j];
        arcs(
          p_mkdir_line5[p]:t_mkdir_step5[p][i][j],
            t_mkdir_step5[p][i][j]:p_mkdir_line6[p],
            d_count[i]:t_mkdir_step5[p][i][j]:cond(tk(d_count[i])>1, 1, 0)
        );
        cond(i!=j, arcs(
            d_count[j]:t_mkdir_step5[p][i][j]:cond(tk(d_count[j])>1, 1, 0)), null);
        guard(
          t_mkdir_step5[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j
        );
      }
    }
    /* ---------- Mkdir step 6 ---------- */
    // --- return ERROR
        trans
          t_mkdir_step6[p];
        arcs(
          p_mkdir_line6[p]:t_mkdir_step6[p],
            t_mkdir_step6[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_mkdir_step6[p]);
    /* ---------- Mkdir step 7 ---------- */
    // --- spin_lock(dcache_lock)
        trans
          t_mkdir_step7[p];
        arcs(
          p_mkdir_line7[p]:t_mkdir_step7[p],
            t_mkdir_step7[p]:p_mkdir_line8[p],
            dcache_lock:t_mkdir_step7[p]
        );
    /* ---------- Mkdir step 8 ---------- */
    // --- allocate_dentry
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_mkdir_step8[p][i][j];
        arcs(
          p_mkdir_line8[p]:t_mkdir_step8[p][i][j],
            t_mkdir_step8[p][i][j]:p_mkdir_line9[p],
            d_allocated[i]:t_mkdir_step8[p][i][j]:tk(d_allocated[i]),
            t_mkdir_step8[p][i][j]:d_allocated[i],
            d_count[i]:t_mkdir_step8[p][i][j]:tk(d_count[i]),
            t_mkdir_step8[p][i][j]:d_count[i],
            d_lock[i]:t_mkdir_step8[p][i][j]:tk(d_lock[i]),
            t_mkdir_step8[p][i][j]:d_lock[i],
            d_parent[i]:t_mkdir_step8[p][i][j]:tk(d_parent[i]),
            t_mkdir_step8[p][i][j]:d_parent[i]:j
        );
        guard(
          t_mkdir_step8[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j & tk(d_allocated[i])==0
        );
      }
    }
    
    for (int i in {1..nd}) {
        trans
          t_mkdir_step8x[p][i];
        arcs(
          p_mkdir_line8[p]:t_mkdir_step8x[p][i],
            t_mkdir_step8x[p][i]:p_mkdir_line10[p]
        );
        guard(
          t_mkdir_step8x[p][i]:tk(p_file[p])==i & tk(d_allocated[i])>0
        );
    }

    /* ---------- Mkdir step 9 ---------- */
    // --- if (!dir.is_allocated)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_mkdir_step9_then[p][i][j],
          t_mkdir_step9_else[p][i][j];
        arcs(
          p_mkdir_line9[p]:t_mkdir_step9_then[p][i][j],
            t_mkdir_step9_then[p][i][j]:p_mkdir_line10[p],
          p_mkdir_line9[p]:t_mkdir_step9_else[p][i][j],
            t_mkdir_step9_else[p][i][j]:p_mkdir_line13[p]
        );
        guard(
          t_mkdir_step9_then[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j & tk(d_subdirs[j])==0,
          t_mkdir_step9_else[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j & tk(d_subdirs[j])>0
        );
      }
    }
    /* ---------- Mkdir step 10 ---------- */
    // --- spin_unlock(dcache_lock)
        trans
          t_mkdir_step10[p];
        arcs(
          p_mkdir_line10[p]:t_mkdir_step10[p],
            t_mkdir_step10[p]:p_mkdir_line11[p],
            t_mkdir_step10[p]:dcache_lock
        );
        inhibit(dcache_lock:t_mkdir_step10[p]);
    /* ---------- Mkdir step 11 ---------- */
    // --- dput(parent)
    for (int j in {1..nd}) {
        trans
          t_mkdir_step11[p][j];
        arcs(
          p_mkdir_line11[p]:t_mkdir_step11[p][j],
            t_mkdir_step11[p][j]:p_mkdir_line12[p],
            d_count[j]:t_mkdir_step11[p][j]:cond(tk(d_count[j])>1, 1, 0)
        );
        guard(
          t_mkdir_step11[p][j]:tk(p_parent[p])==j & tk(d_lock[j])>0
        );
    }
    /* ---------- Mkdir step 12 ---------- */
    // --- return ERROR
        trans
          t_mkdir_step12[p];
        arcs(
          p_mkdir_line12[p]:t_mkdir_step12[p],
            t_mkdir_step12[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_mkdir_step12[p]);
    /* ---------- Mkdir step 13 ---------- */
    // --- dget(dir)
    for (int i in {1..nd}) {
        trans
          t_mkdir_step13[p][i];
        arcs(
          p_mkdir_line13[p]:t_mkdir_step13[p][i],
            t_mkdir_step13[p][i]:p_mkdir_line14[p],
            t_mkdir_step13[p][i]:d_count[i]:cond(tk(d_count[i])>0,1,0)
        );
        guard(
          t_mkdir_step13[p][i]:tk(p_file[p])==i & tk(d_lock[i])>0
        );
        inhibit(d_count[i]:t_mkdir_step13[p][i]:np+1);
    }
    /* ---------- Mkdir step 14 ---------- */
    // --- spin_lock(inode_lock)
        trans
          t_mkdir_step14[p];
        arcs(
          p_mkdir_line14[p]:t_mkdir_step14[p],
            t_mkdir_step14[p]:p_mkdir_line15[p],
            inode_lock:t_mkdir_step14[p]
        );
    /* ---------- Mkdir step 15 ---------- */
    // --- allocate_inode(dir)
    for (int k in {2..ni}) {
        trans
          t_mkdir_step15[p][k];
        arcs(
          p_mkdir_line15[p]:t_mkdir_step15[p][k],
            t_mkdir_step15[p][k]:p_mkdir_line16[p],
            i_allocated[k]:t_mkdir_step15[p][k]:tk(i_allocated[k]),
            t_mkdir_step15[p][k]:i_allocated[k],
            i_count[k]:t_mkdir_step15[p][k]:tk(i_count[k]),
            t_mkdir_step15[p][k]:i_count[k],
            i_mutex[k]:t_mkdir_step15[p][k]:tk(i_mutex[k]),
            t_mkdir_step15[p][k]:i_mutex[k],
            i_lock[k]:t_mkdir_step15[p][k]:tk(i_lock[k]),
            t_mkdir_step15[p][k]:i_lock[k],
            p_inode[p]:t_mkdir_step15[p][k]:tk(p_inode[p]),
            t_mkdir_step15[p][k]:p_inode[p]:k
        );
        guard(
          t_mkdir_step15[p][k]:tk(i_allocated[k])==0
        );
        /* allocate first inode available */
        /* i.e. if allocating inode k, then all inodes before k are already allocated */
        for (int h in {1..k-1}) {
          arcs(
            i_allocated[h]:t_mkdir_step15[p][k],
            t_mkdir_step15[p][k]:i_allocated[h]
          );
        }
    }
        /* no inodes available */
        trans
          t_mkdir_step15x[p];
        arcs(
          p_mkdir_line15[p]:t_mkdir_step15x[p],
            t_mkdir_step15x[p]:p_mkdir_line16[p],
            p_inode[p]:t_mkdir_step15x[p]:tk(p_inode[p]),
            t_mkdir_step15x[p]:p_inode[p]:ni+1
        );
        for (int h in {1..ni}) {
          arcs(
            i_allocated[h]:t_mkdir_step15x[p],
            t_mkdir_step15x[p]:i_allocated[h]
          );
        }
    /* ---------- Mkdir step 16 ---------- */
    // --- dir.d_inode = &itmp
    for (int i in {1..nd}) {
      for (int k in {2..ni+1}) {
        trans
          t_mkdir_step16[p][i][k];
        arcs(
          p_mkdir_line16[p]:t_mkdir_step16[p][i][k],
            t_mkdir_step16[p][i][k]:p_mkdir_line17[p],
            d_inode[i]:t_mkdir_step16[p][i][k]:tk(d_inode[i]),
            t_mkdir_step16[p][i][k]:d_inode[i]:k
        );
        guard(
          t_mkdir_step16[p][i][k]:tk(p_file[p])==i & tk(p_inode[p])==k
        );
      }
    }
    /* ---------- Mkdir step 17 ---------- */
    // --- if (dir.d_inode->is_allocated)
    for (int k in {1..ni}) {
        trans
          t_mkdir_step17_then[p][k],
          t_mkdir_step17_else[p][k];
        arcs(
          p_mkdir_line17[p]:t_mkdir_step17_then[p][k],
            t_mkdir_step17_then[p][k]:p_mkdir_line18[p],
          p_mkdir_line17[p]:t_mkdir_step17_else[p][k],
            t_mkdir_step17_else[p][k]:p_mkdir_line19[p]
        );
        guard(
          t_mkdir_step17_then[p][k]:tk(p_inode[p])==k & tk(i_allocated[k])>0,
          t_mkdir_step17_else[p][k]:tk(p_inode[p])==k & tk(i_allocated[k])==0
        );
    }
        /* none available */
        trans
          t_mkdir_step17_elsex[p];
        arcs(
          p_mkdir_line17[p]:t_mkdir_step17_elsex[p],
            t_mkdir_step17_elsex[p]:p_mkdir_line19[p]
        );
        guard(
          t_mkdir_step17_elsex[p]:tk(p_inode[p])==ni+1
        );
    /* ---------- Mkdir step 18 ---------- */
    // --- down(dir.d_inode->i_mutex)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_mkdir_step18[p][i][k];
        arcs(
          p_mkdir_line18[p]:t_mkdir_step18[p][i][k],
            t_mkdir_step18[p][i][k]:p_mkdir_line19[p],
            i_mutex[k]:t_mkdir_step18[p][i][k]
        );
        guard(
          t_mkdir_step18[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
      }
    }
    /* ---------- Mkdir step 19 ---------- */
    // --- spin_unlock(inode_lock)
        trans
          t_mkdir_step19[p];
        arcs(
          p_mkdir_line19[p]:t_mkdir_step19[p],
            t_mkdir_step19[p]:p_mkdir_line20[p],
            t_mkdir_step19[p]:inode_lock
        );
        inhibit(inode_lock:t_mkdir_step19[p]);
    /* ---------- Mkdir step 20 ---------- */
    // --- if (!dir.d_inode->is_allocated)
    for (int k in {1..ni}) {
        trans
          t_mkdir_step20_then[p][k],
          t_mkdir_step20_else[p][k];
        arcs(
          p_mkdir_line20[p]:t_mkdir_step20_then[p][k],
            t_mkdir_step20_then[p][k]:p_mkdir_line21[p],
          p_mkdir_line20[p]:t_mkdir_step20_else[p][k],
            t_mkdir_step20_else[p][k]:p_mkdir_line25[p]
        );
        guard(
          t_mkdir_step20_then[p][k]:tk(p_inode[p])==k & tk(i_allocated[k])==0,
          t_mkdir_step20_else[p][k]:tk(p_inode[p])==k & tk(i_allocated[k])>0
        );
    }
        /* none available */
        trans
          t_mkdir_step20_thenx[p];
        arcs(
          p_mkdir_line20[p]:t_mkdir_step20_thenx[p],
            t_mkdir_step20_thenx[p]:p_mkdir_line21[p]
        );
        guard(
          t_mkdir_step20_thenx[p]:tk(p_inode[p])==ni+1
        );
    /* ---------- Mkdir step 21 ---------- */
    // --- atomic_write(dir.d_count, 0)
    for (int i in {1..nd}) {
        trans
          t_mkdir_step21[p][i];
        arcs(
          p_mkdir_line21[p]:t_mkdir_step21[p][i],
            t_mkdir_step21[p][i]:p_mkdir_line22[p],
            d_count[i]:t_mkdir_step21[p][i]:tk(d_count[i]),
            d_allocated[i]:t_mkdir_step21[p][i]:tk(d_allocated[i]),
            d_parent[i]:t_mkdir_step21[p][i]:tk(d_parent[i])
        );
        guard(
          t_mkdir_step21[p][i]:tk(p_file[p])==i
        );
    }
    /* ---------- Mkdir step 22 ---------- */
    // --- dput(parent)
    for (int j in {1..nd}) {
        trans
          t_mkdir_step22[p][j];
        arcs(
          p_mkdir_line22[p]:t_mkdir_step22[p][j],
            t_mkdir_step22[p][j]:p_mkdir_line23[p],
            d_count[j]:t_mkdir_step22[p][j]:cond(tk(d_count[j])>1, 1, 0)
        );
        guard(
          t_mkdir_step22[p][j]:tk(p_parent[p])==j & tk(d_lock[j])>0
        );
    }
    /* ---------- Mkdir step 23 ---------- */
    // --- spin_unlock(dcache_lock)
        trans
          t_mkdir_step23[p];
        arcs(
          p_mkdir_line23[p]:t_mkdir_step23[p],
            t_mkdir_step23[p]:p_mkdir_line24[p],
            t_mkdir_step23[p]:dcache_lock
        );
        inhibit(dcache_lock:t_mkdir_step23[p]);
    /* ---------- Mkdir step 24 ---------- */
    // --- return ERROR
        trans
          t_mkdir_step24[p];
        arcs(
          p_mkdir_line24[p]:t_mkdir_step24[p],
            t_mkdir_step24[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_mkdir_step24[p]);
    /* ---------- Mkdir step 25 ---------- */
    // --- dir.subdirs = 1
    for (int i in {1..nd}) {
        trans
          t_mkdir_step25[p][i];
        arcs(
          p_mkdir_line25[p]:t_mkdir_step25[p][i],
            t_mkdir_step25[p][i]:p_mkdir_line26[p],
            d_subdirs[i]:t_mkdir_step25[p][i]:tk(d_subdirs[i]),
            t_mkdir_step25[p][i]:d_subdirs[i]
        );
        guard(
          t_mkdir_step25[p][i]:tk(p_file[p])==i
        );
    }
    /* ---------- Mkdir step 26 ---------- */
    // --- update_parent()
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_mkdir_step26[p][i][j];
        arcs(
          p_mkdir_line26[p]:t_mkdir_step26[p][i][j],
            t_mkdir_step26[p][i][j]:p_mkdir_line27[p],
            t_mkdir_step26[p][i][j]:d_subdirs[j]
        );
        guard(
          t_mkdir_step26[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j
        );
        inhibit(d_subdirs[j]:t_mkdir_step26[p][i][j]:nd);
      }
    }
    /* ---------- Mkdir step 27 ---------- */
    // --- path_release(dir)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_mkdir_step27[p][i][j];
        arcs(
          p_mkdir_line27[p]:t_mkdir_step27[p][i][j],
            t_mkdir_step27[p][i][j]:p_mkdir_line28[p],
            d_count[i]:t_mkdir_step27[p][i][j]:cond(tk(d_count[i])>1, 1, 0)
        );
        cond(i!=j, arcs(
            d_count[j]:t_mkdir_step27[p][i][j]:cond(tk(d_count[j])>1, 1, 0)), null);
        guard(
          t_mkdir_step27[p][i][j]:tk(p_file[p])==i & tk(p_parent[p])==j
        );
      }
    }
    /* ---------- Mkdir step 28 ---------- */
    // --- spin_unlock(dcache_lock)
        trans
          t_mkdir_step28[p];
        arcs(
          p_mkdir_line28[p]:t_mkdir_step28[p],
            t_mkdir_step28[p]:p_mkdir_line29[p],
            t_mkdir_step28[p]:dcache_lock
        );
        inhibit(dcache_lock:t_mkdir_step28[p]);
    /* ---------- Mkdir step 29 ---------- */
    // --- up(dir.d_inode->i_mutex)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_mkdir_step29[p][i][k];
        arcs(
          p_mkdir_line29[p]:t_mkdir_step29[p][i][k],
            t_mkdir_step29[p][i][k]:p_mkdir_line30[p],
            t_mkdir_step29[p][i][k]:i_mutex[k]
        );
        guard(
          t_mkdir_step29[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
        inhibit(i_mutex[k]:t_mkdir_step29[p][i][k]);
      }
    }
    /* ---------- Mkdir step 30 ---------- */
    // --- return SUCCESS
        trans
          t_mkdir_step30[p];
        arcs(
          p_mkdir_line30[p]:t_mkdir_step30[p],
            t_mkdir_step30[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_mkdir_step30[p]);


    /* ----------------------------------- */
    /* Rmdir "program counters" */
    /* ----------------------------------- */
    place
      p_rmdir_line1[p],         // if (!dir.is_allocated)
      p_rmdir_line2[p],         //  return ERROR
      p_rmdir_lookup[p],        // path_lookup(parent, dir)
      p_rmdir_line3[p],         // if(!is_directory(dir))
      p_rmdir_line4[p],         //  path_release(dir)
      p_rmdir_line5[p],         //  return ERROR
      p_rmdir_line6[p],         // down(dir.d_inode->i_mutex)
      p_rmdir_line7[p],         // spin_lock(dcache_lock)
      p_rmdir_line8[p],         // if (num_children != 0)
      p_rmdir_line9[p],         //  spin_unlock(dcache_lock)
      p_rmdir_line10[p],        //  up (dir.d_inode->i_mutex)
      p_rmdir_line11[p],        //  dput(dir)
      p_rmdir_line12[p],        //  dput(parent)
      p_rmdir_line13[p],        //  return ERROR
      p_rmdir_line14[p],        // if (dir.d_inode->i_state & DELETING)
      p_rmdir_line14b[p],       //  spin_unlock(dcache_lock)
      p_rmdir_line15[p],        //  dput(dir)
      p_rmdir_line16[p],        //  dput(parent)
      p_rmdir_line17[p],        //  up (dir.d_inode->i_mutex)
      p_rmdir_line18[p],        //  return SUCCESS
      p_rmdir_line19[p],        // dir.d_inode->i_state |= DELETING
      p_rmdir_line20[p],        // up (dir.d_inode->i_mutex)
      p_rmdir_line21[p],        // parent = &dNULL
      p_rmdir_line22[p],        // update_parent()
      p_rmdir_line23[p],        // dput(parent)
      p_rmdir_line24[p],        // spin_unlock(dcache_lock)
      p_rmdir_line25[p],        // while (!wait_done)
      p_rmdir_line26[p],        //  spin_lock(dcache_lock)
      p_rmdir_line27[p],        //  spin_lock(dir.d_lock)
      p_rmdir_line28[p],        //  if (atomic_read(dir.d_count) == 2)
      p_rmdir_line29[p],        //   spin_lock(dir.d_inode->i_lock)
      p_rmdir_line30[p],        //   dir.d_inode->i_count--
      p_rmdir_line31[p],        //   if (atomic_read(dir.d_inode->i_count) >= 1)
      p_rmdir_line32[p],        //    dir.d_inode->i_state ^= DELETING
      p_rmdir_line32b[p],       //   else deallocate inode
      p_rmdir_line33[p],        //   spin_unlock(dir.d_inode->i_lock)
      p_rmdir_line34[p],        //   atomic_write(dir.d_count, 0)
      p_rmdir_wait_done[p],     //  if (atomic_read(dir.d_count) == 0)
                                //     { wait_done = 1; }
      p_rmdir_line35[p],        //  spin_unlock(dir.d_lock)
      p_rmdir_line36[p],        //  spin_unlock(dcache_lock)
      p_rmdir_line37[p];        // return SUCCESS
    partition(
      3*nd-2+ni+8*p-7:
       p_rmdir_line1[p]:p_rmdir_line2[p]:p_rmdir_line3[p]:
       p_rmdir_line4[p]:p_rmdir_line5[p]:p_rmdir_line6[p]:
       p_rmdir_line7[p]:p_rmdir_line8[p]:p_rmdir_line9[p]:
       p_rmdir_line10[p]:p_rmdir_line11[p]:p_rmdir_line12[p]:
       p_rmdir_line13[p]:p_rmdir_line14[p]:p_rmdir_line14b[p]:p_rmdir_line15[p]:
       p_rmdir_line16[p]:p_rmdir_line17[p]:p_rmdir_line18[p]:
       p_rmdir_line19[p]:p_rmdir_line20[p]:p_rmdir_line21[p]:
       p_rmdir_line22[p]:p_rmdir_line23[p]:p_rmdir_line24[p]:
       p_rmdir_line25[p]:p_rmdir_line26[p]:p_rmdir_line27[p]:
       p_rmdir_line28[p]:p_rmdir_line29[p]:p_rmdir_line30[p]:
       p_rmdir_line31[p]:p_rmdir_line32[p]:p_rmdir_line32b[p]:p_rmdir_line33[p]:
       p_rmdir_line34[p]:p_rmdir_line35[p]:p_rmdir_line36[p]:
       p_rmdir_line37[p]:p_rmdir_wait_done[p]:
       p_rmdir_lookup[p]
    );

    /* ----- rmdir transitions ----- */

    /* ---------- Rmdir step 0 ---------- */
    // --- initiate call: store new params
    for (int i in {2..nd}) {
        trans
          t_rmdir_step0[p][i];
        arcs(
          p_start_rmdir[p]:t_rmdir_step0[p][i],
            t_rmdir_step0[p][i]:p_rmdir_line1[p],
            p_file[p]:t_rmdir_step0[p][i]:tk(p_file[p]),
            p_inode[p]:t_rmdir_step0[p][i]:tk(p_inode[p]),
            p_parent[p]:t_rmdir_step0[p][i]:tk(p_parent[p]),
            /* store new values */
            t_rmdir_step0[p][i]:p_file[p]:i
        );
        inhibit(p_rmdir_lookup[p]:t_rmdir_step0[p][i]);
    }
    /* ---------- Rmdir step 1 ---------- */
    // --- if (!dir.is_allocated)
    for (int i in {1..nd}) {
        trans
          t_rmdir_step1_then[p][i],
          t_rmdir_step1_else[p][i];
        arcs(
          p_rmdir_line1[p]:t_rmdir_step1_then[p][i],
            t_rmdir_step1_then[p][i]:p_rmdir_line2[p],
          p_rmdir_line1[p]:t_rmdir_step1_else[p][i] ,
            t_rmdir_step1_else[p][i]:p_rmdir_lookup[p]
        );
        guard(
          t_rmdir_step1_then[p][i]:tk(p_file[p])==i & tk(d_allocated[i])==0,
          t_rmdir_step1_else[p][i]:tk(p_file[p])==i & tk(d_allocated[i])>0
        );
    }
    /* ---------- Rmdir step 2 ---------- */
    // --- return ERROR
        trans
          t_rmdir_step2[p];
        arcs(
          p_rmdir_line2[p]:t_rmdir_step2[p],
            t_rmdir_step2[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_rmdir_step2[p]);
    /* ---------- rmdir: lookup ---------- */
    // --- path_lookup(parent,file)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_rmdir_lookup[p][i][j];
        arcs(
          p_rmdir_lookup[p]:t_rmdir_lookup[p][i][j],
            t_rmdir_lookup[p][i][j]:p_rmdir_line3[p],
            t_rmdir_lookup[p][i][j]:d_count[i]:cond(tk(d_allocated[i])>0, 1, 0),
            p_parent[p]:t_rmdir_lookup[p][i][j]:tk(p_parent[p]),
            t_rmdir_lookup[p][i][j]:p_parent[p]:j
        );
        cond(i!=j, arcs(
            t_rmdir_lookup[p][i][j]:d_count[j]:cond(tk(d_allocated[j])>0, 1, 0)), null);
        guard(
          t_rmdir_lookup[p][i][j]:tk(dcache_lock)>0 & tk(p_file[p])==i & tk(d_parent[i])==j
        );
        inhibit(d_count[i]:t_rmdir_lookup[p][i][j]:np+1);
        cond(i!=j, inhibit(d_count[j]:t_rmdir_lookup[p][i][j]:np+1), null);
      }
    }
    /* ---------- Rmdir step 3 ---------- */
    // --- if (!is_directory(dir))
    for (int i in {1..nd}) {
        trans
          t_rmdir_step3_then[p][i],
          t_rmdir_step3_else[p][i];
        arcs(
          p_rmdir_line3[p]:t_rmdir_step3_then[p][i],
            t_rmdir_step3_then[p][i]:p_rmdir_line4[p],
          p_rmdir_line3[p]:t_rmdir_step3_else[p][i],
            t_rmdir_step3_else[p][i]:p_rmdir_line7[p]
        );
        guard(
          t_rmdir_step3_then[p][i]:tk(p_file[p])==i & tk(d_subdirs[i])==0,
          t_rmdir_step3_else[p][i]:tk(p_file[p])==i & tk(d_subdirs[i])>0
        );
    }
    /* ---------- Rmdir step 4 ---------- */
    // --- path_release(dir)
    for (int i in {1..nd}) {
      for (int j in {1..nd}) {
        trans
          t_rmdir_step4[p][i][j];
        arcs(
          p_rmdir_line4[p]:t_rmdir_step4[p][i][j],
            t_rmdir_step4[p][i][j]:p_rmdir_line5[p],
            d_count[i]:t_rmdir_step4[p][i][j]:
              cond(tk(d_allocated[i])>0 & tk(d_count[i])>1, 1, 0)
        );
        cond(i!=j, arcs(
            d_count[j]:t_rmdir_step4[p][i][j]:
              cond(tk(d_allocated[j])>0 & tk(d_count[j])>1, 1, 0)), null);
        guard(
          t_rmdir_step4[p][i][j]:tk(p_file[p])==i & tk(d_parent[i])==j
        );
      }
    }
    /* ---------- Rmdir step 5 ---------- */
    // --- return ERROR
        trans
          t_rmdir_step5[p];
        arcs(
          p_rmdir_line5[p]:t_rmdir_step5[p],
            t_rmdir_step5[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_rmdir_step5[p]);
    /* ---------- Rmdir step 6 ---------- */
    // --- down(dir.d_inode->i_mutex)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_rmdir_step6[p][i][k];
        arcs(
          p_rmdir_line6[p]:t_rmdir_step6[p][i][k],
            t_rmdir_step6[p][i][k]:p_rmdir_line8[p],
            i_mutex[k]:t_rmdir_step6[p][i][k]
        );
        guard(
          t_rmdir_step6[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
      }
    }
    /* ---------- Rmdir step 7 ---------- */
    // --- spin_lock(dcache_lock)
        trans
          t_rmdir_step7[p];
        arcs(
          p_rmdir_line7[p]:t_rmdir_step7[p],
            t_rmdir_step7[p]:p_rmdir_line6[p],
            dcache_lock:t_rmdir_step7[p]
        );
    /* ---------- Rmdir step 8 ---------- */
    // --- if (#children != 0)
    for (int i in {1..nd}) {
        trans
          t_rmdir_step8_then[p][i],
          t_rmdir_step8_else[p][i];
        arcs(
          p_rmdir_line8[p]:t_rmdir_step8_then[p][i],
            t_rmdir_step8_then[p][i]:p_rmdir_line9[p],
          p_rmdir_line8[p]:t_rmdir_step8_else[p][i],
            t_rmdir_step8_else[p][i]:p_rmdir_line14[p]
        );
        guard(
          t_rmdir_step8_then[p][i]:tk(p_file[p])==i & tk(d_subdirs[i])>1,
          t_rmdir_step8_else[p][i]:tk(p_file[p])==i & tk(d_subdirs[i])<=1
        );
    }
    /* ---------- Rmdir step 9 ---------- */
    // --- spin_unlock(dcache_lock)
        trans
          t_rmdir_step9[p];
        arcs(
          p_rmdir_line9[p]:t_rmdir_step9[p],
            t_rmdir_step9[p]:p_rmdir_line10[p],
            t_rmdir_step9[p]:dcache_lock
        );
        inhibit(dcache_lock:t_rmdir_step9[p]);
    /* ---------- Rmdir step 10 ---------- */
    // --- up(dir.d_inode->i_mutex)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_rmdir_step10[p][i][k];
        arcs(
          p_rmdir_line10[p]:t_rmdir_step10[p][i][k],
            t_rmdir_step10[p][i][k]:p_rmdir_line11[p],
            t_rmdir_step10[p][i][k]:i_mutex[k]
        );
        guard(
          t_rmdir_step10[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
        inhibit(i_mutex[k]:t_rmdir_step10[p][i][k]:np);
      }
    }
    /* ---------- Rmdir step 11 ---------- */
    // --- dput(dir)
    for (int i in {1..nd}) {
        trans
          t_rmdir_step11[p][i];
        arcs(
          p_rmdir_line11[p]:t_rmdir_step11[p][i],
            t_rmdir_step11[p][i]:p_rmdir_line12[p],
            d_count[i]:t_rmdir_step11[p][i]:
              cond(tk(d_allocated[i])>0 & tk(d_count[i])>1, 1, 0)
        );
        guard(
          t_rmdir_step11[p][i]:tk(p_file[p])==i
        );
    }
    /* ---------- Rmdir step 12 ---------- */
    // --- dput(parent)
      for (int j in {1..nd}) {
        trans
          t_rmdir_step12[p][j];
        arcs(
          p_rmdir_line12[p]:t_rmdir_step12[p][j],
            t_rmdir_step12[p][j]:p_rmdir_line13[p],
            d_count[j]:t_rmdir_step12[p][j]:cond(tk(d_allocated[j])>0 & tk(d_count[j])>1, 1, 0)
        );
        guard(
          t_rmdir_step12[p][j]:tk(p_parent[p])==j
        );
      }
    /* ---------- Rmdir step 13 ---------- */
    // --- return ERROR
        trans
          t_rmdir_step13[p];
        arcs(
          p_rmdir_line13[p]:t_rmdir_step13[p],
            t_rmdir_step13[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_rmdir_step13[p]);
    /* ---------- Rmdir step 14 ---------- */
    // --- if (dir.d_inode->i_state & DELETING)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_rmdir_step14_then[p][i][k],
          t_rmdir_step14_else[p][i][k];
        arcs(
          p_rmdir_line14[p]:t_rmdir_step14_then[p][i][k],
            t_rmdir_step14_then[p][i][k]:p_rmdir_line14b[p],
          p_rmdir_line14[p]:t_rmdir_step14_else[p][i][k],
            t_rmdir_step14_else[p][i][k]:p_rmdir_line19[p]
        );
        guard(
          t_rmdir_step14_then[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k & tk(i_state[k])==DELETING,
          t_rmdir_step14_else[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k & tk(i_state[k])!=DELETING
        );
      }
    }
    /* ---------- Rmdir step 14b ---------- */
    // --- spin_unlock(dcache_lock)
        trans
          t_rmdir_step14b[p];
        arcs(
          p_rmdir_line14b[p]:t_rmdir_step14b[p],
            t_rmdir_step14b[p]:p_rmdir_line15[p],
            t_rmdir_step14b[p]:dcache_lock
        );
        inhibit(dcache_lock:t_rmdir_step14b[p]);
    /* ---------- Rmdir step 15 ---------- */
    // --- dput(dir)
    for (int i in {1..nd}) {
        trans
          t_rmdir_step15[p][i];
        arcs(
          p_rmdir_line15[p]:t_rmdir_step15[p][i],
            t_rmdir_step15[p][i]:p_rmdir_line16[p],
            d_count[i]:t_rmdir_step15[p][i]:
              cond(tk(d_allocated[i])>0 & tk(d_count[i])>1, 1, 0)
        );
        guard(
          t_rmdir_step15[p][i]:tk(p_file[p])==i
        );
    }
    /* ---------- Rmdir step 16 ---------- */
    // --- dput(parent)
      for (int j in {1..nd}) {
        trans
          t_rmdir_step16[p][j];
        arcs(
          p_rmdir_line16[p]:t_rmdir_step16[p][j],
            t_rmdir_step16[p][j]:p_rmdir_line17[p],
            d_count[j]:t_rmdir_step16[p][j]:cond(tk(d_allocated[j])>0 & tk(d_count[j])>1, 1, 0)
        );
        guard(
          t_rmdir_step16[p][j]:tk(p_parent[p])==j
        );
      }
    /* ---------- Rmdir step 17 ---------- */
    // --- up(dir.d_inode->i_mutex)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_rmdir_step17[p][i][k];
        arcs(
          p_rmdir_line17[p]:t_rmdir_step17[p][i][k],
            t_rmdir_step17[p][i][k]:p_rmdir_line18[p],
            t_rmdir_step17[p][i][k]:i_mutex[k]
        );
        guard(
          t_rmdir_step17[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
        inhibit(i_mutex[k]:t_rmdir_step17[p][i][k]:np);
      }
    }
    /* ---------- Rmdir step 18 ---------- */
    // --- return SUCCESS
        trans
          t_rmdir_step18[p];
        arcs(
          p_rmdir_line18[p]:t_rmdir_step18[p],
            t_rmdir_step18[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_rmdir_step18[p]);
    /* ---------- Rmdir step 19 ---------- */
    // --- dir.d_inode->i_state |= DELETING
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_rmdir_step19[p][i][k];
        arcs(
          p_rmdir_line19[p]:t_rmdir_step19[p][i][k],
            t_rmdir_step19[p][i][k]:p_rmdir_line20[p],
            i_state[k]:t_rmdir_step19[p][i][k]:tk(i_state[k]),
            t_rmdir_step19[p][i][k]:i_state[k]:DELETING
        );
        guard(
          t_rmdir_step19[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
      }
    }
    /* ---------- Rmdir step 20 ---------- */
    // --- up(dir.d_inode->i_mutex)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_rmdir_step20[p][i][k];
        arcs(
          p_rmdir_line20[p]:t_rmdir_step20[p][i][k],
            t_rmdir_step20[p][i][k]:p_rmdir_line21[p],
            t_rmdir_step20[p][i][k]:i_mutex[k]
        );
        guard(
          t_rmdir_step20[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
        inhibit(i_mutex[k]:t_rmdir_step20[p][i][k]:np);
      }
    }
    /* ---------- Rmdir step 21 ---------- */
    // --- dir.d_parent = &dNULL
    for (int i in {1..nd}) {
        trans
          t_rmdir_step21[p][i];
        arcs(
          p_rmdir_line21[p]:t_rmdir_step21[p][i],
            t_rmdir_step21[p][i]:p_rmdir_line22[p],
            d_parent[i]:t_rmdir_step21[p][i]:tk(d_parent[i])
        );
        guard(
          t_rmdir_step21[p][i]:tk(p_file[p])==i
        );
    }
    /* ---------- Rmdir step 22 ---------- */
    // --- update_parent()
      for (int j in {1..nd}) {
        trans
          t_rmdir_step22[p][j];
        arcs(
          p_rmdir_line22[p]:t_rmdir_step22[p][j],
            t_rmdir_step22[p][j]:p_rmdir_line23[p],
            d_subdirs[j]:t_rmdir_step22[p][j]
        );
        guard(
          t_rmdir_step22[p][j]:tk(p_parent[p])==j
        );
      }
    /* ---------- Rmdir step 23 ---------- */
    // --- dput(parent)
      for (int j in {1..nd}) {
        trans
          t_rmdir_step23[p][j];
        arcs(
          p_rmdir_line23[p]:t_rmdir_step23[p][j],
            t_rmdir_step23[p][j]:p_rmdir_line24[p],
            d_count[j]:t_rmdir_step23[p][j]:cond(tk(d_count[j])>1, 1, 0)
        );
        guard(
          t_rmdir_step23[p][j]:tk(p_parent[p])==j
        );
      }
    /* ---------- Rmdir step 24 ---------- */
    // --- spin_unlock(dcache_lock)
        trans
          t_rmdir_step24[p];
        arcs(
          p_rmdir_line24[p]:t_rmdir_step24[p],
            t_rmdir_step24[p]:p_rmdir_line25[p],
            t_rmdir_step24[p]:dcache_lock
        );
        inhibit(
          dcache_lock:t_rmdir_step24[p]
        );
    /* ---------- Rmdir step 25 ---------- */
    // --- while (!wait_done)
    for (int i in {1..nd}) {
        trans
          t_rmdir_step25_while[p][i],
          t_rmdir_step25_else[p][i];
        arcs(
          p_rmdir_line25[p]:t_rmdir_step25_while[p][i],
            t_rmdir_step25_while[p][i]:p_rmdir_line26[p],
          p_rmdir_line25[p]:t_rmdir_step25_else[p][i],
            t_rmdir_step25_else[p][i]:p_rmdir_line37[p],
            p_rmdir_wait_done[p]:t_rmdir_step25_else[p][i]
        );
        guard(
          t_rmdir_step25_while[p][i]:tk(p_file[p])==i & tk(p_rmdir_wait_done[p])==0,
          t_rmdir_step25_else[p][i]: tk(p_file[p])==i & tk(p_rmdir_wait_done[p])>0
        );
    }
    /* ---------- Rmdir step 26 ---------- */
    // --- spin_lock(dcache_lock)
        trans
          t_rmdir_step26[p];
        arcs(
          p_rmdir_line26[p]:t_rmdir_step26[p],
            t_rmdir_step26[p]:p_rmdir_line27[p],
            dcache_lock:t_rmdir_step26[p]
        );
    /* ---------- Rmdir step 27 ---------- */
    // --- spin_lock(dir.d_lock)
    for (int i in {1..nd}) {
        trans
          t_rmdir_step27[p][i];
        arcs(
          p_rmdir_line27[p]:t_rmdir_step27[p][i],
            t_rmdir_step27[p][i]:p_rmdir_line28[p],
            d_lock[i]:t_rmdir_step27[p][i]
        );
        guard(
          t_rmdir_step27[p][i]:tk(p_file[p])==i
        );
    }
    /* ---------- Rmdir step 28 ---------- */
    // --- if (atomic_read(dir.d_count) == 2)
    for (int i in {1..nd}) {
        trans
          t_rmdir_step28_then[p][i],
          t_rmdir_step28_else[p][i];
        arcs(
          p_rmdir_line28[p]:t_rmdir_step28_then[p][i],
            t_rmdir_step28_then[p][i]:p_rmdir_line29[p],
          p_rmdir_line28[p]:t_rmdir_step28_else[p][i],
            t_rmdir_step28_else[p][i]:p_rmdir_line35[p]
        );
        guard(
          t_rmdir_step28_then[p][i]:tk(p_file[p])==i & tk(d_count[i])==2,
          t_rmdir_step28_else[p][i]:tk(p_file[p])==i & tk(d_count[i])!=2
        );
    }
    /* ---------- Rmdir step 29 ---------- */
    // --- spin_lock(dir.d_inode->i_lock)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_rmdir_step29[p][i][k];
        arcs(
          p_rmdir_line29[p]:t_rmdir_step29[p][i][k],
            t_rmdir_step29[p][i][k]:p_rmdir_line30[p],
            i_lock[k]:t_rmdir_step29[p][i][k]
        );
        guard(
          t_rmdir_step29[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
      }
    }

    /* ---------- Rmdir step 30 ---------- */
    // --- dir.d_inode->i_count--
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_rmdir_step30[p][i][k];
        arcs(
          p_rmdir_line30[p]:t_rmdir_step30[p][i][k],
            t_rmdir_step30[p][i][k]:p_rmdir_line31[p],
            i_count[k]:t_rmdir_step30[p][i][k]
        );
        guard(
          t_rmdir_step30[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
      }
    }

    /* ---------- Rmdir step 31 ---------- */
    // --- if (atomic_read(dir.d_inode->i_count) >= 1)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_rmdir_step31_then[p][i][k],
          t_rmdir_step31_else[p][i][k];
        arcs(
          p_rmdir_line31[p]:t_rmdir_step31_then[p][i][k],
            t_rmdir_step31_then[p][i][k]:p_rmdir_line32[p],
          p_rmdir_line31[p]:t_rmdir_step31_else[p][i][k],
            t_rmdir_step31_else[p][i][k]:p_rmdir_line32b[p]
        );
        guard(
          t_rmdir_step31_then[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k & tk(i_count[k])>=1,
          t_rmdir_step31_else[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k & tk(i_count[k])<1
        );
      }
    }
    /* ---------- Rmdir step 32 ---------- */
    // --- dir.d_inode->i_state ^= DELETING
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_rmdir_step32[p][i][k];
        arcs(
          p_rmdir_line32[p]:t_rmdir_step32[p][i][k],
            t_rmdir_step32[p][i][k]:p_rmdir_line33[p],
            i_state[k]:t_rmdir_step32[p][i][k]:DELETING
        );
        guard(
          t_rmdir_step32[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
      }
    }
    /* ---------- Rmdir step 32b ---------- */
    // --- deallocate inode ---
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_rmdir_step32b[p][i][k];
        arcs(
          p_rmdir_line32b[p]:t_rmdir_step32b[p][i][k],
            t_rmdir_step32b[p][i][k]:p_rmdir_line33[p],
            i_state[k]:t_rmdir_step32b[p][i][k]:tk(i_state[k]),
            i_allocated[k]:t_rmdir_step32b[p][i][k]:tk(i_allocated[k])
        );
        guard(
          t_rmdir_step32b[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
      }
    }
    /* ---------- Rmdir step 33 ---------- */
    // --- spin_unlock(dir.d_inode->i_lock)
    for (int i in {1..nd}) {
      for (int k in {1..ni}) {
        trans
          t_rmdir_step33[p][i][k];
        arcs(
          p_rmdir_line33[p]:t_rmdir_step33[p][i][k],
            t_rmdir_step33[p][i][k]:p_rmdir_line34[p],
            t_rmdir_step33[p][i][k]:i_lock[k]
        );
        guard(
          t_rmdir_step33[p][i][k]:tk(p_file[p])==i & tk(d_inode[i])==k
        );
        inhibit(i_lock[k]:t_rmdir_step33[p][i][k]);
      }
    }

    /* ---------- Rmdir step 34 ---------- */
    // --- atomic_write(dir.d_count, 0);
    for (int i in {1..nd}) {
        trans
          t_rmdir_step34[p][i];
        arcs(
          p_rmdir_line34[p]:t_rmdir_step34[p][i],
            t_rmdir_step34[p][i]:p_rmdir_line35[p],
            d_count[i]:t_rmdir_step34[p][i]:tk(d_count[i]),
            d_inode[i]:t_rmdir_step34[p][i]:tk(d_inode[i]),
            d_parent[i]:t_rmdir_step34[p][i]:tk(d_parent[i]),
            d_subdirs[i]:t_rmdir_step34[p][i]:tk(d_subdirs[i]),
            d_allocated[i]:t_rmdir_step34[p][i]:tk(d_allocated[i]),
            t_rmdir_step34[p][i]:p_rmdir_wait_done[p]
        );
        guard(
          t_rmdir_step34[p][i]:tk(p_file[p])==i
        );
    }
    /* ---------- Rmdir step 35 ---------- */
    // --- spin_unlock(dir.d_lock)
    for (int i in {1..nd}) {
        trans
          t_rmdir_step35[p][i];
        arcs(
          p_rmdir_line35[p]:t_rmdir_step35[p][i],
            t_rmdir_step35[p][i]:p_rmdir_line36[p],
            t_rmdir_step35[p][i]:d_lock[i]
        );
        guard(
          t_rmdir_step35[p][i]:tk(p_file[p])==i
        );
        inhibit(d_lock[i]:t_rmdir_step35[p][i]);
    }
    /* ---------- Rmdir step 36 ---------- */
    // --- spin_unlock(dcache_lock)
        trans
          t_rmdir_step36[p];
        arcs(
          p_rmdir_line36[p]:t_rmdir_step36[p],
            t_rmdir_step36[p]:p_rmdir_line25[p],
            t_rmdir_step36[p]:dcache_lock
        );
        inhibit(dcache_lock:t_rmdir_step36[p]);
    /* ---------- Rmdir step 37 ---------- */
    // --- return SUCCESS
        trans
          t_rmdir_step37[p];
        arcs(
          p_rmdir_line37[p]:t_rmdir_step37[p],
            t_rmdir_step37[p]:p_begin[p]
        );
        inhibit(p_begin[p]:t_rmdir_step37[p]);


  } // ============= end for process p


  // initialization
  init(
    /* root node is created at mount
       has itself and lost+found as subdirs
       has itself as parent */
    d_allocated[ROOT]:1,
    d_inode[ROOT]:ROOT,
    d_parent[ROOT]:ROOT,
    d_subdirs[ROOT]:2,
    d_count[ROOT]:1,
    i_count[ROOT]:1,
    i_allocated[ROOT]:1,
    /* lost+found node is created at mount
       has itself as subdir
       has root as parent */
    d_allocated[LOST_FOUND]:1,
    d_inode[LOST_FOUND]:LOST_FOUND,
    d_parent[LOST_FOUND]:ROOT,
    d_subdirs[LOST_FOUND]:1,
    d_count[LOST_FOUND]:1,
    i_count[LOST_FOUND]:1,
    i_allocated[LOST_FOUND]:1
  );


  real ro   := reorder;
  bigint ns := num_states(false);
  bool db   := debug;

  stateset Deadlock := difference(reachable, prev(reachable));
  bigint  nDeadlock := card(Deadlock);
  bool    pDeadlock := printset(Deadlock);
  bool    tDeadlock := EFtrace(initialstate, Deadlock);

  stateset RootRemoved := intersection(reachable, potential(tk(d_allocated[ROOT])==0));
  bigint  nRootRemoved := card(RootRemoved);
  bool    pRootRemoved := printset(RootRemoved);

  stateset RootCount0 := intersection(reachable, potential(tk(d_count[ROOT])==0));
  bigint  nRootCount0 := card(RootCount0);
  bool    pRootCount0 := printset(RootCount0);

  // ----- Basic properties

  for (int p in {1..np}) {
    stateset pStable[p] := cond(p==1, intersection(reachable,   potential(tk(p_begin[p])>0)),
                                     intersection(pStable[p-1], potential(tk(p_begin[p])>0)));
  }

  stateset Stable := pStable[np];

  for (int i in {1..nd}) {
    stateset DisUsed[i]  := intersection(reachable, potential(tk(d_count[i])>0));
    stateset DnotUsed[i] := intersection(reachable, potential(tk(d_count[i])==0));
    stateset DisDirectory[i] := intersection(reachable, potential(tk(d_subdirs[i])>1));
    stateset DisFile[i]      := intersection(reachable, potential(tk(d_subdirs[i])<=1));
    stateset DisAllocated[i] := intersection(reachable, potential(tk(d_allocated[i])>0));
    stateset DnotAllocated[i] := intersection(reachable, potential(tk(d_allocated[i])==0));
    stateset DisLocked[i] := intersection(reachable, potential(tk(d_lock[i])==0));
    stateset DisUnlocked[i] := intersection(reachable, potential(tk(d_lock[i])>0));
    stateset DCountDrift[i] := cond(i==1, 
                   intersection(reachable, potential(tk(d_count[i])>1)),
                   intersection(DCountDrift[i-1], potential(tk(d_count[i])>1)));
    for (int j in {1..nd}) {
      stateset DisParent[i][j] := intersection(reachable, potential(tk(d_parent[j])==i));
      stateset DisChild[i][j]  := intersection(reachable, potential(tk(d_parent[i])==j));
    }
  }

  stateset DCountUnsafe := intersection(Stable, DCountDrift[nd]);
  bigint  nDCountUnsafe := card(DCountUnsafe);
  bool    pDCountUnsafe := printset(DCountUnsafe);
  bool    tDCountUnsafe := EFtrace(initialstate, DCountUnsafe);  

  for (int i in {1..ni}) {
    stateset IisUsed[i] := intersection(reachable, potential(tk(i_count[i])>0));
    stateset InotUsed[i] := intersection(reachable, potential(tk(i_count[i])==0));
    stateset IisLocked[i] := intersection(reachable, potential(tk(i_lock[i])==0));
    stateset IisUnlocked[i] := intersection(reachable, potential(tk(i_lock[i])>0));
    stateset IisAllocated[i] := intersection(reachable, potential(tk(i_allocated[i])>0));
    stateset InotAllocated[i] := intersection(reachable, potential(tk(i_allocated[i])==0));
    for (int j in {1..nd}) {
      stateset isInode[i][j] := intersection(reachable, potential(tk(d_inode[j])==i));
    }
  }

  
  // ----- Queries

  for (int i in {1..nd}) {
    stateset DUsedNotAllocated[i] := intersection(DisUsed[i], DnotAllocated[i]);
    bigint  nDUsedNotAllocated[i] := card(DUsedNotAllocated[i]);
    bool    pDUsedNotAllocated[i] := printset(DUsedNotAllocated[i]);
    bool    tDUsedNotAllocated[i] := EFtrace(initialstate, DUsedNotAllocated[i]);

    for (int j in {1..nd}) {
      stateset DUsedParentNotUsed[i][j] := intersection(DisUsed[i], DisParent[j][i], DnotUsed[j]);
      bigint  nDUsedParentNotUsed[i][j] := card(DUsedParentNotUsed[i][j]);
      bool    pDUsedParentNotUsed[i][j] := printset(DUsedParentNotUsed[i][j]);
      bool    tDUsedParentNotUsed[i][j] := EFtrace(initialstate, DUsedParentNotUsed[i][j]);

      stateset AllocationBadProp2[i][j] := intersection(DisAllocated[i], DisUsed[i], DisParent[j][i], DnotAllocated[j]);
      bigint  nAllocationBadProp2[i][j] := card(AllocationBadProp2[i][j]);
      bool    pAllocationBadProp2[i][j] := printset(AllocationBadProp2[i][j]);
      bool    tAllocationBadProp2[i][j] := EFtrace(initialstate, AllocationBadProp2[i][j]);

      stateset ReferenceBadProp2[i][j] := intersection(DisAllocated[i], DisUsed[i], DisParent[j][i], DnotUsed[j]);
      bigint  nReferenceBadProp2[i][j] := card(ReferenceBadProp2[i][j]);
      bool    pReferenceBadProp2[i][j] := printset(ReferenceBadProp2[i][j]);
      bool    tReferenceBadProp2[i][j] := EFtrace(initialstate, ReferenceBadProp2[i][j]);

    }

    for (int j in {1..ni}) {
      stateset DUsedINotAllocated[i][j] := intersection(Stable, DisUsed[i], isInode[j][i], InotAllocated[j]);
      bigint  nDUsedINotAllocated[i][j] := card(DUsedINotAllocated[i][j]);
      bool    pDUsedINotAllocated[i][j] := printset(DUsedINotAllocated[i][j]);
      bool    tDUsedINotAllocated[i][j] := EFtrace(initialstate, DUsedINotAllocated[i][j]);
    }
  }

  for (int i in {1..ni}) {
    stateset IUsedNotAllocated[i] := intersection(IisUsed[i], InotAllocated[i]);
    bigint  nIUsedNotAllocated[i] := card(IUsedNotAllocated[i]);
    bool    pIUsedNotAllocated[i] := printset(IUsedNotAllocated[i]);
    bool    tIUsedNotAllocated[i] := EFtrace(initialstate, IUsedNotAllocated[i]);
  }

  for (int p in {1..np}) {
    stateset pCreate[p] := intersection(reachable, potential(
                             tk(p_create_line1[p])>0 |
                             tk(p_create_line2[p])>0 |
                             tk(p_create_line3[p])>0 |
                             tk(p_create_line4[p])>0 |
                             tk(p_create_line5[p])>0 |
                             tk(p_create_line6[p])>0 |
                             tk(p_create_line7[p])>0 |
                             tk(p_create_line8[p])>0 |
                             tk(p_create_line9[p])>0 |
                             tk(p_create_line10[p])>0 |
                             tk(p_create_line11[p])>0 |
                             tk(p_create_line12[p])>0 |
                             tk(p_create_line13[p])>0 |
                             tk(p_create_line14[p])>0 |
                             tk(p_create_line15[p])>0 |
                             tk(p_create_line16[p])>0 |
                             tk(p_create_line17[p])>0 |
                             tk(p_create_line18[p])>0 |
                             tk(p_create_line19[p])>0 |
                             tk(p_create_line20[p])>0 |
                             tk(p_create_line21[p])>0 |
                             tk(p_create_line22[p])>0 |
                             tk(p_create_line23[p])>0 |
                             tk(p_create_line24[p])>0 |
                             tk(p_create_line25[p])>0 |
                             tk(p_create_line26[p])>0 |
                             tk(p_create_line27[p])>0 |
                             tk(p_create_line28[p])>0 |
                             tk(p_create_line29[p])>0 |
                             tk(p_create_line30[p])>0 |
                             tk(p_create_line31[p])>0 |
                             tk(p_create_line32[p])>0 |
                             tk(p_create_line33[p])>0 |
                             tk(p_create_line34[p])>0 |
                             tk(p_create_lookup[p])>0
                           ));

    stateset pUnlink[p] := intersection(reachable, potential(
                             tk(p_unlink_line1[p])>0 |
                             tk(p_unlink_line2[p])>0 |
                             tk(p_unlink_line3[p])>0 |
                             tk(p_unlink_line4[p])>0 |
                             tk(p_unlink_line5[p])>0 |
                             tk(p_unlink_line6[p])>0 |
                             tk(p_unlink_line7[p])>0 |
                             tk(p_unlink_line8[p])>0 |
                             tk(p_unlink_line9[p])>0 |
                             tk(p_unlink_line10[p])>0 |
                             tk(p_unlink_line11[p])>0 |
                             tk(p_unlink_line12[p])>0 |
                             tk(p_unlink_line13[p])>0 |
                             tk(p_unlink_line14[p])>0 |
                             tk(p_unlink_line15[p])>0 |
                             tk(p_unlink_line16[p])>0 |
                             tk(p_unlink_line17[p])>0 |
                             tk(p_unlink_line18[p])>0 |
                             tk(p_unlink_line19[p])>0 |
                             tk(p_unlink_line20[p])>0 |
                             tk(p_unlink_line21[p])>0 |
                             tk(p_unlink_line22[p])>0 |
                             tk(p_unlink_line23[p])>0 |
                             tk(p_unlink_lookup[p])>0
                           ));
    stateset pMkdir[p] := intersection(reachable, potential(
                             tk(p_mkdir_line1[p])>0 |
                             tk(p_mkdir_line2[p])>0 |
                             tk(p_mkdir_line3[p])>0 |
                             tk(p_mkdir_line4[p])>0 |
                             tk(p_mkdir_line5[p])>0 |
                             tk(p_mkdir_line6[p])>0 |
                             tk(p_mkdir_line7[p])>0 |
                             tk(p_mkdir_line8[p])>0 |
                             tk(p_mkdir_line9[p])>0 |
                             tk(p_mkdir_line10[p])>0 |
                             tk(p_mkdir_line11[p])>0 |
                             tk(p_mkdir_line12[p])>0 |
                             tk(p_mkdir_line13[p])>0 |
                             tk(p_mkdir_line14[p])>0 |
                             tk(p_mkdir_line15[p])>0 |
                             tk(p_mkdir_line16[p])>0 |
                             tk(p_mkdir_line17[p])>0 |
                             tk(p_mkdir_line18[p])>0 |
                             tk(p_mkdir_line19[p])>0 |
                             tk(p_mkdir_line20[p])>0 |
                             tk(p_mkdir_line21[p])>0 |
                             tk(p_mkdir_line22[p])>0 |
                             tk(p_mkdir_line23[p])>0 |
                             tk(p_mkdir_line24[p])>0 |
                             tk(p_mkdir_line25[p])>0 |
                             tk(p_mkdir_line26[p])>0 |
                             tk(p_mkdir_line27[p])>0 |
                             tk(p_mkdir_line28[p])>0 |
                             tk(p_mkdir_line29[p])>0 |
                             tk(p_mkdir_line30[p])>0 |
                             tk(p_mkdir_lookup[p])>0
                           ));

    stateset pRmdir[p] := intersection(reachable, potential(
                             tk(p_rmdir_line1[p])>0 |
                             tk(p_rmdir_line2[p])>0 |
                             tk(p_rmdir_line3[p])>0 |
                             tk(p_rmdir_line4[p])>0 |
                             tk(p_rmdir_line5[p])>0 |
                             tk(p_rmdir_line6[p])>0 |
                             tk(p_rmdir_line7[p])>0 |
                             tk(p_rmdir_line8[p])>0 |
                             tk(p_rmdir_line9[p])>0 |
                             tk(p_rmdir_line10[p])>0 |
                             tk(p_rmdir_line11[p])>0 |
                             tk(p_rmdir_line12[p])>0 |
                             tk(p_rmdir_line13[p])>0 |
                             tk(p_rmdir_line14[p])>0 |
                             tk(p_rmdir_line14b[p])>0 |
                             tk(p_rmdir_line15[p])>0 |
                             tk(p_rmdir_line16[p])>0 |
                             tk(p_rmdir_line17[p])>0 |
                             tk(p_rmdir_line18[p])>0 |
                             tk(p_rmdir_line19[p])>0 |
                             tk(p_rmdir_line20[p])>0 |
                             tk(p_rmdir_line21[p])>0 |
                             tk(p_rmdir_line22[p])>0 |
                             tk(p_rmdir_line23[p])>0 |
                             tk(p_rmdir_line24[p])>0 |
                             tk(p_rmdir_line25[p])>0 |
                             tk(p_rmdir_line26[p])>0 |
                             tk(p_rmdir_line27[p])>0 |
                             tk(p_rmdir_line28[p])>0 |
                             tk(p_rmdir_line29[p])>0 |
                             tk(p_rmdir_line30[p])>0 |
                             tk(p_rmdir_line31[p])>0 |
                             tk(p_rmdir_line32[p])>0 |
                             tk(p_rmdir_line32b[p])>0 |
                             tk(p_rmdir_line33[p])>0 |
                             tk(p_rmdir_line34[p])>0 |
                             tk(p_rmdir_line35[p])>0 |
                             tk(p_rmdir_line36[p])>0 |
                             tk(p_rmdir_line37[p])>0 |
                             tk(p_rmdir_wait_done[p])>0 |
                             tk(p_rmdir_lookup[p])>0
                           ));
  }

  stateset UnlinkLivelock  := EG(intersection(pUnlink[1], pUnlink[2]));
  bool     tUnlinkLivelock := EGtrace(UnlinkLivelock, UnlinkLivelock);

  stateset Cycle1 := intersection(reachable, potential(tk(d_parent[1])==1));
  bigint nCycle1  := card(Cycle1);
  bool pCycle1    := printset(Cycle1);

  stateset Cycle2 := cond(nd>=2, intersection(reachable, potential(tk(d_parent[1])==2 & tk(d_parent[2])==1)), nostates);
  bigint nCycle2  := card(Cycle2);
  bool pCycle2    := printset(Cycle2);

  stateset Cycle3 := cond(nd>=3, intersection(reachable, potential(tk(d_parent[1])==2 & tk(d_parent[2])==3 & tk(d_parent[3])==1)), nostates);
  bigint nCycle3  := card(Cycle3);
  bool pCycle3    := printset(Cycle3);

  stateset Cycle4 := cond(nd>=4, intersection(reachable, potential(tk(d_parent[1])==2 & tk(d_parent[2])==3 & tk(d_parent[3])==4 & tk(d_parent[4])==1)), nostates);
  bigint nCycle4  := card(Cycle4);
  bool pCycle4    := printset(Cycle4);

  stateset Xcycle1 := intersection(reachable, potential(tk(d_parent[2])==2));
  bigint nXcycle1  := card(Xcycle1);
  bool pXcycle1    := printset(Xcycle1);

  stateset Xcycle2 := cond(nd>=3, intersection(reachable, potential(tk(d_parent[2])==3 & tk(d_parent[3])==2)), nostates);
  bigint nXcycle2  := card(Xcycle2);
  bool pXcycle2    := printset(Xcycle2);

  stateset Xcycle3 := cond(nd>=4, intersection(reachable, potential(tk(d_parent[2])==3 & tk(d_parent[3])==4 & tk(d_parent[4])==2)), nostates);
  bigint nXcycle3  := card(Xcycle3);
  bool pXcycle3    := printset(Xcycle3);

  stateset Xcycle4 := cond(nd>=5, intersection(reachable, potential(tk(d_parent[2])==3 & tk(d_parent[3])==4 & tk(d_parent[4])==5 & tk(d_parent[5])==2)), nostates);
  bigint nXcycle4  := card(Xcycle4);
  bool pXcycle4    := printset(Xcycle4);


};

int ND := read_int("Number of d_entries");
int NI := read_int("Number of i_nodes");
int NP := read_int("Number of processes");
compute(ND);
compute(NI);
compute(NP);

print("********************************************************\n");
print("*                  VFS abstract model                  *\n");
print("********************************************************\n");
print("* System parameters:\n");
print("* - Dentry pool size:    ", ND, "\n");
print("* - Inode pool size:     ", NI, "\n");
print("* - Number of processes: ", NP, "\n");

//compute(EXT2(ND,NI,NP).ro);
//compute(EXT2(ND,NI,NP).db);
print("\nNumber of reachable states: ", EXT2(ND,NI,NP).ns, "\n");

print("\nNumber of deadlocked states: ", EXT2(ND,NI,NP).nDeadlock);
compute(EXT2(ND,NI,NP).pDeadlock);
//compute(EXT2(ND,NI,NP).tDeadlock);

print("\nNumber of states where root is removed: ", EXT2(ND,NI,NP).nRootRemoved, "\n");
print("\nNumber of states where root count is 0: ", EXT2(ND,NI,NP).nRootCount0, "\n");

for (int i in {1..ND}) {

  for (int j in {1..ND}) {

    print("\nStates satisfying AllocationBadProp2[", i, "][", j, "]: ");
    print(EXT2(ND,NI,NP).nAllocationBadProp2[i][j]);

    print("\nStates satisfying ReferenceBadProp2[", i, "][", j, "]: ");
    print(EXT2(ND,NI,NP).nReferenceBadProp2[i][j]);
    
  }

/*
  print("\nStates satisfying used(d[", i, "]) AND not allocated(d[", i, "]): ");
  print(EXT2(ND,NI,NP).nDUsedNotAllocated[i]);
  compute(EXT2(ND,NI,NP).pDUsedNotAllocated[i]);
  compute(EXT2(ND,NI,NP).tDUsedNotAllocated[i]);

  for (int j in {1..ND}) {

    print("\nStates satisfying used(d[", i, "]) AND parent, d[", j, "], not used: ");
    print(EXT2(ND,NI,NP).nDUsedParentNotUsed[i][j]);
    compute(EXT2(ND,NI,NP).pDUsedParentNotUsed[i][j]);
    compute(EXT2(ND,NI,NP).tDUsedParentNotUsed[i][j]);
    
  }

  for (int j in {1..NI}) {

    print("\nStates satisfying used(d[", i, "]) AND inode, i[", j, "], not allocated: ");
    print(EXT2(ND,NI,NP).nDUsedINotAllocated[i][j]);
    compute(EXT2(ND,NI,NP).pDUsedINotAllocated[i][j]);
    compute(EXT2(ND,NI,NP).tDUsedINotAllocated[i][j]);
    
  }

*/
}

/*
for (int i in {1..NI}) {

  print("\nStates satisfying used(i[", i, "]) AND not allocated(i[", i, "]): ");
  print(EXT2(ND,NI,NP).nIUsedNotAllocated[i]);
  compute(EXT2(ND,NI,NP).pIUsedNotAllocated[i]);
  compute(EXT2(ND,NI,NP).tIUsedNotAllocated[i]);

}

print("\nLivelock:\n ");
compute(EXT2(ND,NI,NP).tUnlinkLivelock);

print("\nUnsafe drift of d_count:\n ");
compute(EXT2(ND,NI,NP).pDCountUnsafe);

*/


print("\nNumber of Cycle1 states: ", EXT2(ND,NI,NP).nCycle1);
//compute(EXT2(ND,NI,NP).pCycle1);
//compute(EXT2(ND,NI,NP).tCycle1);

print("\nNumber of Cycle2 states: ", EXT2(ND,NI,NP).nCycle2);
//compute(EXT2(ND,NI,NP).pCycle2);
//compute(EXT2(ND,NI,NP).tCycle2);

print("\nNumber of Cycle3 states: ", EXT2(ND,NI,NP).nCycle3);
//compute(EXT2(ND,NI,NP).pCycle3);
//compute(EXT2(ND,NI,NP).tCycle3);

print("\nNumber of Cycle4 states: ", EXT2(ND,NI,NP).nCycle4);
//compute(EXT2(ND,NI,NP).pCycle4);
//compute(EXT2(ND,NI,NP).tCycle4);

print("\n\n");