complete-model-tpcc.problem

/*
 * Copyright (c) 2026-present Contributors to the A Four-Layer Modeling 
 * Framework for Policy-Driven Design in Hyperledger Fabric project.
 *
 * This program and the accompanying materials are made available under the
 * terms of the Eclipse Public License 2.0 which is available at
 * https://www.eclipse.org/legal/epl-2.0/.
 *
 * SPDX-License-Identifier: EPL-2.0
 */

//# Copyright (c) 2026 Contributors to the HLF-Layered-Modeling Project.
//# Licensed under the MIT License. See LICENSE file in the project root for full license information.

import builtin::view.

// ============================================================================
// LAYER 0: CONSORTIUM STRUCTURE
// ============================================================================
//
// Models the organizational landscape: who participates and what business
// collaborations they intend. Intentionally pre-technical — a business
// stakeholder should be able to read and validate this layer.
// ============================================================================

// The root entity. A consortium is a group of organizations that have agreed
// to operate shared DLT infrastructure for specific business purposes.
@color(5)
class Consortium {
    contains Organization[1..*] members
    contains CollaborationIntent[1..*] intents
    
    // Lower-layer elements contained here for single model root
    contains Channel[1..*] channels                      // Layer 1
    contains CommunicationNetwork[] networks             // Layer 3
    contains NetworkInterconnection[] interconnections   // Layer 3
}

// A real-world legal or institutional entity participating in the consortium.
@color(0)
class Organization {
    // Infrastructure owned by this organization (Layer 3)
    contains Host[1..*] hosts
    
    // Networks owned/operated by this organization
    CommunicationNetwork[] ownsNetworks
}

// A declaration that a subset of consortium members intends to share a ledger
// for a specific business purpose. The business-level precursor to a Channel.
@color(5)
class CollaborationIntent {
    // Organizations that intend to transact. Minimum 2 (DLT rationale).
    Organization[2..*] participants
    
    // Realization link to Layer 1
    Channel[0..1] realizedBy opposite realizes
}


// ============================================================================
// LAYER 0: WITHIN-LAYER CONSTRAINTS
// ============================================================================

pred intentInConsortium(CollaborationIntent ci, Consortium c) <->
    intents(c, ci).

pred orgInConsortium(Organization o, Consortium c) <->
    members(c, o).

// All participants must be consortium members
error participantNotInConsortium(CollaborationIntent ci, Organization o) <->
    participants(ci, o),
    intentInConsortium(ci, c),
    !orgInConsortium(o, c).


// ============================================================================
// LAYER 1: NETWORK ARCHITECTURE
// ============================================================================
//
// Fabric-specific technical concepts: channels as isolated ledgers,
// chaincodes deployed on channels, endorsement policies governing validity.
// ============================================================================

// A channel is an isolated ledger shared by a subset of consortium members.
// Technical realization of a CollaborationIntent.
@color(2)
class Channel {
    contains ChaincodeInstance[1..*] chaincodes
    
    // Backlink to Layer 0
    CollaborationIntent[0..1] realizes opposite realizedBy
}

// A deployed chaincode (smart contract) on a specific channel.
@color(2)
class ChaincodeInstance {
    refers Policy[1] policy
    EndorsingNode[2..*] endorsedBy opposite endorses
}

// Endorsement policies define validity requirements for transactions.
@color(4)
abstract class Policy {}

class AnyPolicy      extends Policy {}  // At least one endorser
class MajorityPolicy extends Policy {}  // >50% of participating orgs
class AllPolicy      extends Policy {}  // All participating orgs


// ============================================================================
// LAYER 1: WITHIN-LAYER CONSTRAINTS
// ============================================================================

pred chaincodePolicy(ChaincodeInstance ci, Policy p) <->
    policy(ci, p).

error unusedPolicy(Policy p) <->
    Policy(p),
    !chaincodePolicy(_, p).


// ============================================================================
// LAYER 2: NODE TOPOLOGY
// ============================================================================
//
// Logical node roles: orderers sequence transactions via Raft consensus,
// endorsers execute chaincode and sign proposals. Nodes are deployed on
// infrastructure (Layer 3) but their *roles* are defined here.
// ============================================================================

