AutoPilot : System
    AP_FAA : FunctionalAnalysis          
        frontDriverLidar : FunctionalDevice ?
            [implementation.hardware]
            [degradation = 1]
            [one output]
        frontPassengerLidar : FunctionalDevice ?
            [implementation.hardware]
            [degradation = 1]
            [one output]
        lidarProcessing : AnalysisFunction ?
            [implementation.software]
            [degradation = (if #input = 2 then 1 else 2)]
            [some input && one output]
        pointCloudClustering : AnalysisFunction ?
            [implementation.software]
            [degradation = 1]
            [some input && one output]
        frontRadar : FunctionalDevice ?
            [implementation.hardware]
            [degradation = 1]
            [one output]
        frontCamera : FunctionalDevice ? 
            [implementation.hardware]
            [degradation = 1] 
            [one output]
        dynamicObjectDetection : AnalysisFunction ?
            [implementation.software]
            [degradation = (if frontRadarVal && pointCloudCusterVal then 1 else if frontCameraVal && pointCloudCusterVal then 2 else 3)]  
            [some input && one output]
        trajectoryPlanningAP : AnalysisFunction ?
            [implementation.software]
            [degradation = 1]
            [some input && one output]
        speedControl : AnalysisFunction ?
            [implementation.software]
            [degradation = 1]
            [some input]
        
        // Function Connectors

        frontDriverLidarVal : FunctionConnector ?
            [sender = frontDriverLidar && receiver = lidarProcessing]
        frontPassengerLidarVal : FunctionConnector ?
            [sender = frontPassengerLidar && receiver = lidarProcessing]
        compositePointCloud : FunctionConnector ?
            [sender = lidarProcessing && receiver = pointCloudClustering]
        frontRadarVal : FunctionConnector ?
            [sender = frontRadar && receiver = dynamicObjectDetection]
        frontCameraVal : FunctionConnector ?
            [sender = frontCamera && receiver = dynamicObjectDetection]
        pointCloudCusterVal : FunctionConnector ?
            [sender = pointCloudClustering && receiver = dynamicObjectDetection]
        dynamicObjects : FunctionConnector ?
            [sender = dynamicObjectDetection && receiver = trajectoryPlanningAP]
        velocityProfile : FunctionConnector ?
            [sender = trajectoryPlanningAP && receiver = speedControl]

        // Replacement constraints
        [no frontRadar => frontCamera]


    AP_HA : HardwareArchitecture
        dn -> AP_DN
        AP_DN : DeviceNodeClassification
            visionProcessor1 : DeviceNode ?
                [type = SmartDeviceNode]
            visionProcessor2 : DeviceNode ?
                [type = SmartDeviceNode]
            algorithmProcessor1 : DeviceNode ?
                [type = SmartDeviceNode]
            algorithmProcessor2 : DeviceNode ?
                [type = SmartDeviceNode]

            frontDriverLidarSensor : DeviceNode ?
                [type = EEDeviceNode]
            frontPassengerLidarSensor : DeviceNode ?
                [type = EEDeviceNode]

            frontRadarSensor : DeviceNode ?
                [type = EEDeviceNode]
            frontCameraSensor : DeviceNode ?
                [type = EEDeviceNode]

    AP_Dpl : Deployment
        fa -> AP_FAA
        ha -> AP_HA
        [fa.frontDriverLidar.deployedTo = ha.dn.frontDriverLidarSensor]
        [fa.frontPassengerLidar.deployedTo = ha.dn.frontPassengerLidarSensor]
        [fa.lidarProcessing.deployedTo in (ha.dn.visionProcessor1, ha.dn.visionProcessor2)]
        [fa.pointCloudClustering.deployedTo in (ha.dn.algorithmProcessor1, ha.dn.algorithmProcessor2)]
        [fa.frontRadar.deployedTo = ha.dn.frontRadarSensor]
        [fa.frontCamera.deployedTo = ha.dn.frontCameraSensor]
        [fa.dynamicObjectDetection.deployedTo in (ha.dn.algorithmProcessor1, ha.dn.algorithmProcessor2)]
        [fa.trajectoryPlanningAP.deployedTo in (ha.dn.algorithmProcessor1, ha.dn.algorithmProcessor2)]
        [fa.speedControl.deployedTo in (ha.dn.algorithmProcessor1, ha.dn.algorithmProcessor2)]



[#(DeviceNode) = 7]
assert [AP_FAA.trajectoryPlanningAP && AP_FAA.speedControl]

abstract System
abstract FunctionalAnalysis
abstract HardwareArchitecture
abstract DeviceNodeClassification
abstract Deployment

abstract FunctionalAnalysisComponent
    deployedTo -> DeviceNode 1..2 
    xor implementation
        hardware
            [deployedTo.type in EEDeviceNode, SmartDeviceNode]
        software
            [deployedTo.type in SmartDeviceNode]
    input -> FunctionConnector *
        [this.receiver = parent]
    output -> FunctionConnector *
        [this.sender = parent]
    degradation -> integer
        [this > 0 && this <= 3]
    resultingDegradation -> integer = max (input.sender.resultingDegradation.dref, degradation.dref)
abstract AnalysisFunction : FunctionalAnalysisComponent
abstract FunctionalDevice : FunctionalAnalysisComponent
abstract FunctionConnector
    sender -> FunctionalAnalysisComponent
        [parent in this.output]
    receiver -> FunctionalAnalysisComponent
        [parent in this.input]


enum DeviceNodeType = SmartDeviceNode | EEDeviceNode | PowerDeviceNode

abstract DeviceNode
    [ some fac : FunctionalAnalysisComponent | this in fac.deployedTo ]
    type -> DeviceNodeType