Formalne przekształcenie do PROMELI

     Przestrzeń stanów

type
    EventId = {MEMORY_EVENT,SNARF_EVENT};
    TaskId = byte;

type
    Property_Name = byte;
    Property_Value = byte;

typedef Property {
    Property_Name name;
    Property_Value value};

typedef Lock {
    Property_Value value;
    list sub = [NO_TASKS] of TaskId;
    bool achieved};

typedef Event {
    byte count;
    list pending_tasks = [NO_TASKS] of TaskId};

typedef Task {
    State state;
    list waiting_for = [NO_EVENTS] of EventId;
    Property prop};

type
State = {SUSPENDED, RUNNING, ABORTED, TERMINATED};

     Zdarzenia

     Oczekiwanie na zdarzenie

inline wait_for_event(this,a,p) {
   atomic{
     append(this, Ev[a].pending_ tasks);
     append(a,active tasks[this].waiting for);
     active_tasks [this].prop.name = p.name;
     active_tasks [this].prop.value = p.value;
     active_tasks [this].state = SUSPENDED;
     active_tasks [this].state == RUNNING
     }
  }

     Oczekiwanie na sygnał

inline signal_event(a) {
   atomic{
     TaskId t;
     EventId e;
     list pending = [NO_EVENTS] of EventId;
     Ev[a] .count = Ev[a].count + 1;
     copy(Ev[a].pending_tasks,pending);
     do
     :: pending?t ->
       if
       :: (active_tasks[t].prop.value == undef_value
         ||
         db_query(active_tasks[t].prop) )
        ->
        do
        :: active_tasks[t].waiting_for?e
         -> remove(t,Ev[e].pending_tasks)
        :: empty(active_tasks[t].waiting_for)
         -> break
         od;
        active_tasks[t].state = RUNNING
       :: else
       fi
     :: empty(pending) -> break
     od
   }
  }

     Sprawdzenie zgodności wartości w bazie danych

  #define db_query(p)
    db[p.name] == p.value

     Zadania

   Sprawdzenie czy nie będzie konfliktów (przed blokowaniem właściwości)

 inline fail_if_incompatible_property(p,err) {
   if
   :: (locks[p.name].value != undef_value &
       locks[p.name].value != p.value) -> err = 1
   :: else
   fi
   } 
 }

   Blokowanie właściwości

 inline snarf_property_lock(this,p,err) {
   atomic{
     fail_if_incompatible_property(p,err);
     append(this,locks[p.name].sub);
     if
     :: locks[p.name].value == undef_value ->
        locks[p.name].value = p.value;
        locks[p.name].achieved = db_query(p)
     :: else
     fi;
     signal_event(SNARF_EVENT)
   }
 }

   Odnajdywanie właściciela

 inline find_owner(p,owner) {
  locks[p.name].sub?<owner>
  }

   Blokowanie nie-właścicieli, aż do momentu wykonania

 inline achieve_lock_property(this,p,err) {
  TaskId owner;
  find_owner(p,owner);
  if
  :: owner == this -> achieve(p,err);
     locks[p.name].achieved = true
  :: else -> wait_for_event(this,MEMORY_EVENT,p);
  fi
 }

   Wykonanie

 inline achieve(p,err) {
  if
  :: db_query(p)
  :: else ->
     if
     :: db[p.name] = p. value
     :: err = 1
     fi
  fi
 }

   Powrót po zmianie wartości w BD

 inline closure() {
  if :: true -> skip :: true -> hang fi
 }

   Zwolnienie blokad

 inline release_lock(this,p) {
  atomic{
    remove(this,locks[p.name].sub);
    if
    :: empty(locks[p.name].sub) ->
       locks[p.name].value = undef_value
    :: nempty(locks[p.name].sub)
    fi
  }
 }

   Wykonanie zadania

 inline execute_task(this,p) {
  bool err = 0;
  {
    snarf_property_lock(this,p,err);
    achieve_lock_property(this,p,err);
    closure()
  }
    unless
  {err || active_tasks[this].state == ABORTED};
  active_tasks[this].state = TERMINATED;
  {release_lock(this,p)}
    unless
  {active_tasks[this].state == ABORTED}
 };

 proctype Achieving Task(TaskId this)
  { Property p;
    p.name = 0;
    if
    :: this ==1 -> p value = 1;
    :: this ==2 -> p value = 2
    fi;
    execute task(this p);
  };

     Demon

 inline interrupt_task(t) {
   active tasks[t].state = ABORTED
 }

 inline property_violated(pn,violation) {
   atomic{
     violation =
      (locks[pn].value != undef_value &
       locks[pn].achieved &
       db[pn] != locks[pn] .value)
   }
 }

 inline check_locks(lock_violation) {
   Property_Name pn;
   list sub = [NO_TASKS] of TaskId;
   TaskId t;
   pn = 0;
   do
   :: pn < NO_PROPS ->
      property_violated(pn,lock_violation);
      if
      :: lock_violation -> atomiccopy(locks[pn].sub,sub)};
         do
         :: sub?t -> interrupt_task(t);
         :: empty(sub) -> break
         od
      :: else
      fi;
      pn++
   :: else -> break
   od;
   pn = 0;
   do
   :: pn < NO_PROPS ->
      property_violated(pn,lock_violation);
      if
      :: lock_violation -> break
      :: else
      fi;
      pn++
   :: else -> break
   od
 }

 proctype Daemon(TaskId this) {
   bit lock_violation;
   byte event_count = 0;
   bit first_time = true;
   do
   :: check_locks(lock_violation);
      if
      :: lock_violation -> do_automatic_recovery()
      :: else
      fi;
      if
      :: (!first_time &&
          Ev[MEMORY_EVENT].count +
          Ev[SNARF_EVENT].count != event_count )
            ->
            event_count =
              Ev[MEMORY_EVENT].count +
              Ev[SNARF_EVENT].count
      :: else ->
         first_time = false;
         wait_for_events(this, MEMORY_EVENT,SNARF_EVENT)
      fi
   od
 };
 

     Środowisko