某社のコース申込システムをモデリング。
/*
豆蔵トレーニングコース申込システム
豆蔵のトレーニングコースの概要は以下の通り。
このシステムにおいて、コースへの申込が会場の定員数を超えないように管理したい。
[コース]
コースにはセットコース、単体コースがある。
コースによっては開催日程のうち、初日だけ受講可能なものがある。
セットコース：
UMLモデリング演習コース(5/13,14,15,16,17) 200,000円
(わかるオブジェクト指向、
UMLによるモデリング入門、
UMLによるオブジェクト指向分析設計演習)
単体コース：
わかるオブジェクト指向(5/13) 45,000円
UMLによるモデリング入門(5/14) 30,000円
UMLによるオブジェクト指向分析設計演習(5/15,16,17) 135,000円
オブジェクト指向開発プロセス入門(1日)(5/21)
オブジェクト指向開発プロセス入門(2日)(5/21,22)
[開催日程]
それぞれのコースの開催日程
2010/5/13
2010/5/14
2010/5/13,14,15,16,17,18
[会場]
会場には定員が決まっている。
教室A:20人
教室B:16人
[申込]
1回の申込当り、1名以上5名までの受講者がエントリすることがある。
author: Kenichi Kobayashi ken.coba@gmail.com
*/
/*
コース
わかるオブジェクト指向
UMLによるモデリング入門
UMLによるオブジェクト指向分析設計演習
UMLモデリングコース(セットコース)
など
*/
sig Course {
schedule:some Schedule,
entries:disj set Entry // 複数のコースが申込を共有しないよう、disjをつける
}
//開催日程
sig Schedule {
site:Site
}
//会場
sig Site {
capacity: Int
} {
capacity > 0
}
// 申込
sig Entry {}
//コースを開催している会場の定員を超えてはならない
fact SiteCapacity {
// s.~schedule = ある開催日程に関係しているCourseの集合
all s:Schedule | #(s.~schedule.entries) <= s.site.capacity
}
assert showCapacityOverflowCase {
all disj c1,c2:Course |
c1.schedule == c2.schedule => #c1.entries + #c2.entries <= c1.schedule.site.capacity
}
check showCapacityOverflowCase for 4 but
6 int,
exactly 2 Course,
exactly 1 Site
