{- ============================== 
   Copyright (c) 2026 SysFEAT - Systemic Framework for Enterprise Architecture & Transformation
   This work is released under the MIT License.
   framework.sysfeat.com

Service Interface: 
A Service Interface is an interaction Behavior Type that describes a typical course of Flow Connections, coordinated by Behavioral Events and Outcome Events, and intended to produce Outcomes through the involvement of Agent Types.

Documentation : https://framework.sysfeat.com/pages/24ae31b55ed1c66d.htm

External references:
  OpenGroup - ArchiMate - Service: https://pubs.opengroup.org/architecture/archimate32-doc/ch-Generic-Metamodel.html#sec-Behavior-Elements
  OpenGroup - IT4IT - Defining Service Reference Architecture: https://publications.opengroup.org/w161
 - ============================== -}

{-# OPTIONS --cubical --guardedness #-}

module SysFEAT.SOF.24ae31b55ed1c66d where -- ========== Service Interface

open import Agda.Primitive
open import SysFEAT.SOF.986cd4ec5ffca3ac public -- Behavior Type
open import SysFEAT.SOF.21c5276e655759fb public -- Operating Connection
open import SysFEAT.SOF.30223b5c5ec90c01 public -- Outcome Event

ServiceInterface : ClassOfClassOfBoundedIndividual
ServiceInterface = ClassOfBoundedIndividual


--  ServiceInterface is subTypeOf BehaviorType
st-24ae31b55ed1c66d-986cd4ec5ffca3ac : ServiceInterface ⊏ₑ BehaviorType
st-24ae31b55ed1c66d-986cd4ec5ffca3ac = polySubTypeOf-identity

--  ServiceInterface is subTypeOf OperatingConnection
st-24ae31b55ed1c66d-21c5276e655759fb : ServiceInterface ⊏ₑ OperatingConnection
st-24ae31b55ed1c66d-21c5276e655759fb = polySubTypeOf-identity


-- == Relations =======================

-- -------------------------------------------------------------------------------------------- 
{- Sub Service Interface: -}
-- Aggregate Member : Sub Service Interface
SubServiceInterface : ClassOfClassOfBoundedIndividual
SubServiceInterface = ClassOfBoundedIndividual



--  SubServiceInterface is subTypeOf BehaviorPart
st-f38134c7687e3c48-b776b92668b04c85 : SubServiceInterface ⊏ₑ BehaviorPart
st-f38134c7687e3c48-b776b92668b04c85 = polySubTypeOf-identity

-- Membership relation
membershipOfSubServiceInterface :  Linkage ServiceInterface SubServiceInterface
membershipOfSubServiceInterface = make_upwardNestingRelation "subServiceInterface membership" "nested subServiceInterface"

-- Aggregation relation
aggregationOfServiceInterfaceSubServiceInterface :  Linkage SubServiceInterface ServiceInterface
aggregationOfServiceInterfaceSubServiceInterface = make_Relation "ServiceInterface aggregation" "aggregated ServiceInterface"

{- subServiceInterface : derived relation obtained by composing
   membershipOfSubServiceInterface and aggregationOfServiceInterfaceSubServiceInterface
   It directly links an Service Interface to the final aggregated ServiceInterface
   hiding the reifying SubServiceInterface
-}
subServiceInterface : Linkage ServiceInterface ServiceInterface
subServiceInterface = membershipOfSubServiceInterface  ∘  aggregationOfServiceInterfaceSubServiceInterface



-- -------------------------------------------------------------------------------------------- 
{- Flow Connection: 
A Flow Connection is an Outcome Event event that occurs between the consumer and the provider participant of a Service Interface.
-}
-- Aggregate Member : Flow Connection
FlowConnection : ClassOfClassOfBoundedIndividual
FlowConnection = ClassOfBoundedIndividual



--  FlowConnection is subTypeOf BehaviorPart
st-c561d7e4680f69ce-b776b92668b04c85 : FlowConnection ⊏ₑ BehaviorPart
st-c561d7e4680f69ce-b776b92668b04c85 = polySubTypeOf-identity

-- Membership relation
membershipOfFlowConnection :  Linkage ServiceInterface FlowConnection
membershipOfFlowConnection = make_upwardNestingRelation "flowConnection membership" "nested flowConnection"

-- Aggregation relation
aggregationOfOutcomeEventFlowConnection :  Linkage FlowConnection OutcomeEvent
aggregationOfOutcomeEventFlowConnection = make_Relation "OutcomeEvent aggregation" "aggregated OutcomeEvent"

{- flowConnection : derived relation obtained by composing
   membershipOfFlowConnection and aggregationOfOutcomeEventFlowConnection
   It directly links an Service Interface to the final aggregated OutcomeEvent
   hiding the reifying FlowConnection
-}
flowConnection : Linkage ServiceInterface OutcomeEvent
flowConnection = membershipOfFlowConnection  ∘  aggregationOfOutcomeEventFlowConnection