fixed some layouting issues, still no automatic solver

2024-05-01 22:46:40 +03:00
parent f7d0031d09
commit 6ea69541b7
5 changed files with 479 additions and 120 deletions
--- a/src/main/resources/TestProgram.txt
+++ b/src/main/resources/TestProgram.txt
@@ -1,57 +1,128 @@
-~A package defines a full set of specifications for a general set of features~
-package Database {
+package HospitalManagementSystem {

-    ~An interface holds an abstract structure to be implemented in a specification~
-    critical interface Database {
+    critical interface PatientRecords {
+        critical public FetchPatientDetails(FLOAT patientId) {
+            @ExecTime : "3s";
+            @MaxReturnVals : "1";
+            @DataFormat : "ID: %patientId,DOB: %dob";
+            @DataPrivacy : "High";
+            return "PatientDetails" details;
+        }

-        // lol
-        critical public GetUserList(FLOAT[] x, STRING ag) {
-            @ExecTime : "10s";
-            @MaxReturnVals : "10s";
-            return "CustomDataType" x;
+        critical public UpdatePatientRecord(FLOAT patientId, STRING updates) {
+            @ExecTime : "3s";
+            @DataIntegrity : "High";
+            @DataConcurrency : "Serializable";
+            return "UpdateConfirmation" confirmation;
        }
    }

-    ~A specification is a concrete implementation of requirement specifications~
-    ~It might or might not implement an interface~
-    specification DatabaseAccess implements Database {
+    critical interface AppointmentSystem {
+        critical public ScheduleAppointment(FLOAT patientId, STRING dateTime, STRING doctorId) {
+            @ExecTime : "4s";
+            @Notification : "Email";
+            @DataValidation : "TimeSlotAvailability";
+            return "AppointmentConfirmation" confirmation;
+        }

-        ~This is a concrete non-functional specification~
-        critical DatabaseAccessMember {
+        optional public CancelAppointment(FLOAT appointmentId) {
+            @ExecTime : "2s";
+            @CancellationFee : "NoChargeWithin24h";
+            return "CancellationConfirmation" status;
+        }
+    }
+
+    critical interface StaffManagement {
+        critical public FetchStaffDetails(FLOAT staffId) {
+            @ExecTime : "4s";
+            @MaxReturnVals : "1";
+            @DataFormat : "Staff ID: %staffId, Role: %role";
+            @AccessLevel : "HR_Only";
+            return "StaffDetails" detailList;
+        }
+
+        critical public UpdateStaffRecord(FLOAT staffId, STRING updates) {
+            @ExecTime : "4s";
+            @TransactionType : "Atomic";
+            @DataIntegrity : "EnsureConsistency";
+            return "UpdateConfirmation" status;
+        }
+
+        optional public AssignStaff(FLOAT staffId, STRING departmentId) {
+            @ExecTime : "3s";
+            @AuditTrail : "Enabled";
+            @DataLogging : "Detailed";
+            return "AssignmentConfirmation" confirmation;
+        }
+    }
+
+    specification ComprehensiveMedicalRecords implements PatientRecords {
+
+        critical ComprehensiveRecordsMember {
            optional @UserHasAdminAccess;
-            critical @UserIsNotBanned;
+            critical @UserIsNotInactive;

-            result optional DatabaseAdminPanel;
-            result critical DatabaseVisualizerPanel;
+            result optional AdminPanel;
+            result critical MedicalRecordsDashboard;
            result Clock;
        }

-        ~This is a concrete functional specification, it might implement an interface~
-        critical public GetUserList(FLOAT[] x, STRING ag) implements DatabaseAccessImpl {
-            @ExecTime : "10s";
-            @MaxReturnVals : "10s";
-            return INT x;
+        critical public FetchPatientDetails(FLOAT patientId) implements PatientRecords {
+            @ExecTime : "3s";
+            @DataCache : "Enabled";
+            @CacheExpiry : "24h";
+            return "PatientDetails" patientDetails;
        }

-        critical private GetUserdList(FLOAT[] x, STRING ag) implements Database {
-                    @ExecTime : "10s";
-                    @MaxReturnVals : "10s";
-                    return INT x;
+        critical public UpdatePatientRecord(FLOAT patientId, STRING updates) implements PatientRecords {
+            @ExecTime : "3s";
+            @RecordLocking : "Optimistic";
+            return "UpdateConfirmation" status;
        }

-        critical public GetUserdfList(FLOAT[] x, STRING ag) implements Database {
-                    @ExecTime : "10s";
-                    @MaxReturnVals : "10s";
-                    return INT x;
+        critical public ScheduleAppointment(FLOAT patientId, STRING dateTime, STRING doctorId) implements AppointmentSystem {
+            @ExecTime : "4s";
+            @OverbookingPolicy : "Disallow";
+            return "AppointmentConfirmation" schedule;
        }

-        optional public GetUsesfrList(FLOAT[] x, STRING ag) implements Database {
-                    @ExecTime : "10s";
-                    @MaxReturnVals : "10s";
-                    return INT x;
+        optional public CancelAppointment(FLOAT appointmentId) implements AppointmentSystem {
+            @ExecTime : "2s";
+            @RefundPolicy : "FullIf48hPrior";
+            return "CancellationConfirmation" status;
+        }
    }

+    specification StaffAdministration implements StaffManagement {
+
+        critical StaffAdminMember {
+            optional @UserHasHRAccess;
+            critical @UserIsVerified;
+
+            result optional HRPanel;
+            result critical StaffManagementDashboard;
+            result Clock;
+        }
+
+        critical public FetchStaffDetails(FLOAT staffId) implements StaffManagement {
+            @ExecTime : "4s";
+            @DataAccess : "SecureQuery";
+            @FilterSensitiveData : "Enabled";
+            return "StaffDetails" staffDetails;
+        }
+
+        critical public UpdateStaffRecord(FLOAT staffId, STRING updates) implements StaffManagement {
+            @ExecTime : "4s";
+            @ChangeManagement : "Controlled";
+            @DataHistory : "Logged";
+            return "UpdateConfirmation" status;
+        }
+
+        optional public AssignStaff(FLOAT staffId, STRING departmentId) implements StaffManagement {
+            @ExecTime : "3s";
+            @PermissionCheck : "DepartmentHeadApproval";
+            @RealTimeUpdate : "Required";
+            return "AssignmentConfirmation" status;
+        }
    }
 }
-
-
--- a/winx-serve/package-lock.json
+++ b/winx-serve/package-lock.json
@@ -11,6 +11,8 @@
        "@testing-library/jest-dom": "^5.17.0",
        "@testing-library/react": "^13.4.0",
        "@testing-library/user-event": "^13.5.0",
+        "dagre": "^0.8.5",
+        "elkjs": "^0.9.3",
        "react": "^18.3.1",
        "react-dom": "^18.3.1",
        "react-flow-renderer": "^10.3.17",
@@ -7185,6 +7187,15 @@
        "node": ">=12"
      }
    },
+    "node_modules/dagre": {
+      "version": "0.8.5",
+      "resolved": "https://registry.npmjs.org/dagre/-/dagre-0.8.5.tgz",
+      "integrity": "sha512-/aTqmnRta7x7MCCpExk7HQL2O4owCT2h8NT//9I1OQ9vt29Pa0BzSAkR5lwFUcQ7491yVi/3CXU9jQ5o0Mn2Sw==",
+      "dependencies": {
+        "graphlib": "^2.1.8",
+        "lodash": "^4.17.15"
+      }
+    },
    "node_modules/damerau-levenshtein": {
      "version": "1.0.8",
      "resolved": "https://registry.npmjs.org/damerau-levenshtein/-/damerau-levenshtein-1.0.8.tgz",
@@ -7638,6 +7649,11 @@
      "resolved": "https://registry.npmjs.org/electron-to-chromium/-/electron-to-chromium-1.4.751.tgz",
      "integrity": "sha512-2DEPi++qa89SMGRhufWTiLmzqyuGmNF3SK4+PQetW1JKiZdEpF4XQonJXJCzyuYSA6mauiMhbyVhqYAP45Hvfw=="
    },
+    "node_modules/elkjs": {
+      "version": "0.9.3",
+      "resolved": "https://registry.npmjs.org/elkjs/-/elkjs-0.9.3.tgz",
+      "integrity": "sha512-f/ZeWvW/BCXbhGEf1Ujp29EASo/lk1FDnETgNKwJrsVvGZhUWCZyg3xLJjAsxfOmt8KjswHmI5EwCQcPMpOYhQ=="
+    },
    "node_modules/emittery": {
      "version": "0.8.1",
      "resolved": "https://registry.npmjs.org/emittery/-/emittery-0.8.1.tgz",
@@ -9518,6 +9534,14 @@
      "resolved": "https://registry.npmjs.org/graphemer/-/graphemer-1.4.0.tgz",
      "integrity": "sha512-EtKwoO6kxCL9WO5xipiHTZlSzBm7WLT627TqC/uVRd0HKmq8NXyebnNYxDoBi7wt8eTWrUrKXCOVaFq9x1kgag=="
    },
+    "node_modules/graphlib": {
+      "version": "2.1.8",
+      "resolved": "https://registry.npmjs.org/graphlib/-/graphlib-2.1.8.tgz",
+      "integrity": "sha512-jcLLfkpoVGmH7/InMC/1hIvOPSUh38oJtGhvrOFGzioE1DZ+0YW16RgmOJhHiuWTvGiJQ9Z1Ik43JvkRPRvE+A==",
+      "dependencies": {
+        "lodash": "^4.17.15"
+      }
+    },
    "node_modules/gzip-size": {
      "version": "6.0.0",
      "resolved": "https://registry.npmjs.org/gzip-size/-/gzip-size-6.0.0.tgz",
--- a/winx-serve/package.json
+++ b/winx-serve/package.json
@@ -6,6 +6,8 @@
    "@testing-library/jest-dom": "^5.17.0",
    "@testing-library/react": "^13.4.0",
    "@testing-library/user-event": "^13.5.0",
+    "dagre": "^0.8.5",
+    "elkjs": "^0.9.3",
    "react": "^18.3.1",
    "react-dom": "^18.3.1",
    "react-flow-renderer": "^10.3.17",
--- a/winx-serve/src/CustomNodeComponent.js
+++ b/winx-serve/src/CustomNodeComponent.js
@@ -21,7 +21,7 @@ const CustomNodeComponent = ({data}) => {
            )}


-            <div className="flex flex-col innerBody rounded-bl-lg rounded-tr-lg divide-y sans-font"
+            <div className="flex flex-col innerBody rounded-b-lg rounded-tr-lg divide-y sans-font"
                 style={{
                     backgroundColor: data.importance === 'critical' ? '#F59975' : '#01C6C9',
                 }}>
@@ -89,17 +89,31 @@ const CustomNodeComponent = ({data}) => {
                        {data.specificationEntries && (<div>
                                <strong>Specifications:</strong>
                                {data.specificationEntries.map((entry, idx) => (
-                                    <div key={idx}>{entry.key}: {entry.value}</div>))}
+                                    <div key={idx}>{entry.key}: {entry.value.substring(1, entry.value.length - 1)}</div>))}
                            </div>)}
                    </div>


                    <Handle type="source" position="bottom" style={{borderRadius: 0}}/>
                </div>
+                {data.returnTypes && (<div className="flex flex-col m-0 justify-between">
+                        <div className="bg-amber-400 p-1 rounded-b">
+                            <div className="flex">
+                                <img className="content-center mr-1" alt="outputCog" src="/output.png"
+                                     style={{width: 20 + 'px', height: 20 + 'px'}}/>
+                                <strong className="content-center">Output: </strong>
                            </div>

-
-            {data.returnTypes && (<div className="flex flex-col m-0 justify-between">
+                            {data.returnTypes.map((ret, idx) => (
+                                <div className="text-gray-700 m-1" key={idx}>
+                                    {(ret.type.length > 1 && ret.type[0] === '"' && ret.type[ret.type.length - 1] === '"')
+                                    ? ret.type.substring(1, ret.type.length - 1) + " "
+                                    : ret.type + " "}
+                                    {ret.identifier}</div>))}
+                        </div>
+                    </div>
+                )}
+            </div>
            <div>
                <div className="outerBody">
                            <span className="fade-in-out font-mono text-7xl text-red-700">
@@ -108,20 +122,6 @@ const CustomNodeComponent = ({data}) => {
                </div>
            </div>

-                    <div className="bg-amber-400 p-1 rounded-r">
-                        <div className="flex">
-                            <img className="content-center mr-1" alt="outputCog" src="/output.png"
-                                 style={{width: 20 + 'px', height: 20 + 'px'}}/>
-                            <strong className="content-center">Output: </strong>
-                        </div>
-
-                        {data.returnTypes.map((ret, idx) => (
-                            <div className="text-gray-700 m-1" key={idx}>{ret.type} {ret.identifier}</div>))}
-                    </div>
-                </div>
-            )}
-
-
        </div>);
 };

--- a/winx-serve/src/Data.js
+++ b/winx-serve/src/Data.js
@@ -1,148 +1,410 @@
 export const jsonData = [ {
-  "name" : "Database",
+  "name" : "HospitalManagementSystem",
  "interfaces" : [ {
-    "name" : "Database",
+    "name" : "PatientRecords",
    "functions" : [ {
-      "name" : "GetUserList",
+      "name" : "FetchPatientDetails",
      "access_modifier" : "public",
      "implemented_interface" : "none",
      "importance" : "critical",
      "inputTypes" : [ {
        "type" : "FLOAT",
-        "identifier" : "x"
-      }, {
-        "type" : "STRING",
-        "identifier" : "ag"
+        "identifier" : "patientId"
      } ],
      "returnTypes" : [ {
-        "type" : "\"CustomDataType\"",
-        "identifier" : "x"
+        "type" : "\"PatientDetails\"",
+        "identifier" : "details"
      } ],
      "specificationEntries" : [ {
        "key" : "ExecTime",
-        "value" : "\"10s\""
+        "value" : "\"3s\""
      }, {
        "key" : "MaxReturnVals",
-        "value" : "\"10s\""
+        "value" : "\"1\""
+      }, {
+        "key" : "DataFormat",
+        "value" : "\"ID: %patientId, DOB: %dob\""
+      }, {
+        "key" : "DataPrivacy",
+        "value" : "\"High\""
+      } ]
+    }, {
+      "name" : "UpdatePatientRecord",
+      "access_modifier" : "public",
+      "implemented_interface" : "none",
+      "importance" : "critical",
+      "inputTypes" : [ {
+        "type" : "FLOAT",
+        "identifier" : "patientId"
+      }, {
+        "type" : "STRING",
+        "identifier" : "updates"
+      } ],
+      "returnTypes" : [ {
+        "type" : "\"UpdateConfirmation\"",
+        "identifier" : "confirmation"
+      } ],
+      "specificationEntries" : [ {
+        "key" : "ExecTime",
+        "value" : "\"3s\""
+      }, {
+        "key" : "DataIntegrity",
+        "value" : "\"High\""
+      }, {
+        "key" : "DataConcurrency",
+        "value" : "\"Serializable\""
+      } ]
+    } ]
+  }, {
+    "name" : "AppointmentSystem",
+    "functions" : [ {
+      "name" : "ScheduleAppointment",
+      "access_modifier" : "public",
+      "implemented_interface" : "none",
+      "importance" : "critical",
+      "inputTypes" : [ {
+        "type" : "FLOAT",
+        "identifier" : "patientId"
+      }, {
+        "type" : "STRING",
+        "identifier" : "dateTime"
+      }, {
+        "type" : "STRING",
+        "identifier" : "doctorId"
+      } ],
+      "returnTypes" : [ {
+        "type" : "\"AppointmentConfirmation\"",
+        "identifier" : "confirmation"
+      } ],
+      "specificationEntries" : [ {
+        "key" : "ExecTime",
+        "value" : "\"4s\""
+      }, {
+        "key" : "Notification",
+        "value" : "\"Email\""
+      }, {
+        "key" : "DataValidation",
+        "value" : "\"TimeSlotAvailability\""
+      } ]
+    }, {
+      "name" : "CancelAppointment",
+      "access_modifier" : "public",
+      "implemented_interface" : "none",
+      "importance" : "optional",
+      "inputTypes" : [ {
+        "type" : "FLOAT",
+        "identifier" : "appointmentId"
+      } ],
+      "returnTypes" : [ {
+        "type" : "\"CancellationConfirmation\"",
+        "identifier" : "status"
+      } ],
+      "specificationEntries" : [ {
+        "key" : "ExecTime",
+        "value" : "\"2s\""
+      }, {
+        "key" : "CancellationFee",
+        "value" : "\"NoChargeWithin24h\""
+      } ]
+    } ]
+  }, {
+    "name" : "StaffManagement",
+    "functions" : [ {
+      "name" : "FetchStaffDetails",
+      "access_modifier" : "public",
+      "implemented_interface" : "none",
+      "importance" : "critical",
+      "inputTypes" : [ {
+        "type" : "FLOAT",
+        "identifier" : "staffId"
+      } ],
+      "returnTypes" : [ {
+        "type" : "\"StaffDetails\"",
+        "identifier" : "detailList"
+      } ],
+      "specificationEntries" : [ {
+        "key" : "ExecTime",
+        "value" : "\"4s\""
+      }, {
+        "key" : "MaxReturnVals",
+        "value" : "\"1\""
+      }, {
+        "key" : "DataFormat",
+        "value" : "\"Staff ID: %staffId, Role: %role\""
+      }, {
+        "key" : "AccessLevel",
+        "value" : "\"HR_Only\""
+      } ]
+    }, {
+      "name" : "UpdateStaffRecord",
+      "access_modifier" : "public",
+      "implemented_interface" : "none",
+      "importance" : "critical",
+      "inputTypes" : [ {
+        "type" : "FLOAT",
+        "identifier" : "staffId"
+      }, {
+        "type" : "STRING",
+        "identifier" : "updates"
+      } ],
+      "returnTypes" : [ {
+        "type" : "\"UpdateConfirmation\"",
+        "identifier" : "status"
+      } ],
+      "specificationEntries" : [ {
+        "key" : "ExecTime",
+        "value" : "\"4s\""
+      }, {
+        "key" : "TransactionType",
+        "value" : "\"Atomic\""
+      }, {
+        "key" : "DataIntegrity",
+        "value" : "\"EnsureConsistency\""
+      } ]
+    }, {
+      "name" : "AssignStaff",
+      "access_modifier" : "public",
+      "implemented_interface" : "none",
+      "importance" : "optional",
+      "inputTypes" : [ {
+        "type" : "FLOAT",
+        "identifier" : "staffId"
+      }, {
+        "type" : "STRING",
+        "identifier" : "departmentId"
+      } ],
+      "returnTypes" : [ {
+        "type" : "\"AssignmentConfirmation\"",
+        "identifier" : "confirmation"
+      } ],
+      "specificationEntries" : [ {
+        "key" : "ExecTime",
+        "value" : "\"3s\""
+      }, {
+        "key" : "AuditTrail",
+        "value" : "\"Enabled\""
+      }, {
+        "key" : "DataLogging",
+        "value" : "\"Detailed\""
      } ]
    } ]
  } ],
  "specifications" : [ {
-    "name" : "DatabaseAccess",
-    "implemented_interface" : "Database",
+    "name" : "ComprehensiveMedicalRecords",
+    "implemented_interface" : "PatientRecords",
    "requirements" : [ {
-      "name" : "DatabaseAccessMember",
+      "name" : "ComprehensiveRecordsMember",
      "annotations" : [ {
        "importance" : "optional",
        "name" : "UserHasAdminAccess"
      }, {
        "importance" : "critical",
-        "name" : "UserIsNotBanned"
+        "name" : "UserIsNotInactive"
      } ]
    } ],
    "results" : [ {
-      "name" : "DatabaseAdminPanel",
+      "name" : "AdminPanel",
      "importance" : "optional"
    }, {
-      "name" : "DatabaseVisualizerPanel",
+      "name" : "MedicalRecordsDashboard",
      "importance" : "critical"
    }, {
      "name" : "Clock",
      "importance" : "none"
    } ],
    "functions" : [ {
-      "name" : "GetUserList",
+      "name" : "FetchPatientDetails",
      "access_modifier" : "public",
-      "implemented_interface" : "DatabaseAccessImpl",
+      "implemented_interface" : "PatientRecords",
      "importance" : "critical",
      "inputTypes" : [ {
        "type" : "FLOAT",
-        "identifier" : "x"
-      }, {
-        "type" : "STRING",
-        "identifier" : "ag"
+        "identifier" : "patientId"
      } ],
      "returnTypes" : [ {
-        "type" : "INT",
-        "identifier" : "x"
+        "type" : "\"PatientDetails\"",
+        "identifier" : "patientDetails"
      } ],
      "specificationEntries" : [ {
        "key" : "ExecTime",
-        "value" : "\"10s\""
+        "value" : "\"3s\""
      }, {
-        "key" : "MaxReturnVals",
-        "value" : "\"10s\""
+        "key" : "DataCache",
+        "value" : "\"Enabled\""
+      }, {
+        "key" : "CacheExpiry",
+        "value" : "\"24h\""
      } ]
    }, {
-      "name" : "GetUserdList",
-      "access_modifier" : "private",
-      "implemented_interface" : "Database",
+      "name" : "UpdatePatientRecord",
+      "access_modifier" : "public",
+      "implemented_interface" : "PatientRecords",
      "importance" : "critical",
      "inputTypes" : [ {
        "type" : "FLOAT",
-        "identifier" : "x"
+        "identifier" : "patientId"
      }, {
        "type" : "STRING",
-        "identifier" : "ag"
+        "identifier" : "updates"
      } ],
      "returnTypes" : [ {
-        "type" : "INT",
-        "identifier" : "x"
+        "type" : "\"UpdateConfirmation\"",
+        "identifier" : "status"
      } ],
      "specificationEntries" : [ {
        "key" : "ExecTime",
-        "value" : "\"10s\""
+        "value" : "\"3s\""
      }, {
-        "key" : "MaxReturnVals",
-        "value" : "\"10s\""
+        "key" : "RecordLocking",
+        "value" : "\"Optimistic\""
      } ]
    }, {
-      "name" : "GetUserdfList",
+      "name" : "ScheduleAppointment",
      "access_modifier" : "public",
-      "implemented_interface" : "Database",
+      "implemented_interface" : "AppointmentSystem",
      "importance" : "critical",
      "inputTypes" : [ {
        "type" : "FLOAT",
-        "identifier" : "x"
+        "identifier" : "patientId"
      }, {
        "type" : "STRING",
-        "identifier" : "ag"
+        "identifier" : "dateTime"
+      }, {
+        "type" : "STRING",
+        "identifier" : "doctorId"
      } ],
      "returnTypes" : [ {
-        "type" : "INT",
-        "identifier" : "x"
+        "type" : "\"AppointmentConfirmation\"",
+        "identifier" : "schedule"
      } ],
      "specificationEntries" : [ {
        "key" : "ExecTime",
-        "value" : "\"10s\""
+        "value" : "\"4s\""
      }, {
-        "key" : "MaxReturnVals",
-        "value" : "\"10s\""
+        "key" : "OverbookingPolicy",
+        "value" : "\"Disallow\""
      } ]
    }, {
-      "name" : "GetUsesfrList",
+      "name" : "CancelAppointment",
      "access_modifier" : "public",
-      "implemented_interface" : "Database",
+      "implemented_interface" : "AppointmentSystem",
      "importance" : "optional",
      "inputTypes" : [ {
        "type" : "FLOAT",
-        "identifier" : "x"
-      }, {
-        "type" : "STRING",
-        "identifier" : "ag"
+        "identifier" : "appointmentId"
      } ],
      "returnTypes" : [ {
-        "type" : "INT",
-        "identifier" : "x"
+        "type" : "\"CancellationConfirmation\"",
+        "identifier" : "status"
      } ],
      "specificationEntries" : [ {
        "key" : "ExecTime",
-        "value" : "\"10s\""
+        "value" : "\"2s\""
      }, {
-        "key" : "MaxReturnVals",
-        "value" : "\"10s\""
+        "key" : "RefundPolicy",
+        "value" : "\"FullIf48hPrior\""
      } ]
    } ],
-    "implementedInterface" : "Database"
+    "implementedInterface" : "PatientRecords"
+  }, {
+    "name" : "StaffAdministration",
+    "implemented_interface" : "StaffManagement",
+    "requirements" : [ {
+      "name" : "StaffAdminMember",
+      "annotations" : [ {
+        "importance" : "optional",
+        "name" : "UserHasHRAccess"
+      }, {
+        "importance" : "critical",
+        "name" : "UserIsVerified"
+      } ]
+    } ],
+    "results" : [ {
+      "name" : "HRPanel",
+      "importance" : "optional"
+    }, {
+      "name" : "StaffManagementDashboard",
+      "importance" : "critical"
+    }, {
+      "name" : "Clock",
+      "importance" : "none"
+    } ],
+    "functions" : [ {
+      "name" : "FetchStaffDetails",
+      "access_modifier" : "public",
+      "implemented_interface" : "StaffManagement",
+      "importance" : "critical",
+      "inputTypes" : [ {
+        "type" : "FLOAT",
+        "identifier" : "staffId"
+      } ],
+      "returnTypes" : [ {
+        "type" : "\"StaffDetails\"",
+        "identifier" : "staffDetails"
+      } ],
+      "specificationEntries" : [ {
+        "key" : "ExecTime",
+        "value" : "\"4s\""
+      }, {
+        "key" : "DataAccess",
+        "value" : "\"SecureQuery\""
+      }, {
+        "key" : "FilterSensitiveData",
+        "value" : "\"Enabled\""
+      } ]
+    }, {
+      "name" : "UpdateStaffRecord",
+      "access_modifier" : "public",
+      "implemented_interface" : "StaffManagement",
+      "importance" : "critical",
+      "inputTypes" : [ {
+        "type" : "FLOAT",
+        "identifier" : "staffId"
+      }, {
+        "type" : "STRING",
+        "identifier" : "updates"
+      } ],
+      "returnTypes" : [ {
+        "type" : "\"UpdateConfirmation\"",
+        "identifier" : "status"
+      } ],
+      "specificationEntries" : [ {
+        "key" : "ExecTime",
+        "value" : "\"4s\""
+      }, {
+        "key" : "ChangeManagement",
+        "value" : "\"Controlled\""
+      }, {
+        "key" : "DataHistory",
+        "value" : "\"Logged\""
+      } ]
+    }, {
+      "name" : "AssignStaff",
+      "access_modifier" : "public",
+      "implemented_interface" : "StaffManagement",
+      "importance" : "optional",
+      "inputTypes" : [ {
+        "type" : "FLOAT",
+        "identifier" : "staffId"
+      }, {
+        "type" : "STRING",
+        "identifier" : "departmentId"
+      } ],
+      "returnTypes" : [ {
+        "type" : "\"AssignmentConfirmation\"",
+        "identifier" : "status"
+      } ],
+      "specificationEntries" : [ {
+        "key" : "ExecTime",
+        "value" : "\"3s\""
+      }, {
+        "key" : "PermissionCheck",
+        "value" : "\"DepartmentHeadApproval\""
+      }, {
+        "key" : "RealTimeUpdate",
+        "value" : "\"Required\""
+      } ]
+    } ],
+    "implementedInterface" : "StaffManagement"
  } ]
 } ];