From c0f22e210a5d0f10df1db4d0712efd37854a1726 Mon Sep 17 00:00:00 2001
From: Nuvin Godakanda Arachchi <nu.vv.in@gmail.com>
Date: Mon, 23 Jan 2023 20:08:48 +0530
Subject: [PATCH] feat: lts file added

---
 Printer.lts | 58 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100644 Printer.lts

diff --git a/Printer.lts b/Printer.lts
new file mode 100644
index 0000000..09a066d
--- /dev/null
+++ b/Printer.lts
@@ -0,0 +1,58 @@
+/*
+	Printer.lts
+	This file includes three types of FSP processes to model the following: 
+	Printer, Student & Technician, and a parallel composite process to model the complete printer system
+
+	Author: Nuwin Godakanda Arachchi
+	W-Id: W1761350
+	IIT-Id: 2019443
+*/
+
+const MINIMUM_PAPER_LEVEL = 0
+const MAXIMUM_PAPER_LEVEL = 3
+const MINIMUM_DOCUMENTS = 1
+range PAPER_TRAY_LIMIT = 0..3
+
+// the system processes
+set PrinterUsers = { technician, student3Docs, student2Docs }
+
+// prohibited actions that shall not be performed or shared with each other
+set StudentProhibitedActions = { acquireLockForRefill, refillBlocked, performRefill }
+set TechnicianProhibitedActions = { acquireLockForPrint }
+
+// printer process
+PRINTER = PRINT_OPERATION[MAXIMUM_PAPER_LEVEL],
+PRINT_OPERATION[paperCount : PAPER_TRAY_LIMIT] = 
+	if (paperCount > MINIMUM_PAPER_LEVEL)
+	then ( // paper is adequet => student can print + refill blocked
+		acquireLockForPrint -> releaseLock -> PRINT_OPERATION[paperCount - 1] | 
+		acquireLockForRefill -> refillBlocked -> releaseLock -> PRINT_OPERATION[paperCount]
+	) else ( // out of paper => no printing allowed + refill performed
+		acquireLockForRefill -> performRefill -> releaseLock -> PRINT_OPERATION[MAXIMUM_PAPER_LEVEL]
+	).
+
+// student process
+STUDENT(DOCUMENTS = MINIMUM_DOCUMENTS) = USE_PRINTER[MINIMUM_DOCUMENTS],
+USE_PRINTER[documentsCount : MINIMUM_DOCUMENTS..DOCUMENTS] = (
+	acquireLockForPrint -> printDocument[documentsCount] -> releaseLock ->
+		if ((documentsCount + 1) <= DOCUMENTS) 
+		then // student has more documents for print => recalls the printer with next document count
+			USE_PRINTER[documentsCount + 1]
+		else // all documents are printer => process terminates
+			(terminate -> END)
+) + StudentProhibitedActions. // technician actions blocked for the student
+
+// technician process
+TECHNICIAN = (
+	acquireLockForRefill -> { performRefill, refillBlocked } -> releaseLock -> TECHNICIAN | terminate -> END
+) + TechnicianProhibitedActions. // student actions blocked for the technician
+
+// printing system paralell processing system
+||PRINTING_SYSTEM = ( 
+	student3Docs: STUDENT(3) || 
+	student2Docs: STUDENT(2) || 
+	technician: TECHNICIAN || 
+	PrinterUsers :: PRINTER 
+) / { terminate / PrinterUsers.terminate }.  // synchronizes the termination with all the printer users
+
+/* END */
\ No newline at end of file