postconditions :: Model Concrete -> Command Concrete -> Response Concrete -> Logic
postconditions (Model m) cmd resp = case cmd of
  NewBook    Exist _ _ _ -> resp .== UniqueError
  NewBook    New   _ _ _ -> resp .== Inserted
  AddCopy      Invalid _ -> resp .== NotFound
  Return       Invalid _ -> resp .== NotFound
  Borrow       Invalid _ -> resp .== NotFound
  Return       Full    _ -> resp .== NotFound
  Borrow       Unavail _ -> resp .== NotFound
  Borrow       Avail   _ -> resp .== Updated
  AddCopy      Exist   _ -> resp .== Updated
  Return       Taken   _ -> resp .== Updated
  FindByIsbn   Invalid _ -> resp .== Rows []
  FindByAuthor Invalid _ -> resp .== Rows []
  FindByTitle  Invalid _ -> resp .== Rows []
  FindByIsbn Exist key -> case lookup key m of
    Just x -> Rows [x] .== resp
    _      -> error "Should not happen"
  FindByAuthor Exist x -> case resp of
    Rows rs -> Forall rs (Boolean . isInfixOf x . author) .&&
               Forall rs (\b -> Just b .== lookup (Isbn $ isbn b) m)
    _ -> Bot .// "findByAuthor returned " ++ (show resp)
  FindByTitle Exist x -> case resp of
    Rows rs -> Forall rs (Boolean . isInfixOf x . title) .&&
               Forall rs (\b -> Just b .== lookup (Isbn $ isbn b) m)
    _ -> Bot .// "findByTitle returned " ++ (show resp)
  _ -> Bot

-- Transitions of the state machine that models SUT
postconditions :: Model Concrete -> Command Concrete -> Response Concrete -> Logic
postconditions (Model m) cmd resp = case cmd of
  NewBook    Exist _ _ _ -> resp .== UniqueError
  NewBook    New   _ _ _ -> resp .== Inserted
  AddCopy      Invalid _ -> resp .== NotFound
  Return       Invalid _ -> resp .== NotFound
  Borrow       Invalid _ -> resp .== NotFound
  Return       Full    _ -> resp .== NotFound
  Borrow       Unavail _ -> resp .== NotFound
  Borrow       Avail   _ -> resp .== Updated
  AddCopy      Exist   _ -> resp .== Updated
  Return       Taken   _ -> resp .== Updated
  FindByIsbn   Invalid _ -> resp .== Rows []
  FindByAuthor Invalid _ -> resp .== Rows []
  FindByTitle  Invalid _ -> resp .== Rows []
  FindByIsbn Exist key -> case lookup key m of
    Just x -> Rows [x] .== resp
    _      -> error "Should not happen"
  FindByAuthor Exist x -> case resp of
    Rows rs -> Forall rs (Boolean . isInfixOf x . author) .&&
               Forall rs (\b -> Just b .== lookup (Isbn $ isbn b) m)
    _ -> Bot .// "findByAuthor returned " ++ (show resp)
  FindByTitle Exist x -> case resp of
    Rows rs -> Forall rs (Boolean . isInfixOf x . title) .&&
               Forall rs (\b -> Just b .== lookup (Isbn $ isbn b) m)
    _ -> Bot .// "findByTitle returned " ++ (show resp)
  _ -> Bot

-- Transitions of the state machine that models SUT
postconditions (Model m) cmd resp = case cmd of
  NewBook    Exist _ _ _ -> resp .== UniqueError
  NewBook    New   _ _ _ -> resp .== Inserted
  AddCopy      Invalid _ -> resp .== NotFound
  Return       Invalid _ -> resp .== NotFound
  Borrow       Invalid _ -> resp .== NotFound
  Return       Full    _ -> resp .== NotFound
  Borrow       Unavail _ -> resp .== NotFound
  Borrow       Avail   _ -> resp .== Updated
  AddCopy      Exist   _ -> resp .== Updated
  Return       Taken   _ -> resp .== Updated
  FindByIsbn   Invalid _ -> resp .== Rows []
  FindByAuthor Invalid _ -> resp .== Rows []
  FindByTitle  Invalid _ -> resp .== Rows []
  FindByIsbn Exist key -> case lookup key m of
    Just x -> Rows [x] .== resp
    _      -> error "Should not happen"
  FindByAuthor Exist x -> case resp of
    Rows rs -> Forall rs (Boolean . isInfixOf x . author) .&&
               Forall rs (\b -> Just b .== lookup (Isbn $ isbn b) m)
    _ -> Bot .// "findByAuthor returned " ++ (show resp)
  FindByTitle Exist x -> case resp of
    Rows rs -> Forall rs (Boolean . isInfixOf x . title) .&&
               Forall rs (\b -> Just b .== lookup (Isbn $ isbn b) m)
    _ -> Bot .// "findByTitle returned " ++ (show resp)
  _ -> Bot

-- Transitions of the state machine that models SUT