// A model of disconnected operation in the Coda file system

module CodaModel

sig FileName {}
sig File {} // the contents of a file
static disj sig Error, Locked extends File {}

sig Server 
{
  files: FileName ?->? File
}{
  some files
}


sig Venus
{
  server: option Server,
  cache: FileName ?->? File,
  replayLog: FileName ?->? File
}

fun InHoardingState (v: Venus) { some v.server && no v.replayLog }
fun InEmulationState (v: Venus) { no v.server }
fun InReintegrationState (v: Venus) { some v.server && some v.replayLog }


fun SameExceptCache (v1,v2: Venus)
{
  v1.server = v2.server 
  v1.replayLog = v2.replayLog
}

fun SameExceptServer (v1,v2: Venus)
{
  v1.cache = v2.cache 
  v1.replayLog = v2.replayLog
}

fun SameExceptLog (v1,v2: Venus)
{
  v1.cache = v2.cache 
  v1.server = v2.server}


fun FileAvailable (v: Venus, f: FileName)
{
  InHoardingState(v) || InReintegrationState(v) && some v.replayLog[f]
}

fun NameOf (f:File, v:Venus): FileName { result = ~(v.cache)[f] }
fun FileInCache (f:File, v:Venus) { some ~(v.cache)[f] }

fun FileOpen (v,v': Venus, fn: FileName, f: File)
{
  InEmulationState(v) => 
    v=v' && f = Error // cannot open a file that isn't there

  FileAvailable(v,fn) && some v.cache[fn] => 
    v=v' && f = v.cache[fn]

  FileAvailable(v,fn) && no v.cache[fn] => 
    SameExceptCache(v,v') && v'.cache = v.cache + fn->f && f = v.server.files[fn]

  InReintegrationState(v) && some v.replayLog[fn] =>
    f = Locked
}


fun Read (v,v': Venus, f: File)
{
  FileInCache(f,v)
  v = v' // reading doesn't change any state
}


fun Write (v,v': Venus, f,f': File)
{
  FileInCache(f,v)
  f' != f // it's more interesting (but necessary) if the contents change
  SameExceptCache(v,v')
  let fn = NameOf(f,v) |
  v'.cache = v.cache - fn->f + fn->f'
}


fun Close (v,v': Venus, s,s': Server, f: File)
{
  InHoardingState(v) =>
    // write our local changes back to the server
    (s = v.server && SameExceptServer(v,v') && v'.server = s' && 
     let fn = NameOf(f,v) | let oldfile = s.files[fn] |
     s'.files = s.files - fn->oldfile + fn->f),
    // otherwise
    (SameExceptLog(v,v') && s=s' && v'.replayLog = v.replayLog + NameOf(f,v)->f)
}


fun Disconnect (v,v': Venus)
{
  some v.server // we can only disconnect when connected
  SameExceptServer(v,v')
  no v'.server
}


fun Reconnect (v,v': Venus, s: Server) // s is server's state at time of reintegration
{
  no v.server // we can only reconnect when disconnected
  SameExceptServer(v,v')
  v'.server = s
}


fun ReintegrateOneFile (v,v': Venus, s,s': Server)
{
  InReintegrationState(v)
  s = v.server
  s' = v'.server
  some fn:FileName, f:File | fn->f in v.replayLog &&
    v'.replayLog = v.replayLog - fn->f && 
    let oldfile = s.files[fn] |
    s'.files = s.files - fn->oldfile + fn->f 
}

------------------ Test various scenarios --------------------

fun InitialState (v0:Venus, s:Server, fn:FileName, f0:File)
{
  InHoardingState(v0)
  no v0.cache
  v0.server = s
  s.files[fn] = f0
}

fun NetworkHiccup (v0,v1,v2,v3,v4,v5:Venus, s0,s1:Server, fn:FileName, f0,f1:File)
{
  InitialState(v0,s0,fn,f0)
  FileOpen(v0,v1,fn,f0)
  Disconnect(v1,v2)
  Reconnect(v2,v3,s0)
  Write(v3,v4,f0,f1)
  Close(v4,v5,s0,s1,f1)
}

fun WriteDuringDisconnect (v0,v1,v2,v3,v4,v5:Venus, s0,s1:Server, fn:FileName, f0,f1:File)
{
  InitialState(v0,s0,fn,f0) 
  FileOpen(v0,v1,fn,f0) 
  Disconnect(v1,v2) 
  Write(v2,v3,f0,f1) 
  Reconnect(v3,v4,s0) 
  Close(v4,v5,s0,s1,f1)
}

fun WholeChangeDuringDisconnect (v0,v1,v2,v3,v4,v5,v6:Venus, s0,s1:Server, fn:FileName, f0,f1:File)
{
  InitialState(v0,s0,fn,f0)
  FileOpen(v0,v1,fn,f0)
  Disconnect(v1,v2)
  Write(v2,v3,f0,f1)
  Close(v3,v4,s0,s0,f1)
  Reconnect(v4,v5,s0)
  ReintegrateOneFile(v5,v6,s0,s1)
}

fun ClientStillReintegrating (v0,v1,v2,v3,v4,v5:Venus, s:Server, fn:FileName, f0,f1:File)
{
  InitialState(v0,s,fn,f0) 
  FileOpen(v0,v1,fn,f0) 
  Disconnect(v1,v2) 
  Write(v2,v3,f0,f1) 
  Close(v3,v4,s,s,f1) 
  Reconnect(v4,v5,s)
  // no reintegration
}

assert Scenario0 
{
  all v0,v1,v2,v3,v4,v5:Venus, s0,s1:Server, fn:FileName, f0,f1:File |
  NetworkHiccup(v0,v1,v2,v3,v4,v5,s0,s1,fn,f0,f1) => s1.files[fn] = f1
}

assert Scenario1
{
  all v0,v1,v2,v3,v4,v5:Venus, s0,s1:Server, fn:FileName, f0,f1:File |
  WriteDuringDisconnect(v0,v1,v2,v3,v4,v5,s0,s1,fn,f0,f1) => s1.files[fn] = f1
}

assert Scenario2
{
  all v0,v1,v2,v3,v4,v5,v6:Venus, s0,s1:Server, fn:FileName, f0,f1:File |
  WholeChangeDuringDisconnect(v0,v1,v2,v3,v4,v5,v6,s0,s1,fn,f0,f1) => s1.files[fn] = f1
}

assert Scenario3
{
  all v0,v1,v2,v3,v4,v5:Venus, s:Server, fn:FileName, f0,f1:File |
  ClientStillReintegrating(v0,v1,v2,v3,v4,v5,s,fn,f0,f1) => v5.server.files[fn] = f0 
}


// If these runs don't produce instances, then the checks are meaningless!
//
run NetworkHiccup for 2 Server, 6 Venus, 1 FileName, 2 File
run WriteDuringDisconnect for 2 Server, 6 Venus, 1 FileName, 2 File
run WholeChangeDuringDisconnect for 2 Server, 7 Venus, 1 FileName, 2 File
run ClientStillReintegrating for 2 Server, 6 Venus, 1 FileName, 2 File

check Scenario0 for 2 Server, 6 Venus, 1 FileName, 2 File
check Scenario1 for 2 Server, 6 Venus, 1 FileName, 2 File
check Scenario2 for 2 Server, 7 Venus, 1 FileName, 2 File
check Scenario3 for 2 Server, 6 Venus, 1 FileName, 2 File