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

*From*: Amir Hossein Sayyad Abdi <amir.ahsa.2011@xxxxxxxxx>*Date*: Wed, 3 Jul 2019 18:47:09 +0430*References*: <6a66a2c1-8dd9-4247-aecd-d82fb04146b1@googlegroups.com> <e300c1d3-53c0-4d1e-9ac6-234d0c532304@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

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,SomayehOn 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 soltaniI 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/e300c1d3-53c0-4d1e-9ac6-234d0c532304%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/CAKxfy0tBmGYztmsf5g6bU8n8HaGQRMiVRrTYN2WSDRXcYRaumA%40mail.gmail.com.

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

**References**:**[tlaplus] Some edges are missing***From:*somayeh soltani

**[tlaplus] Re: Some edges are missing***From:*somayeh soltani

- Prev by Date:
**[tlaplus] Re: Some edges are missing** - Next by Date:
**[tlaplus] Using pcal.trans to write to different file** - Previous by thread:
**[tlaplus] Re: Some edges are missing** - Next by thread:
**[tlaplus] Re: Some edges are missing** - Index(es):