@color(3)
abstract class Node {
    // Deployment link to Layer 3
    Host[1] deployedOn
}

// Orderers participate in Raft consensus to sequence transactions.
@color(3)
class OrderingNode extends Node {
    Channel[1..*] orders
}

// Endorsers execute chaincode and sign transaction proposals.
// Also maintain ledger copies (committing peers).
@color(3)
class EndorsingNode extends Node {
    ChaincodeInstance[1..*] endorses opposite endorsedBy
}


// ============================================================================
// LAYER 2: PARTICIPATION PREDICATES
// ============================================================================

// Node participates in channel if it orders or endorses there
pred nodeParticipatesInChannel(Node n, Channel c) <->
    OrderingNode(n), orders(n, c)
    ;
    EndorsingNode(n), endorses(n, ci), chaincodes(c, ci).

// Organization participates if it owns a host with a participating node
pred orgParticipatesInChannel(Organization o, Channel c) <->
    hosts(o, h),
    deployedOn(n, h),
    nodeParticipatesInChannel(n, c).

// Channel needs multiple orgs (DLT rationale)
pred channelHasMultipleOrgs(Channel c) <->
    orgParticipatesInChannel(o1, c),
    orgParticipatesInChannel(o2, c),
    o1 != o2.

error singleOrgChannel(Channel c) <->
    Channel(c),
    !channelHasMultipleOrgs(c).

// Channel needs at least one orderer
error channelWithoutOrderer(Channel c) <->
    Channel(c),
    !orders(_, c).


// ============================================================================
// LAYER 2: ENDORSEMENT VALIDATION
// ============================================================================

pred canEndorse(EndorsingNode n, ChaincodeInstance ci) <->
    nodeParticipatesInChannel(n, ch),
    chaincodes(ch, ci).

error crossChannelEndorsement(EndorsingNode n, ChaincodeInstance ci) <->
    endorses(n, ci),
    !canEndorse(n, ci).

// Organization-level endorsement
pred orgParticipatesInChaincode(Organization o, ChaincodeInstance ci) <->
    chaincodes(ch, ci),
    orgParticipatesInChannel(o, ch).

pred orgEndorsesChaincode(Organization o, ChaincodeInstance ci) <->
    endorses(n, ci),
    deployedOn(n, h),
    hosts(o, h).

// AllPolicy: every participating org must endorse
pred fullyEndorsed(ChaincodeInstance ci) <->
    count { orgParticipatesInChaincode(_, ci) } ==
    count { orgEndorsesChaincode(_, ci) }.

error allPolicyNotSatisfied(ChaincodeInstance ci) <->
    chaincodePolicy(ci, p),
    AllPolicy(p),
    !fullyEndorsed(ci).

// MajorityPolicy: >50% of participating orgs
pred majorityEndorsed(ChaincodeInstance ci) <->
    count { orgEndorsesChaincode(_, ci) } >
    count { orgParticipatesInChaincode(_, ci) } / 2.

error majorityPolicyNotSatisfied(ChaincodeInstance ci) <->
    chaincodePolicy(ci, p),
    MajorityPolicy(p),
    !majorityEndorsed(ci).

// AnyPolicy: at least one org
pred anyEndorsed(ChaincodeInstance ci) <->
    count { orgEndorsesChaincode(_, ci) } >= 1.

error anyPolicyNotSatisfied(ChaincodeInstance ci) <->
    chaincodePolicy(ci, p),
    AnyPolicy(p),
    !anyEndorsed(ci).


// ============================================================================
// LAYER 3: INFRASTRUCTURE
// ============================================================================
//
// Physical deployment: hosts (servers/VMs), communication networks, and
// interconnections between networks. This layer grounds the logical
// architecture in physical reality.
// ============================================================================

// A physical or virtual machine that can host nodes.
@color(1)
class Host {
    // Networks this host is connected to
    CommunicationNetwork[1..*] connectedTo
}

// A network segment (e.g., org's internal network, cloud VPC, DMZ).
@color(1)
class CommunicationNetwork {}

