# Re: [tlaplus] Some edges are missing

Dear Ms. Soltani,

The attached state transition graph shows exactly what you have specified. the actions addA and addB state that if either of the entries are A or B, then do nothing.

In your two specific states, both actiona are enabled and they will both end up not changing the state.

The state transition diagram is correct, but your algorithm is not doing what you intend it to do.

Also I still believe that in the two aforementioned states, the action "addB" is never taken (although it is enabled), because addA is also enabled and it will be taken (since you have your Next formula as a disjunction of addA and addB actions). I may well be wrong about this.

Sincerely,
AmirHossein

On Tue, Jul 2, 2019, 3:59 PM somayeh soltani <soltanicomp@xxxxxxxxx> wrote:
Dear AmirHossein,
The output graph is attached.
Regards,
Somayeh

On Tuesday, July 2, 2019 at 2:32:30 PM UTC+4:30, AmirHossein wrote:
This is an error in the algorithm that needs correction.

You want each node in the state graph to have exactly 3 outgoing edges (why?), which is not possible due to your Next formula and addA/addB actions predicates.

There are two states that satisfy both addA and addB actions which you have found them as well.

Since addA and addB actions are both enabled in those two states, and since your Next formula is a disjunction of addA and addB actions, then only one of them will be taken (depending on the order in which you have written addA and addB in the Next formula).

Sincerely,
AmirHossein

On Tue, Jul 2, 2019, 11:31 AM somayeh soltani <solta...@xxxxxxxxx> wrote:
Dear AmirHossein,
Regards,
Somayeh

On Tuesday, July 2, 2019 at 10:57:12 AM UTC+4:30, AmirHossein wrote:
Perhaps this is due to the predicates of "addA" and "addB" actions and your two specific states, because in thosI e two states both of the action predicates are satisfied, yet since addA has come first (before addB) in your "Next" formula it will cause the addB action to never occur in those two states.

I suggest you change the order of addA and addB actions in your Next formula and then examine the new output graph to see which two actions are taken in those two states.

Sincerely,
AmirHossein

On Tue, Jul 2, 2019, 9:46 AM somayeh soltani <solta...@xxxxxxxxx> wrote:
Dear AmirHossein,
Thank you for your consideration. This specification is related to a digital forensic case study:
The local area network at ACME Manufacturing consists of two personal computers and a networked printer. The cost of running the network is shared by its two users Alice (A) and Bob (B). Alice, however, claims that she never uses the printer and should not be paying for the printer consumables. Bob disagrees; he says that he saw Alice collecting printouts. The system administrator, Carl, has been assigned to investigate this dispute.
To get more information about how the printer works, Carl contacted the manufacturer. According to the manufacturer, the printer works as follows:
(1) When a print job is received from the user it is stored in the first unallocated directory entry of the print job directory.
(2) The printing mechanism scans the print job directory from the beginning and picks the first active job.
(3) After the job is printed, the corresponding directory entry is marked as ‘‘deleted’’, but the name of the job owner is preserved.
(4) The printer can accept only one print job from each user at a time.
(5) Initially, all directory entries are empty.
After that, Carl examined the print job directory. It contained traces of Bob’s two print jobs, and the rest of the directory was empty:
job from B (deleted)
job from B (deleted)
empty
empty
empty
...

I want to model this dispute and then specify some formula to see whether Alice's claim is true or not. I have just considered the first two entries of the printer job directory. Every node in the output graph represent these two entries. Each node should have three outgoing actions, add_A, add_B, and take. However, two of them named (/\ entry1 = "A"/\ entry2 = "B") and (/\ entry1 = "B"/\ entry2 = "A") have just two outgoing edges, add_A and take.
I will appreciate any help!

Regards,
Somayeh

On Monday, July 1, 2019 at 11:01:32 PM UTC+4:30, AmirHossein wrote:
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 <solta...@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 tla...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.

--
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 tla...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.

--
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 tla...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.

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