| cache_files[entries[str]] = mkfile(m2, md0, # links(entries[str], cache_dirs), content0), ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[entries[str]] = mkfile(m0, md, m1, content), cache_dirs[m] = mkdir(m3, md1, # links(m, cache_dirs), m5, entries), cache_icache[entries[str]] = mkientry(boolvar0, mkinode(m4, md2, boolvar, m6, m7, m8)), afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), m ∈ cache_dirs, str ∈ entries, entries[str] ∈ cache_files, entries[str] ∈ cache_icache → m4 = entries[str] ∧ (boolvar0 ⊃ m6 = # links(entries[str], cache_dirs) ∧ m7 = 0 ∧ ¬ boolvar ;mkinode(entries[str], md2, boolvar, m6, m7, m8) = mkinode(entries[str], md0, false, # links(entries[str], cache_dirs), 0, m2) ), cache_sync → synced(cache_files, cache_icache, cache_pcache), links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ m1 = # links(entries[str], cache_dirs), entries[str] ∈ cache_icache ∧ ¬ boolvar |
Used simplifier rules: ⊦ ¬ ino ∈ icache → (files ⊕ icache)[ino] = files[ino]; (s)%⊦ (files ⊕ pcache)[ino] = mkfile (files[ino].size, files[ino].meta, files[ino].nlink, files[ino].content ⊕ mkcontent(ino, pcache)); (s)%⊦ mkfile(m, md, m0, content) = mkfile(m1, md0, m2, content0) ↔ m = m1 ∧ md = md0 ∧ m0 = m2 ∧ content = content0; (ws)% ⊦ ¬ ino ∈ icache → icache[ino] = (∅)[ino]; (s)% ⊦ mkfile(m, md, m0, content).nlink = m0; (s)%⊦ mkinode(m, md, boolvar, m0, m1, m2) = mkinode(m3, md0, boolvar0, m4, m5, m6) ↔ m = m3 ∧ md = md0 ∧ (boolvar ↔ boolvar0) ∧ m0 = m4 ∧ m1 = m5 ∧ m2 = m6; (ws) Used formulas: entries[str] ∈ cache_icache