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

*From*: somayeh soltani <soltanicomp@xxxxxxxxx>*Date*: Wed, 3 Jul 2019 11:40:45 -0700 (PDT)*References*: <6a66a2c1-8dd9-4247-aecd-d82fb04146b1@googlegroups.com>

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 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/4eb7e6c6-108c-472b-8d2f-91244c208106%40googlegroups.com.

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

**Follow-Ups**:**Re: [tlaplus] Re: Some edges are missing***From:*Amir Hossein Sayyad Abdi

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

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