// An interconnection between two networks (e.g., VPN, peering, gateway).
// Enables communication across network boundaries.
@color(1)
class NetworkInterconnection {
    CommunicationNetwork[2] links
}


// ============================================================================
// LAYER 3: CONNECTIVITY PREDICATES
// ============================================================================

// Two networks are directly connected if an interconnection links them
pred networksDirectlyConnected(CommunicationNetwork n1, CommunicationNetwork n2) <->
    links(ni, n1),
    links(ni, n2),
    n1 != n2.

// Networks are reachable (transitively) through interconnections
pred networksConnected(CommunicationNetwork n1, CommunicationNetwork n2) <->
    n1 == n2
    ;
    networksDirectlyConnected+(n1, n2).

// Hosts can communicate if their networks are connected
pred hostsCanCommunicate(Host h1, Host h2) <->
    h1 == h2
    ;
    connectedTo(h1, net1),
    connectedTo(h2, net2),
    networksConnected(net1, net2).

// Nodes can communicate if their hosts can
pred nodesCanCommunicate(Node n1, Node n2) <->
    deployedOn(n1, h1),
    deployedOn(n2, h2),
    hostsCanCommunicate(h1, h2).


// ============================================================================
// LAYER 3: WITHIN-LAYER CONSTRAINTS
// ============================================================================

// A host must be reachable (connected to at least one network)
// Already enforced by CommunicationNetwork[1..*] multiplicity

// Network interconnection must link two different networks
error selfInterconnection(NetworkInterconnection ni) <->
    links(ni, n1),
    links(ni, n2),
    n1 == n2.


// ============================================================================
// CROSS-LAYER PREDICATES: Layer 0 ↔ Layer 1
// (Consortium Structure ↔ Network Architecture)
// ============================================================================

// CL.1: Every intent must be realized by a channel
error unrealizedIntent(CollaborationIntent ci) <->
    CollaborationIntent(ci),
    !realizedBy(ci, _).

// CL.2: Intended participant must actually participate
error intendedParticipantNotOnChannel(CollaborationIntent ci, Organization o) <->
    participants(ci, o),
    realizedBy(ci, ch),
    !orgParticipatesInChannel(o, ch).

// CL.3: Channel participant not in the original intent (unexpected inclusion)
pred orgIntendedForChannel(Organization o, Channel ch) <->
    realizes(ch, ci),
    participants(ci, o).

pred channelRealizesIntent(Channel ch) <->
    realizes(ch, _).

error unintendedParticipant(Channel ch, Organization o) <->
    channelRealizesIntent(ch),
    orgParticipatesInChannel(o, ch),
    !orgIntendedForChannel(o, ch).


// ============================================================================
// CROSS-LAYER PREDICATES: Layer 0 ↔ Layer 2
// (Consortium Structure ↔ Node Topology)
// ============================================================================

// CL.4: Collaboration implies distributed ordering (trust distribution)
// Single-org ordering means that org controls transaction sequencing
pred channelOrdererOrg(Channel ch, Organization o) <->
    orders(n, ch),
    deployedOn(n, h),
    hosts(o, h).

pred channelHasDistributedOrdering(Channel ch) <->
    channelOrdererOrg(ch, o1),
    channelOrdererOrg(ch, o2),
    o1 != o2.

error singleOrgOrdering(CollaborationIntent ci) <->
    realizedBy(ci, ch),
    !channelHasDistributedOrdering(ch).


// ============================================================================
// CROSS-LAYER PREDICATES: Layer 2 ↔ Layer 3
// (Node Topology ↔ Infrastructure)
// ============================================================================

// CL.5: Orderers for the same channel on the same host = single point of failure
error colocatedOrderers(Channel ch, OrderingNode n1, OrderingNode n2) <->
    n1 != n2,
    orders(n1, ch),
    orders(n2, ch),
    deployedOn(n1, h),
    deployedOn(n2, h).

// CL.6: Channel participants must be able to communicate
// If two orgs are on the same channel but have no network path, the channel
// is unrealizable — it exists on paper but not in physical reality.
pred orgsCanCommunicateOnChannel(Organization o1, Organization o2, Channel ch) <->
    hosts(o1, h1),
    deployedOn(n1, h1),
    nodeParticipatesInChannel(n1, ch),
    hosts(o2, h2),
    deployedOn(n2, h2),
    nodeParticipatesInChannel(n2, ch),
    hostsCanCommunicate(h1, h2).

