abstract final Feature
abstract final FeatureModel
c0_FeatureModel
WinFeatures : FeatureModel
manualUpDown : Feature
express : Feature ?
pinchProtection : Feature ?
reference
abstract final Component
abstract Port
abstract final Command
c0_Command
abstract State
abstract final StateMachine
c0_StateMachine
motorUp : Command
motorStop : Command
motorDown : Command
reference
abstract WinMotor : Component
cmd : Port -> Command
reference
abstract final UserRequest
up : UserRequest
expressUp : UserRequest ?
stop : UserRequest
down : UserRequest
reference
[ express <=> expressUp ]
keyword
[ pinchProtection <=> pinchDetector ]
keyword
abstract WinController : Component
motor : WinMotor
pinchDetector : Component ?
req : Port -> UserRequest ?
endOfTravel : Port ?
objectDetected : Port ?
[ lone req, endOfTravel, objectDetected ]
[ always req = stop between req = down and req = up ]
[ always req = stop between req = up and req = down ]
[ always req = up between req = stop and req = expressUp ]
[ always req = expressUp => next no req ]
final xor WinStates : StateMachine
xor movingUp : State
[ motor.cmd = motorUp ]
[ req = down --> movingDown ]
[ endOfTravel --> closed ]
[ req = up --> movingUp ]
initial basic : State
[ req = stop --> stopped ]
[ req = expressUp --> movingUpX ]
movingUpX : State
[ this -[objectDetected]--> stopped ]
initial xor stopped : State
[ motor.cmd = motorStop ]
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
[ motor.cmd = motorDown ]
[ req = up --> movingUp ]
[ endOfTravel --> open ]
[ req = stop --> stopped ]
[ req = down --> movingDown ]
keyword
[ no pinchProtection => no objectDetected ]
keyword
WinCtrWithContChime : WinController ?
chime : Port ?
[ movingUpX <=> chime ]
keyword
WinCtrWithChime : WinController ?
chime : Port ?
[ no movingUpX => no chime ]
[ chime --> no chime ]
[ no chime && movingUpX --> movingUpX => chime ]
keyword
abstract ChimingStrategy
active : State ?
audible : State ?
reference
NoChiming : ChimingStrategy
[ not audible ]
keyword
Continuous : ChimingStrategy
[ active => audible ]
keyword
Intermittent : ChimingStrategy
[ audible --> not audible ]
[ not audible --> active => audible ]
keyword
WinControllerStrategies : WinController ?
chime : Port ?
strategy -> ChimingStrategy
[ strategy.active <=> movingUpX ]
[ strategy.active.audible <=> chime ]
keyword
[ WinControllerStrategies.strategy = Intermittent ]
keyword
wc1 : WinController
assert [ initially wc1.WinStates.stopped.closed && wc1.req = down --> wc1.WinStates.movingDown -->> wc1.req = expressUp --> wc1.WinStates.movingUp.movingUpX --> wc1.objectDetected --> wc1.WinStates.stopped ]
keyword
wc2 : WinController
assert [ sometime wc2.WinStates.stopped.closed -->> wc2.WinStates.stopped.partlyOpen -->> wc2.WinStates.stopped.open ]
keyword
wc3 : WinController
assert [ never wc3.req = down --> wc3.WinStates.stopped.closed ]
keyword
wc4 : WinController
assert [ never wc4.WinStates.stopped.closed && wc4.motor.cmd = motorUp ]
keyword
wc5 : WinController
assert [ never wc5.objectDetected --> wc5.WinStates.movingUp ]