[tlaplus] Re: Some edges are missing

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

On Monday, July 1, 2019 at 1:57:40 PM UTC+4:30, somayeh soltani 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