-- Pre-requisites and invariants

preconditions :: Model Symbolic -> Command Symbolic -> Logic
preconditions (Model m) cmd = case cmd of
  AddCopy    Invalid key   -> Not $ hasKey key
  Borrow     Invalid key   -> Not $ hasKey key
  Return     Invalid key   -> Not $ hasKey key
  FindByIsbn Invalid key   -> Not $ hasKey key
  NewBook    New   key _ _ -> Not $ hasKey key
  NewBook    Exist key _ _ -> hasKey key
  AddCopy    Exist key     -> hasKey key
  FindByIsbn Exist key     -> hasKey key
  Borrow     Avail   key -> keyPred key (\b -> avail b .> 0)
  Borrow     Unavail key -> keyPred key (\b -> avail b .== 0)
  Return     Taken   key -> keyPred key (\b -> owned b .> avail b)
  Return     Full    key -> keyPred key (\b -> owned b .== avail b)
  FindByAuthor Invalid x -> Not $ Exists values (Boolean . isInfixOf x . author)
  FindByTitle Invalid x  -> Not $ Exists values (Boolean . isInfixOf x . title)
  FindByTitle Exist x -> Exists values (Boolean . isInfixOf x . title)
  _ -> Top
  where
    values = codomain m
    hasKey key = key `member` (domain m)
    keyPred key p = maybe Bot p (lookup key m)
preconditions :: Model Symbolic -> Command Symbolic -> Logic
preconditions (Model m) cmd = case cmd of
  AddCopy    Invalid key   -> Not $ hasKey key
  Borrow     Invalid key   -> Not $ hasKey key
  Return     Invalid key   -> Not $ hasKey key
  FindByIsbn Invalid key   -> Not $ hasKey key
  NewBook    New   key _ _ -> Not $ hasKey key
  NewBook    Exist key _ _ -> hasKey key
  AddCopy    Exist key     -> hasKey key
  FindByIsbn Exist key     -> hasKey key
  Borrow     Avail   key -> keyPred key (\b -> avail b .> 0)
  Borrow     Unavail key -> keyPred key (\b -> avail b .== 0)
  Return     Taken   key -> keyPred key (\b -> owned b .> avail b)
  Return     Full    key -> keyPred key (\b -> owned b .== avail b)
  FindByAuthor Invalid x -> Not $ Exists values (Boolean . isInfixOf x . author)
  FindByTitle Invalid x  -> Not $ Exists values (Boolean . isInfixOf x . title)
  FindByTitle Exist x -> Exists values (Boolean . isInfixOf x . title)
  _ -> Top
  where
    values = codomain m
    hasKey key = key `member` (domain m)
    keyPred key p = maybe Bot p (lookup key m)
preconditions (Model m) cmd = case cmd of
  AddCopy    Invalid key   -> Not $ hasKey key
  Borrow     Invalid key   -> Not $ hasKey key
  Return     Invalid key   -> Not $ hasKey key
  FindByIsbn Invalid key   -> Not $ hasKey key
  NewBook    New   key _ _ -> Not $ hasKey key
  NewBook    Exist key _ _ -> hasKey key
  AddCopy    Exist key     -> hasKey key
  FindByIsbn Exist key     -> hasKey key
  Borrow     Avail   key -> keyPred key (\b -> avail b .> 0)
  Borrow     Unavail key -> keyPred key (\b -> avail b .== 0)
  Return     Taken   key -> keyPred key (\b -> owned b .> avail b)
  Return     Full    key -> keyPred key (\b -> owned b .== avail b)
  FindByAuthor Invalid x -> Not $ Exists values (Boolean . isInfixOf x . author)
  FindByTitle Invalid x  -> Not $ Exists values (Boolean . isInfixOf x . title)
  FindByTitle Exist x -> Exists values (Boolean . isInfixOf x . title)
  _ -> Top
  where
    values = codomain m
    hasKey key = key `member` (domain m)
    keyPred key p = maybe Bot p (lookup key m)