# Re: [tlaplus] Some edges are missing

Dear Ms. Soltani,

Would please clarify the algorithm that you are trying to specify in TLA+?

Perhaps by adding comments or by pointing out the original name of the algorithm?

AmirHossein

On Mon, Jul 1, 2019, 1:57 PM somayeh soltani <soltanicomp@xxxxxxxxx> 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.