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

Behavioral Rule: 
A Behavioral Rule is a Directive intended to guide the Behavior of Agent Types, in compliance with enterprise Policy(ies) or regulations.Often, a Behavioral Rule is derived from a Policy. Behavioral Rules are enforced in Processes and Agent Types.

Documentation : https://framework.sysfeat.com/pages/190c74f868966584.htm

External references:
  OMG - BMM - Business Rule: https://www.omg.org/spec/BMM/1.3/PDF#page=46
  OMG - SBVR - Business Rule (Behavioral): https://www.omg.org/spec/SBVR/1.5/PDF#page=129
 - ============================== -}

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

module SysFEAT.SOF.190c74f868966584 where -- ========== Behavioral Rule

open import Agda.Primitive
open import SysFEAT.SOF.515c6b23689335c3 public -- Directive
open import SysFEAT.SOF.190c7429689664b5 public -- Policy

BehavioralRule : PropertyType
BehavioralRule = Property

--  BehavioralRule is subTypeOf Directive
st-190c74f868966584-515c6b23689335c3 : BehavioralRule ⊏ₑ Directive
st-190c74f868966584-515c6b23689335c3 = polySubTypeOf-identity


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

-- -------------------------------------------------------------------------------------------- 
{- Specialized Behavioral Rule: -}
specializedBehavioralRule :  Linkage BehavioralRule BehavioralRule
specializedBehavioralRule = make_subTypeOf "Specialized Behavioral Rule" "Specialized Behavioral Rule"

postulate -- specializedBehavioralRule is subTypeOf specializedDirective
  st-01f10e56689b5157-190c79c26896690d  : specializedBehavioralRule  ⊏⋆ᵣ  specializedDirective

-- -------------------------------------------------------------------------------------------- 
{- Policy Derivation: 
Statement that a Behavioral Rule is the realization of a Policy.
-}
-- Aggregate Member : Policy Derivation
PolicyDerivation : ClassOfClassOfIndividual
PolicyDerivation = ClassOfIndividual


--  PolicyDerivation withAspect RealizedDirective
st-7bc2add56899a8e3-190c7a7f6896696e : PolicyDerivation ⊏ₐₑ (RealizedDirective (lsuc(lzero)))
st-7bc2add56899a8e3-190c7a7f6896696e = polySubTypeOf-identity

--  PolicyDerivation withAspect UnboundedMember
st-7bc2add56899a8e3-8cfaf71a6852b042 : PolicyDerivation ⊏ₐₑ (UnboundedMember (lsuc(lzero)))
st-7bc2add56899a8e3-8cfaf71a6852b042 = polySubTypeOf-identity

-- Membership relation
membershipOfPolicyDerivation :  Linkage BehavioralRule PolicyDerivation
membershipOfPolicyDerivation = make_upwardNestingRelation "policyDerivation membership" "nested policyDerivation"

-- Aggregation relation
aggregationOfPolicyPolicyDerivation :  Linkage PolicyDerivation Policy
aggregationOfPolicyPolicyDerivation = make_Relation "Policy aggregation" "aggregated Policy"

{- policyDerivation : derived relation obtained by composing
   membershipOfPolicyDerivation and aggregationOfPolicyPolicyDerivation
   It directly links an Behavioral Rule to the final aggregated Policy
   hiding the reifying PolicyDerivation
-}
policyDerivation : Linkage BehavioralRule Policy
policyDerivation = membershipOfPolicyDerivation  ∘  aggregationOfPolicyPolicyDerivation