Three FSA Conversation Protocol Examples


Go to directory wsatDemo-1.0/Samples/FSA_Protocol/OnlyOneFail, you will find the following three FSA conversation protocols:

autoerr.spec     an FSA protocol which violates the autonomous condition only

comperr.spec     an FSA protocol which violates the synchronous compatible condition only.

joinerr.spec     an FSA protocol which violates the lossless join condition only.


type the following commands, and you can conduct the realizability analysis on these three examples.

    java wsat -a autoerr.spec
    java wsat -a comperr.spec
    java wsat -a joinerros.spec

WSAT will give detailed error-trace for each example on how the property is violated.  Note that these three protocols are used to show that the three sufficient realizability conditions are independent, i.e., none of them can be represented as a boolean combination of the other two, and missing any one of them can leads to non-realizability.  The technical results of realizability analysis is introduced in [CIAA'03].