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
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