Commit eb905658 by Paul Fiterau Brostean

removed extra models

parent 20a3b340
Counterexample for hyp1
CONNECT
!SYN(FRESH,ZERO,0) s1
SYN(V,V,0)
!ACK+SYN(CURRENT,NEXT,0) s4
ACK(V,V,0)
!TIMEOUT s4
ACK(V,V,0)
!TIMEOUT s4
SYN(V,V,0)
!TIMEOUT s4
ACK(V,V,0)
!TIMEOUT s4
RCV
!TIMEOUT s4
SYN+ACK(V,V,0)
!ACK(NEXT,CURRENT,0) s4
ACK+PSH(V,V,1)
!ACK(NEXT,NEXT,0) s7
SYN+ACK(V,V,0)
!ACK(NEXT,CURRENT,0) s7
SYN+ACK(V,V,0)
!ACK(NEXT,CURRENT,0) s7
CLOSE
!ACK+RST(NEXT,CURRENT,0) s2
#!ACK+FIN(NEXT,CURRENT,0)
learningParams:
seed: 1299777356020
minValue: 0
maxValue: 300
minTraceLength: 6
maxTraceLength: 6
maxNumTraces: 20000
sutInterface: sutinfo.yaml
yanCommand2: "/home/cav/GitHub/Yannakakis/build/main --seed 123456789 = fixed 3 2"
yanCommand: "/home/cav/GitHub/Yannakakis/build/main --prefix buggy --seed 123456789 = random 4 4"
mapper: linux
testTraces: []
# - ["CONNECT" , "SYN(V,V,0)" , "ACK(V,V,0)" , "FIN+ACK(V,V,0)" , "SEND" , "SEND" , "SEND" , "CLOSE" , "ACK+PSH(V,V,1)"]
# - ["CONNECT" ,"SYN(V,V,0)" ,"ACK(V,V,0)" ,"ACK+PSH(V,V,1)" ,"FIN+ACK(V,V,0)" ,"SEND" ,"RCV" ,"ACK(V,V,0)" ,"FIN+ACK(V,V,0)"]
# - ["CONNECT" ,"SYN(V,V,0)" ,"ACK+PSH(V,V,1)" ,"SEND" ,"RCV" ,"CONNECT" ,"SYN(V,V,0)" ,"SEND" ,"CLOSE" ,"SEND" ,"SEND" ,"ACK(V,V,0)"]
# - ["LISTEN" , "ACCEPT" , "SYN(V,V,0)" , "ACK+PSH(V,V,1)" , "CLOSECONNECTION"]
# - ["LISTEN" , "ACCEPT" , "SYN(V,V,0)" , "ACK(V,V,0)" , "ACK+PSH(V,V,1)" , "FIN+ACK(V,V,0)" , "ACK+RST(V,V,0)" , "SYN(V,V,0)" , "ACK+PSH(V,V,1)" , "CLOSECONNECTION" , "ACCEPT" , "CLOSECONNECTION" ]
# - ["LISTEN" , "ACCEPT" , "SYN(V,V,0)" , "ACK(V,V,0)" , "CLOSECONNECTION" , "ACK(V,V,0)" , "ACCEPT" , "ACK+RST(V,V,0)" , "SYN+ACK(V,V,0)" , "SYN(V,V,0)" , "ACK(V,V,0)" , "CLOSECONNECTION" ]
# - ["LISTEN" , "ACCEPT" , "SYN(V,V,0)" , "ACK(V,V,0)" , "RST(V,V,0)" , "FIN+ACK(V,V,0)" , "SYN+ACK(V,V,0)" , "ACCEPT" , "SYN(V,V,0)" , "ACK(V,V,0)" , "CLOSECONNECTION" ]
# - ["LISTEN" , "ACCEPT" , "SYN(V,V,0)" , "ACK(V,V,0)" , "ACK+PSH(V,V,1)" , "FIN+ACK(V,V,0)" , "ACK+RST(V,V,0)" , "SYN(V,V,0)" , "ACK+PSH(V,V,1)" , "CLOSECONNECTION" , "ACCEPT" , "CLOSECONNECTION" ]
# - ["LISTEN" , "SYN(V,V,0)" , "ACK+PSH(V,V,1)" , "ACK+RST(V,V,0)" , "SYN(V,V,0)" , "ACK(V,V,0)" , "ACK+RST(V,V,0)" , "ACK+RST(V,V,0)" , "SYN+ACK(V,V,0)" , "LISTEN" , "LISTEN" , "ACK+PSH(V,V,1)" , "LISTEN" , "SYN(V,V,0)" , "ACK+PSH(V,V,1)" ]
# - ["LISTEN" , "ACCEPT" , "SYN(V,V,0)" , "ACK(V,V,0)" , "ACK+PSH(V,V,1)" , "FIN+ACK(V,V,0)" , "RST(V,V,0)" , "SYN(V,V,0)" , "FIN+ACK(V,V,0)" , "ACK+RST(V,V,0)" , "ACCEPT" , "RST(V,V,0)" , "LISTEN" , "SYN(V,V,0)" , "ACK+PSH(V,V,1)" , "RST(V,V,0)" , "SYN(V,V,0)" , "ACK+PSH(V,V,1)" ]
# - ["LISTEN" , "RST(V,V,0)" , "SYN(V,V,0)" , "ACK+PSH(V,V,1)" , "ACK+RST(V,V,0)" , "SYN(V,V,0)" , "ACK(V,V,0)" , "RST(V,V,0)" , "RST(V,V,0)" , "ACK+PSH(V,V,1)" , "RST(V,V,0)" , "LISTEN" , "ACCEPT" , "SYN+ACK(V,V,0)" , "ACK+PSH(V,V,1)" , "RST(V,V,0)" , "SYN(V,V,0)" , "FIN+ACK(V,V,0)" , "ACCEPT" , "LISTEN" , "ACK+RST(V,V,0)" , "SYN(V,V,0)" , "ACK+PSH(V,V,1)" ]
# - ["LISTEN" , "SYN(V,V,0)" , "ACK(V,V,0)" , "ACK+PSH(V,V,1)" , "FIN+ACK(V,V,0)" , "RST(V,V,0)" , "SYN(V,V,0)" , "SYN+ACK(V,V,0)" , "LISTEN" , "SYN(V,V,0)" , "ACK+PSH(V,V,1)" , "ACCEPT" , "FIN+ACK(V,V,0)" , "CLOSECONNECTION" , "ACCEPT" , "CLOSECONNECTION" ]
# - ["LISTEN" , "SYN(V,V,0)" , "ACK(V,V,0)" , "ACK+PSH(V,V,1)" , "FIN+ACK(V,V,0)" , "RST(V,V,0)" , "SYN(V,V,0)" , "FIN+ACK(V,V,0)" , "SYN+ACK(V,V,0)" , "RST(V,V,0)" , "ACK+RST(V,V,0)" , "ACK+RST(V,V,0)" , "ACCEPT" , "RST(V,V,0)" , "SYN+ACK(V,V,0)" , "ACK(V,V,0)" , "RST(V,V,0)" , "SYN(V,V,0)" , "RST(V,V,0)" , "LISTEN" , "ACK+PSH(V,V,1)" , "ACK+PSH(V,V,1)" , "ACK+RST(V,V,0)" , "ACCEPT" , "ACCEPT" , "RCV" , "RCV" , "LISTEN" , "ACCEPT" , "SYN(V,V,0)" , "ACK(V,V,0)" , "ACK(V,V,0)" , "ACK+PSH(V,V,1)" , "LISTEN" , "ACCEPT" , "CLOSECONNECTION" , "FIN+ACK(V,V,0)" , "RCV" , "ACK(V,V,0)" , "ACCEPT" , "CLOSECONNECTION" , "ACCEPT" , "CLOSECONNECTION"]
# - ["LISTEN" , "ACCEPT" , "SYN(V,V,0)" , "ACK(V,V,0)" , "ACK+PSH(V,V,1)" , "SEND" , "ACCEPT" , "SEND" , "LISTEN" , "SEND"]
tcpParams:
runsPerQuery: 2
confidence: 85
sutPort: 18300
sutIP: 127.0.0.1
oracle: client
ENUM
absin {VALID, INV}
ENUM
abssut {CURRENT, NEXT, ZERO, FRESH}
ENUM
abslearner {CURRENT, NEXT, ZERO, FRESH}
STATE
int learnerSeqProposed = -3;
int sutSeq = -3;
int learnerSeq = -3;
int lastLearnerSeq = -3;
int lastSeqPlusDataReceived = -3;
int lastAckReceived = -3;
flags lastFlagsSent = $;
MAP incomingResponse (flags flagsIn, int concSeqIn, int concAckIn, int concDataIn
-> abssut absSeqIn, abslearner absAckIn)
if (concSeqIn == sutSeq+1) {
absSeqIn = abssut.NEXT;
} else { if (concSeqIn == sutSeq) {
absSeqIn = abssut.CURRENT;
} else { if (concSeqIn == 0) {
absSeqIn = abssut.ZERO;
} else {
absSeqIn = abssut.FRESH;
}}}
if ((concAckIn == learnerSeq+1) | (concAckIn == learnerSeqProposed+1)) {
absAckIn = abslearner.NEXT;
} else { if (concAckIn == learnerSeq) {
absAckIn = abslearner.CURRENT;
} else { if (concAckIn == 0) {
absAckIn = abslearner.ZERO;
} else {
absAckIn = abslearner.FRESH;
}}}
UPDATE
if ((lastFlagsSent has $S) & (lastFlagsSent has $A) & (flagsIn has $R) & (!(flagsIn has $A))) {
sutSeq = sutSeq;
learnerSeq = learnerSeq;
} else { if ((flagsIn has $R) | ((learnerSeqProposed != -3) & (concAckIn != learnerSeqProposed+1))) {
// upon reset, or if a fresh seq from the learner is not acknowledged
sutSeq = -3;
learnerSeq = -3;
} else { if ((learnerSeqProposed != -3) | (concSeqIn == sutSeq+1)) {
// if a fresh seq from the learner is acknowledged, or if the sequence number is valid
if ((flagsIn has $S) | (flagsIn has $F)) {
sutSeq = concSeqIn + concDataIn;
} else { if (flagsIn has $P) {
sutSeq = sutSeq + concDataIn;
} else {
sutSeq = sutSeq;
}}
learnerSeq = concAckIn;
} else {if (flagsIn has $S) {
// fresh sequence number
sutSeq = concSeqIn;
if (concAckIn == 0) {
learnerSeq = learnerSeq;
} else {
learnerSeq = concAckIn;
}
} else {
sutSeq = sutSeq;
learnerSeq = learnerSeq;
}}}}
if (learnerSeq != -3) {
lastLearnerSeq = learnerSeq;
} else {
lastLearnerSeq = lastLearnerSeq;
}
learnerSeqProposed = -3;
if (flagsIn has $S | flagsIn has $F) {
lastSeqPlusDataReceived = concSeqIn + concDataIn + 1;
} else {
lastSeqPlusDataReceived = concSeqIn + concDataIn;
}
lastAckReceived = concAckIn;
lastFlagsSent=$;
MAP outgoingRequest (int concSeqOut, int concAckOut, flags flagsOut, int concDataOut
-> absin absSeqOut, absin absAckOut, flags flagsOut2, int absDataOut)
flagsOut2 = flagsOut;
absDataOut = concDataOut;
if (
(learnerSeq == -3)
| (concSeqOut == learnerSeq)
| ((flagsOut has $R) & (!(flagsOut has $A)) & (lastAckReceived != 0) & (learnerSeq == -3) & (concSeqOut == lastAckReceived))
) {
absSeqOut = absin.VALID;
} else {
absSeqOut = absin.INV;
}
if ( ( ((sutSeq == -3) & (concAckOut == 0)) | ((sutSeq != -3) & (concAckOut == sutSeq+1)) )
| (!(flagsOut has $A))
) {
absAckOut = absin.VALID;
} else {
absAckOut = absin.INV;
}
UPDATE
if ((flagsOut has $R) & (absAckOut == absin.VALID) & (absSeqOut == absin.VALID)) {
learnerSeqProposed = -3;
sutSeq = -3;
learnerSeq = -3;
} else {
if (learnerSeq == -3) {
learnerSeqProposed = concSeqOut;
} else {
learnerSeqProposed = learnerSeqProposed;
}
sutSeq = sutSeq;
learnerSeq = learnerSeq;
}
if (learnerSeq != -3) {
lastLearnerSeq = learnerSeq;
} else {
lastLearnerSeq = lastLearnerSeq;
}
lastSeqPlusDataReceived = lastSeqPlusDataReceived;
lastAckReceived = lastAckReceived;
lastFlagsSent = flagsOut;
MAP incomingTimeout (int tmp -> int tmp2)
tmp2 = tmp;
UPDATE
lastFlagsSent = $;
learnerSeqProposed = -3;
sutSeq = sutSeq;
learnerSeq = learnerSeq;
lastLearnerSeq = lastLearnerSeq;
lastSeqPlusDataReceived = lastSeqPlusDataReceived;
lastAckReceived = lastAckReceived;
\ No newline at end of file
ENUM
absin {VALID, INV}
ENUM
abssut {CURRENT, NEXT, ZERO, FRESH}
ENUM
abslearner {CURRENT, NEXT, ZERO, FRESH}
STATE
int learnerSeqProposed = -3;
int sutSeq = -3;
int learnerSeq = -3;
int lastSeqPlusDataReceived = -3;
int lastAckReceived = -3;
MAP incomingResponse (flags flagsIn, int concSeqIn, int concAckIn, int concDataIn
-> abssut absSeqIn, abslearner absAckIn)
if (concSeqIn == sutSeq+1) {
absSeqIn = abssut.NEXT;
} else { if (concSeqIn == sutSeq) {
absSeqIn = abssut.CURRENT;
} else { if (concSeqIn == 0) {
absSeqIn = abssut.ZERO;
} else {
absSeqIn = abssut.FRESH;
}}}
if ((concAckIn == learnerSeq+1) | (concAckIn == learnerSeqProposed+1)) {
absAckIn = abslearner.NEXT;
} else { if (concAckIn == learnerSeq) {
absAckIn = abslearner.CURRENT;
} else { if (concAckIn == 0) {
absAckIn = abslearner.ZERO;
} else {
absAckIn = abslearner.FRESH;
}}}
UPDATE
if ((flagsIn has $R) | ((learnerSeqProposed != -3) & (concAckIn != learnerSeqProposed+1))) {
// upon reset, or if a fresh seq from the learner is not acknowledged
sutSeq = -3;
learnerSeq = -3;
} else { if ((learnerSeqProposed != -3) | (concSeqIn == sutSeq+1)) {
// if a fresh seq from the learner is acknowledged, or if the sequence number is valid
if ((flagsIn has $S) | (flagsIn has $F)) {
sutSeq = concSeqIn;
} else { if (flagsIn has $P) {
sutSeq = sutSeq + concDataIn;
} else {
sutSeq = sutSeq;
}}
learnerSeq = concAckIn;
} else {if (flagsIn has $S) {
// fresh sequence number
sutSeq = concSeqIn;
if (concAckIn == 0) {
learnerSeq = learnerSeq;
} else {
learnerSeq = concAckIn;
}
} else {
sutSeq = sutSeq;
learnerSeq = learnerSeq;
}}}
learnerSeqProposed = -3;
if (flagsIn has $S | flagsIn has $F) {
lastSeqPlusDataReceived = concSeqIn + concDataIn + 1;
} else {
lastSeqPlusDataReceived = concSeqIn + concDataIn;
}
lastAckReceived = concAckIn;
MAP outgoingRequest (int concSeqOut, int concAckOut, flags flagsOut, int concDataOut
-> absin absSeqOut, absin absAckOut, flags flagsOut2, int absDataOut)
flagsOut2 = flagsOut;
absDataOut = concDataOut;
if (((learnerSeq == -3)
| (learnerSeq == concSeqOut))
| ((flagsOut has $R) & (!(flagsOut has $A)) & (lastAckReceived != 0) & (learnerSeq == -3) & (concSeqOut == lastAckReceived))
) {
absSeqOut = absin.VALID;
} else {
absSeqOut = absin.INV;
}
if ((((sutSeq == -3) & (concAckOut == 0)) | ((sutSeq != -3) & (concAckOut == sutSeq+1)))
// | ((lastAckReceived == 0) & (concAckOut == lastSeqPlusDataReceived) & (flagsOut has $R) & (flagsOut has $A))
| (!(flagsOut has $A))
) {
absAckOut = absin.VALID;
} else {
absAckOut = absin.INV;
}
UPDATE
if ((flagsOut has $R) & (absAckOut == absin.VALID) & (absSeqOut == absin.VALID)) {
learnerSeqProposed = -3;
sutSeq = -3;
learnerSeq = -3;
} else {
if (learnerSeq == -3) {
learnerSeqProposed = concSeqOut;
} else {
learnerSeqProposed = learnerSeqProposed;
}
sutSeq = sutSeq;
learnerSeq = learnerSeq;
}
lastSeqPlusDataReceived = lastSeqPlusDataReceived;
lastAckReceived = lastAckReceived;
MAP incomingTimeout (int tmp -> int tmp2)
tmp2 = tmp;
UPDATE
learnerSeqProposed = -3;
sutSeq = sutSeq;
learnerSeq = learnerSeq;
lastSeqPlusDataReceived = lastSeqPlusDataReceived;
lastAckReceived = lastAckReceived;
ENUM
absin {VALID, INV}
ENUM
abssut {CURRENT, NEXT, ZERO, FRESH}
ENUM
abslearner {CURRENT, NEXT, ZERO, FRESH}
STATE
int learnerSeqProposed = -3;
int sutSeq = -3;
int learnerSeq = -3;
int lastLearnerSeq = -3;
int lastSeqPlusDataReceived = -3;
int lastAckReceived = -3;
flags lastFlagsSent = $;
MAP incomingResponse (flags flagsIn, int concSeqIn, int concAckIn, int concDataIn
-> abssut absSeqIn, abslearner absAckIn)
if (concSeqIn == sutSeq+1) {
absSeqIn = abssut.NEXT;
} else { if (concSeqIn == sutSeq) {
absSeqIn = abssut.CURRENT;
} else { if (concSeqIn == 0) {
absSeqIn = abssut.ZERO;
} else {
absSeqIn = abssut.FRESH;
}}}
if ((concAckIn == learnerSeq+1) | (concAckIn == learnerSeqProposed+1)) {
absAckIn = abslearner.NEXT;
} else { if (concAckIn == learnerSeq) {
absAckIn = abslearner.CURRENT;
} else { if (concAckIn == 0) {
absAckIn = abslearner.ZERO;
} else {
absAckIn = abslearner.FRESH;
}}}
UPDATE
if ((lastFlagsSent has $S) & (lastFlagsSent has $A) & (flagsIn has $R)) {
sutSeq = sutSeq;
learnerSeq = learnerSeq;
} else { if ((flagsIn has $R) | ((learnerSeqProposed != -3) & (concAckIn != learnerSeqProposed+1))) {
// upon reset, or if a fresh seq from the learner is not acknowledged
sutSeq = -3;
learnerSeq = -3;
} else { if ((learnerSeqProposed != -3) | (concSeqIn == sutSeq+1)) {
// if a fresh seq from the learner is acknowledged, or if the sequence number is valid
if ((flagsIn has $S) | (flagsIn has $F)) {
sutSeq = concSeqIn + concDataIn;
} else { if (flagsIn has $P) {
sutSeq = sutSeq + concDataIn;
} else {
sutSeq = sutSeq;
}}
learnerSeq = concAckIn;
} else {if (flagsIn has $S) {
// fresh sequence number
sutSeq = concSeqIn;
if (concAckIn == 0) {
learnerSeq = learnerSeq;
} else {
learnerSeq = concAckIn;
}
} else {
sutSeq = sutSeq;
learnerSeq = learnerSeq;
}}}}
if (learnerSeq != -3) {
lastLearnerSeq = learnerSeq;
} else {
lastLearnerSeq = lastLearnerSeq;
}
learnerSeqProposed = -3;
if (flagsIn has $S | flagsIn has $F) {
lastSeqPlusDataReceived = concSeqIn + concDataIn + 1;
} else {
lastSeqPlusDataReceived = concSeqIn + concDataIn;
}
lastAckReceived = concAckIn;
lastFlagsSent=$;
MAP outgoingRequest (int concSeqOut, int concAckOut, flags flagsOut, int concDataOut
-> absin absSeqOut, absin absAckOut, flags flagsOut2, int absDataOut)
flagsOut2 = flagsOut;
absDataOut = concDataOut;
if (
(learnerSeq == -3)
| (concSeqOut == learnerSeq)
| ((flagsOut has $R) & (!(flagsOut has $A)) & (lastAckReceived != 0) & (learnerSeq == -3) & (concSeqOut == lastAckReceived))
) {
absSeqOut = absin.VALID;
} else {
absSeqOut = absin.INV;
}
if ( ( ((sutSeq == -3) & (concAckOut == 0)) | ((sutSeq != -3) & (concAckOut == sutSeq+1)) )
| (!(flagsOut has $A))
) {
absAckOut = absin.VALID;
} else {
absAckOut = absin.INV;
}
UPDATE
if ((flagsOut has $R) & (absAckOut == absin.VALID) & (absSeqOut == absin.VALID)) {
learnerSeqProposed = -3;
sutSeq = -3;
learnerSeq = -3;
} else {
if (learnerSeq == -3) {
learnerSeqProposed = concSeqOut;
} else {
learnerSeqProposed = learnerSeqProposed;
}
sutSeq = sutSeq;
learnerSeq = learnerSeq;
}
if (learnerSeq != -3) {
lastLearnerSeq = learnerSeq;
} else {
lastLearnerSeq = lastLearnerSeq;
}
lastSeqPlusDataReceived = lastSeqPlusDataReceived;
lastAckReceived = lastAckReceived;
lastFlagsSent = flagsOut;
MAP incomingTimeout (int tmp -> int tmp2)
tmp2 = tmp;
UPDATE
lastFlagsSent = $;
learnerSeqProposed = -3;
sutSeq = sutSeq;
learnerSeq = learnerSeq;
lastLearnerSeq = lastLearnerSeq;
lastSeqPlusDataReceived = lastSeqPlusDataReceived;
lastAckReceived = lastAckReceived;
\ No newline at end of file
name: TCP
inputInterfaces:
# LISTEN: []
# ACCEPT: []
CONNECT: []
RCV: []
# CLOSECONNECTION: []
SYN(V,V,0): []
ACK(V,V,0): []
ACK+PSH(V,V,1): []
FIN+ACK(V,V,0): []
SYN+ACK(V,V,0): []
RST(V,V,0): []
ACK+RST(V,V,0): []
CLOSE: []
# SEND: []
outputInterfaces:
ACK(ARECV,ARECV): []
ACK(ARECV,ASENT): []
ACK(ARECV,INV): []
ACK(ARECV,S+1SENT): []
ACK(ARECV,S+D+1SENT): []
ACK(ARECV,S+DSENT): []
ACK(FRESH,ARECV): []
ACK(FRESH,ASENT): []
ACK(FRESH,INV): []
ACK(FRESH,S+1SENT): []
ACK(FRESH,S+D+1SENT): []
ACK(FRESH,S+DSENT): []
ACK(INV,ARECV): []
ACK(INV,ASENT): []
ACK(INV,INV): []
ACK(INV,S+1SENT): []
ACK(INV,S+D+1SENT): []
ACK(INV,S+DSENT): []
ACK(S+1RECV,ARECV): []
ACK(S+1RECV,ASENT): []
ACK(S+1RECV,INV): []
ACK(S+1RECV,S+1SENT): []
ACK(S+1RECV,S+D+1SENT): []
ACK(S+1RECV,S+DSENT): []
ACK(SRECV,ARECV): []
ACK(SRECV,ASENT): []
ACK(SRECV,INV): []
ACK(SRECV,S+1SENT): []
ACK(SRECV,S+D+1SENT): []
ACK(SRECV,S+DSENT): []
ACK(ZERO,ARECV): []
ACK(ZERO,ASENT): []
ACK(ZERO,INV): []
ACK(ZERO,S+1SENT): []
ACK(ZERO,S+D+1SENT): []
ACK(ZERO,S+DSENT): []
ACK+FIN(ARECV,ARECV): []
ACK+FIN(ARECV,ASENT): []
ACK+FIN(ARECV,INV): []
ACK+FIN(ARECV,S+1SENT): []
ACK+FIN(ARECV,S+D+1SENT): []
ACK+FIN(ARECV,S+DSENT): []
ACK+FIN(FRESH,ARECV): []
ACK+FIN(FRESH,ASENT): []
ACK+FIN(FRESH,INV): []
ACK+FIN(FRESH,S+1SENT): []
ACK+FIN(FRESH,S+D+1SENT): []
ACK+FIN(FRESH,S+DSENT): []
ACK+FIN(INV,ARECV): []
ACK+FIN(INV,ASENT): []
ACK+FIN(INV,INV): []
ACK+FIN(INV,S+1SENT): []
ACK+FIN(INV,S+D+1SENT): []
ACK+FIN(INV,S+DSENT): []
ACK+FIN(S+1RECV,ARECV): []
ACK+FIN(S+1RECV,ASENT): []
ACK+FIN(S+1RECV,INV): []
ACK+FIN(S+1RECV,S+1SENT): []
ACK+FIN(S+1RECV,S+D+1SENT): []
ACK+FIN(S+1RECV,S+DSENT): []
ACK+FIN(SRECV,ARECV): []
ACK+FIN(SRECV,ASENT): []
ACK+FIN(SRECV,INV): []
ACK+FIN(SRECV,S+1SENT): []
ACK+FIN(SRECV,S+D+1SENT): []
ACK+FIN(SRECV,S+DSENT): []
ACK+FIN(ZERO,ARECV): []
ACK+FIN(ZERO,ASENT): []
ACK+FIN(ZERO,INV): []
ACK+FIN(ZERO,S+1SENT): []
ACK+FIN(ZERO,S+D+1SENT): []
ACK+FIN(ZERO,S+DSENT): []
ACK+RST(ARECV,ARECV): []
ACK+RST(ARECV,ASENT): []
ACK+RST(ARECV,INV): []
ACK+RST(ARECV,S+1SENT): []
ACK+RST(ARECV,S+D+1SENT): []
ACK+RST(ARECV,S+DSENT): []
ACK+RST(FRESH,ARECV): []
ACK+RST(FRESH,ASENT): []
ACK+RST(FRESH,INV): []
ACK+RST(FRESH,S+1SENT): []
ACK+RST(FRESH,S+D+1SENT): []
ACK+RST(FRESH,S+DSENT): []
ACK+RST(INV,ARECV): []
ACK+RST(INV,ASENT): []
ACK+RST(INV,INV): []
ACK+RST(INV,S+1SENT): []
ACK+RST(INV,S+D+1SENT): []
ACK+RST(INV,S+DSENT): []
ACK+RST(S+1RECV,ARECV): []
ACK+RST(S+1RECV,ASENT): []
ACK+RST(S+1RECV,INV): []
ACK+RST(S+1RECV,S+1SENT): []
ACK+RST(S+1RECV,S+D+1SENT): []
ACK+RST(S+1RECV,S+DSENT): []
ACK+RST(SRECV,ARECV): []
ACK+RST(SRECV,ASENT): []
ACK+RST(SRECV,INV): []
ACK+RST(SRECV,S+1SENT): []
ACK+RST(SRECV,S+D+1SENT): []
ACK+RST(SRECV,S+DSENT): []
ACK+RST(ZERO,ARECV): []
ACK+RST(ZERO,ASENT): []
ACK+RST(ZERO,INV): []
ACK+RST(ZERO,S+1SENT): []
ACK+RST(ZERO,S+D+1SENT): []
ACK+RST(ZERO,S+DSENT): []
FIN(ARECV,ARECV): []
FIN(ARECV,ASENT): []
FIN(ARECV,INV): []
FIN(ARECV,S+1SENT): []
FIN(ARECV,S+D+1SENT): []
FIN(ARECV,S+DSENT): []
FIN(FRESH,ARECV): []
FIN(FRESH,ASENT): []
FIN(FRESH,INV): []
FIN(FRESH,S+1SENT): []
FIN(FRESH,S+D+1SENT): []
FIN(FRESH,S+DSENT): []
FIN(INV,ARECV): []
FIN(INV,ASENT): []
FIN(INV,INV): []
FIN(INV,S+1SENT): []
FIN(INV,S+D+1SENT): []
FIN(INV,S+DSENT): []
FIN(S+1RECV,ARECV): []
FIN(S+1RECV,ASENT): []
FIN(S+1RECV,INV): []
FIN(S+1RECV,S+1SENT): []
FIN(S+1RECV,S+D+1SENT): []
FIN(S+1RECV,S+DSENT): []
FIN(SRECV,ARECV): []
FIN(SRECV,ASENT): []
FIN(SRECV,INV): []
FIN(SRECV,S+1SENT): []
FIN(SRECV,S+D+1SENT): []
FIN(SRECV,S+DSENT): []
FIN(ZERO,ARECV): []
FIN(ZERO,ASENT): []
FIN(ZERO,INV): []
FIN(ZERO,S+1SENT): []
FIN(ZERO,S+D+1SENT): []
FIN(ZERO,S+DSENT): []
RST(ARECV,ARECV): []
RST(ARECV,ASENT): []
RST(ARECV,INV): []
RST(ARECV,S+1SENT): []
RST(ARECV,S+D+1SENT): []
RST(ARECV,S+DSENT): []
RST(FRESH,ARECV): []
RST(FRESH,ASENT): []
RST(FRESH,INV): []
RST(FRESH,S+1SENT): []
RST(FRESH,S+D+1SENT): []
RST(FRESH,S+DSENT): []
RST(INV,ARECV): []
RST(INV,ASENT): []
RST(INV,INV): []
RST(INV,S+1SENT): []
RST(INV,S+D+1SENT): []
RST(INV,S+DSENT): []
RST(S+1RECV,ARECV): []
RST(S+1RECV,ASENT): []
RST(S+1RECV,INV): []
RST(S+1RECV,S+1SENT): []
RST(S+1RECV,S+D+1SENT): []
RST(S+1RECV,S+DSENT): []
RST(SRECV,ARECV): []
RST(SRECV,ASENT): []
RST(SRECV,INV): []
RST(SRECV,S+1SENT): []
RST(SRECV,S+D+1SENT): []
RST(SRECV,S+DSENT): []
RST(ZERO,ARECV): []
RST(ZERO,ASENT): []
RST(ZERO,INV): []
RST(ZERO,S+1SENT): []
RST(ZERO,S+D+1SENT): []
RST(ZERO,S+DSENT): []
SYN(ARECV,ARECV): []
SYN(ARECV,ASENT): []
SYN(ARECV,INV): []
SYN(ARECV,S+1SENT): []
SYN(ARECV,S+D+1SENT): []
SYN(ARECV,S+DSENT): []
SYN(FRESH,ARECV): []
SYN(FRESH,ASENT): []
SYN(FRESH,INV): []
SYN(FRESH,S+1SENT): []
SYN(FRESH,S+D+1SENT): []
SYN(FRESH,S+DSENT): []
SYN(INV,ARECV): []
SYN(INV,ASENT): []
SYN(INV,INV): []
SYN(INV,S+1SENT): []
SYN(INV,S+D+1SENT): []
SYN(INV,S+DSENT): []
SYN(S+1RECV,ARECV): []
SYN(S+1RECV,ASENT): []
SYN(S+1RECV,INV): []
SYN(S+1RECV,S+1SENT): []
SYN(S+1RECV,S+D+1SENT): []
SYN(S+1RECV,S+DSENT): []
SYN(SRECV,ARECV): []
SYN(SRECV,ASENT): []
SYN(SRECV,INV): []
SYN(SRECV,S+1SENT): []
SYN(SRECV,S+D+1SENT): []
SYN(SRECV,S+DSENT): []
SYN(ZERO,ARECV): []
SYN(ZERO,ASENT): []
SYN(ZERO,INV): []
SYN(ZERO,S+1SENT): []
SYN(ZERO,S+D+1SENT): []
SYN(ZERO,S+DSENT): []
SYN+ACK(ARECV,ARECV): []
SYN+ACK(ARECV,ASENT): []
SYN+ACK(ARECV,INV): []
SYN+ACK(ARECV,S+1SENT): []
SYN+ACK(ARECV,S+D+1SENT): []
SYN+ACK(ARECV,S+DSENT): []
SYN+ACK(FRESH,ARECV): []
SYN+ACK(FRESH,ASENT): []
SYN+ACK(FRESH,INV): []
SYN+ACK(FRESH,S+1SENT): []
SYN+ACK(FRESH,S+D+1SENT): []
SYN+ACK(FRESH,S+DSENT): []
SYN+ACK(INV,ARECV): []
SYN+ACK(INV,ASENT): []
SYN+ACK(INV,INV): []
SYN+ACK(INV,S+1SENT): []
SYN+ACK(INV,S+D+1SENT): []
SYN+ACK(INV,S+DSENT): []
SYN+ACK(S+1RECV,ARECV): []
SYN+ACK(S+1RECV,ASENT): []
SYN+ACK(S+1RECV,INV): []
SYN+ACK(S+1RECV,S+1SENT): []
SYN+ACK(S+1RECV,S+D+1SENT): []
SYN+ACK(S+1RECV,S+DSENT): []
SYN+ACK(SRECV,ARECV): []
SYN+ACK(SRECV,ASENT): []
SYN+ACK(SRECV,INV): []
SYN+ACK(SRECV,S+1SENT): []
SYN+ACK(SRECV,S+D+1SENT): []
SYN+ACK(SRECV,S+DSENT): []
SYN+ACK(ZERO,ARECV): []
SYN+ACK(ZERO,ASENT): []
SYN+ACK(ZERO,INV): []
SYN+ACK(ZERO,S+1SENT): []
SYN+ACK(ZERO,S+D+1SENT): []
SYN+ACK(ZERO,S+DSENT): []
constants: []
This source diff could not be displayed because it is too large. You can view the blob instead.
Running time of membership queries: 151ms.
Running time of membership queries: 20ms.
Total states in learned abstract Mealy machine: 15
STATISTICS SUMMARY:
Total running time: 60891ms.
Total time Membership queries: 171
Total time Equivalence queries: 60720
Total number of runs: 2
Total Membership queries: 1974
Total Equivalence queries: 110126
Total unique Equivalence queries: 71450
Number of equivalence queries per hypothesis:
hyp 0: 15268
hyp 1: 56174