-
Notifications
You must be signed in to change notification settings - Fork 0
/
smartHome.als
16 lines (14 loc) · 927 Bytes
/
smartHome.als
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
module smartHome
open smartHomeCore
// Our home has to have at least two outlets in each room
fact { all a : Room | (some b : a.accessories, c : a.accessories | b.category = AccessoryCategoryOutlet && c.category = AccessoryCategoryOutlet && b != c) }
// ... and al least lightbulb in each room
fact { all a : Room | (some b : a.accessories | b.category = AccessoryCategoryLightbulb) }
// ... and at least one window in each room
fact { all a : Room | (some b : a.accessories | b.category = AccessoryCategoryWindow) }
// ... and one fan for the whole home
fact { all a : Home | (one b : a.accessories | b.category = AccessoryCategoryFan) }
// ... and one alarm for the whole home
fact { all a : Home | (one b : a.accessories | b.category = AccessoryCategoryAlarm) }
run addAccessory for 20 but exactly 1 Home, exactly 4 Room, exactly 18 Accessory
// run addRoom for 20 but exactly 1 Home, exactly 4 Room, exactly 18 Accessory