[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Some edges are missing



I am sorry, it was my mistake that I said:
"Also I still believe that in the two aforementioned states, the action "addB" is never taken (although it is enabled), because addA is also enabled and it will be taken (since you have your Next formula as a disjunction of addA and addB actions)".

Your question was "why is it that two of the states in the graph have only two outgoing edges ("taken" and "addA" edges), instead of three edges?".

The two states were:
/\entry1 = "B" /\ entry2 = "A"
/\entry1 = "A" /\ entry2 = "B"

The above two states both satisfy the first IF statements in the actions "addA" and "addB". Then I suggested you change the order of addA and addB actions in your Next formula to see the change in the output graph. After that you observed that by changing the order of addA and addB, the resulting state graph has edges "taken" and "addB" for the two above states!!!

We have to figure out why is it that when you change the order of "addA" and "addB" actions in your Next formula, then your output graph shows the "addB" edge (instead of "addA"). Perhaps both edges "addA" and "addB" are painted but they are drawn on top of each other?

AmirHossein


On Tue, Jul 2, 2019 at 4:42 PM Amir Hossein Sayyad Abdi <amir.ahsa.2011@xxxxxxxxx> wrote:
Dear Ms. Soltani,

The attached state transition graph shows exactly what you have specified. the actions addA and addB state that if either of the entries are A or B, then do nothing.

In your two specific states, both actiona are enabled and they will both end up not changing the state.

The state transition diagram is correct, but your algorithm is not doing what you intend it to do.

Also I still believe that in the two aforementioned states, the action "addB" is never taken (although it is enabled), because addA is also enabled and it will be taken (since you have your Next formula as a disjunction of addA and addB actions). I may well be wrong about this.

Sincerely,
AmirHossein

On Tue, Jul 2, 2019, 3:59 PM somayeh soltani <soltanicomp@xxxxxxxxx> wrote:
Dear AmirHossein,
Thank you for your reply. I accept that both addA and addB are enabled in those two aforementioned states. However, addA and addB are enabled in every states. The difference is that in these two states, addA and addB refer to the states themselves.
The output graph is attached.
Regards,
Somayeh

On Tuesday, July 2, 2019 at 2:32:30 PM UTC+4:30, AmirHossein wrote:
This is an error in the algorithm that needs correction.

You want each node in the state graph to have exactly 3 outgoing edges (why?), which is not possible due to your Next formula and addA/addB actions predicates.

There are two states that satisfy both addA and addB actions which you have found them as well.

Since addA and addB actions are both enabled in those two states, and since your Next formula is a disjunction of addA and addB actions, then only one of them will be taken (depending on the order in which you have written addA and addB in the Next formula).

Sincerely,
AmirHossein

On Tue, Jul 2, 2019, 11:31 AM 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...@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/d66375d3-86b9-4acc-a0b9-f77acc7af97a%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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@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/ca78344f-fd1c-4356-aef4-b863b9ecbdde%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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@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/CAKxfy0uqSn7Gj-7vsC0W79YprG24n41D7Z3X-zQuxPHoOHMtZQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.