error unreachableChannelParticipants(Channel ch, Organization o1, Organization o2) <->
    o1 != o2,
    orgParticipatesInChannel(o1, ch),
    orgParticipatesInChannel(o2, ch),
    !orgsCanCommunicateOnChannel(o1, o2, ch).


// ============================================================================
// CROSS-LAYER PREDICATES: Layer 0 ↔ Layer 3
// (Consortium Structure ↔ Infrastructure — spanning all layers)
// ============================================================================

// CL.7: Illusory distribution — all channel peers hosted by single org
// The trust requirement (multiple orgs) is formally met, but one org
// physically hosts everyone's infrastructure, undermining trust separation.
pred channelNodeHostedByOrg(Channel ch, Organization hostOrg) <->
    nodeParticipatesInChannel(n, ch),
    deployedOn(n, h),
    hosts(hostOrg, h).

pred channelHasDistributedHosting(Channel ch) <->
    channelNodeHostedByOrg(ch, h1),
    channelNodeHostedByOrg(ch, h2),
    h1 != h2.

error illusoryDistribution(CollaborationIntent ci) <->
    realizedBy(ci, ch),
    participants(ci, o1),
    participants(ci, o2),
    o1 != o2,
    !channelHasDistributedHosting(ch).

// CL.8: Network single point of failure — all cross-org communication
// through one network owned by single org
pred networkOwnedBy(CommunicationNetwork net, Organization o) <->
    ownsNetworks(o, net).

pred channelDependsOnNetwork(Channel ch, CommunicationNetwork net) <->
    nodeParticipatesInChannel(n, ch),
    deployedOn(n, h),
    connectedTo(h, net).

// Warning-level: all channel traffic through single-org network
pred channelNetworkMonopoly(Channel ch, Organization o) <->
    channelDependsOnNetwork(ch, net),
    networkOwnedBy(net, o),
    // All participating hosts connect through this network
    !channelHasAlternativeNetwork(ch, o).

pred channelHasAlternativeNetwork(Channel ch, Organization monopolyOrg) <->
    channelDependsOnNetwork(ch, net),
    !networkOwnedBy(net, monopolyOrg).



// The consortium
Consortium(SupplyChainConsortium).

// Organizations (by business role)
Organization(Manufacturer).
Organization(Distributor).
Organization(Retailer).
Organization(Courier).
Organization(Regulator).

members(SupplyChainConsortium, Manufacturer).
members(SupplyChainConsortium, Distributor).
members(SupplyChainConsortium, Retailer).
members(SupplyChainConsortium, Courier).
members(SupplyChainConsortium, Regulator).

// Collaboration Intents
CollaborationIntent(ReferenceDataSharing).
CollaborationIntent(InventoryTracking).
CollaborationIntent(OrderProcessing).
CollaborationIntent(CustomerFulfillment).

intents(SupplyChainConsortium, ReferenceDataSharing).
intents(SupplyChainConsortium, InventoryTracking).
intents(SupplyChainConsortium, OrderProcessing).
intents(SupplyChainConsortium, CustomerFulfillment).

// ReferenceDataSharing: All 5 organizations
participants(ReferenceDataSharing, Manufacturer).
participants(ReferenceDataSharing, Distributor).
participants(ReferenceDataSharing, Retailer).
participants(ReferenceDataSharing, Courier).
participants(ReferenceDataSharing, Regulator).

// InventoryTracking: Manufacturer, Distributor, Retailer, Regulator (not Courier)
participants(InventoryTracking, Manufacturer).
participants(InventoryTracking, Distributor).
participants(InventoryTracking, Retailer).
participants(InventoryTracking, Regulator).

// OrderProcessing: Manufacturer, Distributor, Retailer (not Courier, Regulator)
participants(OrderProcessing, Manufacturer).
participants(OrderProcessing, Distributor).
participants(OrderProcessing, Retailer).

// CustomerFulfillment: Retailer, Courier only
participants(CustomerFulfillment, Retailer).
participants(CustomerFulfillment, Courier).


