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 final StateMachine

motorUp : Command
motorStop : Command
motorDown : Command

abstract WinMotor : Component
    cmd : Port -> Command

abstract final UserRequest
up : UserRequest
expressUp : UserRequest ?
stop : UserRequest
down : UserRequest

[ express <=> expressUp ]

[ pinchProtection <=> pinchDetector ]

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 ]

[ no pinchProtection => no 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 ]

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 ]

wc2 : WinController
assert [ sometime wc2.WinStates.stopped.closed -->> wc2.WinStates.stopped.partlyOpen -->> wc2.WinStates.stopped.open ]

wc3 : WinController
assert [ never wc3.req = down --> wc3.WinStates.stopped.closed ]

wc4 : WinController
assert [ never wc4.WinStates.stopped.closed && wc4.motor.cmd=motorUp ]

wc5 : WinController
assert [ never wc5.objectDetected --> wc5.WinStates.movingUp ]