/* 
The basic idea was to have a resources, of which there are two kinds,
custodians and threads. All resources know their parent (except one)
and the parents form a tree. There is one distinguished custodian
called the root custodian and one distinguished thread, called the
drscheme thread. the drscheme thread's parent custodian is the root
custodian and the root custodian has no parent. Every custodian except
the root custodian has a parent.

Additionally, there are states. The states have a list of allocated
resources, a list of live (unkilled) resources, a mapping from threads
to each one's active custodian (that mapping just dictates how certain
thread's operations will behave -- it is only indirectly related to the
parent custodian of the thread), and a mapping from threads to visible
custodians. That last is kind of a cheat, but modeling the connection
between threads and the visible custodians requires a lot more and
might be best left to a revision of this spec...

Finally, we had some state transitions that were predicated on the
thread making the transition and a fact that let the threads run. We
had a transition to kill the active custodian in a thread, a transition
that corresponded to the execute button (but I'm not sure we had the
best modeling of that one) and one or two others that I forget.
*/

module systems/drscheme

open std/ord

sig Resource {
   owner: option Custodian
}

disj sig Thread extends Resource {
}

disj sig Custodian extends Resource {
}

static sig RootCustodian extends Custodian {
} { no owner } 

static sig DrSchemeThread extends Thread {
}
{ owner = RootCustodian }


sig State {
   allocated: set Resource,
   live: set Resource,
   canAccess: Thread -> Custodian,
   currentCustodian: Thread ->! Custodian
}

fun State::Init ( ) {
   with this | {
      allocated = RootCustodian + DrSchemeThread
      live = RootCustodian + DrSchemeThread
      canAccess = DrSchemeThread -> RootCustodian
      currentCustodian = DrSchemeThread -> RootCustodian
   }
}

fun State::NOP (actingThrea: Thread): State {
   result.allocated = this.allocated
   result.live = this.live
   result.canAccess = this.canAccess
   result.currentCustodian = this.currentCustodian
}

fun State::KillCustodian (actingThread: Thread): State {
    result.allocated = this.allocated
    result.live = this.live - actingThread.this::currentCustodian.*~owner
    result.canAccess = this.canAccess
    result.currentCustodian = this.currentCustodian
}



fun DictateStateTransitions ( ) {
   Ord[State].first..Init()
   all s: State - Ord[State].last |
     some actingThread: s.live & Thread |
       (
          OrdNext(s) = s..NOP(actingThread) ||
          OrdNext(s) = s..KillCustodian(actingThread)
       )  
}

run DictateStateTransitions for 3 but 1 Ord[State]