Re: [tlaplus] Some edges are missing

Dear Alexander,

Thank you for your consideration. I think the spec is correct. The output graph is attached. All of the nodes have three outgoing edges, except the two aforementioned nodes.

I appreciate any help!

Regards,

Somayeh

On Tuesday, July 2, 2019 at 2:09:57 PM UTC+4:30, Alexander Vasilev wrote:

Dear Somayeh,

The first line of add_A, i.e. IF (entry1 = "A") \/ (entry2 = "A")
and term #4 The printer can accept only one print job from each user at a time.
contradict each other.

The add_A action also permits step
entry1=A, entry2=B -> entry1'=A, entry2'=A
when Alice' print job overwrites Bob's one. This is not a correct spec I suppose

On Tue, Jul 2, 2019 at 2:01 PM somayeh soltani <solta...@xxxxxxxxx> wrote:
Dear AmirHossein,
Thank you for your reply. If I change the order of addA and addB then addB will occur and addA won't occur. I need a solution to see both of these actions.
Regards,
Somayeh

On Tuesday, July 2, 2019 at 10:57:12 AM UTC+4:30, AmirHossein wrote:
Perhaps this is due to the predicates of "addA" and "addB" actions and your two specific states, because in thosI e two states both of the action predicates are satisfied, yet since addA has come first (before addB) in your "Next" formula it will cause the addB action to never occur in those two states.

I suggest you change the order of addA and addB actions in your Next formula and then examine the new output graph to see which two actions are taken in those two states.

Sincerely,
AmirHossein

On Tue, Jul 2, 2019, 9:46 AM somayeh soltani <solta...@xxxxxxxxx> wrote:
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

On Mon, Jul 1, 2019, 1:57 PM somayeh soltani <solta...@xxxxxxxxx> wrote:
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.

--
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/f2022d98-9d74-4288-869f-8f22756ea704%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
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...@googlegroups.com.
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/d66375d3-86b9-4acc-a0b9-f77acc7af97a%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
с уважением,
Александр Васильев