// ============================================================================
// LAYER 1: NETWORK ARCHITECTURE
// ============================================================================

// Channels
Channel(ChCommon).
Channel(ChInventory).
Channel(ChNewOrders).
Channel(ChCustomer).

channels(SupplyChainConsortium, ChCommon).
channels(SupplyChainConsortium, ChInventory).
channels(SupplyChainConsortium, ChNewOrders).
channels(SupplyChainConsortium, ChCustomer).

// Realization links (Intent → Channel)
realizedBy(ReferenceDataSharing, ChCommon).
realizedBy(InventoryTracking, ChInventory).
realizedBy(OrderProcessing, ChNewOrders).
realizedBy(CustomerFulfillment, ChCustomer).

// Policies
AllPolicy(PolicyAll).
MajorityPolicy(PolicyMajority).

// Chaincodes on ChCommon (reference data)
ChaincodeInstance(CC_Warehouse).
ChaincodeInstance(CC_District).
chaincodes(ChCommon, CC_Warehouse).
chaincodes(ChCommon, CC_District).
policy(CC_Warehouse, PolicyAll).
policy(CC_District, PolicyAll).

// Chaincodes on ChInventory (inventory tracking)
ChaincodeInstance(CC_Item).
ChaincodeInstance(CC_Stock).
ChaincodeInstance(CC_Order).
ChaincodeInstance(CC_OrderLine).
chaincodes(ChInventory, CC_Item).
chaincodes(ChInventory, CC_Stock).
chaincodes(ChInventory, CC_Order).
chaincodes(ChInventory, CC_OrderLine).
policy(CC_Item, PolicyMajority).
policy(CC_Stock, PolicyMajority).
policy(CC_Order, PolicyMajority).
policy(CC_OrderLine, PolicyMajority).

// Chaincodes on ChNewOrders (order processing)
ChaincodeInstance(CC_NewOrder).
chaincodes(ChNewOrders, CC_NewOrder).
policy(CC_NewOrder, PolicyMajority).

// Chaincodes on ChCustomer (customer fulfillment)
ChaincodeInstance(CC_Customer).
ChaincodeInstance(CC_Payment).
chaincodes(ChCustomer, CC_Customer).
chaincodes(ChCustomer, CC_Payment).
policy(CC_Customer, PolicyAll).
policy(CC_Payment, PolicyAll).


// ============================================================================
// LAYER 3: INFRASTRUCTURE (defined before Layer 2 for deployment references)
// ============================================================================

// Communication network (single shared network for simplicity)
CommunicationNetwork(ConsortiumNetwork).
networks(SupplyChainConsortium, ConsortiumNetwork).

// Hosts (one per organization)
Host(HostMfr).
Host(HostDist).
Host(HostRet).
Host(HostCour).
Host(HostReg).

hosts(Manufacturer, HostMfr).
hosts(Distributor, HostDist).
hosts(Retailer, HostRet).
hosts(Courier, HostCour).
hosts(Regulator, HostReg).

// All hosts connected to the shared network
connectedTo(HostMfr, ConsortiumNetwork).
connectedTo(HostDist, ConsortiumNetwork).
connectedTo(HostRet, ConsortiumNetwork).
connectedTo(HostCour, ConsortiumNetwork).
connectedTo(HostReg, ConsortiumNetwork).


// ============================================================================
// LAYER 2: NODE TOPOLOGY
// ============================================================================

// --- Ordering Nodes ---
// One orderer per organization

OrderingNode(OrdererMfr).
OrderingNode(OrdererDist).
OrderingNode(OrdererRet).
OrderingNode(OrdererCour).
OrderingNode(OrdererReg).

// Deployment (Node → Host)
deployedOn(OrdererMfr, HostMfr).
deployedOn(OrdererDist, HostDist).
deployedOn(OrdererRet, HostRet).
deployedOn(OrdererCour, HostCour).
deployedOn(OrdererReg, HostReg).

// Orderer → Channel assignments (orderers serve channels their org participates in)

