abstract final Feature
abstract final FeatureModel
WinFeatures : FeatureModel
manualUpDown : Feature
express : Feature ?
pinchProtection : Feature ?
abstract final Component
abstract Port
abstract final Command
abstract State
abstract StateMachine
motorUp : Command
motorStop : Command
motorDown : Command
WinMotor : Component
cmd : Port -> Command
abstract final UserRequest
up : UserRequest
expressUp : UserRequest ?
stop : UserRequest
down : UserRequest
[ express <=> expressUp ]
abstract WinController : Component
final motor -> WinMotor
pinchDetector : Component ?
req : Port -> UserRequest ?
endOfTravel : Port ?
objectDetected : Port ?
[ lone req, endOfTravel, objectDetected ]
final xor WinStates : StateMachine
xor movingUp : State
[ req = down --> movingDown ]
[ req = up --> movingUp ]
initial basic : State
[ req = stop --> stopped ]
movingUpX : State
[ this -[objectDetected]--> stopped ]
initial xor stopped : State
closed : State
[ req = down --> movingDown ]
[ req = up || req = stop --> closed ]
partlyOpen : State
[ req = up --> movingUp ]
[ req = down --> movingDown ]
[ req = stop --> partlyOpen ]
open : State
[ req = up --> movingUp ]
[ req = down || req = stop --> open ]
movingDown : State
[ req = up --> movingUp ]
[ endOfTravel --> open ]
[ req = stop --> stopped ]
[ req = down --> movingDown ]
[ pinchProtection <=> pinchDetector ]
[ no pinchProtection => no WinController.objectDetected ]
WinCtrWithContChime : WinController ?
chime : Port ?
[ movingUpX <=> chime ]
WinCtrWithChime : WinController ?
chime : Port ?
[ no movingUpX => no chime ]
[ chime --> no chime ]
[ no chime && movingUpX --> movingUpX => chime ]
abstract ChimingStrategy
active : State ?
audible : State ?
NoChiming : ChimingStrategy
[ not audible ]
Continuous : ChimingStrategy
[ active => audible ]
Intermittent : ChimingStrategy
[ audible --> not audible ]
[ not audible --> active => audible ]
WinControllerStrategies : WinController ?
chime : Port ?
strategy -> ChimingStrategy
[ strategy.active <=> movingUpX ]
[ strategy.active.audible <=> chime ]
[ WinControllerStrategies.strategy = Intermittent ]
assert [ initially closed && req = down --> movingDown -->> req = expressUp --> movingUpX --> objectDetected --> stopped ]
assert [ sometime closed -->> partlyOpen -->> open ]
assert [ never req = down --> closed ]
assert [ never closed && cmd = motorUp ]
assert [ never objectDetected --> movingUp ]