tmp_powerwindow_total.cfr

/* **************** */
/* Feature Modeling */
/* **************** */

abstract final Feature
abstract final FeatureModel

WinFeatures : FeatureModel
    manualUpDown : Feature
    express : Feature ?
        pinchProtection : Feature ?

/* ********************************** */
/* Linking Features with Other Models */
/* ********************************** */

// linking the feature with the optional component (structural variability)
[ pinchProtection <=> pinchDetector ]

// without the pinch protection feature, the port is inactive
// having the feature will allow receiving objectDetected signal
[ no pinchProtection => no WinController.objectDetected ]

// user request only available when feature present (alphabet variability)
[ express <=> expressUp ]

/* ************************************************* */
/* Architectural Model With Behavior and Variability */
/* ************************************************* */

abstract final Component
    abstract Port
abstract final Command
motorUp : Command
motorStop : Command
motorDown : Command

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



abstract State
abstract StateMachine

WinMotor : Component
    // cmd : Port -> Command
    cmd -> Command

abstract WinController : Component
    // link to actuator
    final motor -> WinMotor

    // subcomponent
    pinchDetector : Component ?

    // inputs
    // req : Port -> UserRequest ?
    req -> UserRequest ?
    endOfTravel : Port ?
    objectDetected : Port ?

    // sequence of user request that can happen.
    [ 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]


    // only allow at most one input at the time
    [ lone (req, endOfTravel, objectDetected)]

    // the state will remain same if no input
    [no (req, endOfTravel, objectDetected) => (let oldState = State | next (State = oldState))]

    final xor WinStates : StateMachine
        xor movingUp : State
            [ motor.cmd = motorUp ]
            [ endOfTravel  --> closed ]
            [ req=down       --> movingDown ]
            [ req=up       --> movingUp ]
            [ req=expressUp --> movingUpX ]            
            initial basic : State
                [ req=stop --> stopped ]
                [ this -[objectDetected]-> basic ]

            movingUpX : State
                [ this -[objectDetected]-> stopped ]
                [ req=stop --> movingUpX ] 

        initial xor stopped : State
            [ motor.cmd = motorStop ]
            closed : State
                [ req=down --> movingDown ]
                [ req!=down --> closed ]
            partlyOpen : State
                [ req=up   --> movingUp   ]
                [ req=down --> movingDown ]
                [ (req!=up || req != down) --> partlyOpen ]
            open : State
                [ req=up   --> movingUp ]
                [ req!=up --> open ]

        movingDown : State
            [ motor.cmd = motorDown ]
            [ (req=up||req=expressUp)   --> movingUp ]
            [ endOfTravel  --> open     ]
            [ req=stop     --> stopped  ]
            [ (req=down || no req) => always (movingDown until endOfTravel) ]
            //[ (req=down || no req) => G (movingDown until endOfTravel) ]


/* ***************************************** */
/* Variability in Behavior Using Inheritance */
/* ***************************************** */

WinCtrWithContChime : WinController ?
    chime : Port ?
    [ movingUpX <=> chime ]

WinCtrWithChime : WinController ?
    chime : Port ?
    [ no movingUpX => no chime ]
    [ chime --> no chime ]
    [ no chime && movingUpX --> (movingUpX => chime) ]

/* ********************************************** */
/* Variability in Behavior Using Strategy Pattern */
/* ********************************************** */

abstract ChimingStrategy
    active : State ?
    audible : State ?
    [ not active => not audible ]

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.audible <=> chime ]

// configure the controller with a given strategy
[ WinControllerStrategies.strategy = Intermittent ]

/* ************************ */
/* Scenarios and Properties */
/* ************************ */

// an example positive scenario
assert [ initially closed && req=down --> movingDown -->>
         req=expressUp --> movingUpX --> objectDetected --> stopped ]

// must be possible to go from closed to open via partiallyOpen state
assert [ sometime closed -->> partlyOpen -->> open ]

// must be impossible for the user to request opening and the window remains closed
assert [ never req = down --> closed ]

// must be impossible for the window to be closed and continue sending motorUp command
// safety property: prevent burning the motor
assert [ never closed && cmd=motorUp ]

// safety: the window must never continue movingUp after an object was detected
assert [ never objectDetected --> movingUp ]