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

*From*: somayeh soltani <soltanicomp@xxxxxxxxx>*Date*: Mon, 1 Jul 2019 02:27:40 -0700 (PDT)

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

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/6a66a2c1-8dd9-4247-aecd-d82fb04146b1%40googlegroups.com.

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

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

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

**Re: [tlaplus] Some edges are missing***From:*Amir A.H.S.A

- Prev by Date:
**[tlaplus] Re: Which symbols need to be defined? (new to TLA+)** - Next by Date:
**Re: [tlaplus] Which symbols need to be defined? (new to TLA+)** - Previous by thread:
**Re: [tlaplus] Which symbols need to be defined? (new to TLA+)** - Next by thread:
**Re: [tlaplus] Some edges are missing** - Index(es):