@@ -124,7 +124,7 @@ process(fuerte = "fuertethread") {
124124 or connectDone: \* VERIFIED
125125 if (/\ Len(iocontext) >= 1
126126 /\ Head(iocontext) \in {"connect", "connectBAD"}) {
127- assert state \in {"Connecting", "Created", " Closed"};
127+ assert state \in {"Connecting", "Closed"};
128128 alarm := "off";
129129 if (Head(iocontext) = "connect" /\ state = "Connecting") {
130130 assert active;
@@ -259,7 +259,7 @@ process(cancel = "cancelthread") {
259259
260260}
261261*)
262- \* BEGIN TRANSLATION - the hash of the PCal code: PCal-925ea62a5ed7f2fd7841f2836c7d799c
262+ \* BEGIN TRANSLATION - the hash of the PCal code: PCal-925ea62a5ed7f2fd7841f2836c7d799c (chksum(pcal) = "c5aa3da3" /\ chksum(tla) = "af7613cb")
263263VARIABLES state , active , queueSize , alarm , asyncRunning , iocontext , reading ,
264264 writing , pc , stack
265265
@@ -464,12 +464,12 @@ activate == /\ pc["fuertethread"] = "activate"
464464connectDone == /\ pc [ "fuertethread" ] = "connectDone"
465465 /\ IF /\ Len ( iocontext ) >= 1
466466 /\ Head ( iocontext ) \in { "connect" , "connectBAD" }
467- THEN /\ Assert ( state \in { "Connecting" , "Created" , " Closed"} ,
468- "Failure of assertion at line 127 , column 11." )
467+ THEN /\ Assert ( state \in { "Connecting" , "Closed" } ,
468+ "Failure of assertion at line 128 , column 11." )
469469 /\ alarm ' = "off"
470470 /\ IF Head ( iocontext ) = "connect" /\ state = "Connecting"
471471 THEN /\ Assert ( active ,
472- "Failure of assertion at line 130 , column 13." )
472+ "Failure of assertion at line 131 , column 13." )
473473 /\ iocontext ' = Tail ( iocontext )
474474 /\ state ' = "Connected"
475475 /\ stack ' = [ stack EXCEPT ! [ "fuertethread" ] = << [ procedure |-> "asyncWriteNextRequest" ,
@@ -492,7 +492,7 @@ writeDone == /\ pc["fuertethread"] = "writeDone"
492492 /\ Head ( iocontext ) \in { "write" , "writeBAD" }
493493 THEN /\ Assert ( /\ state \in { "Connected" , "Closed" }
494494 /\ writing ,
495- "Failure of assertion at line 145 , column 11." )
495+ "Failure of assertion at line 146 , column 11." )
496496 /\ writing ' = FALSE
497497 /\ IF Head ( iocontext ) = "write" /\ state = "Connected"
498498 THEN /\ iocontext ' = Tail ( iocontext )
@@ -517,7 +517,7 @@ readDone == /\ pc["fuertethread"] = "readDone"
517517 /\ IF /\ Len ( iocontext ) >= 1
518518 /\ Head ( iocontext ) \in { "read" , "readBAD" }
519519 THEN /\ Assert ( state \in { "Connected" , "Closed" } ,
520- "Failure of assertion at line 163 , column 11." )
520+ "Failure of assertion at line 164 , column 11." )
521521 /\ alarm ' = "off"
522522 /\ reading ' = FALSE
523523 /\ IF Head ( iocontext ) = "read" /\ state = "Connected"
@@ -714,6 +714,6 @@ NoSleepingBarber == /\ NothingForgottenOnQueue
714714
715715=============================================================================
716716\* Modification History
717- \* Last modified Fri Aug 21 16:03:16 CEST 2020 by neunhoef
717+ \* Last modified Thu Aug 19 14:45:44 CEST 2021 by neunhoef
718718\* Last modified Wed Jul 22 12:06:32 CEST 2020 by simon
719719\* Created Mi 22. Apr 22:46:19 CEST 2020 by neunhoef
0 commit comments