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

[tlaplus] Re: Some edges are missing



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:
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 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/4eb7e6c6-108c-472b-8d2f-91244c208106%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.