// ChCommon: all 5 orderers
orders(OrdererMfr, ChCommon).
orders(OrdererDist, ChCommon).
orders(OrdererRet, ChCommon).
orders(OrdererCour, ChCommon).
orders(OrdererReg, ChCommon).

// ChInventory: Mfr, Dist, Ret, Reg (not Courier)
orders(OrdererMfr, ChInventory).
orders(OrdererDist, ChInventory).
orders(OrdererRet, ChInventory).
orders(OrdererReg, ChInventory).

// ChNewOrders: Mfr, Dist, Ret (not Courier, Reg)
orders(OrdererMfr, ChNewOrders).
orders(OrdererDist, ChNewOrders).
orders(OrdererRet, ChNewOrders).

// ChCustomer: Ret, Cour only
orders(OrdererRet, ChCustomer).
orders(OrdererCour, ChCustomer).


// --- Endorsing Nodes ---
// One endorser per organization

EndorsingNode(EndorserMfr).
EndorsingNode(EndorserDist).
EndorsingNode(EndorserRet).
EndorsingNode(EndorserCour).
EndorsingNode(EndorserReg).

// Deployment (Node → Host)
deployedOn(EndorserMfr, HostMfr).
deployedOn(EndorserDist, HostDist).
deployedOn(EndorserRet, HostRet).
deployedOn(EndorserCour, HostCour).
deployedOn(EndorserReg, HostReg).

// Endorser → Chaincode assignments
// Each endorser endorses chaincodes on channels their org participates in

// Manufacturer endorses: ChCommon, ChInventory, ChNewOrders chaincodes
endorses(EndorserMfr, CC_Warehouse).
endorses(EndorserMfr, CC_District).
endorses(EndorserMfr, CC_Item).
endorses(EndorserMfr, CC_Stock).
endorses(EndorserMfr, CC_Order).
endorses(EndorserMfr, CC_OrderLine).
endorses(EndorserMfr, CC_NewOrder).

// Distributor endorses: ChCommon, ChInventory, ChNewOrders chaincodes
endorses(EndorserDist, CC_Warehouse).
endorses(EndorserDist, CC_District).
endorses(EndorserDist, CC_Item).
endorses(EndorserDist, CC_Stock).
endorses(EndorserDist, CC_Order).
endorses(EndorserDist, CC_OrderLine).
endorses(EndorserDist, CC_NewOrder).

// Retailer endorses: ChCommon, ChInventory, ChNewOrders, ChCustomer chaincodes
endorses(EndorserRet, CC_Warehouse).
endorses(EndorserRet, CC_District).
endorses(EndorserRet, CC_Item).
endorses(EndorserRet, CC_Stock).
endorses(EndorserRet, CC_Order).
endorses(EndorserRet, CC_OrderLine).
endorses(EndorserRet, CC_NewOrder).
endorses(EndorserRet, CC_Customer).
endorses(EndorserRet, CC_Payment).

// Courier endorses: ChCommon, ChCustomer chaincodes
endorses(EndorserCour, CC_Warehouse).
endorses(EndorserCour, CC_District).
endorses(EndorserCour, CC_Customer).
endorses(EndorserCour, CC_Payment).

// Regulator endorses: ChCommon, ChInventory chaincodes
endorses(EndorserReg, CC_Warehouse).
endorses(EndorserReg, CC_District).
endorses(EndorserReg, CC_Item).
endorses(EndorserReg, CC_Stock).
endorses(EndorserReg, CC_Order).
endorses(EndorserReg, CC_OrderLine).

!exists(Consortium::new).
!exists(Organization::new).
!exists(CollaborationIntent::new).
!exists(Channel::new).
!exists(ChaincodeInstance::new).
!exists(AnyPolicy::new).
!exists(MajorityPolicy::new).
!exists(AllPolicy::new).
!exists(OrderingNode::new).
!exists(EndorsingNode::new).
!exists(Host::new).
!exists(CommunicationNetwork::new).
!exists(NetworkInterconnection::new).
default !ownsNetworks(*, *).
default !participants(*, *).
default !realizedBy(*, *).
default !policy(*, *).
default !endorses(*, *).
default !deployedOn(*, *).
default !orders(*, *).
default !connectedTo(*, *).
default !links(*, *).