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