| files[entries[str]] = mkfile(m0, md4, # links(entries[str], dirs), content0), dirs[m] = mkdir(m1, md2, # links(m, dirs), m5, entries1), dirs[ino1] = mkdir(m4, md3, # links(ino1, dirs), m6, entries0), entries0[str] = entries[str], dirs[ino0] = mkdir(m2, md1, # links(ino0, dirs), m8, entries), dirs1 = dirs[m, mkdir(m1 + 1, md2, # links(m, dirs), m5, entries1[str0, entries[str]])], files0 = files, afs-cons(dirs, files), ino1 ∈ dirs, m ∈ dirs, entries[str] ∈ files, ino0 ∈ dirs, str ∈ entries, str ∈ entries0, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO, links(ino0, dirs) ≠ ∅ ∨ ino0 = ROOT_INO ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced := ?⟩ asynced, ⟨afs_inc_nlink#(mkdentry(str, entries0[str]).ino; dirs1, files); new_dent := mkdentry(str0, mkdentry(str, entries0[str]).ino); afs_inode_sync#(mkinode(m, md, true, # links(m, dirs), m5, m1); dirs1, files); afs_inode_sync#(mkinode(entries0[str], md0, false, # links(entries0[str], dirs), 0, m3); dirs1, files); p_inode := (m ∈ dirs1 ⊃ mkinode(m, dirs1[m].meta, true, dirs1[m].nlink, dirs1[m].nsubdirs, dirs1[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); c_inode := getinode(mkdentry(str, entries0[str]).ino, dirs1, files); err := ESUCCESS; asynced := ?⟩ (asynced ∧ dirs \ orphans(dirs, files0) = dirs1 \ orphans(dirs1, files) ∧ files0 \ orphans(dirs, files0) = files \ orphans(dirs1, files)), str0 ∈ entries1 |
dirs[ino0] = mkdir(m2, md1, # links(ino0, dirs), m8, entries), entries0[str] = entries[str], dirs[ino1] = mkdir(m4, md3, # links(ino1, dirs), m6, entries0), dirs[m] = mkdir(m1, md2, # links(m, dirs), m5, entries1), files[entries[str]] = mkfile(m0, md4, # links(entries[str], dirs), content0), dirs1 = dirs[m, mkdir(m1 + 1, md2, # links(m, dirs), m5, entries1[str0, entries[str]])], files0 = files, afs-cons(dirs, files), str ∈ entries0, str ∈ entries, ino0 ∈ dirs, entries[str] ∈ files, m ∈ dirs, ino1 ∈ dirs, ¬ str0 ∈ entries1, links(ino0, dirs) ≠ ∅ ∨ ino0 = ROOT_INO, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced := ?⟩ asynced, ⟨afs_inc_nlink#(mkdentry(str, entries0[str]).ino; dirs1, files); new_dent := mkdentry(str0, mkdentry(str, entries0[str]).ino); afs_inode_sync#(mkinode(m, md, true, # links(m, dirs), m5, m1); dirs1, files); afs_inode_sync#(mkinode(entries0[str], md0, false, # links(entries0[str], dirs), 0, m3); dirs1, files); p_inode := (m ∈ dirs1 ⊃ mkinode(m, dirs1[m].meta, true, dirs1[m].nlink, dirs1[m].nsubdirs, dirs1[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); c_inode := getinode(mkdentry(str, entries0[str]).ino, dirs1, files); err := ESUCCESS; asynced := ?⟩ (asynced ∧ dirs \ orphans(dirs, files0) = dirs1 \ orphans(dirs1, files) ∧ files0 \ orphans(dirs, files0) = files \ orphans(dirs1, files))