# Re: [tlaplus] Re: Some edges are missing

Dear Ms. Soltani,

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

On Wed, Jul 3, 2019 at 6:08 PM somayeh soltani <soltanicomp@xxxxxxxxx> wrote:
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

\/ take

=============================================================================
\* Modification History
\* 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.