Some edges are missing

32 views
Skip to first unread message

somayeh soltani

unread,
Jul 1, 2019, 5:27:40 AM7/1/19
to tlaplus
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

Amir A.H.S.A

unread,
Jul 1, 2019, 2:31:32 PM7/1/19
to tla...@googlegroups.com
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

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
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.

somayeh soltani

unread,
Jul 2, 2019, 1:16:02 AM7/2/19
to tlaplus
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
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

Amir Hossein Sayyad Abdi

unread,
Jul 2, 2019, 2:27:12 AM7/2/19
to tla...@googlegroups.com
Perhaps this is due to the predicates of "addA" and "addB" actions and your two specific states, because in those 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


To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.

somayeh soltani

unread,
Jul 2, 2019, 3:01:53 AM7/2/19
to tlaplus
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.

Александр Васильев

unread,
Jul 2, 2019, 5:39:57 AM7/2/19
to tla...@googlegroups.com
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

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.

For more options, visit https://groups.google.com/d/optout.


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

Amir Hossein Sayyad Abdi

unread,
Jul 2, 2019, 6:02:30 AM7/2/19
to tla...@googlegroups.com
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

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.

somayeh soltani

unread,
Jul 2, 2019, 6:03:14 AM7/2/19
to tlaplus
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
acme-tla.png

somayeh soltani

unread,
Jul 2, 2019, 7:29:43 AM7/2/19
to tlaplus
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
acme-tla.png

Amir Hossein Sayyad Abdi

unread,
Jul 2, 2019, 8:12:30 AM7/2/19
to tla...@googlegroups.com
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

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.

Amir Hossein Sayyad Abdi

unread,
Jul 3, 2019, 6:10:57 AM7/3/19
to tla...@googlegroups.com
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

somayeh soltani

unread,
Jul 3, 2019, 9:38:39 AM7/3/19
to tlaplus
Dear AmirHossein,
Thank you for your kindness. I have tried your suggestion before. I have used the gvpr tool which shows the statistics of graphs. Unfortunately, it shows that the graph has 17 nodes and 49 edges.
I have tried to model the same case study using mCRL2 specification language. It is OK and shows a graph with 17 nodes and 51 edges. The graph generated by mCRL2 is given in the attachment.
Regards,
Somayeh
ACME2.png

Amir Hossein Sayyad Abdi

unread,
Jul 3, 2019, 10:17:26 AM7/3/19
to tla...@googlegroups.com
Dear Ms. Soltani,

Thanks for your clarification.

Is it possible that gvpr tool draws two self-loops of the state [entry1="A", entry2="B"] at the same location (on top of each other, so only one of them is visible)?

Sincerely,
AmirHossein


--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.

somayeh soltani

unread,
Jul 3, 2019, 2:40:45 PM7/3/19
to tlaplus
Dear AmirHossein,
No, gvpr is a command line tool and it says the number of nodes and edges.
Regards,
Somayeh

On Monday, July 1, 2019 at 1:57:40 PM UTC+4:30, somayeh soltani wrote:

Amir Hossein Sayyad Abdi

unread,
Jul 3, 2019, 3:15:39 PM7/3/19
to tla...@googlegroups.com
Have you tried the GraphViz project to visualize the generated state graph by the TLC model checker?

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
Reply all
Reply to author
Forward
0 new messages