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
On Monday, July 1, 2019 at 11:01:32 PM UTC+4:30, AmirHossein wrote:
Dear Ms. Soltani,
Would please clarify the algorithm that you are trying to specify in TLA+?
Perhaps by adding comments or by pointing out the original name of the algorithm?
AmirHossein
Dear All,
I am new in TLA+, and I have tried to model a simple specification, which is given below:
-------------------------------- MODULE ACME --------------------------------
EXTENDS Integers
VARIABLES entry1, entry2
-----------------------------------------------------------------------------
TypeOk == /\ entry1 \in {"e", "A", "B", "A_del", "B_del"}
/\ entry2 \in {"e", "A", "B", "A_del", "B_del"}
Init == /\ entry1 = "e"
/\ entry2 = "e"
add_A == IF (entry1 = "A") \/ (entry2 = "A")
THEN /\ UNCHANGED entry1
/\ UNCHANGED entry2
ELSE IF (entry1 = "e") \/ (entry1 = "A_del") \/ (entry1 = "B_del")
THEN /\ entry1' = "A"
/\ UNCHANGED entry2
ELSE
/\ entry2' = "A"
/\ UNCHANGED entry1
add_B == IF (entry1 = "B") \/ (entry2 = "B")
THEN /\ UNCHANGED entry1
/\ UNCHANGED entry2
ELSE IF (entry1 = "e") \/ (entry1 = "A_del") \/ (entry1 = "B_del")
THEN /\ entry1' = "B"
/\ UNCHANGED entry2
ELSE
/\ entry2' = "B"
/\ UNCHANGED entry1
take == IF entry1 = "A"
THEN /\ entry1' = "A_del"
/\ UNCHANGED entry2
ELSE IF entry1 = "B"
THEN /\ entry1' = "B_del"
/\ UNCHANGED entry2
ELSE IF entry2 = "A"
THEN /\ entry2' = "A_del"
/\ UNCHANGED entry1
ELSE IF entry2 = "B"
THEN /\ entry2' = "B_del"
/\ UNCHANGED entry1
ELSE /\ UNCHANGED entry1
/\ UNCHANGED entry2
Next == \/ add_A
\/ add_B
\/ take
=============================================================================
\* Modification History
\* Last modified Mon Jul 01 13:49:57 IRDT 2019 by soltani
\* Created Sun Jun 30 15:22:19 IRDT 2019 by soltani
I expect a graph with 17 nodes and 17*3 edges. I mean every node should have three outgoing edges. However, two of the nodes, named (/\ entry1 = "A"/\ entry2 = "B") and (/\ entry1 = "B"/\ entry2 = "A") have just two outgoing edges.
Is there a way to get the complete graph!
Regards,
Somayeh
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6a66a2c1-8dd9-4247-aecd-d82fb04146b1%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.