newAuthCode
  :: (MonadWhatever m)
  => DB.Client
  -> DB.SessionId
  -> m DB.AuthorizationCode
newAuthCode clid sid = do
  let codeData = mkAuthCodeFor clid sid
  void $ DB.deleteAllCodes clid sid
  void $ DB.insertAuthCode codeData
  return code

open util/time  // Импортируем предопределённые объекты Time
sig Operation       // У нас есть операции...
  { delete : Time   // ...которые удаляют в какой-то момент времени
  , insert : Time   // ...и производят вставку в какой-то другой
  }
  { lt[delete,insert]  // Удаления происходят до вставок
    lt[first,delete]   // По техническим причинам в первый
                       // момент времени ничего не происходит
  }
  run {some Operation} for 4 // Показать произвольный пример модели
                             // с <= 4 операциями

┌──────────────┬──────┬──────┐
│this/Operation│delete│insert│
├──────────────┼──────┼──────┤
│Operation⁰    │Time¹ │Time³ │ ← Operation⁰ удаляет в момент Time¹ и
├──────────────┼──────┼──────┤   вставляет в момент Time³
│Operation¹    │Time² │Time³ │ ← Operation¹ удаляет в момент Time² и
└──────────────┴──────┴──────┘   и вставляет в момент Time³
                         ↑
                        ОЙ!

code <- run $ do
  handleJust constraintViolation
    (launchPG $ selectCodeForSession clid scope sid
    (launchPG . pgWithTransaction $ newAuthCode clid scope sid)

open util/time // Импортируем Time
sig Token {} // Объекты с названием Token
one sig DBState // База данных с токенами
{userToken : Token lone -> Time}
    // В БД не более одного токена в каждый момент врвмени
    // (т.к. ограничения БД не позволяют хранить больше одного)
sig Operation {
   delete : Time
, insert : Time
, select : Time // Наши операции теперь могут выполнять select
}
{
  lt[first,delete]   // Ничего не происходит в первый момент времени
                     // по техническим причинам
  lt[delete,insert]  // Первой выполняется операция delete
  lte[insert,select] // select выполняется после или во время insert'а
  no userToken.(insert.prev) // Если вставка сработала (т.е. таблица
  => insert = select         // была пустой во время выполнения),
                             // получаем значение в тот же самый
                             // момент времени (т.е. у нас запрос
                             // 'INSERT RETURNING').
                             // В противном случае вызываем обработчик
                             // исключения, и select выполняется чуть позже
}

fact Trace {                           // Факт Trace описывает поведение системы
all t : Time - first | {              // на всех шагах, кроме первого:
   some delete.t => no userToken.t       // Если происходит удаление, таблица пуста
   some insert.t => some userToken.t     // Если происходит вставка, таблица не пуста
   no delete.t and no insert.t           // Если не происходит ни вставок, ни удалений,
    => userToken.t = userToken.(t.prev)  // таблица не меняется
  }
}

assert selectIsGood {         // То, что мы хотим проверить
all s : Operation.select |   // Всегда, когда выполняется select,
  some userToken.s            // в базе присутствуем токен
}
check selectIsGood for 6 // Проверить, что selectIsGood всегда истинно

┌────────┬────────────┐
│DBState │userToken   │
├────────┼──────┬─────┤
│DBState⁰│Token²│Time³│
│        │      ├─────┤  ← Token² находится в БД в моменты Time³ и Time⁵
│        │      │Time⁵│
│        ├──────┼─────┤
│        │Token³│Time²│  ← Token³ в БД в момент Time².
└────────┴──────┴─────┘
                   ↑
                 Токены есть в таблице только
                 моменты Time², Time³ и Time⁵
                 Заменит, что в момент
                 Time⁴ токенов нет!
┌──────────────┬──────┬──────┬──────┐
│Operation     │delete│insert│select│
├──────────────┼──────┼──────┼──────┤
│Operation⁰    │ TIME⁴│ Time⁵│ Time⁵│
├──────────────┼──────┼──────┼──────┤
│Operation¹    │ Time¹│ Time³│ TIME⁴│   ← Таблица пуста в момент Time⁴ и
├──────────────┼──────┼──────┼──────┤     select не работает для Operation¹!
│Operation²    │ Time¹│ Time²│ Time²│
└──────────────┴──────┴──────┴──────┘
                  ↑       ↑      ↑
                Это моменты времени, когда
                происходят соответствующие действия