Standard declarationsUNITcolset UNIT = unit;INTBOOLSTRINGrNumbersxixyiyqiqcolset rNumbers = with x | ix | y | iy | q |iq;StateIDLEWAIT_YRECEIVED_YRECEIVED_XSENT_YSENT_XWAIT_ZRECEIVED_ZABORTEDCOMPLETEDcolset State = with IDLE | WAIT_Y | RECEIVED_Y |RECEIVED_X| SENT_Y |SENT_X|
WAIT_Z | RECEIVED_Z | ABORTED | COMPLETED;listMessageSTRINGcolset listMessage = STRING;SEC_KEYKxKycolset SEC_KEY = with Kx | Ky;HASH_PRMTkSEC_KEYnumbrNumberscolset HASH_PRMT=union k:SEC_KEY+numb:rNumbers;MsglistMessagecolset Msg=list listMessage;rMsgrNumbersMsgcolset rMsg = product rNumbers * Msg;Function Declarationsfun Hash(prmt:HASH_PRMT):STRING=
if HASH_PRMT.of_k(prmt)
then HASH_PRMT.mkstr(prmt)
else if HASH_PRMT.of_numb(prmt)
then HASH_PRMT.mkstr(prmt)
else "";
fun Hash(prmt:HASH_PRMT):STRING=
if HASH_PRMT.of_k(prmt)
then HASH_PRMT.mkstr(prmt)
else if HASH_PRMT.of_numb(prmt)
then HASH_PRMT.mkstr(prmt)
else "";Variables DeclarationsrNumbersx1var x1:rNumbers;rNumbersy1var y1:rNumbers;Msgxlistylistzxlistzylistxknownlistyknownlistvar xlist, ylist, zxlist, zylist,
xknownlist, yknownlist:Msg;Values Declarationsval lCouples=[(x,ix),(y,iy),(q,iq)];
val lCouples=[(x,ix),(y,iy),(q,iq)];X_to_YrNumbersY_to_XrNumbersX_to_ZMsgZ_to_XMsgY_to_ZMsgZ_to_YMsgXStateIDLEYStateIDLEZStateIDLEYZXXStateX_to_ZMsgZ_to_XMsgX_to_YrNumbersY_to_XrNumbersStore_YBOOLKnown_valuesrMsg1`(#1 (List.nth(lCouples,0)),
[Hash(k(Kx)),
Hash(k(Ky)),
Hash(k(Kx))^Hash(numb(#2 (List.nth(lCouples,0)))),
Hash(numb(#1 (List.nth(lCouples,1))))])X1X2X3X4X5X6T1IDLEWAIT_YRECEIVED_YRECEIVED_YWAIT_ZWAIT_ZRECEIVED_ZRECEIVED_ZCOMPLETEDRECEIVED_ZABORTEDxknownlisty1WAIT_Yx1truezxlisty1falsezxlistRECEIVED_Z(x1, xknownlist)(x1, xknownlist)if (Hash(numb(y1))=
List.nth(xknownlist, 3) andalso
(zxlist <> []))
then true
else false(x1, xknownlist)YStateX_to_YrNumbersY_to_XrNumbersY_to_ZMsgZ_to_YMsgStore_XBOOLKnown_valuesrMsg1`(#1 (List.nth(lCouples,1)),
[Hash(k(Ky)),
Hash(k(Kx)),
Hash(k(Ky))^Hash(numb(#2 (List.nth(lCouples,1)))),
Hash(numb(#1 (List.nth(lCouples,0))))])Y1Y2Y3Y4Y5Y6T2IDLERECEIVED_XRECEIVED_XSENT_YSENT_YWAIT_ZWAIT_ZRECEIVED_ZRECEIVED_ZCOMPLETEDRECEIVED_ZABORTEDx1y1yknownlistzylistx1if (Hash(numb(x1))=
List.nth(yknownlist, 3) andalso
(zylist <> []))
then true
else falsezylistfalsetrueRECEIVED_Z(y1,yknownlist)(y1,yknownlist)(y1, yknownlist)Hash(key(Kx))ZStateX_to_ZMsgZ_to_XMsgY_to_ZMsgZ_to_YMsgZ1Z2Z3Z4IDLERECEIVED_XRECEIVED_XRECEIVED_YRECEIVED_YSENT_XSENT_XSENT_Yxlistif (List.nth(xlist,0) = List.nth(ylist,1) andalso
List.nth(ylist,2) = List.nth(xlist,1)^
substring(List.nth(xlist,3),0,5)^"i"^
substring(List.nth(xlist,3),5,2))
then [List.nth(ylist,2)]
else []ylistif (List.nth(xlist,0) = List.nth(ylist,1) andalso
List.nth(xlist,2) = List.nth(ylist,1)^
substring(List.nth(ylist,3),0,5)^"i"^
substring(List.nth(ylist,3),5,2))
then [List.nth(xlist,2)]
else []ylistxlistxlistylistfun SelfLoopTerminal n=(OutNodes(n)=[n])
fun InValidTerminal()=PredNodes(EntireGraph,
fn n => (SelfLoopTerminal n),
NoLimit);
let
val fid = TextIO.openOut "ListOfSelfLoops.txt"
val _ = TextIO.output(fid, "List of self loop terminals: \n")
val _ = EvalNodes(InValidTerminal(),
fn n => INT.output(fid,n) )
in
TextIO.closeOut(fid)
enduse (ogpath^"ASKCTL/BitArray.sml");
use (ogpath^"ASKCTL/ASKCTL.sml");
open ASKCTL;fun SelfLoopTerminal n=(OutNodes(n)=[n])
fun InValidTerminal()=PredNodes(EntireGraph,
fn n => (SelfLoopTerminal n),
NoLimit);
let
val fid = TextIO.openOut "ListOfSelfLoops.txt"
val _ = TextIO.output(fid, "List of self loop terminals: \n")
val _ = EvalNodes(InValidTerminal(),
fn n => INT.output(fid,n) )
in
TextIO.closeOut(fid)
endfun ListTerminalSCCs()=PredAllSccs(SccTerminal);
fun InValidTermSCC()=PredSccs(ListTerminalSCCs(),
fn n => not (SccTrivial n),
NoLimit);
let
val fid = TextIO.openOut "AbsenceOfLivelocks.txt"
val _ = if InValidTermSCC()=[]
then TextIO.output(fid, "No Livelocks!")
else TextIO.output(fid, "Livelocks detected!")
in
TextIO.closeOut(fid)
endlet
val fid = TextIO.openOut "ListOfDeadMarkings.txt"
val _ = TextIO.output(fid, "List of dead markings: \n")
val _ = EvalNodes(ListDeadMarkings(),
fn n => INT.output(fid,n) )
val _ = TextIO.output(fid, "\nNumber of dead markings: ")
val _ = INT.output(fid,length (ListDeadMarkings()))
in
TextIO.closeOut(fid)
end