Dear AmirHossein,
Thank you for your consideration. This specification is related to a digital forensic case study:
The local area network at ACME Manufacturing consists of two personal computers and a networked printer. The cost of running the network is shared by its two users Alice (A) and Bob (B). Alice, however, claims that she never uses the printer and should not be paying for the printer consumables. Bob disagrees; he says that he saw Alice collecting printouts. The system administrator, Carl, has been assigned to investigate this dispute.
To get more information about how the printer works, Carl contacted the manufacturer. According to the manufacturer, the printer works as follows:
(1) When a print job is received from the user it is stored in the first unallocated directory entry of the print job directory.
(2) The printing mechanism scans the print job directory from the beginning and picks the first active job.
(3) After the job is printed, the corresponding directory entry is marked as ‘‘deleted’’, but the name of the job owner is preserved.
(4) The printer can accept only one print job from each user at a time.
(5) Initially, all directory entries are empty.
After that, Carl examined the print job directory. It contained traces of Bob’s two print jobs, and the rest of the directory was empty:
job from B (deleted)
job from B (deleted)
empty
empty
empty
...
I want to model this dispute and then specify some formula to see whether Alice's claim is true or not. I have just considered the first two entries of the printer job directory. Every node in the output graph represent these two entries. Each node should have three outgoing actions, add_A, add_B, and take. However, two of them named (/\ entry1 = "A"/\ entry2 = "B") and (/\ entry1 = "B"/\ entry2 = "A") have just two outgoing edges, add_A and take.
I will appreciate any help!
Regards,
Somayeh