osiire’s blog

ふしぎなそふとやさん

陶器のカタログ受発注の仕組みをAlloyで

仕事に関連して、とあるビジネスの仕組みを記述する必要があったので、Alloyで書いてみた。具体的には、

  • 陶器を製造・販売している企業がたくさんいる。
  • その企業が集まってカタログを作り、そのカタログを見たお客さんから受注を受ける。
  • もちろん、カタログに載っている自社製品以外の陶器を注文受けることもあるので、それはカタログを共同で出している企業さんから仕入れて売る。
  • 企業は複数のカタログに参加している。

という、よくあるカタログ販売の仕組み。本当は日付とか請求書とか納品書とかも定義してあったけど、大きくなりすぎるので割愛。コードは以下。

//
// 陶器のカタログ販売受発注のモデル化
//

// カタログから注文をするお客さん
sig Customer { }

// カタログ参加業者
sig Seller {
   belong : some Catalog,  // 属しているカタログ
   products : set Product // 自社製品
} {
   products.owner = this
}

// カタログ商品
sig Product { owner : Seller }

// カタログ
sig Catalog { 
   member : some Seller, // 参加企業
   products : some Product // カタログ全商品
} {
   products in Seller.products
} 

// カタログを見た人からの注文
sig Order {
   client : Customer,
   seller : Seller, // カタログ参加企業のどこかに注文が出される
   targets : some OrderUnit // 注文内容
} {
   targets.product in Catalog.products
}

//注文内容
sig OrderUnit {
   product : Product, // 商品
   amount : Int // 個数
} {
   amount > 0
   OrderUnit in Order.targets
}

// カタログ参加企業同士での発注
// カタログ参加企業は、お客からの注文のうち、
// 自社製品以外の商品を仕入れる必要がある。
sig GroupOrder {
   dir : GroupDir,
   targets : some OrderUnit // 仕入れる内容
} {
   // 仕入れようとしている商品は、
   // 仕入れ先の自社商品である。
   targets.product in dir.seller.products
}

sig GroupDir { 
   disj seller, buyer : Seller
} {
   some seller.belong & buyer.belong // 必ず同じカタログに参加している事
   GroupDir in GroupOrder.dir // GroupOrderと関係ない無意味なGroupDirは存在しない
}

fact {
   // 参加していると所属しているは、対象的
   member = ~belong

   // カタログ参加企業は、それぞれ自社製品を持っており(0の可能性もあるけど)
   // それらは全て独自製品である。 
   all disj a, b : Seller | no a.products & b.products 
}

pred show () {}
run show for 3 but 
  6 int, 
  exactly 1 Catalog,
  exactly 2 Product,
  exactly 1 Order,
  exactly 2 OrderUnit

あぁ、やっぱりalloyシンタックスハイライトされないな...。